Documentation

GibbsMeasure.Mathlib.MeasureTheory.Constructions.Cylinders

theorem mem_congr_of_measurableSet_cylinderEvents {S : Type u_1} {E : Type u_2} {mE : MeasurableSpace E} {Δ : Set S} {B : Set (S → E)} (hB : MeasurableSet B) {f₁ f₂ : S → E} (h : ∀ i ∈ Δ, f₁ i = f₂ i) :

f₁ ∈ B ↔ f₂ ∈ B

theorem MeasureTheory.cylinderEvents_eq_comap_domRestrict {ι : Type u_3} {X : ι → Type u_4} [(i : ι) → MeasurableSpace (X i)] (Δ : Set ι) :

cylinderEvents Δ = MeasurableSpace.comap Δ.domRestrict inferInstance

theorem MeasureTheory.cylinderEvents_eq_comap_finsetRestrict {ι : Type u_3} {X : ι → Type u_4} [(i : ι) → MeasurableSpace (X i)] (Λ : Finset ι) :

cylinderEvents ↑Λ = MeasurableSpace.comap Λ.restrict inferInstance

theorem Measurable.dependsOn_of_cylinderEvents {ι : Type u_3} {X : ι → Type u_4} [(i : ι) → MeasurableSpace (X i)] {Δ : Set ι} {Z : Type u_5} [MeasurableSpace Z] {f : ((i : ι) → X i) → Z} [MeasurableSingletonClass Z] (hf : Measurable f) :

theorem Measurable.cylinderEvents_of_dependsOn {ι : Type u_3} {X : ι → Type u_4} [(i : ι) → MeasurableSpace (X i)] {Δ : Set ι} {Z : Type u_5} [MeasurableSpace Z] {f : ((i : ι) → X i) → Z} (hf : Measurable f) (hdep : DependsOn f Δ) :

theorem MeasureTheory.measurable_cylinderEvents_iff_dependsOn {ι : Type u_3} {X : ι → Type u_4} [(i : ι) → MeasurableSpace (X i)] {Δ : Set ι} {Z : Type u_5} [MeasurableSpace Z] {f : ((i : ι) → X i) → Z} [MeasurableSingletonClass Z] :

Measurable f ↔ Measurable f ∧ DependsOn f Δ

@[reducible, inline]

abbrev MeasureTheory.measurableSquareCylinders (ι : Type u_3) (X : ι → Type u_4) [(i : ι) → MeasurableSpace (X i)] :

Set (Set ((i : ι) → X i))

Equations

MeasureTheory.measurableSquareCylinders ι X = MeasureTheory.squareCylinders fun (x : ι) => {s : Set (X x) | MeasurableSet s}

Instances For

theorem MeasureTheory.IsPiSystem.measurableSquareCylinders {ι : Type u_3} {X : ι → Type u_4} [(i : ι) → MeasurableSpace (X i)] :

IsPiSystem (measurableSquareCylinders ι X)

theorem MeasureTheory.generateFrom_measurableSquareCylinders {ι : Type u_3} {X : ι → Type u_4} [(i : ι) → MeasurableSpace (X i)] :

MeasurableSpace.generateFrom (measurableSquareCylinders ι X) = MeasurableSpace.pi

theorem MeasureTheory.univ_mem_measurableSquareCylinders {ι : Type u_3} {X : ι → Type u_4} [(i : ι) → MeasurableSpace (X i)] :

Set.univ ∈ measurableSquareCylinders ι X

theorem MeasurableSet.pi_cylinderEvents {ι : Type u_3} {X : ι → Type u_4} [(i : ι) → MeasurableSpace (X i)] {Δ s : Set ι} (hs : s ⊆ Δ) (hsc : s.Countable) {t : (i : ι) → Set (X i)} (ht : ∀ i ∈ s, MeasurableSet (t i)) :

MeasurableSet (s.pi t)