MeasureTheory.IsProjectiveLimit.unique
theorem MeasureTheory.IsProjectiveLimit.unique :
∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → MeasurableSpace (α i)]
{P : (J : Finset ι) → MeasureTheory.Measure ((j : { x // x ∈ J }) → α ↑j)}
{μ ν : MeasureTheory.Measure ((i : ι) → α i)} [inst_1 : ∀ (i : Finset ι), MeasureTheory.IsFiniteMeasure (P i)],
MeasureTheory.IsProjectiveLimit μ P → MeasureTheory.IsProjectiveLimit ν P → μ = ν
The theorem states that the projective limit of a family of finite measures is unique. In other words, given a type `ι`, a function `α` from `ι` to another type, a measurable space for each `α i`, and a measure `P` on each finset of `ι`, if two measures `μ` and `ν` on the space of all functions from `ι` to `α i` are both projective limits of the family `P`, then `μ` and `ν` must be equal. A projective limit, in this case, means that for each finset `I` of `ι`, the measure `μ` or `ν` mapped via a projection function to the space of functions from `I` to `α i` is equal to the measure `P I`. Further, each measure `P i` for a finset `i` of `ι` is assumed to be finite.
More concisely: Given a family of finite measures `{P_i : Finset ι -> MeasurableSpace α i | i : Finset ι}`, if for all finsets `I` of `ι`, the projection measures `μ_I : MeasurableSpace (Functor.map α I) -> MeasurableSpace α, μ_I = ∫ i in I, P_i i`, and `ν_I : MeasurableSpace (Functor.map α I) -> MeasurableSpace α, ν_I = ∫ i in I, P_i i`, then `μ = ν`, where `μ` and `ν` are the projective limits of `{P_i}` on the measurable space of functions from `ι` to `α`.
|
MeasureTheory.IsProjectiveLimit.measure_univ_eq
theorem MeasureTheory.IsProjectiveLimit.measure_univ_eq :
∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → MeasurableSpace (α i)]
{P : (J : Finset ι) → MeasureTheory.Measure ((j : { x // x ∈ J }) → α ↑j)}
{μ : MeasureTheory.Measure ((i : ι) → α i)},
MeasureTheory.IsProjectiveLimit μ P → ∀ (I : Finset ι), ↑↑μ Set.univ = ↑↑(P I) Set.univ
This theorem states that for any type `ι` and a type map `α : ι → Type`, given a measure `μ` on the product of the types `α i` and a family of measures `P` indexed by finite subsets of `ι`, if `μ` is the projective limit of the family `P`, then the measure of the universal set with respect to `μ` is equal to the measure of the universal set with respect to each measure in the family `P`. In mathematical terms, if `μ` is the projective limit of `P`, then for every finite subset `I` of `ι`, we have that `μ(Universe) = P_I(Universe)`. The universal set in this context represents the set of all possible values of a given type.
More concisely: If `μ` is the projective limit of a family `P` of measures on types `α i`, then `μ(Universe) = ∏ I in Finset ι, P I(Universe)`.
Here, `Universe` represents the universal set of each type `α i`, and `Finset ι` is the type of finite subsets of `ι`. The notation `∏ I in Finset ι, P I(Universe)` denotes the product of measures `P I(Universe)` over all finite subsets `I` of `ι`.
|
MeasureTheory.IsProjectiveMeasureFamily.measure_univ_eq_of_subset
theorem MeasureTheory.IsProjectiveMeasureFamily.measure_univ_eq_of_subset :
∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → MeasurableSpace (α i)]
{P : (J : Finset ι) → MeasureTheory.Measure ((j : { x // x ∈ J }) → α ↑j)} {I J : Finset ι},
MeasureTheory.IsProjectiveMeasureFamily P → J ⊆ I → ↑↑(P I) Set.univ = ↑↑(P J) Set.univ
The theorem `MeasureTheory.IsProjectiveMeasureFamily.measure_univ_eq_of_subset` states that for any types `ι` and α, which is a function from `ι` to another type, and for any measurable space over these types, given a projective measure family `P` and two finite sets `I` and `J` of `ι`, if `P` is a projective measure family and `J` is a subset of `I`, then the measure of the universal set with respect to `P I` equals the measure of the universal set with respect to `P J`. In other words, if you have a family of measures that projects properly across subsets, then the measure of the whole space remains the same regardless of which finite subset of indices you consider.
More concisely: For any measurable space and a projective measure family over types ι and α, if J is a subset of I, then the measure of the universal set with respect to Pi equals the measure of the universal set with respect to Pj.
|