Kolmogorov extension theorem

Given a projective family of finite measures P J on the finite products Π j : J, α j, we construct its projective limit, a measure on Π i, α i, when the spaces α i are second-countable and completely pseudo-metrizable (for example Polish spaces).

Main definitions

• projectiveLimit P hP: the projective limit of a projective family of finite measures.

Main statements

• projectiveFamilyContent_iUnion_eq_tsum_of_innerRegular: the content projectiveFamilyContent hP is σ-additive if the measures P J are inner regular with respect to compact closed sets.
• isProjectiveLimit_projectiveLimit: Kolmogorov extension theorem, projectiveLimit P hP is the projective limit of P.

theorem MeasureTheory.innerRegular_projectiveFamilyContent {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] {P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)} [(i : ι) → TopologicalSpace (α i)] [∀ (i : ι), OpensMeasurableSpace (α i)] [∀ (i : ι), SecondCountableTopology (α i)] [∀ (I : Finset ι), IsFiniteMeasure (P I)] (hP : IsProjectiveMeasureFamily P) (hP_inner : ∀ (J : Finset ι), (P J).InnerRegularWRT (fun (s : Set ((j : ↥J) → α ↑j)) => IsCompact s ∧ IsClosed s) MeasurableSet) {s : Set ((i : ι) → α i)} (hs : s ∈ measurableCylinders α) (ε : ENNReal) (hε : 0 < ε) : ∃ K ∈ closedCompactCylinders α, K ⊆ s ∧ (projectiveFamilyContent hP) (s \ K) ≤ ε

If the measures P J are inner regular with respect to compact closed sets, then the content projectiveFamilyContent hP is inner regular with respect to cylinders with compact closed bases.

theorem MeasureTheory.projectiveFamilyContent_iUnion_eq_tsum_of_innerRegular {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] {P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)} [(i : ι) → TopologicalSpace (α i)] [∀ (i : ι), OpensMeasurableSpace (α i)] [∀ (i : ι), SecondCountableTopology (α i)] [∀ (I : Finset ι), IsFiniteMeasure (P I)] (hP : IsProjectiveMeasureFamily P) (hP_inner : ∀ (J : Finset ι), (P J).InnerRegularWRT (fun (s : Set ((j : ↥J) → α ↑j)) => IsCompact s ∧ IsClosed s) MeasurableSet) ⦃f : ℕ → Set ((i : ι) → α i)⦄ (hf : ∀ (i : ℕ), f i ∈ measurableCylinders α) (hf_Union : ⋃ (i : ℕ), f i ∈ measurableCylinders α) (h_disj : Pairwise (Function.onFun Disjoint f)) : (projectiveFamilyContent hP) (⋃ (i : ℕ), f i) = ∑' (i : ℕ), (projectiveFamilyContent hP) (f i)

If the measures P J are inner regular with respect to compact closed sets, then the content projectiveFamilyContent hP is σ-additive.

theorem MeasureTheory.isSigmaSubadditive_projectiveFamilyContent_of_innerRegular {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] {P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)} [(i : ι) → TopologicalSpace (α i)] [∀ (i : ι), OpensMeasurableSpace (α i)] [∀ (i : ι), SecondCountableTopology (α i)] [∀ (I : Finset ι), IsFiniteMeasure (P I)] (hP : IsProjectiveMeasureFamily P) (hP_inner : ∀ (J : Finset ι), (P J).InnerRegularWRT (fun (s : Set ((j : ↥J) → α ↑j)) => IsCompact s ∧ IsClosed s) MeasurableSet) : (projectiveFamilyContent hP).IsSigmaSubadditive

If the measures P J are inner regular with respect to compact closed sets, then the content projectiveFamilyContent hP is σ-subadditive.

theorem MeasureTheory.projectiveFamilyContent_iUnion_eq_tsum {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] {P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)} [(i : ι) → TopologicalSpace (α i)] [∀ (i : ι), SecondCountableTopology (α i)] [∀ (i : ι), TopologicalSpace.IsCompletelyPseudoMetrizableSpace (α i)] [∀ (i : ι), BorelSpace (α i)] [∀ (I : Finset ι), IsFiniteMeasure (P I)] (hP : IsProjectiveMeasureFamily P) ⦃f : ℕ → Set ((i : ι) → α i)⦄ (hf : ∀ (i : ℕ), f i ∈ measurableCylinders α) (hf_Union : ⋃ (i : ℕ), f i ∈ measurableCylinders α) (h_disj : Pairwise (Function.onFun Disjoint f)) : (projectiveFamilyContent hP) (⋃ (i : ℕ), f i) = ∑' (i : ℕ), (projectiveFamilyContent hP) (f i)

The content projectiveFamilyContent hP is σ-additive.

theorem MeasureTheory.isSigmaSubadditive_projectiveFamilyContent {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] {P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)} [(i : ι) → TopologicalSpace (α i)] [∀ (i : ι), SecondCountableTopology (α i)] [∀ (i : ι), TopologicalSpace.IsCompletelyPseudoMetrizableSpace (α i)] [∀ (i : ι), BorelSpace (α i)] [∀ (I : Finset ι), IsFiniteMeasure (P I)] (hP : IsProjectiveMeasureFamily P) : (projectiveFamilyContent hP).IsSigmaSubadditive

The content projectiveFamilyContent hP is σ-subadditive.

noncomputable def MeasureTheory.projectiveLimit {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] [(i : ι) → TopologicalSpace (α i)] [∀ (i : ι), SecondCountableTopology (α i)] [∀ (i : ι), TopologicalSpace.IsCompletelyPseudoMetrizableSpace (α i)] [∀ (i : ι), BorelSpace (α i)] (P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)) [∀ (i : Finset ι), IsFiniteMeasure (P i)] (hP : IsProjectiveMeasureFamily P) : Measure ((i : ι) → α i)

The projective limit of a projective family of finite measures on products of second-countable completely pseudo-metrizable spaces (for example Polish spaces). See isProjectiveLimit_projectiveLimit.

Equations

• MeasureTheory.projectiveLimit P hP = (MeasureTheory.projectiveFamilyContent hP).measure ⋯ ⋯ ⋯

theorem MeasureTheory.isProjectiveLimit_projectiveLimit {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] {P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)} [(i : ι) → TopologicalSpace (α i)] [∀ (i : ι), SecondCountableTopology (α i)] [∀ (i : ι), TopologicalSpace.IsCompletelyPseudoMetrizableSpace (α i)] [∀ (i : ι), BorelSpace (α i)] [∀ (I : Finset ι), IsFiniteMeasure (P I)] (hP : IsProjectiveMeasureFamily P) : IsProjectiveLimit (projectiveLimit P hP) P

Kolmogorov extension theorem: for any projective measure family P of finite measures, there exists a measure on Π i, α i which is the projective limit of P. That measure is given by projectiveLimit P hP, where hP : IsProjectiveMeasureFamily P. The projective limit is unique: see IsProjectiveLimit.unique. The spaces α i are assumed to be second-countable and completely pseudo-metrizable (for example Polish spaces)

instance MeasureTheory.isFiniteMeasure_projectiveLimit {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] {P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)} [(i : ι) → TopologicalSpace (α i)] [∀ (i : ι), SecondCountableTopology (α i)] [∀ (i : ι), TopologicalSpace.IsCompletelyPseudoMetrizableSpace (α i)] [∀ (i : ι), BorelSpace (α i)] [∀ (I : Finset ι), IsFiniteMeasure (P I)] (hP : IsProjectiveMeasureFamily P) : IsFiniteMeasure (projectiveLimit P hP)

instance MeasureTheory.isProbabilityMeasure_projectiveLimit {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] [(i : ι) → TopologicalSpace (α i)] [∀ (i : ι), SecondCountableTopology (α i)] [∀ (i : ι), TopologicalSpace.IsCompletelyPseudoMetrizableSpace (α i)] [∀ (i : ι), BorelSpace (α i)] {P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)} [∀ (J : Finset ι), IsProbabilityMeasure (P J)] (hP : IsProjectiveMeasureFamily P) : IsProbabilityMeasure (projectiveLimit P hP)