Projective measure families and projective limits

A family of measures indexed by finite sets of ι is projective if, for finite sets J ⊆ I, the projection from ∀ i : I, α i to ∀ i : J, α i maps P I to P J. A measure μ is the projective limit of such a family of measures if for all I : Finset ι, the projection from ∀ i, α i to ∀ i : I, α i maps μ to P I.

Main definitions

• MeasureTheory.IsProjectiveMeasureFamily: P : ∀ J : Finset ι, Measure (∀ j : J, α j) is projective if the projection from ∀ i : I, α i to ∀ i : J, α i maps P I to P J for all J ⊆ I.
• MeasureTheory.IsProjectiveLimit: μ is the projective limit of the measure family P if for all I : Finset ι, the map of μ by the projection to I is P I.

Main statements

• MeasureTheory.IsProjectiveLimit.unique: the projective limit of a family of finite measures is unique.

def MeasureTheory.IsProjectiveMeasureFamily {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] (P : (J : Finset ι) → MeasureTheory.Measure ((j : { x : ι // x ∈ J }) → α ↑j)) : Prop

A family of measures indexed by finite sets of ι is projective if, for finite sets J ⊆ I, the projection from ∀ i : I, α i to ∀ i : J, α i maps P I to P J.

Equations

• One or more equations did not get rendered due to their size.

theorem MeasureTheory.IsProjectiveMeasureFamily.measure_univ_eq_of_subset {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] {P : (J : Finset ι) → MeasureTheory.Measure ((j : { x : ι // x ∈ J }) → α ↑j)} {I : Finset ι} {J : Finset ι} (hP : MeasureTheory.IsProjectiveMeasureFamily P) (hJI : J ⊆ I) : (P I) Set.univ = (P J) Set.univ

Auxiliary lemma for measure_univ_eq.

theorem MeasureTheory.IsProjectiveMeasureFamily.measure_univ_eq {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] {P : (J : Finset ι) → MeasureTheory.Measure ((j : { x : ι // x ∈ J }) → α ↑j)} (hP : MeasureTheory.IsProjectiveMeasureFamily P) (I : Finset ι) (J : Finset ι) : (P I) Set.univ = (P J) Set.univ

theorem MeasureTheory.IsProjectiveMeasureFamily.congr_cylinder_of_subset {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] {P : (J : Finset ι) → MeasureTheory.Measure ((j : { x : ι // x ∈ J }) → α ↑j)} {I : Finset ι} {J : Finset ι} (hP : MeasureTheory.IsProjectiveMeasureFamily P) {S : Set ((i : { x : ι // x ∈ I }) → α ↑i)} {T : Set ((i : { x : ι // x ∈ J }) → α ↑i)} (hT : MeasurableSet T) (h_eq : MeasureTheory.cylinder I S = MeasureTheory.cylinder J T) (hJI : J ⊆ I) : (P I) S = (P J) T

theorem MeasureTheory.IsProjectiveMeasureFamily.congr_cylinder {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] {P : (J : Finset ι) → MeasureTheory.Measure ((j : { x : ι // x ∈ J }) → α ↑j)} {I : Finset ι} {J : Finset ι} (hP : MeasureTheory.IsProjectiveMeasureFamily P) {S : Set ((i : { x : ι // x ∈ I }) → α ↑i)} {T : Set ((i : { x : ι // x ∈ J }) → α ↑i)} (hS : MeasurableSet S) (hT : MeasurableSet T) (h_eq : MeasureTheory.cylinder I S = MeasureTheory.cylinder J T) : (P I) S = (P J) T

def MeasureTheory.IsProjectiveLimit {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] (μ : MeasureTheory.Measure ((i : ι) → α i)) (P : (J : Finset ι) → MeasureTheory.Measure ((j : { x : ι // x ∈ J }) → α ↑j)) : Prop

A measure μ is the projective limit of a family of measures indexed by finite sets of ι if for all I : Finset ι, the projection from ∀ i, α i to ∀ i : I, α i maps μ to P I.

Equations

• MeasureTheory.IsProjectiveLimit μ P = ∀ (I : Finset ι), MeasureTheory.Measure.map (fun (x : (i : ι) → α i) (i : { x : ι // x ∈ I }) => x ↑i) μ = P I

theorem MeasureTheory.IsProjectiveLimit.measure_cylinder {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] {P : (J : Finset ι) → MeasureTheory.Measure ((j : { x : ι // x ∈ J }) → α ↑j)} {μ : MeasureTheory.Measure ((i : ι) → α i)} (h : MeasureTheory.IsProjectiveLimit μ P) (I : Finset ι) {s : Set ((i : { x : ι // x ∈ I }) → α ↑i)} (hs : MeasurableSet s) : μ (MeasureTheory.cylinder I s) = (P I) s

theorem MeasureTheory.IsProjectiveLimit.measure_univ_eq {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] {P : (J : Finset ι) → MeasureTheory.Measure ((j : { x : ι // x ∈ J }) → α ↑j)} {μ : MeasureTheory.Measure ((i : ι) → α i)} (hμ : MeasureTheory.IsProjectiveLimit μ P) (I : Finset ι) : μ Set.univ = (P I) Set.univ

theorem MeasureTheory.IsProjectiveLimit.isFiniteMeasure {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] {P : (J : Finset ι) → MeasureTheory.Measure ((j : { x : ι // x ∈ J }) → α ↑j)} {μ : MeasureTheory.Measure ((i : ι) → α i)} [∀ (i : Finset ι), MeasureTheory.IsFiniteMeasure (P i)] (hμ : MeasureTheory.IsProjectiveLimit μ P) : MeasureTheory.IsFiniteMeasure μ

theorem MeasureTheory.IsProjectiveLimit.isProbabilityMeasure {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] {P : (J : Finset ι) → MeasureTheory.Measure ((j : { x : ι // x ∈ J }) → α ↑j)} {μ : MeasureTheory.Measure ((i : ι) → α i)} [∀ (i : Finset ι), MeasureTheory.IsProbabilityMeasure (P i)] (hμ : MeasureTheory.IsProjectiveLimit μ P) : MeasureTheory.IsProbabilityMeasure μ

theorem MeasureTheory.IsProjectiveLimit.measure_univ_unique {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] {P : (J : Finset ι) → MeasureTheory.Measure ((j : { x : ι // x ∈ J }) → α ↑j)} {μ : MeasureTheory.Measure ((i : ι) → α i)} {ν : MeasureTheory.Measure ((i : ι) → α i)} (hμ : MeasureTheory.IsProjectiveLimit μ P) (hν : MeasureTheory.IsProjectiveLimit ν P) : μ Set.univ = ν Set.univ

theorem MeasureTheory.IsProjectiveLimit.unique {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] {P : (J : Finset ι) → MeasureTheory.Measure ((j : { x : ι // x ∈ J }) → α ↑j)} {μ : MeasureTheory.Measure ((i : ι) → α i)} {ν : MeasureTheory.Measure ((i : ι) → α i)} [∀ (i : Finset ι), MeasureTheory.IsFiniteMeasure (P i)] (hμ : MeasureTheory.IsProjectiveLimit μ P) (hν : MeasureTheory.IsProjectiveLimit ν P) : μ = ν

The projective limit of a family of finite measures is unique.