Bridge: Bochner Marginals → Projective Measure Family

Bridges the finite-dimensional Bochner marginals (measures on EuclideanSpace ℝ (Fin n)) to the IsProjectiveMeasureFamily API from Mathlib (measures on ∀ j : J, ℝ indexed by Finset E), enabling application of the Kolmogorov extension theorem.

Main definitions

• marginalFamily — for each J : Finset E, a probability measure on ∀ j : J, ℝ
• marginalFamily_isProjective — the family is projective (consistent under restriction)

Transport equivalence

noncomputable def finsetReindexEquiv {E : Type u_1} (J : Finset E) : (↥J → ℝ) ≃ᵐ (Fin J.card → ℝ)

Measurable equivalence between ∀ j : J, ℝ and Fin |J| → ℝ via J.equivFin.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def finsetPiMeasEquiv {E : Type u_1} (J : Finset E) : (↥J → ℝ) ≃ᵐ EuclideanSpace ℝ (Fin J.card)

Measurable equivalence between ∀ j : J, ℝ and EuclideanSpace ℝ (Fin |J|). Composition of reindexing by J.equivFin and MeasurableEquiv.toLp.

Equations

• finsetPiMeasEquiv J = (finsetReindexEquiv J).trans (MeasurableEquiv.toLp 2 (Fin J.card → ℝ))

Marginal family

noncomputable def finsetTestVectors {E : Type u_1} (J : Finset E) : Fin J.card → E

The test vectors for a finset J, as a function Fin |J| → E.

Equations

• finsetTestVectors J i = ↑(J.equivFin.symm i)

noncomputable def marginalMeasure {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] (Φ : E → ℂ) (hΦ_cont : Continuous Φ) (hΦ_pd : IsPositiveDefinite Φ) (hΦ_norm : Φ 0 = 1) (J : Finset E) : MeasureTheory.ProbabilityMeasure (EuclideanSpace ℝ (Fin J.card))

Choose the unique Bochner marginal measure for test vectors from a finset.

Equations

• marginalMeasure Φ hΦ_cont hΦ_pd hΦ_norm J = Exists.choose ⋯

theorem marginalMeasure_charFun {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] (Φ : E → ℂ) (hΦ_cont : Continuous Φ) (hΦ_pd : IsPositiveDefinite Φ) (hΦ_norm : Φ 0 = 1) (J : Finset E) (ξ : EuclideanSpace ℝ (Fin J.card)) : MeasureTheory.charFun (↑(marginalMeasure Φ hΦ_cont hΦ_pd hΦ_norm J)) ξ = marginalCF Φ (finsetTestVectors J) ξ

noncomputable def marginalFamily {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] (Φ : E → ℂ) (hΦ_cont : Continuous Φ) (hΦ_pd : IsPositiveDefinite Φ) (hΦ_norm : Φ 0 = 1) (J : Finset E) : MeasureTheory.Measure ((j : ↥J) → (fun (x : E) => ℝ) ↑j)

The projective family of measures indexed by Finset E. For each J, we take the Bochner marginal on EuclideanSpace ℝ (Fin |J|) and transport it to ∀ j : J, ℝ via the finsetPiMeasEquiv.

Equations

• marginalFamily Φ hΦ_cont hΦ_pd hΦ_norm J = MeasureTheory.Measure.map ⇑(finsetPiMeasEquiv J).symm ↑(marginalMeasure Φ hΦ_cont hΦ_pd hΦ_norm J)

instance marginalFamilyIsFiniteMeasure {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] (Φ : E → ℂ) (hΦ_cont : Continuous Φ) (hΦ_pd : IsPositiveDefinite Φ) (hΦ_norm : Φ 0 = 1) (J : Finset E) : MeasureTheory.IsFiniteMeasure (marginalFamily Φ hΦ_cont hΦ_pd hΦ_norm J)

instance marginalFamilyIsProbabilityMeasure {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] (Φ : E → ℂ) (hΦ_cont : Continuous Φ) (hΦ_pd : IsPositiveDefinite Φ) (hΦ_norm : Φ 0 = 1) (J : Finset E) : MeasureTheory.IsProbabilityMeasure (marginalFamily Φ hΦ_cont hΦ_pd hΦ_norm J)

Projectivity

The marginal family is projective. The proof uses characteristic function uniqueness: for J ⊆ I, the pushforward of P(I) along Finset.restrict₂ has the same characteristic function as P(J), namely ξ ↦ Φ(∑_{j∈J} ξⱼ fⱼ).

theorem marginalFamily_isProjective {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] (Φ : E → ℂ) (hΦ_cont : Continuous Φ) (hΦ_pd : IsPositiveDefinite Φ) (hΦ_norm : Φ 0 = 1) : MeasureTheory.IsProjectiveMeasureFamily (marginalFamily Φ hΦ_cont hΦ_pd hΦ_norm)

The marginal family is projective: for J ⊆ I, the restriction of P(I) to J-coordinates equals P(J).

Application of Kolmogorov Extension

noncomputable def marginalProjectiveLimit {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] (Φ : E → ℂ) (hΦ_cont : Continuous Φ) (hΦ_pd : IsPositiveDefinite Φ) (hΦ_norm : Φ 0 = 1) [hE : Nonempty E] : MeasureTheory.Measure (E → ℝ)

The Kolmogorov projective limit of the marginal family.

Equations

• marginalProjectiveLimit Φ hΦ_cont hΦ_pd hΦ_norm = MeasureTheory.projectiveLimit (marginalFamily Φ hΦ_cont hΦ_pd hΦ_norm) ⋯

instance marginalProjectiveLimitIsProbability {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] (Φ : E → ℂ) (hΦ_cont : Continuous Φ) (hΦ_pd : IsPositiveDefinite Φ) (hΦ_norm : Φ 0 = 1) [Nonempty E] : MeasureTheory.IsProbabilityMeasure (marginalProjectiveLimit Φ hΦ_cont hΦ_pd hΦ_norm)

theorem marginalProjectiveLimit_isProjectiveLimit {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] (Φ : E → ℂ) (hΦ_cont : Continuous Φ) (hΦ_pd : IsPositiveDefinite Φ) (hΦ_norm : Φ 0 = 1) [Nonempty E] : MeasureTheory.IsProjectiveLimit (marginalProjectiveLimit Φ hΦ_cont hΦ_pd hΦ_norm) (marginalFamily Φ hΦ_cont hΦ_pd hΦ_norm)

The projective limit projects correctly onto each finite-dimensional marginal.

theorem marginalProjectiveLimit_unique {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] (Φ : E → ℂ) (hΦ_cont : Continuous Φ) (hΦ_pd : IsPositiveDefinite Φ) (hΦ_norm : Φ 0 = 1) [Nonempty E] {ν : MeasureTheory.Measure (E → ℝ)} (hν : MeasureTheory.IsProjectiveLimit ν (marginalFamily Φ hΦ_cont hΦ_pd hΦ_norm)) : ν = marginalProjectiveLimit Φ hΦ_cont hΦ_pd hΦ_norm

The projective limit of the marginal family is unique.