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.

@[instance_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 ⇑(γ Λ₁) = (γ Λ₂) η

theorem Specification.lintegral_bind {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} {γ : Specification S E} {Λ₁ Λ₂ : Finset S} (hΛ : Λ₁ ⊆ Λ₂) {f : (S → E) → ENNReal} (hf : Measurable f) (η : S → E) : ∫⁻ (x : S → E), f x ∂(γ Λ₂) η = ∫⁻ (ζ : S → E), ∫⁻ (x : S → E), f x ∂(γ Λ₁) ζ ∂(γ Λ₂) η

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 ⋯

theorem Specification.IsIndep.bind_eq_union {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} {γ : Specification S E} [DecidableEq S] (hγ : γ.IsIndep) (Λ₁ Λ₂ : Finset S) (η : S → E) : ((γ Λ₂) η).bind ⇑(γ Λ₁) = (γ (Λ₁ ∪ Λ₂)) η

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} [MeasureTheory.IsProbabilityMeasure ν] (Λ : 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) [MeasureTheory.IsProbabilityMeasure ν] (Λ : 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) [MeasureTheory.IsProbabilityMeasure ν] (Λ : Finset S) : ⇑(isssdFun ν Λ) = fun (η : S → E) => MeasureTheory.Measure.map (juxt (↑Λ) η) (MeasureTheory.Measure.pi fun (x : ↥Λ) => ν)

instance Specification.instIsMarkovKernel_isssdFun {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} {ν : MeasureTheory.Measure E} [MeasureTheory.IsProbabilityMeasure ν] {Λ : Finset S} : ProbabilityTheory.IsMarkovKernel (isssdFun ν Λ)

theorem Specification.isssdFun_pi {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} {ν : MeasureTheory.Measure E} [MeasureTheory.IsProbabilityMeasure ν] [DecidableEq S] (Λ s : Finset S) (t : S → Set E) (ht : ∀ (i : S), MeasurableSet (t i)) (η : S → E) : ((isssdFun ν Λ) η) ((↑s).pi t) = ((↑(s \ Λ)).pi t).indicator (fun (x : S → E) => ∏ i ∈ s ∩ Λ, ν (t i)) η

theorem Specification.lintegral_isssdFun_pi {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} {ν : MeasureTheory.Measure E} [MeasureTheory.IsProbabilityMeasure ν] [DecidableEq S] {μ : MeasureTheory.Measure (S → E)} (Λ s : Finset S) (t : S → Set E) (ht : ∀ (i : S), MeasurableSet (t i)) : ∫⁻ (ω : S → E), ((isssdFun ν Λ) ω) ((↑s).pi t) ∂μ = (∏ i ∈ s ∩ Λ, ν (t i)) * μ ((↑(s \ Λ)).pi t)

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

Resampling Λ₁ then Λ₂ is resampling Λ₁ ∪ Λ₂.

noncomputable def Specification.isssd {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} (ν : MeasureTheory.Measure E) [MeasureTheory.IsProbabilityMeasure ν] : 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) [MeasureTheory.IsProbabilityMeasure ν] (Λ : Finset S) : (isssd ν) Λ = isssdFun ν Λ

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

theorem Specification.IsProper.isssd {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} {ν : MeasureTheory.Measure E} [MeasureTheory.IsProbabilityMeasure ν] : (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.isssd_pi {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} {ν : MeasureTheory.Measure E} [MeasureTheory.IsProbabilityMeasure ν] {Λ s : Finset S} (hs : s ⊆ Λ) (t : S → Set E) (ht : ∀ (i : S), MeasurableSet (t i)) (η : S → E) : (((isssd ν) Λ) η) ((↑s).pi t) = ∏ i ∈ s, ν (t i)

theorem Specification.bind_isssd_pi {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} {ν : MeasureTheory.Measure E} [MeasureTheory.IsProbabilityMeasure ν] (μ : MeasureTheory.Measure (S → E)) {Λ s : Finset S} (hs : s ⊆ Λ) (t : S → Set E) (ht : ∀ (i : S), MeasurableSet (t i)) : (μ.bind ⇑((isssd ν) Λ)) ((↑s).pi t) = μ Set.univ * ∏ i ∈ s, ν (t i)

theorem Specification.infinitePi_bind_isssd {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} {ν : MeasureTheory.Measure E} [MeasureTheory.IsProbabilityMeasure ν] (Λ : Finset S) : (MeasureTheory.Measure.infinitePi fun (x : S) => ν).bind ⇑((isssd ν) Λ) = MeasureTheory.Measure.infinitePi fun (x : S) => ν

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.

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

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.comp_modificationKer_apply {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} {γ : Specification S E} {Λ₁ Λ₂ : Finset S} {ρ : Finset S → (S → E) → ENNReal} (hγ : γ.IsProper) (hρ : ∀ (Λ : Finset S), Measurable (ρ Λ)) (hΛ : Λ₁ ⊆ Λ₂) (η : S → E) : (((modificationKer (⇑γ) ρ hρ Λ₁).comap id ⋯).comp (modificationKer (⇑γ) ρ hρ Λ₂)) η = ((γ Λ₂) η).withDensity fun (ω : S → E) => ρ Λ₁ ω * ∫⁻ (ζ : S → E), ρ Λ₂ ζ ∂(γ Λ₁) ω

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} [γ.IsMarkov] (hγ : γ.IsProper) : γ.IsModifier ρ ↔ (∀ (Λ : Finset S), Measurable (ρ Λ)) ∧ ∀ ⦃Λ₁ Λ₂ : Finset S⦄, Λ₁ ⊆ Λ₂ → ∀ (η : S → E), ρ Λ₂ =ᵐ[(γ Λ₂) η] fun (ω : S → E) => ρ Λ₁ ω * ∫⁻ (ζ : S → E), ρ Λ₂ ζ ∂(γ Λ₁) ω

theorem Specification.ae_eq_mul_lintegral_iff_ae_mul_comm {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} {γ : Specification S E} {Λ₁ Λ₂ : Finset S} {ρ : Finset S → (S → E) → ENNReal} [ProbabilityTheory.IsMarkovKernel (γ Λ₁)] (hγ : γ.IsProper) (hmeas : ∀ (Λ : Finset S), Measurable (ρ Λ)) (η₂ : S → E) (hnorm : ∫⁻ (ζ : S → E), ρ Λ₁ ζ ∂(γ Λ₁) η₂ = 1) : (ρ Λ₂ =ᵐ[(γ Λ₁) η₂] fun (ω : S → E) => ρ Λ₁ ω * ∫⁻ (ζ : S → E), ρ Λ₂ ζ ∂(γ Λ₁) ω) ↔ ∀ᵐ (z : (S → E) × (S → E)) ∂((γ Λ₁) η₂).prod ((γ Λ₁) η₂), ρ Λ₂ z.1 * ρ Λ₁ z.2 = ρ Λ₂ z.2 * ρ Λ₁ z.1

theorem Specification.ae_eq_mul_lintegral_iff_ae_eq_sdiff {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} {γ : Specification S E} {Λ₁ Λ₂ : Finset S} {ρ : Finset S → (S → E) → ENNReal} [DecidableEq S] (hindep : γ.IsIndep) (hmeas : ∀ (Λ : Finset S), Measurable (ρ Λ)) (hΛ : Λ₁ ⊆ Λ₂) (η₁ : S → E) : (ρ Λ₂ =ᵐ[(γ Λ₂) η₁] fun (ω : S → E) => ρ Λ₁ ω * ∫⁻ (ζ : S → E), ρ Λ₂ ζ ∂(γ Λ₁) ω) ↔ ∀ᵐ (η₂ : S → E) ∂(γ (Λ₂ \ Λ₁)) η₁, ρ Λ₂ =ᵐ[(γ Λ₁) η₂] fun (ω : S → E) => ρ Λ₁ ω * ∫⁻ (ζ : S → E), ρ Λ₂ ζ ∂(γ Λ₁) ω

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] [γ.IsMarkov] (hγ : γ.IsProper) (hindep : γ.IsIndep) (hnorm : ∀ (Λ : Finset S) (η : S → E), ∫⁻ (ζ : S → E), ρ Λ ζ ∂(γ Λ) η = 1) : γ.IsModifier ρ ↔ (∀ (Λ : Finset S), Measurable (ρ Λ)) ∧ ∀ ⦃Λ₁ Λ₂ : Finset S⦄, Λ₁ ⊆ Λ₂ → ∀ (η₁ : S → E), ∀ᵐ (η₂ : S → E) ∂(γ (Λ₂ \ Λ₁)) η₁, ∀ᵐ (z : (S → E) × (S → E)) ∂((γ Λ₁) η₂).prod ((γ Λ₁) η₂), ρ Λ₂ z.1 * ρ Λ₁ z.2 = ρ Λ₂ z.2 * ρ Λ₁ z.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.mul_lintegral_isssd {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} {Λ₁ Λ₂ : Finset S} {ρ : Finset S → (S → E) → ENNReal} {ν : MeasureTheory.Measure E} [MeasureTheory.IsProbabilityMeasure ν] (hρ : IsPremodifier ρ) (hΛ : Λ₁ ⊆ Λ₂) (ξ : S → E) : ρ Λ₂ ξ * ∫⁻ (ζ : S → E), ρ Λ₁ ζ ∂((isssd ν) Λ₁) ξ = ρ Λ₁ ξ * ∫⁻ (ζ : S → E), ρ Λ₂ ζ ∂((isssd ν) Λ₁) ξ

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 ν] (hZ : ∀ (Λ : Finset S) (σ : S → E), 0 < ∫⁻ (x : S → E), ρ Λ x ∂((isssd ν) Λ) σ ∧ ∫⁻ (x : S → E), ρ Λ x ∂((isssd ν) Λ) σ < ⊤) : (isssd ν).IsModifier fun (Λ : Finset S) (σ : S → E) => ρ Λ σ / ∫⁻ (x : S → E), ρ Λ x ∂((isssd ν) Λ) σ