MeasureTheory.Measure.pi_eq_generateFrom
theorem MeasureTheory.Measure.pi_eq_generateFrom :
∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
{μ : (i : ι) → MeasureTheory.Measure (α i)} {C : (i : ι) → Set (Set (α i))},
(∀ (i : ι), MeasurableSpace.generateFrom (C i) = inst_1 i) →
(∀ (i : ι), IsPiSystem (C i)) →
((i : ι) → (μ i).FiniteSpanningSetsIn (C i)) →
∀ {μν : MeasureTheory.Measure ((i : ι) → α i)},
(∀ (s : (i : ι) → Set (α i)),
(∀ (i : ι), s i ∈ C i) → ↑↑μν (Set.univ.pi s) = Finset.univ.prod fun i => ↑↑(μ i) (s i)) →
MeasureTheory.Measure.pi μ = μν
This theorem states that for a finite product space, a given measure equals the product measure if and only if they coincide on all rectangles formed by sets that generate the corresponding σ-algebras. More specifically, for any finite set ι and a family of measurable spaces {α i}, if we have a family of measure spaces {μ i} and a family of sets {C i} such that the space generated from each C i equals the corresponding measurable space and each C i forms a π-system, and if each measure μ i forms finite spanning sets in each C i, then for any measure μν on the product space, if μν equals the product of the measures μ i for all rectangles formed by the sets in C i, then the product measure formed by μ i equals μν.
More concisely: Given finite product spaces Π(α i) with measurable spaces (α i, Σ i, μ i) and sets C i generating Σ i and forming a π-system, if each μ i has finite spanning sets in C i and μν equals the product measure of μ i on all rectangles formed by C i, then μν is the product measure of μ i.
|
MeasureTheory.Measure.ae_eq_set_pi
theorem MeasureTheory.Measure.ae_eq_set_pi :
∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
{μ : (i : ι) → MeasureTheory.Measure (α i)} [inst_2 : ∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] {I : Set ι}
{s t : (i : ι) → Set (α i)},
(∀ i ∈ I, (μ i).ae.EventuallyEq (s i) (t i)) → (MeasureTheory.Measure.pi μ).ae.EventuallyEq (I.pi s) (I.pi t)
This theorem states that for all index sets `ι`, every function `α : ι → Type u_3`, any finite instance of `ι`, measurable space of `α i` for every `i : ι`, measure `μ : (i : ι) → MeasureTheory.Measure (α i)` and sigma-finite measure `μ i` for every `i : ι`, if `I` is a set of `ι` and `s` and `t` are two functions such that for every `i` in `I`, `s i` is almost everywhere equal to `t i` with respect to the measure `μ i`, then the set of dependent functions `f : Πa, π a` such that `f a` belongs to `t a` whenever `a ∈ s` is almost everywhere equal to the set of dependent functions `f : Πa, π a` such that `f a` belongs to `t a` whenever `a ∈ t` with respect to the measure `MeasureTheory.Measure.pi μ`. This theorem is essentially stating that if two sets are almost everywhere equal with respect to their individual measures, then the sets of dependent functions are also almost everywhere equal with respect to the product measure.
More concisely: Given index sets `ι`, functions `α : ι → Type u_3`, measurable spaces `(α i, μ i)` for every `i : ι`, sigma-finite measures `μ i`, a set `I ⊆ ι`, and functions `s, t : I → ι`, if for all `i` in `I`, `μ i`-almost everywhere `s i = t i`, then the sets of dependent functions `{f : Πa, π a | f a ∈ t a ∧ a ∈ s}` and `{f : Πa, π a | f a ∈ t a}` have equal `MeasureTheory.Measure.pi μ`-measure.
|
MeasureTheory.Measure.pi_of_empty
theorem MeasureTheory.Measure.pi_of_empty :
∀ {α : Type u_4} [inst : Fintype α] [inst_1 : IsEmpty α] {β : α → Type u_5} {m : (a : α) → MeasurableSpace (β a)}
(μ : (a : α) → MeasureTheory.Measure (β a)) (x : optParam ((a : α) → β a) fun a => isEmptyElim a),
MeasureTheory.Measure.pi μ = MeasureTheory.Measure.dirac x
This theorem, `MeasureTheory.Measure.pi_of_empty`, states that for any type `α` that is a Fintype (i.e., it has a finite number of elements) and is also empty, and for any function `β : α → Type u_5` that maps each element of `α` to a measurable space, and for any measure `μ : (a : α) → MeasureTheory.Measure (β a)`, which is a function that assigns a measure to each element of `α`, then the finite product of these measures, `MeasureTheory.Measure.pi μ`, is equal to the Dirac measure at a point `x`, where `x` is a function from `α` to `β a` that uses the elimination of emptiness if `α` is empty. The Dirac measure `MeasureTheory.Measure.dirac x` is a measure that is zero everywhere except at the point `x`.
More concisely: For any empty Fintype `α` and function `β : α → Type u_5`, if `μ : α → MeasureTheory.Measure (β α)` assigns a measure to each `α` element, then the product measure `MeasureTheory.Measure.pi μ` equals the Dirac measure at a point `x : α → β α`.
|
MeasureTheory.measurePreserving_piUnique
theorem MeasureTheory.measurePreserving_piUnique :
∀ {ι : Type u_1} [inst : Fintype ι] {π : ι → Type u_4} [inst_1 : Unique ι] {m : (i : ι) → MeasurableSpace (π i)}
(μ : (i : ι) → MeasureTheory.Measure (π i)),
MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.piUnique π)) (MeasureTheory.Measure.pi μ) (μ default)
The theorem `MeasureTheory.measurePreserving_piUnique` states that for any finite type `ι` with a unique element, and for any measurable spaces `π i` indexed by `ι`, the function `MeasurableEquiv.piUnique π` is measure preserving. Specifically, if `μ` is a family of measures indexed by `ι`, then applying the `MeasurableEquiv.piUnique π` mapping to the product measure `MeasureTheory.Measure.pi μ` gives the same measure as `μ default`, where `default` is the unique element of `ι`. In other words, this theorem asserts that the product measure of a one-element index set behaves as expected: it is equivalent to the measure of the single indexed element.
More concisely: The theorem asserts that for any finite type with a unique element and corresponding measurable spaces indexed by it, the measure preserving function `MeasurableEquiv.piUnique` maps the product measure to the measure of the unique indexed element.
|
MeasureTheory.Measure.pi_eq
theorem MeasureTheory.Measure.pi_eq :
∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
{μ : (i : ι) → MeasureTheory.Measure (α i)} [inst_2 : ∀ (i : ι), MeasureTheory.SigmaFinite (μ i)]
{μ' : MeasureTheory.Measure ((i : ι) → α i)},
(∀ (s : (i : ι) → Set (α i)),
(∀ (i : ι), MeasurableSet (s i)) → ↑↑μ' (Set.univ.pi s) = Finset.univ.prod fun i => ↑↑(μ i) (s i)) →
MeasureTheory.Measure.pi μ = μ'
This theorem states that for a measure on a finite product space, it equals the product measure if they coincide on rectangles. Specifically, given an index set `ι`, a family of measurable spaces `α i` for each `i` in `ι`, a family of measures `μ i` for each `i` in `ι`, and a measure `μ'` on the product space, if for every family of sets `s i` such that each `s i` is measurable, the measure `μ'` of the set of all functions from `ι` to `α i` that map each `i` to an element of `s i` equals the product (over all `i` in `ι`) of the measures `μ i` of `s i`, then the product measure of the `μ i` is equal to `μ'`. In mathematical terms, given $s_i \subseteq \alpha_i$ for all $i \in \mathbb{I}$, if $\mu'(\prod_{i \in \mathbb{I}} s_i) = \prod_{i \in \mathbb{I}} \mu_i(s_i)$, then the measure on the product space induced by the $\mu_i$ equals $\mu'$.
More concisely: If for all families of sets {Si : i ∈ I} with each Si measurable, the product measure of the family {Mi : i ∈ I} of measures and the measure of their product in the product space coincide, then the product measure of the family equals the given measure on the product space.
|
MeasureTheory.volume_pi_pi
theorem MeasureTheory.volume_pi_pi :
∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasureTheory.MeasureSpace (α i)]
[inst_2 : ∀ (i : ι), MeasureTheory.SigmaFinite MeasureTheory.volume] (s : (i : ι) → Set (α i)),
↑↑MeasureTheory.volume (Set.univ.pi s) = Finset.univ.prod fun i => ↑↑MeasureTheory.volume (s i)
This theorem, called `MeasureTheory.volume_pi_pi`, states that for any finite type `ι`, and a function `α` that maps each element of `ι` to a type, under the assumptions that each `α i` is a measure space and that the measure volume is sigma-finite for all `i` in `ι`, the measure of the product of sets `s : (i : ι) → Set (α i)` equals the product of the measures of each individual set `s i`. Specifically, it says that the measure of the set of all functions `f : ι → α i` such that for all `i` in `ι`, `f i` is in `s i`, is equal to the product of the measures of all `s i` as `i` ranges over all elements of `ι`.
More concisely: For any sigma-finite measure space `(α i)` indexed by a finite type `ι`, the measure of the product of sets `{f : ι → α i | ∀ i, f i ∈ s i}` equals the product of the measures of `s i` as `i` ranges over `ι`.
|
IsCountablySpanning.pi
theorem IsCountablySpanning.pi :
∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Finite ι] {C : (i : ι) → Set (Set (α i))},
(∀ (i : ι), IsCountablySpanning (C i)) → IsCountablySpanning (Set.univ.pi '' Set.univ.pi C)
The theorem `IsCountablySpanning.pi` states that for any finite type `ι` and a type function `α : ι → Type u_3`, if for each `i : ι`, the set `C i` is countably spanning, then the set of all functions from `Set.univ.pi '' Set.univ.pi C`, which is the set of all products of the `C i`'s, is also countably spanning. In other words, if every set `C i` for each `i : ι` can be covered by countably many of its subsets, then the Cartesian product of these sets `C i` can also be covered by countably many of its "box-shaped" subsets.
More concisely: If each `C i` for `i` in a finite type `ι` is countably spanning, then the Cartesian product of the `C i`'s is also countably spanning.
|
MeasureTheory.Measure.tendsto_eval_ae_ae
theorem MeasureTheory.Measure.tendsto_eval_ae_ae :
∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
{μ : (i : ι) → MeasureTheory.Measure (α i)} [inst_2 : ∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] {i : ι},
Filter.Tendsto (Function.eval i) (MeasureTheory.Measure.pi μ).ae (μ i).ae
This theorem, `MeasureTheory.Measure.tendsto_eval_ae_ae`, states that for every index `i` in a finite type `ι`, the evaluation function at index `i` tends to the "almost everywhere" (ae) filter of the measure `μ i` when taken over the "almost everywhere" filter of the product measure of all `μ i`.
More concretely, given a set of measures `μ : (i : ι) → MeasureTheory.Measure (α i)` indexed by `ι` where each `α i` is a measurable space, and `μ i` is sigma-finite for each `i`, the theorem asserts that if you consider sequences of functions in the product space (viewed as sequences of vectors), then the sequence of i-th components of these vectors (given by `Function.eval i`) converge "almost everywhere" to the same value as the sequence in the individual space "almost everywhere" with respect to the measure `μ i`. This is a form of the Fubini's theorem for measures, asserting the commutation of limits and integral when passing from the product space to the individual spaces.
More concisely: Given a family of sigma-finite measures `μ i` on measurable spaces `(α i)` indexed by `ι`, the evaluation function `Function.eval i` at each index `i` tends to the same value almost everywhere with respect to the product measure of all `μ i`s. (This is a form of Fubini's theorem for measures.)
|
generateFrom_pi
theorem generateFrom_pi :
∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Finite ι] [inst : (i : ι) → MeasurableSpace (α i)],
MeasurableSpace.generateFrom (Set.univ.pi '' Set.univ.pi fun i => {s | MeasurableSet s}) = MeasurableSpace.pi
This theorem, named `generateFrom_pi`, states that for any finite type `ι` and any family of types `α` indexed by `ι`, where each type `α i` is equipped with a measurable space, the product measurable space is generated from all rectangles `s ×ˢ t`, where `s` and `t` are measurable sets in some `α i`. Here, `Set.univ.pi` refers to the product of all sets in the universe, and `MeasurableSet s` indicates that `s` is a measurable set. The theorem thereby provides a basic description of the structure of the product σ-algebra in terms of these "box" sets.
More concisely: The product measurable space of a family of measurable spaces indexed by a finite type is generated by the rectangles formed by measurable sets in each space.
|
IsPiSystem.pi
theorem IsPiSystem.pi :
∀ {ι : Type u_1} {α : ι → Type u_3} {C : (i : ι) → Set (Set (α i))},
(∀ (i : ι), IsPiSystem (C i)) → IsPiSystem (Set.univ.pi '' Set.univ.pi C)
This theorem states that if for each index `ι`, a collection of subsets `C i` of a set `α i` forms a π-system (i.e., it is closed under the intersection of non-disjoint sets), then the boxes formed by these π-systems also form a π-system. Here, a box is a Cartesian product of sets, one from each `C i`, so 'universally indexed' by `ι`. The theorem thus asserts a closure property of π-systems under formation of "product sets" in this way.
More concisely: If each `ι` gives a π-system `C i` of subsets of `α i`, then the collection of boxes formed by their products `∏ i C i` is also a π-system.
|
isPiSystem_pi
theorem isPiSystem_pi :
∀ {ι : Type u_1} {α : ι → Type u_3} [inst : (i : ι) → MeasurableSpace (α i)],
IsPiSystem (Set.univ.pi '' Set.univ.pi fun i => {s | MeasurableSet s})
The theorem `isPiSystem_pi` states that the collection of all boxes (i.e., Cartesian products of sets) forms a π-system. In more detail, for any index type `ι` and a family of measurable types `α i` indexed by `ι`, the image of the universal set under the function that forms the Cartesian product of all `s` such that `s` is a measurable set, forms a π-system. In particular, this collection is closed under taking the intersection of any two of its non-disjoint subsets.
More concisely: For any index type ι and measurable sets `α i` (i ∈ ι), the collection of their Cartesian products forms a π-system and is closed under intersections of non-disjoint subsets.
|
generateFrom_pi_eq
theorem generateFrom_pi_eq :
∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Finite ι] {C : (i : ι) → Set (Set (α i))},
(∀ (i : ι), IsCountablySpanning (C i)) →
MeasurableSpace.pi = MeasurableSpace.generateFrom (Set.univ.pi '' Set.univ.pi C)
This theorem states that for any finite set of indices `ι` and a function `α` mapping each index to a type, if for each index `i` the set `C i` is countably spanning, then the product of the generated σ-algebras is equal to the smallest measure space containing the Cartesian product of the universal set and the images of the sets `C i` under the function `Set.univ.pi`. In other words, this theorem provides a condition under which the σ-algebra generated by the product of a collection of sets is equivalent to the one generated by "boxes" of these sets, which is a crucial part of measure theory and its applications.
More concisely: For any finite index set `ι` and function `α : ι → Type`, if each `C i := α i ^^ coe Set.univ` is countably spanning, then `∏ i in ι` `C i` is equivalent to the σ-algebra generated by the Cartesian product of the universal set and the images of the sets `C i` under `α`.
|
MeasureTheory.Measure.pi_noAtoms
theorem MeasureTheory.Measure.pi_noAtoms :
∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
{μ : (i : ι) → MeasureTheory.Measure (α i)} [inst_2 : ∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] (i : ι)
[inst_3 : MeasureTheory.NoAtoms (μ i)], MeasureTheory.NoAtoms (MeasureTheory.Measure.pi μ)
This theorem, `MeasureTheory.Measure.pi_noAtoms`, states that if you take a finite number of measure spaces indexed by `ι`, each with measure `μ i`, and if one of these measures `μ i` has no atoms (that is, there are no subsets of the space that have positive probability but whose subsets all have zero probability), then the product measure `Measure.pi μ` also has no atoms. This theorem assumes that all of the measures `μ i` are sigma-finite, meaning they can be decomposed into a countable union of finite measures.
More concisely: If each measure in a finite family of sigma-finite, atomless measure spaces has no atoms, then their product measure also has no atoms.
|
MeasureTheory.Measure.pi'_pi
theorem MeasureTheory.Measure.pi'_pi :
∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
(μ : (i : ι) → MeasureTheory.Measure (α i)) [inst_2 : Encodable ι]
[inst_3 : ∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] (s : (i : ι) → Set (α i)),
↑↑(MeasureTheory.Measure.pi' μ) (Set.univ.pi s) = Finset.univ.prod fun i => ↑↑(μ i) (s i)
This theorem, `MeasureTheory.Measure.pi'_pi`, states that for a given index set `ι` and a family of types `α : ι → Type` where `ι` has a `Fintype` instance, and each `α i` has a `MeasurableSpace` instance, then given `μ` (a function that for each index `i` of type `ι` returns a measure on `α i`), and `s` (a function that for each index `i` of type `ι` returns a set of `α i`), if each measure `μ i` is sigma finite and `ι` is encodable, then the measure of the set of all possible functions (`Set.pi Set.univ s`) under the product measure (`MeasureTheory.Measure.pi' μ`) is equal to the product of the measures of all `s i` under their corresponding measures `μ i`. That is, the total measure of the set of all possible functions from `ι` to their corresponding sets `s i` (which are subsets of their corresponding `α i`) is the product of the measures of all `s i` under their corresponding measures `μ i`. This theorem is a formalization of the concept of the product measure in measure theory.
More concisely: Given a family of measurable spaces `(α i : ι → Type)` indexed by a finite set `ι`, if each `μ i : MeasurableMeasure α i` is sigma-finite and `ι` is encodable, then `MeasureTheory.Measure.pi' μ (Set.pi Set.univ (λ i, s i)) = ∏ i : ι, μ i (s i)`.
|
MeasureTheory.measurePreserving_sumPiEquivProdPi_symm
theorem MeasureTheory.measurePreserving_sumPiEquivProdPi_symm :
∀ {ι : Type u_1} {ι' : Type u_2} [inst : Fintype ι] [inst_1 : Fintype ι'] {π : ι ⊕ ι' → Type u_4}
{m : (i : ι ⊕ ι') → MeasurableSpace (π i)} (μ : (i : ι ⊕ ι') → MeasureTheory.Measure (π i))
[inst_2 : ∀ (i : ι ⊕ ι'), MeasureTheory.SigmaFinite (μ i)],
MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.sumPiEquivProdPi π).symm)
((MeasureTheory.Measure.pi fun i => μ (Sum.inl i)).prod (MeasureTheory.Measure.pi fun i => μ (Sum.inr i)))
(MeasureTheory.Measure.pi μ)
This theorem states that for any two types `ι` and `ι'`, along with a measurable space `π` indexed over the disjoint union of `ι` and `ι'`, and a collection of sigma-finite measures `μ` indexed over the disjoint union of `ι` and `ι'`, the measure preserving property holds for the inverse of the measurable equivalence given by `MeasurableEquiv.sumPiEquivProdPi π`. This means that the product measure of the pi-measure over `ι` and the pi-measure over `ι'` under this inverse equivalence is the same as the pi-measure over the disjoint union of `ι` and `ι'`.
More concisely: Given measurable spaces `π` over disjoint unions of types `ι` and `ι'`, and sigma-finite measures `μ` indexed over them, the product measure of `μ` under the inverse of `MeasurableEquiv.sumPiEquivProdPi π` is equal to the measure `μ` on the disjoint union.
|
generateFrom_eq_pi
theorem generateFrom_eq_pi :
∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Finite ι] [h : (i : ι) → MeasurableSpace (α i)]
{C : (i : ι) → Set (Set (α i))},
(∀ (i : ι), MeasurableSpace.generateFrom (C i) = h i) →
(∀ (i : ι), IsCountablySpanning (C i)) →
MeasurableSpace.generateFrom (Set.univ.pi '' Set.univ.pi C) = MeasurableSpace.pi
This theorem states that if we have a finite index set `ι` and for each `i` in `ι`, `C(i)` generates the σ-algebra on the type `α(i)`, then the rectangles formed by `C(i)` (i.e., sets of the form `{x | ∀i, x(i) ∈ C(i)}`) generate the σ-algebra on the product space `(i : ι) → α(i)`. It requires the additional assumption that each `C(i)` is countably spanning, which means that there exists a countable subset that spans the whole type.
More concisely: If `ι` is finite and for each `i` in `ι`, `C(i)` is a countably spanning generator of the σ-algebra on `α(i)`, then the rectangular sets generated by `C(i)` form a σ-algebra on the product space `(i : ι) → α(i)`.
|
MeasureTheory.Measure.pi_pi
theorem MeasureTheory.Measure.pi_pi :
∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
(μ : (i : ι) → MeasureTheory.Measure (α i)) [inst_2 : ∀ (i : ι), MeasureTheory.SigmaFinite (μ i)]
(s : (i : ι) → Set (α i)),
↑↑(MeasureTheory.Measure.pi μ) (Set.univ.pi s) = Finset.univ.prod fun i => ↑↑(μ i) (s i)
The theorem `MeasureTheory.Measure.pi_pi` states that for a finite index set ι and a family of measurable spaces (α i) indexed by ι, given a family of measures (μ i), each of which is sigma-finite, and a family of sets (s i), the measure of the product set (which is the set of all dependent functions that map each index to its corresponding set) under the product measure is equal to the product of measures of each individual set. More formally, if we apply the product measure to the set of all dependent functions, it's equal to the product, over all indices in our finite set, of the measure of each individual set. This theorem relates the measure of a product space to the measures of the individual component spaces.
More concisely: Given finite index set ι, measurable spaces (α\_i) with sigma-finite measures (μ\_i), the product measure of the family of measurable sets (s\_i) equals the product of the measures of the individual sets.
|