Finite-Dimensional Marginals for Minlos' Theorem

For a continuous positive-definite normalized functional Φ on a TVS E, we construct finite-dimensional marginal measures via Bochner's theorem.

Given test vectors f₁,...,fₙ ∈ E, the marginal characteristic function Φ_F(t) = Φ(∑ tᵢfᵢ) is continuous PD on ℝⁿ, so Bochner gives a probability measure μ_F on ℝⁿ.

Main results

• marginalCF — the finite-dimensional marginal CF
• marginalCF_continuous — marginalCF is continuous
• marginalCF_pd — marginalCF is positive definite
• marginalCF_normalized — marginalCF(0) = 1
• marginal_measure_exists — Bochner gives a probability measure with matching CF

Marginal characteristic function

def marginalCF {E : Type u_1} [AddCommGroup E] [Module ℝ E] (Φ : E → ℂ) {n : ℕ} (f : Fin n → E) : EuclideanSpace ℝ (Fin n) → ℂ

The finite-dimensional marginal CF: Φ_F(t) = Φ(∑ tᵢ • fᵢ).

Defined on EuclideanSpace ℝ (Fin n) (which is PiLp 2 (fun _ => ℝ)) so that we can apply Bochner's theorem (which requires inner product spaces).

Equations

• marginalCF Φ f t = Φ (∑ i : Fin n, t.ofLp i • f i)

theorem marginalCF_continuous {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] (Φ : E → ℂ) {n : ℕ} (f : Fin n → E) (hΦ : Continuous Φ) : Continuous (marginalCF Φ f)

The marginal CF is continuous.

Proof: Each summand tᵢ • fᵢ is continuous in t (scalar multiplication by a continuous coordinate projection), and a finite sum of continuous functions is continuous. Then compose with continuous Φ.

theorem marginalCF_pd {E : Type u_1} [AddCommGroup E] [Module ℝ E] (Φ : E → ℂ) {n : ℕ} (f : Fin n → E) (hPD : IsPositiveDefinite Φ) : IsPositiveDefinite (marginalCF Φ f)

The marginal CF is positive definite.

Uses isPositiveDefinite_precomp_linear: if Φ is PD on E and T : V →ₗ E is linear, then Φ ∘ T is PD on V.

theorem marginalCF_normalized {E : Type u_1} [AddCommGroup E] [Module ℝ E] (Φ : E → ℂ) {n : ℕ} (f : Fin n → E) (h_norm : Φ 0 = 1) : marginalCF Φ f 0 = 1

The marginal CF is normalized: Φ_F(0) = Φ(0) = 1.

theorem marginal_measure_exists {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] (Φ : E → ℂ) {n : ℕ} (f : Fin n → E) (hΦ_cont : Continuous Φ) (hΦ_pd : IsPositiveDefinite Φ) (hΦ_norm : Φ 0 = 1) : ∃! μ : MeasureTheory.ProbabilityMeasure (EuclideanSpace ℝ (Fin n)), ∀ (ξ : EuclideanSpace ℝ (Fin n)), MeasureTheory.charFun (↑μ) ξ = marginalCF Φ f ξ

For each finite set of test vectors, Bochner's theorem gives a probability measure on ℝⁿ whose characteristic function equals the marginal CF.

This is the core step connecting the infinite-dimensional Minlos problem to the finite-dimensional Bochner theorem.