Gibbs measures

This file defines Gibbs measures.

def IsConsistent {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} (γ : (Λ : Finset S) → ProbabilityTheory.Kernel (S → E) (S → E)) : Prop

A family of kernels γ is consistent if γ Λ₁ ∘ₖ γ Λ₂ = γ Λ₂ for all Λ₁ ⊆ Λ₂.

Morally, the LHS should be thought of as discovering Λ₁ then Λ₂, while the RHS should be thought of as discovering Λ₂ straight away.

Equations

• IsConsistent γ = ∀ ⦃Λ₁ Λ₂ : Finset S⦄, Λ₁ ⊆ Λ₂ → ((γ Λ₁).comap id ⋯).comp (γ Λ₂) = γ Λ₂

theorem isConsistentKernel_cylinderEventsCompl {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} {γ : (Λ : Finset S) → ProbabilityTheory.Kernel (S → E) (S → E)} : (MeasureTheory.Filtration.cylinderEventsCompl.IsConsistentKernel fun (Λ : (Finset S)ᵒᵈ) => γ (OrderDual.ofDual Λ)) ↔ IsConsistent γ

structure Specification (S : Type u_1) (E : Type u_2) [MeasurableSpace E] : Type (max u_1 u_2)

A specification from S to E is a collection of "boundary condition kernels" on the complement of finite sets, compatible under restriction.

The term "boundary condition kernels" is chosen because for a Gibbs measure associated to a specification, the kernels of the specification are precisely the regular conditional probabilities of the Gibbs measure conditionally on the configurations in the complements of finite sets (which serve as "boundary conditions").

• toFun (Λ : Finset S) : ProbabilityTheory.Kernel (S → E) (S → E)

  The boundary condition kernels of a specification.

  DO NOT USE. Instead use the coercion to function ⇑γ. Lean should insert it automatically in most cases.

• isConsistent' : IsConsistent self.toFun

  The boundary condition kernels of a specification are consistent.

  DO NOT USE. Instead use Specification.isConsistent.

@[implicit_reducible]

instance Specification.instDFunLike {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} : DFunLike (Specification S E) (Finset S) fun (Λ : Finset S) => ProbabilityTheory.Kernel (S → E) (S → E)

Equations

• Specification.instDFunLike = { coe := Specification.toFun, coe_injective' := ⋯ }

theorem Specification.isConsistent {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} (γ : Specification S E) : IsConsistent ⇑γ

The boundary condition kernels of a specification are consistent.

theorem Specification.ext {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} {γ₁ γ₂ : Specification S E} : (∀ (Λ : Finset S), γ₁ Λ = γ₂ Λ) → γ₁ = γ₂

theorem Specification.ext_iff {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} {γ₁ γ₂ : Specification S E} : γ₁ = γ₂ ↔ ∀ (Λ : Finset S), γ₁ Λ = γ₂ Λ

theorem Specification.bind {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} {γ : Specification S E} {Λ₁ Λ₂ : Finset S} (hΛ : Λ₁ ⊆ Λ₂) (η : S → E) : ((γ Λ₂) η).bind ⇑(γ Λ₁) = (γ Λ₂) η

def Specification.IsIndep {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} (γ : Specification S E) : Prop

An independent specification is a specification γ where γ Λ₁ ∘ₖ γ Λ₂ = γ (Λ₁ ∪ Λ₂) for all Λ₁ Λ₂.

Equations

• γ.IsIndep = ∀ ⦃Λ₁ Λ₂ : Finset S⦄ [inst : DecidableEq S], ((γ Λ₁).comap id ⋯).comp (γ Λ₂) = (γ (Λ₁ ∪ Λ₂)).comap id ⋯

class Specification.IsMarkov {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} (γ : Specification S E) : Prop

A Markov specification is a specification whose boundary condition kernels are all Markov kernels.

• isMarkovKernel (Λ : Finset S) : ProbabilityTheory.IsMarkovKernel (γ Λ)

instance Specification.IsMarkov.toIsMarkovKernel {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} {γ : Specification S E} [γ.IsMarkov] {Λ : Finset S} : ProbabilityTheory.IsMarkovKernel (γ Λ)

def Specification.IsProper {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} (γ : Specification S E) : Prop

A specification is proper if all its boundary condition kernels are.

Equations

• γ.IsProper = ∀ (Λ : Finset S), (γ Λ).IsProper

theorem Specification.isProper_iff_restrict_eq_indicator_smul {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} {γ : Specification S E} : γ.IsProper ↔ ∀ (Λ : Finset S) ⦃B : Set (S → E)⦄ (hB : MeasurableSet B) (x : S → E), ((γ Λ).restrict ⋯) x = B.indicator 1 x • (γ Λ) x

theorem Specification.isProper_iff_inter_eq_indicator_mul {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} {γ : Specification S E} : γ.IsProper ↔ ∀ (Λ : Finset S) ⦃A : Set (S → E)⦄, MeasurableSet A → ∀ ⦃B : Set (S → E)⦄, MeasurableSet B → ∀ (η : S → E), ((γ Λ) η) (A ∩ B) = B.indicator 1 η * ((γ Λ) η) A

theorem Specification.IsProper.restrict_eq_indicator_smul {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} {γ : Specification S E} : γ.IsProper → ∀ (Λ : Finset S) ⦃B : Set (S → E)⦄ (hB : MeasurableSet B) (x : S → E), ((γ Λ).restrict ⋯) x = B.indicator 1 x • (γ Λ) x

Alias of the forward direction of Specification.isProper_iff_restrict_eq_indicator_smul.

theorem Specification.IsProper.of_restrict_eq_indicator_smul {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} {γ : Specification S E} : (∀ (Λ : Finset S) ⦃B : Set (S → E)⦄ (hB : MeasurableSet B) (x : S → E), ((γ Λ).restrict ⋯) x = B.indicator 1 x • (γ Λ) x) → γ.IsProper

Alias of the reverse direction of Specification.isProper_iff_restrict_eq_indicator_smul.

theorem Specification.IsProper.inter_eq_indicator_mul {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} {γ : Specification S E} : γ.IsProper → ∀ (Λ : Finset S) ⦃A : Set (S → E)⦄ (_hA : MeasurableSet A) ⦃B : Set (S → E)⦄ (_hB : MeasurableSet B) (η : S → E), ((γ Λ) η) (A ∩ B) = B.indicator 1 η * ((γ Λ) η) A

Alias of the forward direction of Specification.isProper_iff_inter_eq_indicator_mul.

theorem Specification.IsProper.of_inter_eq_indicator_mul {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} {γ : Specification S E} : (∀ (Λ : Finset S) ⦃A : Set (S → E)⦄, MeasurableSet A → ∀ ⦃B : Set (S → E)⦄, MeasurableSet B → ∀ (η : S → E), ((γ Λ) η) (A ∩ B) = B.indicator 1 η * ((γ Λ) η) A) → γ.IsProper

Alias of the reverse direction of Specification.isProper_iff_inter_eq_indicator_mul.

theorem Specification.IsProper.setLIntegral_eq_indicator_mul_lintegral {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} {γ : Specification S E} {B : Set (S → E)} {f : (S → E) → ENNReal} {η₀ : S → E} (hγ : γ.IsProper) (Λ : Finset S) (hf : Measurable f) (hB : MeasurableSet B) : ∫⁻ (x : S → E) in B, f x ∂(γ Λ) η₀ = B.indicator 1 η₀ * ∫⁻ (x : S → E), f x ∂(γ Λ) η₀

theorem Specification.IsProper.setLIntegral_inter_eq_indicator_mul_setLIntegral {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} {γ : Specification S E} {A B : Set (S → E)} {f : (S → E) → ENNReal} {η₀ : S → E} (Λ : Finset S) (hγ : γ.IsProper) (hf : Measurable f) (hA : MeasurableSet A) (hB : MeasurableSet B) : ∫⁻ (x : S → E) in A ∩ B, f x ∂(γ Λ) η₀ = B.indicator 1 η₀ * ∫⁻ (x : S → E) in A, f x ∂(γ Λ) η₀

theorem Specification.IsProper.lintegral_mul {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} {γ : Specification S E} {f g : (S → E) → ENNReal} {η₀ : S → E} (hγ : γ.IsProper) (Λ : Finset S) (hf : Measurable f) (hg : Measurable g) : ∫⁻ (x : S → E), g x * f x ∂(γ Λ) η₀ = g η₀ * ∫⁻ (x : S → E), f x ∂(γ Λ) η₀

def Specification.IsGibbsMeasure {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} (γ : Specification S E) (μ : MeasureTheory.Measure (S → E)) : Prop

For a specification γ, a Gibbs measure is a measure whose conditional expectation kernels conditionally on configurations exterior to finite sets agree with the boundary condition kernels of the specification γ.

Equations

• γ.IsGibbsMeasure μ = ∀ (Λ : Finset S), (γ Λ).IsCondExp μ

theorem Specification.isGibbsMeasure_iff_forall_bind_eq {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} {γ : Specification S E} {μ : MeasureTheory.Measure (S → E)} (hγ : γ.IsProper) [MeasureTheory.IsFiniteMeasure μ] : γ.IsGibbsMeasure μ ↔ ∀ (Λ : Finset S), μ.bind ⇑(γ Λ) = μ

theorem Specification.isGibbsMeasure_iff_frequently_bind_eq {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} {γ : Specification S E} {μ : MeasureTheory.Measure (S → E)} (hγ : γ.IsProper) [MeasureTheory.IsFiniteMeasure μ] [γ.IsMarkov] : γ.IsGibbsMeasure μ ↔ ∃ᶠ (Λ : Finset S) in Filter.atTop, μ.bind ⇑(γ Λ) = μ

theorem Specification.measurable_isssdFun {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} (ν : MeasureTheory.Measure E) (Λ : Finset S) : Measurable fun (η : S → E) => MeasureTheory.Measure.map (juxt (↑Λ) η) (MeasureTheory.Measure.pi fun (x : ↥Λ) => ν)

noncomputable def Specification.isssdFun {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} (ν : MeasureTheory.Measure E) (Λ : Finset S) : ProbabilityTheory.Kernel (S → E) (S → E)

Auxiliary definition for Specification.isssd.

Equations

• Specification.isssdFun ν Λ = { toFun := fun (η : S → E) => MeasureTheory.Measure.map (juxt (↑Λ) η) (MeasureTheory.Measure.pi fun (x : ↥Λ) => ν), measurable' := ⋯ }

@[simp]

theorem Specification.isssdFun_apply {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} (ν : MeasureTheory.Measure E) (Λ : Finset S) : ⇑(isssdFun ν Λ) = fun (η : S → E) => MeasureTheory.Measure.map (juxt (↑Λ) η) (MeasureTheory.Measure.pi fun (x : ↥Λ) => ν)

theorem Specification.isssdFun_comp_isssdFun {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} (ν : MeasureTheory.Measure E) [DecidableEq S] (Λ₁ Λ₂ : Finset S) : ((isssdFun ν Λ₁).comap id ⋯).comp (isssdFun ν Λ₂) = (isssdFun ν (Λ₁ ∪ Λ₂)).comap id ⋯

The ISSSD of a measure is strongly consistent.

noncomputable def Specification.isssd {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} (ν : MeasureTheory.Measure E) : Specification S E

The Independent Specification with Single Spin Distribution.

This is the specification corresponding to the product measure.

Equations

• Specification.isssd ν = { toFun := Specification.isssdFun ν, isConsistent' := ⋯ }

@[simp]

theorem Specification.isssd_apply {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} (ν : MeasureTheory.Measure E) (Λ : Finset S) : (isssd ν) Λ = isssdFun ν Λ

theorem Specification.isssd_comp_isssd {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} (ν : MeasureTheory.Measure E) [DecidableEq S] (Λ₁ Λ₂ : Finset S) : (((isssd ν) Λ₁).comap id ⋯).comp ((isssd ν) Λ₂) = ((isssd ν) (Λ₁ ∪ Λ₂)).comap id ⋯

The ISSSD of a measure is strongly consistent.

theorem Specification.IsProper.isssd {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} (ν : MeasureTheory.Measure E) : (isssd ν).IsProper

instance Specification.isssd.instIsMarkov {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} (ν : MeasureTheory.Measure E) [MeasureTheory.IsProbabilityMeasure ν] : (isssd ν).IsMarkov

theorem Specification.isGibbsMeasure_isssd_infinitePi {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} (ν : MeasureTheory.Measure E) [MeasureTheory.IsProbabilityMeasure ν] : (isssd ν).IsGibbsMeasure (MeasureTheory.Measure.infinitePi fun (x : S) => ν)

The product measure ν ^ S is a isssd μ-Gibbs measure.

noncomputable def Specification.modificationKer {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} (γ : (Λ : Finset S) → ProbabilityTheory.Kernel (S → E) (S → E)) (ρ : Finset S → (S → E) → ENNReal) (hρ : ∀ (Λ : Finset S), Measurable (ρ Λ)) (Λ : Finset S) : ProbabilityTheory.Kernel (S → E) (S → E)

The kernel of a modification specification.

Modifying the specification γ by a family indexed by finsets Λ : Finset S of densities ρ Λ : (S → E) → ℝ≥0∞ results in a family of kernels γ.modificationKer ρ _ Λ whose density is that of γ Λ multiplied by ρ Λ.

This is an auxiliary definition for Specification.modification, which you should generally use instead of Specification.modificationKer.

Equations

• Specification.modificationKer γ ρ hρ Λ = { toFun := fun (η : S → E) => ((γ Λ) η).withDensity (ρ Λ), measurable' := ⋯ }

@[simp]

theorem Specification.modificationKer_apply {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} (γ : (Λ : Finset S) → ProbabilityTheory.Kernel (S → E) (S → E)) (ρ : Finset S → (S → E) → ENNReal) (hρ : ∀ (Λ : Finset S), Measurable (ρ Λ)) (Λ : Finset S) (η : S → E) : (modificationKer γ ρ hρ Λ) η = ((γ Λ) η).withDensity (ρ Λ)

@[simp]

theorem Specification.modificationKer_one' {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} (γ : (Λ : Finset S) → ProbabilityTheory.Kernel (S → E) (S → E)) : modificationKer γ (fun (_Λ : Finset S) (_η : S → E) => 1) ⋯ = γ

@[simp]

theorem Specification.modificationKer_one {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} (γ : (Λ : Finset S) → ProbabilityTheory.Kernel (S → E) (S → E)) : modificationKer γ 1 ⋯ = γ

structure Specification.IsModifier {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} (γ : Specification S E) (ρ : Finset S → (S → E) → ENNReal) : Prop

A modifier of a specification γ is a family indexed by finsets Λ : Finset S of densities ρ Λ : (S → E) → ℝ≥0∞ such that:

• Each ρ Λ is measurable.
• γ.modificationKer ρ (informally, ρ * γ) is consistent.

• measurable (Λ : Finset S) : Measurable (ρ Λ)
• isConsistent : IsConsistent (modificationKer (⇑γ) ρ ⋯)

theorem Specification.isModifier_iff {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} (γ : Specification S E) (ρ : Finset S → (S → E) → ENNReal) : γ.IsModifier ρ ↔ ∃ (measurable : ∀ (Λ : Finset S), Measurable (ρ Λ)), IsConsistent (modificationKer (⇑γ) ρ measurable)

@[simp]

theorem Specification.IsModifier.one' {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} {γ : Specification S E} : γ.IsModifier fun (_Λ : Finset S) (_η : S → E) => 1

@[simp]

theorem Specification.IsModifier.one {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} {γ : Specification S E} : γ.IsModifier 1

theorem Specification.isModifier_iff_ae_eq {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} {γ : Specification S E} {ρ : Finset S → (S → E) → ENNReal} (hγ : γ.IsProper) : γ.IsModifier ρ ↔ (∀ (Λ : Finset S), Measurable (ρ Λ)) ∧ ∀ ⦃Λ₁ Λ₂ : Finset S⦄, Λ₁ ⊆ Λ₂ → ∀ (η : S → E), ρ Λ₂ =ᵐ[(γ Λ₂) η] fun (η : S → E) => ∫⁻ (ζ : S → E), ρ Λ₂ ζ ∂((γ Λ₁) η).withDensity (ρ Λ₁)

theorem Specification.isModifier_iff_ae_comm {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} {γ : Specification S E} {ρ : Finset S → (S → E) → ENNReal} [DecidableEq S] : γ.IsModifier ρ ↔ (∀ (Λ : Finset S), Measurable (ρ Λ)) ∧ ∀ ⦃Λ₁ Λ₂ : Finset S⦄, Λ₁ ⊆ Λ₂ → ∀ (η₁ : S → E), ∀ᵐ (η₂ : S → E) ∂(γ (Λ₂ \ Λ₁)) η₁, ∀ᵐ (ζ : (S → E) × (S → E)) ∂((γ Λ₁) η₂).prod ((γ Λ₂) η₂), ρ Λ₂ ζ.1 * ρ Λ₁ ζ.2 = ρ Λ₂ ζ.2 * ρ Λ₁ ζ.1

noncomputable def Specification.modification {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} (γ : Specification S E) (ρ : Finset S → (S → E) → ENNReal) (hρ : γ.IsModifier ρ) : Specification S E

Modification specification.

Modifying the specification γ by a family indexed by finsets Λ : Finset S of densities ρ Λ : (S → E) → ℝ≥0∞ results in a family of kernels γ.modificationKer ρ _ Λ whose density is that of γ Λ multiplied by ρ Λ.

When the family of densities ρ is a modifier (Specification.IsModifier), modifying a specification results in a specification γ.modification ρ _.

Equations

• γ.modification ρ hρ = { toFun := Specification.modificationKer (⇑γ) ρ ⋯, isConsistent' := ⋯ }

theorem Specification.coe_modification {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} (γ : Specification S E) (ρ : Finset S → (S → E) → ENNReal) (hρ : γ.IsModifier ρ) : ⇑(γ.modification ρ hρ) = modificationKer (⇑γ) ρ ⋯

@[simp]

theorem Specification.modification_apply {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} (γ : Specification S E) (ρ : Finset S → (S → E) → ENNReal) (hρ : γ.IsModifier ρ) (Λ : Finset S) (η : S → E) : ((γ.modification ρ hρ) Λ) η = ((γ Λ) η).withDensity (ρ Λ)

@[simp]

theorem Specification.modificationKer_modification {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} {γ : Specification S E} {ρ₁ ρ₂ : Finset S → (S → E) → ENNReal} (hρ₁ : γ.IsModifier ρ₁) (hρ₂ : ∀ (Λ : Finset S), Measurable (ρ₂ Λ)) : modificationKer (⇑(γ.modification ρ₁ hρ₁)) ρ₂ hρ₂ = modificationKer (⇑γ) (ρ₁ * ρ₂) ⋯

@[simp]

theorem Specification.IsModifier.mul {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} {γ : Specification S E} {ρ₁ ρ₂ : Finset S → (S → E) → ENNReal} (hρ₁ : γ.IsModifier ρ₁) (hρ₂ : (γ.modification ρ₁ hρ₁).IsModifier ρ₂) : γ.IsModifier (ρ₁ * ρ₂)

@[simp]

theorem Specification.modification_one' {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} (γ : Specification S E) : γ.modification (fun (_Λ : Finset S) (_η : S → E) => 1) ⋯ = γ

@[simp]

theorem Specification.modification_one {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} (γ : Specification S E) : γ.modification 1 ⋯ = γ

@[simp]

theorem Specification.modification_modification {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} (γ : Specification S E) (ρ₁ ρ₂ : Finset S → (S → E) → ENNReal) (hρ₁ : γ.IsModifier ρ₁) (hρ₂ : (γ.modification ρ₁ hρ₁).IsModifier ρ₂) : (γ.modification ρ₁ hρ₁).modification ρ₂ hρ₂ = γ.modification (ρ₁ * ρ₂) ⋯

theorem Specification.IsProper.modification {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} {γ : Specification S E} {ρ : Finset S → (S → E) → ENNReal} (hγ : γ.IsProper) {hρ : γ.IsModifier ρ} : (γ.modification ρ hρ).IsProper

structure Specification.IsPremodifier {S : Type u_1} {E : Type u_2} [MeasurableSpace E] (ρ : Finset S → (S → E) → ENNReal) : Prop

A premodifier is a family indexed by finsets Λ : Finset S of densities ρ Λ : (S → E) → ℝ≥0∞ such that:

• each ρ Λ is measurable,
• ρ Λ₂ ζ * ρ Λ₁ η = ρ Λ₁ ζ * ρ Λ₂ η for all Λ₁ Λ₂ : Finset S and ζ η : S → E such that Λ₁ ⊆ Λ₂ and ∀ (s : Λ₁ᶜ), ζ s = η s.

• measurable (Λ : Finset S) : Measurable (ρ Λ)
• comm_of_subset ⦃Λ₁ Λ₂ : Finset S⦄ ⦃ζ η : S → E⦄ (hΛ : Λ₁ ⊆ Λ₂) (hrestrict : ∀ s ∉ Λ₁, ζ s = η s) : ρ Λ₂ ζ * ρ Λ₁ η = ρ Λ₁ ζ * ρ Λ₂ η

theorem Specification.IsPremodifier.isModifier_div {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} {ρ : Finset S → (S → E) → ENNReal} (hρ : IsPremodifier ρ) (ν : MeasureTheory.Measure E) [MeasureTheory.IsProbabilityMeasure ν] : (isssd ν).IsModifier fun (Λ : Finset S) (σ : S → E) => ρ Λ σ / ∫⁻ (x : S → E), ρ Λ x ∂((isssd ν) Λ) σ