Documentation

Mathlib.MeasureTheory.Constructions.Cylinders

π-systems of cylinders and square cylinders #

The instance MeasurableSpace.pi on ∀ i, α i, where each α i has a MeasurableSpace m i, is defined as ⨆ i, (m i).comap (fun a => a i). That is, a function g : β → ∀ i, α i is measurable iff for all i, the function b ↦ g b i is measurable.

We define two π-systems generating MeasurableSpace.pi, cylinders and square cylinders.

Main definitions #

Given a finite set s of indices, a cylinder is the product of a set of ∀ i : s, α i and of univ on the other indices. A square cylinder is a cylinder for which the set on ∀ i : s, α i is a product set.

Main statements #

def MeasureTheory.squareCylinders {ι : Type u_1} {α : ιType u_2} (C : (i : ι) → Set (Set (α i))) :
Set (Set ((i : ι) → α i))

Given a finite set s of indices, a square cylinder is the product of a set S of ∀ i : s, α i and of univ on the other indices. The set S is a product of sets t i such that for all i : s, t i ∈ C i. squareCylinders is the set of all such squareCylinders.

Equations
Instances For
    theorem MeasureTheory.squareCylinders_eq_iUnion_image {ι : Type u_2} {α : ιType u_1} (C : (i : ι) → Set (Set (α i))) :
    MeasureTheory.squareCylinders C = ⋃ (s : Finset ι), (fun (t : (i : ι) → Set (α i)) => (↑s).pi t) '' Set.univ.pi C
    theorem MeasureTheory.isPiSystem_squareCylinders {ι : Type u_2} {α : ιType u_1} {C : (i : ι) → Set (Set (α i))} (hC : ∀ (i : ι), IsPiSystem (C i)) (hC_univ : ∀ (i : ι), Set.univ C i) :
    theorem MeasureTheory.comap_eval_le_generateFrom_squareCylinders_singleton {ι : Type u_2} (α : ιType u_1) [m : (i : ι) → MeasurableSpace (α i)] (i : ι) :
    MeasurableSpace.comap (Function.eval i) (m i) MeasurableSpace.generateFrom ((fun (t : (i : ι) → Set (α i)) => {i}.pi t) '' Set.univ.pi fun (i : ι) => {s : Set (α i) | MeasurableSet s})
    theorem MeasureTheory.generateFrom_squareCylinders {ι : Type u_2} {α : ιType u_1} [(i : ι) → MeasurableSpace (α i)] :
    MeasurableSpace.generateFrom (MeasureTheory.squareCylinders fun (i : ι) => {s : Set (α i) | MeasurableSet s}) = MeasurableSpace.pi

    The square cylinders formed from measurable sets generate the product σ-algebra.

    def MeasureTheory.cylinder {ι : Type u_1} {α : ιType u_2} (s : Finset ι) (S : Set ((i : { x : ι // x s }) → α i)) :
    Set ((i : ι) → α i)

    Given a finite set s of indices, a cylinder is the preimage of a set S of ∀ i : s, α i by the projection from ∀ i, α i to ∀ i : s, α i.

    Equations
    Instances For
      @[simp]
      theorem MeasureTheory.mem_cylinder {ι : Type u_1} {α : ιType u_2} (s : Finset ι) (S : Set ((i : { x : ι // x s }) → α i)) (f : (i : ι) → α i) :
      f MeasureTheory.cylinder s S s.restrict f S
      @[simp]
      theorem MeasureTheory.cylinder_empty {ι : Type u_1} {α : ιType u_2} (s : Finset ι) :
      @[simp]
      theorem MeasureTheory.cylinder_univ {ι : Type u_1} {α : ιType u_2} (s : Finset ι) :
      MeasureTheory.cylinder s Set.univ = Set.univ
      @[simp]
      theorem MeasureTheory.cylinder_eq_empty_iff {ι : Type u_1} {α : ιType u_2} [h_nonempty : Nonempty ((i : ι) → α i)] (s : Finset ι) (S : Set ((i : { x : ι // x s }) → α i)) :
      theorem MeasureTheory.inter_cylinder {ι : Type u_1} {α : ιType u_2} (s₁ : Finset ι) (s₂ : Finset ι) (S₁ : Set ((i : { x : ι // x s₁ }) → α i)) (S₂ : Set ((i : { x : ι // x s₂ }) → α i)) [DecidableEq ι] :
      theorem MeasureTheory.inter_cylinder_same {ι : Type u_1} {α : ιType u_2} (s : Finset ι) (S₁ : Set ((i : { x : ι // x s }) → α i)) (S₂ : Set ((i : { x : ι // x s }) → α i)) :
      theorem MeasureTheory.union_cylinder {ι : Type u_1} {α : ιType u_2} (s₁ : Finset ι) (s₂ : Finset ι) (S₁ : Set ((i : { x : ι // x s₁ }) → α i)) (S₂ : Set ((i : { x : ι // x s₂ }) → α i)) [DecidableEq ι] :
      theorem MeasureTheory.union_cylinder_same {ι : Type u_1} {α : ιType u_2} (s : Finset ι) (S₁ : Set ((i : { x : ι // x s }) → α i)) (S₂ : Set ((i : { x : ι // x s }) → α i)) :
      theorem MeasureTheory.compl_cylinder {ι : Type u_1} {α : ιType u_2} (s : Finset ι) (S : Set ((i : { x : ι // x s }) → α i)) :
      theorem MeasureTheory.diff_cylinder_same {ι : Type u_1} {α : ιType u_2} (s : Finset ι) (S : Set ((i : { x : ι // x s }) → α i)) (T : Set ((i : { x : ι // x s }) → α i)) :
      theorem MeasureTheory.eq_of_cylinder_eq_of_subset {ι : Type u_1} {α : ιType u_2} [h_nonempty : Nonempty ((i : ι) → α i)] {I : Finset ι} {J : Finset ι} {S : Set ((i : { x : ι // x I }) → α i)} {T : Set ((i : { x : ι // x J }) → α i)} (h_eq : MeasureTheory.cylinder I S = MeasureTheory.cylinder J T) (hJI : J I) :
      theorem MeasureTheory.cylinder_eq_cylinder_union {ι : Type u_1} {α : ιType u_2} [DecidableEq ι] (I : Finset ι) (S : Set ((i : { x : ι // x I }) → α i)) (J : Finset ι) :
      theorem MeasureTheory.disjoint_cylinder_iff {ι : Type u_1} {α : ιType u_2} [Nonempty ((i : ι) → α i)] {s : Finset ι} {t : Finset ι} {S : Set ((i : { x : ι // x s }) → α i)} {T : Set ((i : { x : ι // x t }) → α i)} [DecidableEq ι] :
      theorem MeasureTheory.IsClosed.cylinder {ι : Type u_2} {α : ιType u_1} [(i : ι) → TopologicalSpace (α i)] (s : Finset ι) {S : Set ((i : { x : ι // x s }) → α i)} (hs : IsClosed S) :
      theorem MeasurableSet.cylinder {ι : Type u_2} {α : ιType u_1} [(i : ι) → MeasurableSpace (α i)] (s : Finset ι) {S : Set ((i : { x : ι // x s }) → α i)} (hS : MeasurableSet S) :
      def MeasureTheory.measurableCylinders {ι : Type u_2} (α : ιType u_1) [(i : ι) → MeasurableSpace (α i)] :
      Set (Set ((i : ι) → α i))

      Given a finite set s of indices, a cylinder is the preimage of a set S of ∀ i : s, α i by the projection from ∀ i, α i to ∀ i : s, α i. measurableCylinders is the set of all cylinders with measurable base S.

      Equations
      Instances For
        @[simp]
        theorem MeasureTheory.mem_measurableCylinders {ι : Type u_1} {α : ιType u_2} [(i : ι) → MeasurableSpace (α i)] (t : Set ((i : ι) → α i)) :
        t MeasureTheory.measurableCylinders α ∃ (s : Finset ι) (S : Set ((i : { x : ι // x s }) → α i)), MeasurableSet S t = MeasureTheory.cylinder s S
        theorem MeasurableSet.of_mem_measurableCylinders {ι : Type u_1} {α : ιType u_2} [(i : ι) → MeasurableSpace (α i)] {s : Set ((i : ι) → α i)} (hs : s MeasureTheory.measurableCylinders α) :
        noncomputable def MeasureTheory.measurableCylinders.finset {ι : Type u_1} {α : ιType u_2} [(i : ι) → MeasurableSpace (α i)] {t : Set ((i : ι) → α i)} (ht : t MeasureTheory.measurableCylinders α) :

        A finset s such that t = cylinder s S. S is given by measurableCylinders.set.

        Equations
        Instances For
          def MeasureTheory.measurableCylinders.set {ι : Type u_1} {α : ιType u_2} [(i : ι) → MeasurableSpace (α i)] {t : Set ((i : ι) → α i)} (ht : t MeasureTheory.measurableCylinders α) :
          Set ((i : { x : ι // x MeasureTheory.measurableCylinders.finset ht }) → α i)

          A set S such that t = cylinder s S. s is given by measurableCylinders.finset.

          Equations
          Instances For
            theorem MeasureTheory.measurableCylinders.measurableSet {ι : Type u_1} {α : ιType u_2} [(i : ι) → MeasurableSpace (α i)] {t : Set ((i : ι) → α i)} (ht : t MeasureTheory.measurableCylinders α) :
            theorem MeasureTheory.cylinder_mem_measurableCylinders {ι : Type u_1} {α : ιType u_2} [(i : ι) → MeasurableSpace (α i)] (s : Finset ι) (S : Set ((i : { x : ι // x s }) → α i)) (hS : MeasurableSet S) :
            theorem MeasureTheory.inter_mem_measurableCylinders {ι : Type u_1} {α : ιType u_2} [(i : ι) → MeasurableSpace (α i)] {s : Set ((i : ι) → α i)} {t : Set ((i : ι) → α i)} (hs : s MeasureTheory.measurableCylinders α) (ht : t MeasureTheory.measurableCylinders α) :
            theorem MeasureTheory.compl_mem_measurableCylinders {ι : Type u_1} {α : ιType u_2} [(i : ι) → MeasurableSpace (α i)] {s : Set ((i : ι) → α i)} (hs : s MeasureTheory.measurableCylinders α) :
            theorem MeasureTheory.univ_mem_measurableCylinders {ι : Type u_2} (α : ιType u_1) [(i : ι) → MeasurableSpace (α i)] :
            theorem MeasureTheory.union_mem_measurableCylinders {ι : Type u_1} {α : ιType u_2} [(i : ι) → MeasurableSpace (α i)] {s : Set ((i : ι) → α i)} {t : Set ((i : ι) → α i)} (hs : s MeasureTheory.measurableCylinders α) (ht : t MeasureTheory.measurableCylinders α) :
            theorem MeasureTheory.diff_mem_measurableCylinders {ι : Type u_1} {α : ιType u_2} [(i : ι) → MeasurableSpace (α i)] {s : Set ((i : ι) → α i)} {t : Set ((i : ι) → α i)} (hs : s MeasureTheory.measurableCylinders α) (ht : t MeasureTheory.measurableCylinders α) :
            theorem MeasureTheory.generateFrom_measurableCylinders {ι : Type u_1} {α : ιType u_2} [(i : ι) → MeasurableSpace (α i)] :

            The measurable cylinders generate the product σ-algebra.