Measurable Modification for Minlos' Theorem #
Constructs a measurable pushforward from the Kolmogorov extension to the topological dual.
The key idea: instead of pulling back ν (a measure on E → ℝ) through the embedding E' ↪ (E → ℝ), we push forward ν through a measurable projection P : (E → ℝ) → WeakDual ℝ E that agrees with the identity on "good paths" (ω that are ℚ-linear and bounded on a countable dense subset).
Main definitions #
qLinearPaths— set of ω that are ℚ-linear on the dense sequence (Finsupp version)boundedPaths— set of ω bounded by a IsHilbertNuclear seminorm (Finsupp version)goodPaths— intersection (measurable, full measure under ν)measurableProjection— P : (E → ℝ) → WeakDual ℝ EweakDualEmbed— the embedding WeakDual ℝ E → (E → ℝ)
Axioms (6 textbook results) #
extensionCLM— BLT: construct ContinuousLinearMap from good pathextensionCLM_eq_on_dense— extension agrees with ω on dense sequencemeasurable_measurableProjection— P is measurableqLinearPaths_ae— ℚ-linearity a.e. (joint CF → X = 0 a.s.)boundedPaths_ae— boundedness a.e. (Markov + CF continuity)projection_ae_eq— P(ω)(f) = ω(f) ν-a.e.
References #
- Gel'fand-Vilenkin, "Generalized Functions" Vol. 4, Ch. IV, §3.3
- Minlos, "Generalized random processes and their extension to measures" (1959)
Embedding: WeakDual ℝ E → (E → ℝ) #
The evaluation embedding sending a continuous linear functional to its underlying function. This is measurable (but NOT a MeasurableEmbedding when E is uncountable-dimensional).
Equations
- weakDualEmbed E = fun (l : WeakDual ℝ E) (f : E) => l f
Instances For
The embedding is measurable: each coordinate l ↦ l(f) is measurable w.r.t. the cylinder σ-algebra (by definition).
Good Paths (Finsupp version) #
The set of "ℚ-linear paths" on a sequence d : ℕ → E. ω respects all finite ℚ-linear combinations: ω(∑ cᵢ • d(i)) = ∑ cᵢ * ω(d(i)) for every c : ℕ →₀ ℚ.
This is a countable intersection (ℕ →₀ ℚ is countable) of measurable sets.
Equations
Instances For
The set of "bounded paths" on a sequence d : ℕ → E with respect to seminorms p : ℕ → Seminorm ℝ E. ω is bounded on all finite ℚ-linear combinations: ∃ s : Finset ℕ, ∃ C : ℕ, ∀ c : ℕ →₀ ℚ, |ω(∑ cᵢ • d(i))| ≤ C * (s.sup p)(∑ cᵢ • d(i)).
Combined with ℚ-linearity, this gives uniform continuity of ω on the ℚ-span of range(d).
This is measurable (countable ⋃/⋂ over ℕ × ℕ × (ℕ →₀ ℚ)).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The "good paths" set: ω that are ℚ-linear and bounded on the dense sequence. This is measurable (countable Boolean operations on measurable sets).
Equations
- goodPaths d p = qLinearPaths d ∩ boundedPaths d p
Instances For
Extension on Good Paths #
The continuous extension function on good paths. Uses extendFrom to continuously extend ω from range(d) to all of E.
Construction (BLT / uniform extension theorem) #
- Continuous extension: On good paths, ω restricted to range(d) satisfies |ω(d_i) - ω(d_j)| ≤ C * q(d_i - d_j) (from ℚ-linearity + boundedness). This gives uniform continuity w.r.t. the seminorm q, so extendFrom gives a continuous function g : E → ℝ with g(d_n) = ω(d_n).
- ℚ-linearity of g: g(a•x + b•y) = a•g(x) + b•g(y) for a, b ∈ ℚ. Both sides are continuous in x, y, and agree on range(d) × range(d).
- ℝ-linearity: g(r•x) = r•g(x) for r ∈ ℝ by density of ℚ in ℝ.
Ref: Rudin, Functional Analysis, Thm 1.18 (bounded linear extension).
Equations
- extensionFun d _hd p ω _hω = extendFrom (Set.range d) ω
Instances For
The continuous linear extension associated to a good path.
Equations
- extensionCLM d hd p hp_top ω hω = { toFun := extensionFun d hd p ω hω, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
Instances For
The extension agrees with ω on the dense sequence. Follows from the BLT construction: Dense.extend agrees with ω on range(d).
Ref: follows from extensionCLM construction.
For a continuous linear functional l, embed(l) ∈ goodPaths. Proof: l is ℝ-linear (hence ℚ-linear on all Finsupp combinations), and bounded by continuity.
The extension of embed(l) recovers l. Proof: both are ContinuousLinearMaps that agree on the dense set D, hence they agree everywhere by uniqueness of continuous extension.
Measurable Projection #
Auxiliary projection given explicit dense sequence and seminorms. On good paths, extends ω to a ContinuousLinearMap; on bad paths, returns 0.
Equations
- measurableProjectionAux d hd p hp_top ω = if hω : ω ∈ goodPaths d p then extensionCLM d hd p hp_top ω hω else 0
Instances For
The measurable projection P : (E → ℝ) → WeakDual ℝ E.
On good paths (ℚ-linear + bounded on dense sequence), P(ω) is the unique continuous linear extension of ω|_D. On bad paths, P(ω) = 0.
Equations
Instances For
The projection map is measurable. Strategy: The MeasurableSpace on WeakDual is the cylinder σ-algebra (generated by evaluations). So measurability of P : (E → ℝ) → WeakDual reduces to showing each composition eval_f ∘ P is measurable, which is measurable_eval_comp_projection.
Ref: standard measurability of piecewise + pointwise limits (Billingsley, §13).
The projection composed with the embedding is the identity on WeakDual ℝ E. For l ∈ WeakDual ℝ E, embed(l) ∈ goodPaths (l is linear + bounded), and extensionCLM(embed(l)) = l by uniqueness of continuous extension from dense.
Almost-everywhere properties #
These axioms use the joint characteristic function hypothesis: h_cf_joint : ∀ (n : ℕ) (s : Fin n → ℝ) (x : Fin n → E), ∫ ω, exp(I * ↑(∑ i, s i * ω(x i))) dν = Φ(∑ i, s i • x i)
This captures all finite-dimensional marginals of ν, not just the 1D marginals. It is provable from the projective limit property.
ℚ-linearity holds ν-a.e.
For fixed c : ℕ →₀ ℚ, the random variable X(ω) = ω(∑ cᵢ•dᵢ) - ∑ cᵢ*ω(dᵢ) has CF E[e^{itX}] = Φ(t·∑cᵢ•dᵢ - t·∑cᵢ•dᵢ) = Φ(0) = 1 (using h_cf_joint with test vectors {∑cᵢ•dᵢ, d_{i₁}, ..., d_{iₖ}} and scalars {t, -tc₁, ..., -tcₖ}). Hence X = 0 a.s. (by Measure.ext_of_charFun with δ₀). Countable intersection over c ∈ ℕ →₀ ℚ preserves full measure.
Ref: Gel'fand-Vilenkin, "Generalized Functions" Vol. 4, Ch. IV, §3.3.
Boundedness holds ν-a.e.
For each element x in the ℚ-span, the Markov/Chebyshev inequality gives: P(|ω(x)| ≥ R) ≤ 2(1 - Re(Φ(tx))) for appropriate t. By continuity of Φ at 0, the numerator is small when x is in a seminorm ball. IsHilbertNuclear Hilbert-Schmidt embeddings give summability over countable ℚ-linear combinations, and Borel-Cantelli yields the result.
Ref: Gel'fand-Vilenkin, "Generalized Functions" Vol. 4, Ch. IV, §3.3; also Billingsley, "Convergence of Probability Measures", §6.
The good paths have full ν-measure. Combines ℚ-linearity and boundedness a.e.
For each f : E, P(ω)(f) = ω(f) for ν-a.e. ω.
On good paths (full measure by goodPaths_ae):
- P(ω)(d_n) = ω(d_n) for all n (by extensionCLM_eq_on_dense)
- P(ω) is continuous, so P(ω)(d_n) → P(ω)(f) for any d_n → f
- ω(d_n) → ω(f) in probability: using h_cf_joint with test vectors (f, d_n) and scalars (t, -t), CF = Φ(t(f-d_n)) → Φ(0) = 1 by continuity
- A.s. + in-probability convergence to the same limit → P(ω)(f) = ω(f) a.e.
Ref: Gel'fand-Vilenkin, "Generalized Functions" Vol. 4, Ch. IV, §3.3.
Derived Properties #
The pushforward μ = ν.map P is a probability measure when P is measurable.
The characteristic functional of ν.map P equals Φ.
Uniqueness via pushforward factoring: μ' = ν.map P.