MeasureTheory.mem_measurableCylinders
theorem MeasureTheory.mem_measurableCylinders :
∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → MeasurableSpace (α i)] (t : Set ((i : ι) → α i)),
t ∈ MeasureTheory.measurableCylinders α ↔ ∃ s S, MeasurableSet S ∧ t = MeasureTheory.cylinder s S
This theorem, `MeasureTheory.mem_measurableCylinders`, states that for any type `ι`, for any function `α` from `ι` to a type `u_2`, and given any measurable space over the type that `α` maps to, for any set `t` of functions from `ι` to `α i`, `t` is in the set of measurable cylinders of `α` if and only if there exists a finite set `s` and a set `S` such that `S` is a measurable set and `t` equals to the cylinder of `s` and `S`. Here, a cylinder is defined as the preimage of a set `S` of functions (for all `i` in `s`, `α i`) by the projection from functions (for all `i`, `α i`) to functions (for all `i` in `s`, `α i`). In other words, a cylinder is the set of all functions mapping from `ι` to `α i` that map elements of `s` to the corresponding elements of `S`.
More concisely: A set of functions from a type `ι` to a measurable space is a measurable cylinder if and only if it is the preimage of a measurable set under the projection from functions to their values on a finite subset of `ι`.
|
MeasureTheory.compl_mem_measurableCylinders
theorem MeasureTheory.compl_mem_measurableCylinders :
∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → MeasurableSpace (α i)] {s : Set ((i : ι) → α i)},
s ∈ MeasureTheory.measurableCylinders α → sᶜ ∈ MeasureTheory.measurableCylinders α
This theorem, `MeasureTheory.compl_mem_measurableCylinders`, states that for any type `ι`, any function `α` from `ι` to another type, and given that each `α i` has a measurable space, if a set `s` of functions from `ι` to `α i` belongs to the set of all measurable cylinders over `α`, then the complement of `s`, denoted `sᶜ`, also belongs to the set of all measurable cylinders over `α`. In other words, if a set is a measurable cylinder, then its complement is also a measurable cylinder.
More concisely: If `s` is a measurable cylinder over a function `α : ι → αi` with each `α i` having a measurable space, then the complement `sᶜ` is also a measurable cylinder over `α`.
|
MeasureTheory.generateFrom_squareCylinders
theorem MeasureTheory.generateFrom_squareCylinders :
∀ {ι : Type u_2} {α : ι → Type u_1} [inst : (i : ι) → MeasurableSpace (α i)],
MeasurableSpace.generateFrom (MeasureTheory.squareCylinders fun i => {s | MeasurableSet s}) =
MeasurableSpace.pi
This theorem states that for any type `ι` and a function `α` mapping `ι` to another type, given a measurable space `α i` for every `ι i`, the smallest measure space containing the square cylinders formed from measurable sets is equal to the product of the measurable spaces over the entire domain. Here, a square cylinder is defined as the product of a set over a finite subset of the domain and the universal set over the rest of the domain. The sets are defined by the property that they are measurable.
More concisely: The smallest measurable space containing all square cylinders formed from measurable sets over a type `ι` and a function `α` is equal to the product measurable space of `α i` for all `ι i`.
|
Mathlib.MeasureTheory.Constructions.Cylinders._auxLemma.13
theorem Mathlib.MeasureTheory.Constructions.Cylinders._auxLemma.13 :
∀ {ι : Type u_1} {α : ι → Type u_2} (s : Finset ι) (S : Set ((i : { x // x ∈ s }) → α ↑i)) (f : (i : ι) → α i),
(f ∈ MeasureTheory.cylinder s S) = ((fun i => f ↑i) ∈ S)
This theorem states that for any type `ι`, a function `α` from `ι`, a finite set `s` of indices of type `ι`, a set `S` of functions from indices in `s` to `α` and a function `f` from `ι` to `α`, the function `f` being in the cylinder of `s` and `S` (which is the preimage of a set `S` of `∀ i : s, α i` by the projection from `∀ i, α i` to `∀ i : s, α i`) is equivalent to the function that maps each index in `s` to `f` of that index being in `S`. This essentially provides a condition to check if a function is in the cylinder set for given `s` and `S`.
More concisely: For any type `ι`, function `α : ι → Type`, finite set `s ⊆ ι`, set `S ⊆ ∀ i : s, α i`, and function `f : ι → α`, `f` is in the cylinder of `s` and `S` if and only if `{i | i ∈ s ∧ f i ∈ S}` equals `s`.
|
Mathlib.MeasureTheory.Constructions.Cylinders._auxLemma.1
theorem Mathlib.MeasureTheory.Constructions.Cylinders._auxLemma.1 :
∀ {α : Type u} {ι : Sort v} {x : α} {s : ι → Set α}, (x ∈ ⋃ i, s i) = ∃ i, x ∈ s i
The theorem `Mathlib.MeasureTheory.Constructions.Cylinders._auxLemma.1` states that for any type `α`, any type `ι`, any element `x` of type `α`, and any function `s` from `ι` to the set of `α`, the condition that `x` belongs to the union over `i` of the sets `s i` is equivalent to the existence of some `i` such that `x` belongs to `s i`. In mathematical terms, this is expressing the property that an element is in the union of a collection of sets if and only if it is in at least one of the sets in the collection.
More concisely: For any type `α`, any type `ι`, any element `x` of type `α`, and any function `s` from `ι` to `α`, the element `x` belongs to the union of the sets `s i` if and only if there exists some `i`, such that `x` belongs to `s i`.
|
MeasureTheory.inter_cylinder
theorem MeasureTheory.inter_cylinder :
∀ {ι : Type u_1} {α : ι → Type u_2} (s₁ s₂ : Finset ι) (S₁ : Set ((i : { x // x ∈ s₁ }) → α ↑i))
(S₂ : Set ((i : { x // x ∈ s₂ }) → α ↑i)) [inst : DecidableEq ι],
MeasureTheory.cylinder s₁ S₁ ∩ MeasureTheory.cylinder s₂ S₂ =
MeasureTheory.cylinder (s₁ ∪ s₂) ((fun f j => f ⟨↑j, ⋯⟩) ⁻¹' S₁ ∩ (fun f j => f ⟨↑j, ⋯⟩) ⁻¹' S₂)
The theorem `MeasureTheory.inter_cylinder` states that for any two finite sets of indices `s₁` and `s₂` and their respective sets `S₁` and `S₂` with elements of types determined by `s₁` and `s₂`, the intersection of their corresponding cylinders is equal to the cylinder of the union of `s₁` and `s₂`, whose elements are the intersection of the preimages of `S₁` and `S₂` through a function `f`. This theorem holds given that equality is decidable for the type of the indices `ι`. In other words, this theorem describes how the intersection of two cylinders over finite index sets relates to the cylinder over the union of these index sets.
More concisely: For sets $S\_1$ and $S\_2$ determined by finite index sets $s\_1$ and $s\_2$, respectively, the intersection of their cylinders equals the cylinder of their union, where elements are in the intersection of the preimages of $S\_1$ and $S\_2$ through a function $f$.
|
MeasureTheory.inter_mem_measurableCylinders
theorem MeasureTheory.inter_mem_measurableCylinders :
∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → MeasurableSpace (α i)] {s t : Set ((i : ι) → α i)},
s ∈ MeasureTheory.measurableCylinders α →
t ∈ MeasureTheory.measurableCylinders α → s ∩ t ∈ MeasureTheory.measurableCylinders α
This theorem states that for any type `ι` and a function `α` mapping `ι` to some type, given that each element of type `ι` is associated with a measurable space, if two sets `s` and `t` of functions from `ι` to `α i` are both in the set of measurable cylinders of `α`, then their intersection is also in the set of measurable cylinders of `α`. In other words, the intersection of two measurable cylinders is also a measurable cylinder.
More concisely: Given types `ι` and `α`, if `s` and `t` are measurable cylinders of functions from `ι` to `α`, then their intersection is also a measurable cylinder of functions from `ι` to `α`.
|
Mathlib.MeasureTheory.Constructions.Cylinders._auxLemma.12
theorem Mathlib.MeasureTheory.Constructions.Cylinders._auxLemma.12 :
∀ {α : Type u} {β : Type v} {f : α → β} {s : Set β} {a : α}, (a ∈ f ⁻¹' s) = (f a ∈ s)
This theorem states that for any types `α` and `β`, any function `f` from `α` to `β`, any set `s` of elements of type `β`, and any element `a` of type `α`, the statement "the element `a` is in the preimage of the set `s` under the function `f`" is equivalent to the statement "the image of `a` under `f` is in the set `s`". In mathematical terms, it says that $a \in f^{-1}(s)$ if and only if $f(a) \in s$.
More concisely: For any functions $f:\alpha \to \beta$ and sets $s \subseteq \beta$, the elements $a \in \alpha$ and $x \in \beta$ satisfy $a \in f^{-1}(s)$ if and only if $x = f(a) \in s$.
|
MeasureTheory.generateFrom_measurableCylinders
theorem MeasureTheory.generateFrom_measurableCylinders :
∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → MeasurableSpace (α i)],
MeasurableSpace.generateFrom (MeasureTheory.measurableCylinders α) = MeasurableSpace.pi
The theorem `MeasureTheory.generateFrom_measurableCylinders` states that for any type `ι` and a function `α` from `ι` to some type, given that each type `α i` has a `MeasurableSpace`, the smallest measure space containing all measurable cylinders (cylinders with measurable base `S`) is equivalent to the product of the individual measurable spaces. In other words, generating a measure space from all measurable cylinders in a product space yields the same result as combining each individual measurable space ("π-algebra") using the function `α`.
More concisely: The theorem asserts that the σ-algebra generated by measurable cylinders in the product of measurable spaces is equivalent to the product of their individual σ-algebras.
|