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

theorem MeasureTheory.innerRegular_projectiveFamilyContent {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] {P : (J : Finset ι) → Measure ((j : { x : ι // x ∈ 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 : { x : ι // x ∈ 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) ≤ ε

theorem MeasureTheory.projectiveFamilyContent_sigma_additive_of_innerRegular {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] {P : (J : Finset ι) → Measure ((j : { x : ι // x ∈ 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 : { x : ι // x ∈ 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)

theorem MeasureTheory.projectiveFamilyContent_iUnion_le_sum_of_innerRegular {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] {P : (J : Finset ι) → Measure ((j : { x : ι // x ∈ 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 : { x : ι // x ∈ J }) → α ↑j)) => IsCompact s ∧ IsClosed s) MeasurableSet) ⦃f : ℕ → Set ((i : ι) → α i)⦄ (hf : ∀ (i : ℕ), f i ∈ measurableCylinders α) (hf_Union : ⋃ (i : ℕ), f i ∈ measurableCylinders α) : (projectiveFamilyContent hP) (⋃ (i : ℕ), f i) ≤ ∑' (i : ℕ), (projectiveFamilyContent hP) (f i)

noncomputable def MeasureTheory.projectiveLimitWithWeakestHypotheses {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] [(i : ι) → PseudoEMetricSpace (α i)] [∀ (i : ι), BorelSpace (α i)] [∀ (i : ι), SecondCountableTopology (α i)] [∀ (i : ι), CompleteSpace (α i)] (P : (J : Finset ι) → Measure ((j : { x : ι // x ∈ J }) → α ↑j)) [∀ (i : Finset ι), IsFiniteMeasure (P i)] (hP : IsProjectiveMeasureFamily P) : Measure ((i : ι) → α i)

Projective limit of a projective measure family.

Equations

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

theorem MeasureTheory.projectiveFamilyContent_sigma_additive {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] {P : (J : Finset ι) → Measure ((j : { x : ι // x ∈ J }) → α ↑j)} [(i : ι) → TopologicalSpace (α i)] [∀ (i : ι), BorelSpace (α i)] [∀ (i : ι), PolishSpace (α 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)

theorem MeasureTheory.projectiveFamilyContent_iUnion_le_sum {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] {P : (J : Finset ι) → Measure ((j : { x : ι // x ∈ J }) → α ↑j)} [(i : ι) → TopologicalSpace (α i)] [∀ (i : ι), BorelSpace (α i)] [∀ (i : ι), PolishSpace (α i)] [∀ (I : Finset ι), IsFiniteMeasure (P I)] (hP : IsProjectiveMeasureFamily P) ⦃f : ℕ → Set ((i : ι) → α i)⦄ (hf : ∀ (i : ℕ), f i ∈ measurableCylinders α) (hf_Union : ⋃ (i : ℕ), f i ∈ measurableCylinders α) : (projectiveFamilyContent hP) (⋃ (i : ℕ), f i) ≤ ∑' (i : ℕ), (projectiveFamilyContent hP) (f i)

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

Projective limit of a projective measure family.

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 : { x : ι // x ∈ J }) → α ↑j)} [(i : ι) → TopologicalSpace (α i)] [∀ (i : ι), BorelSpace (α i)] [∀ (i : ι), PolishSpace (α 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 : { x : ι // x ∈ J }) → α ↑j)} [(i : ι) → TopologicalSpace (α i)] [∀ (i : ι), BorelSpace (α i)] [∀ (i : ι), PolishSpace (α 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 : ι), BorelSpace (α i)] [∀ (i : ι), PolishSpace (α i)] [hι : Nonempty ι] {P : (J : Finset ι) → Measure ((j : { x : ι // x ∈ J }) → α ↑j)} [∀ (i : Finset ι), IsProbabilityMeasure (P i)] (hP : IsProjectiveMeasureFamily P) : IsProbabilityMeasure (projectiveLimit P hP)