noncomputable def MeasureTheory.kolmogorovFun {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] (P : (J : Finset ι) → MeasureTheory.Measure ((j : { x : ι // x ∈ J }) → α ↑j)) (s : Set ((i : ι) → α i)) (hs : s ∈ MeasureTheory.measurableCylinders α) : ENNReal

We will show that this is an additive set function that defines a measure.

Equations

• MeasureTheory.kolmogorovFun P s hs = (P (MeasureTheory.measurableCylinders.finset hs)) (MeasureTheory.measurableCylinders.set hs)

theorem MeasureTheory.kolmogorovFun_congr_set {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] {P : (J : Finset ι) → MeasureTheory.Measure ((j : { x : ι // x ∈ J }) → α ↑j)} {s : Set ((i : ι) → α i)} {t : Set ((i : ι) → α i)} (hs : s ∈ MeasureTheory.measurableCylinders α) (h_eq : s = t) : MeasureTheory.kolmogorovFun P s hs = MeasureTheory.kolmogorovFun P t ⋯

theorem MeasureTheory.kolmogorovFun_congr {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] {P : (J : Finset ι) → MeasureTheory.Measure ((j : { x : ι // x ∈ J }) → α ↑j)} (hP : MeasureTheory.IsProjectiveMeasureFamily P) {s : Set ((i : ι) → α i)} (hs : s ∈ MeasureTheory.measurableCylinders α) {I : Finset ι} {S : Set ((i : { x : ι // x ∈ I }) → α ↑i)} (hs_eq : s = MeasureTheory.cylinder I S) (hS : MeasurableSet S) : MeasureTheory.kolmogorovFun P s hs = (P I) S

theorem MeasureTheory.kolmogorovFun_empty {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] {P : (J : Finset ι) → MeasureTheory.Measure ((j : { x : ι // x ∈ J }) → α ↑j)} (hP : MeasureTheory.IsProjectiveMeasureFamily P) : MeasureTheory.kolmogorovFun P ∅ ⋯ = 0

theorem MeasureTheory.kolmogorovFun_union {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] {P : (J : Finset ι) → MeasureTheory.Measure ((j : { x : ι // x ∈ J }) → α ↑j)} {s : Set ((i : ι) → α i)} {t : Set ((i : ι) → α i)} (hP : MeasureTheory.IsProjectiveMeasureFamily P) (hs : s ∈ MeasureTheory.measurableCylinders α) (ht : t ∈ MeasureTheory.measurableCylinders α) (hst : Disjoint s t) : MeasureTheory.kolmogorovFun P (s ∪ t) ⋯ = MeasureTheory.kolmogorovFun P s hs + MeasureTheory.kolmogorovFun P t ht

theorem MeasureTheory.kolmogorovFun_additive {ι : 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 (Set ((i : ι) → α i))) (h_ss : ↑I ⊆ MeasureTheory.measurableCylinders α) (h_dis : (↑I).PairwiseDisjoint id) (h_mem : ⋃₀ ↑I ∈ MeasureTheory.measurableCylinders α) : MeasureTheory.kolmogorovFun P (⋃₀ ↑I) h_mem = ∑ u : { x : Set ((i : ι) → α i) // x ∈ I }, MeasureTheory.kolmogorovFun P ↑u ⋯

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

kolmogorovFun as an additive content.

Equations

• MeasureTheory.kolContent hP = MeasureTheory.extendContent ⋯ (MeasureTheory.kolmogorovFun P) ⋯ ⋯

theorem MeasureTheory.kolContent_eq {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] {P : (J : Finset ι) → MeasureTheory.Measure ((j : { x : ι // x ∈ J }) → α ↑j)} {s : Set ((i : ι) → α i)} (hP : MeasureTheory.IsProjectiveMeasureFamily P) (hs : s ∈ MeasureTheory.measurableCylinders α) : (MeasureTheory.kolContent hP) s = MeasureTheory.kolmogorovFun P s hs

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

theorem MeasureTheory.kolContent_cylinder {ι : 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 ι} {S : Set ((i : { x : ι // x ∈ I }) → α ↑i)} (hS : MeasurableSet S) : (MeasureTheory.kolContent hP) (MeasureTheory.cylinder I S) = (P I) S

theorem MeasureTheory.kolContent_mono {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] {P : (J : Finset ι) → MeasureTheory.Measure ((j : { x : ι // x ∈ J }) → α ↑j)} {s : Set ((i : ι) → α i)} {t : Set ((i : ι) → α i)} (hP : MeasureTheory.IsProjectiveMeasureFamily P) (hs : s ∈ MeasureTheory.measurableCylinders α) (ht : t ∈ MeasureTheory.measurableCylinders α) (hst : s ⊆ t) : (MeasureTheory.kolContent hP) s ≤ (MeasureTheory.kolContent hP) t

theorem MeasureTheory.kolContent_iUnion_le {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] {P : (J : Finset ι) → MeasureTheory.Measure ((j : { x : ι // x ∈ J }) → α ↑j)} (hP : MeasureTheory.IsProjectiveMeasureFamily P) ⦃s : ℕ → Set ((i : ι) → α i)⦄ (hs : ∀ (n : ℕ), s n ∈ MeasureTheory.measurableCylinders α) (n : ℕ) : (MeasureTheory.kolContent hP) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), s i) ≤ ∑ i ∈ Finset.range (n + 1), (MeasureTheory.kolContent hP) (s i)

theorem MeasureTheory.kolContent_diff {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] {P : (J : Finset ι) → MeasureTheory.Measure ((j : { x : ι // x ∈ J }) → α ↑j)} {s : Set ((i : ι) → α i)} {t : Set ((i : ι) → α i)} (hP : MeasureTheory.IsProjectiveMeasureFamily P) (hs : s ∈ MeasureTheory.measurableCylinders α) (ht : t ∈ MeasureTheory.measurableCylinders α) : (MeasureTheory.kolContent hP) s - (MeasureTheory.kolContent hP) t ≤ (MeasureTheory.kolContent hP) (s \ t)

theorem MeasureTheory.kolContent_ne_top {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] {P : (J : Finset ι) → MeasureTheory.Measure ((j : { x : ι // x ∈ J }) → α ↑j)} {s : Set ((i : ι) → α i)} [∀ (J : Finset ι), MeasureTheory.IsFiniteMeasure (P J)] (hP : MeasureTheory.IsProjectiveMeasureFamily P) (hs : s ∈ MeasureTheory.measurableCylinders α) : (MeasureTheory.kolContent hP) s ≠ ⊤

theorem MeasureTheory.kolContent_diff_of_subset {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] {P : (J : Finset ι) → MeasureTheory.Measure ((j : { x : ι // x ∈ J }) → α ↑j)} {s : Set ((i : ι) → α i)} {t : Set ((i : ι) → α i)} [∀ (J : Finset ι), MeasureTheory.IsFiniteMeasure (P J)] (hP : MeasureTheory.IsProjectiveMeasureFamily P) (hs : s ∈ MeasureTheory.measurableCylinders α) (ht : t ∈ MeasureTheory.measurableCylinders α) (hts : t ⊆ s) : (MeasureTheory.kolContent hP) (s \ t) = (MeasureTheory.kolContent hP) s - (MeasureTheory.kolContent hP) t

theorem MeasureTheory.exists_compact {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] {P : (J : Finset ι) → MeasureTheory.Measure ((j : { x : ι // x ∈ J }) → α ↑j)} [(i : ι) → TopologicalSpace (α i)] [∀ (i : ι), OpensMeasurableSpace (α i)] [∀ (i : ι), SecondCountableTopology (α i)] [∀ (I : Finset ι), MeasureTheory.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_kolContent {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] {P : (J : Finset ι) → MeasureTheory.Measure ((j : { x : ι // x ∈ J }) → α ↑j)} [(i : ι) → TopologicalSpace (α i)] [∀ (i : ι), OpensMeasurableSpace (α i)] [∀ (i : ι), SecondCountableTopology (α i)] [∀ (I : Finset ι), MeasureTheory.IsFiniteMeasure (P I)] (hP : MeasureTheory.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 ∈ MeasureTheory.measurableCylinders α) (ε : ENNReal) (hε : 0 < ε) : ∃ K ∈ closedCompactCylinders α, K ⊆ s ∧ (MeasureTheory.kolContent hP) (s \ K) ≤ ε

theorem MeasureTheory.kolContent_sigma_additive_of_innerRegular {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] {P : (J : Finset ι) → MeasureTheory.Measure ((j : { x : ι // x ∈ J }) → α ↑j)} [(i : ι) → TopologicalSpace (α i)] [∀ (i : ι), OpensMeasurableSpace (α i)] [∀ (i : ι), SecondCountableTopology (α i)] [∀ (I : Finset ι), MeasureTheory.IsFiniteMeasure (P I)] (hP : MeasureTheory.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 ∈ MeasureTheory.measurableCylinders α) (hf_Union : ⋃ (i : ℕ), f i ∈ MeasureTheory.measurableCylinders α) (h_disj : Pairwise (Disjoint on f)) : (MeasureTheory.kolContent hP) (⋃ (i : ℕ), f i) = ∑' (i : ℕ), (MeasureTheory.kolContent hP) (f i)

theorem MeasureTheory.kolContent_sigma_subadditive_of_innerRegular {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] {P : (J : Finset ι) → MeasureTheory.Measure ((j : { x : ι // x ∈ J }) → α ↑j)} [(i : ι) → TopologicalSpace (α i)] [∀ (i : ι), OpensMeasurableSpace (α i)] [∀ (i : ι), SecondCountableTopology (α i)] [∀ (I : Finset ι), MeasureTheory.IsFiniteMeasure (P I)] (hP : MeasureTheory.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 ∈ MeasureTheory.measurableCylinders α) (hf_Union : ⋃ (i : ℕ), f i ∈ MeasureTheory.measurableCylinders α) : (MeasureTheory.kolContent hP) (⋃ (i : ℕ), f i) ≤ ∑' (i : ℕ), (MeasureTheory.kolContent 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 ι) → MeasureTheory.Measure ((j : { x : ι // x ∈ J }) → α ↑j)) [∀ (i : Finset ι), MeasureTheory.IsFiniteMeasure (P i)] (hP : MeasureTheory.IsProjectiveMeasureFamily P) : MeasureTheory.Measure ((i : ι) → α i)

Projective limit of a projective measure family.

Equations

• MeasureTheory.projectiveLimitWithWeakestHypotheses P hP = MeasureTheory.Measure.ofAddContent ⋯ ⋯ (MeasureTheory.kolContent hP) ⋯

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

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

Projective limit of a projective measure family.

Equations

• MeasureTheory.projectiveLimit P hP = MeasureTheory.Measure.ofAddContent ⋯ ⋯ (MeasureTheory.kolContent hP) ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯