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).

If the measures P J are inner regular with respect to compact closed sets, the additive content projectiveFamilyContent hP on the measurable cylinders is inner regular with respect to a compact system of square cylinders, hence it is σ-additive and extends to a measure.

Main definitions

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

Main statements

• projectiveFamilyContent_sigma_additive_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 : ι), R1Space (α 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 ∈ measurableCylinders α ∩ countableInfClosure (supClosure (insert ∅ (compactClosedSquareCylinders α))), 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 countable intersections of finite unions of compact closed square cylinders.

theorem MeasureTheory.projectiveFamilyContent_sigma_additive_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 : ι), R1Space (α 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 : ι), R1Space (α 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_sigma_additive {ι : 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, 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.

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)} [∀ (i : Finset ι), IsProbabilityMeasure (P i)] (hP : IsProjectiveMeasureFamily P) : IsProbabilityMeasure (projectiveLimit P hP)