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
mapsP I
toP J
for allJ ⊆ I
.MeasureTheory.IsProjectiveLimit
:μ
is the projective limit of the measure familyP
if for allI : Finset ι
, the map ofμ
by the projection toI
isP 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))
:
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
- MeasureTheory.IsProjectiveMeasureFamily P = ∀ (I J : Finset ι) (hJI : J ⊆ I), P J = MeasureTheory.Measure.map (Finset.restrict₂ hJI) (P I)
Instances For
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))
:
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 I.restrict μ = P I
Instances For
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)
:
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)
:
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.