Minlos Concentration Bound #
Proves nuclear_cylindrical_concentration — the concentration bound for
nuclear cylindrical measures. minlos_concentration is a convenience wrapper.
Architecture #
Helper lemmas (proved): pointwise CF estimates (
cf_norm_le_one,cf_nhds_ball,one_sub_re_nonneg,quadratic_bound_outside).Monotonicity lemmas (proved):
seminorm_mono_of_le,finset_sup_le_of_monoderive seminorm monotonicity from consecutive HS embeddings.Core bounds (proved):
joint_kernel_bound_finite: Gaussian averaging on kernel elementstail_bound_uniform: Dimension-free Gaussian averaging + Gram matrix + Chebyshevgram_schmidt_seminorm: ONB construction for Hilbertian seminorms
Theorem
nuclear_cylindrical_concentration: fully proved via Gram-Schmidt ONB, kernel concentration, tail bound, and continuity from below.Theorem
minlos_concentration: wrapper applying the above.
References #
- Gel'fand-Vilenkin, "Generalized Functions" Vol. 4, Ch. IV, §3.3
- Bogachev, "Gaussian Measures", Ch. 2-3
- Trèves, "Topological Vector Spaces", Ch. 50-51
CF constantly 1 implies random variable is 0 a.e. #
If X : Ω → ℝ is measurable and ∫ exp(I * ↑(t * X(ω))) dν = 1 for all t ∈ ℝ, then X = 0 ν-a.e.
Proof sketch: Re(1 - ∫ exp(itX)) = ∫ (1 - cos(tX)) = 0. Since 1 - cos ≥ 0, cos(tX) = 1 a.e. for each t. Over countably many t ∈ ℚ simultaneously, this forces X = 0.
Helper lemmas #
The characteristic functional satisfies ‖Φ(x)‖ ≤ 1, as the integral
of a unit-modulus function against a probability measure.
From Continuous Φ, Φ 0 = 1, and WithSeminorms p: extract a finite set
of seminorm indices s and radius r > 0 such that (s.sup p)(x) < r
implies ‖1 - Φ(x)‖ < ε.
Monotonicity from consecutive HS embeddings #
From consecutive HS embeddings, p n ≤ p m whenever n ≤ m.
For a finite set of indices, s.sup p ≤ p m when m dominates every index in s
(which holds when m ≥ max s, given monotonicity).
Combined quadratic bound #
Combined quadratic bound from CF continuity: for any ε > 0, there exist m₀ : ℕ
and K ≥ 0 such that 1 - Re(Φ(x)) ≤ ε + K · (p m₀)(x)² for all x.
CF vanishes on seminorm kernel #
If q(z) = 0 and q dominates the CF near 0 (i.e., for any ε > 0, there's a q-ball
where ‖1 - Φ‖ < ε), then Φ(t • z) = 1 for all t.
Proof: q(t•z) = |t| · q(z) = 0 < r for any r > 0, so ‖1 - Φ(t•z)‖ < ε
for all ε > 0.
Linear combination a.e. from joint CF #
If x = ∑ j, β j • e j in E (real coefficients), then ω(x) = ∑ j, β j * ω(e j)
for ν-a.e. ω. Uses h_cf_joint directly — no linearity of ω assumed.
This is the key trick: the joint CF condition forces the "linear decomposition" to hold a.e. even for real (not just rational) coefficients.
Pushforward CF for finite evaluation maps #
The pushforward of ν to Fin k → ℝ via evaluation at vectors e₀,...,e_{k-1}
has characteristic function v ↦ Φ(∑ vⱼ • eⱼ). This is a direct consequence
of h_cf_joint and integral_map.
Concentration on good set via Cauchy-Schwarz + Parseval #
Cauchy-Schwarz + Parseval concentration bound: if ω is linear on combinations of
a p-orthonormal sequence {eⱼ} and ∑ ω(eⱼ)² ≤ R², then for any linear combination
x = ∑ βⱼ eⱼ, we have |ω(x)| ≤ R · p(x).
This is the pointwise bound at the heart of the concentration argument: ω in the "good set" (bounded evaluation norm) respects the seminorm.
Kernel elements vanish a.e. #
If p(z) = 0 and p dominates the CF (i.e., the CF at multiples of z
is always 1), then ω(z) = 0 for ν-a.e. ω. Proof: the CF of ω(z)
is constantly 1, so ω(z) = 0 a.e. by ae_eq_zero_of_charfun_eq_one.
ℚ-linearity for all Finsupp simultaneously #
For ν-a.e. ω, the evaluation ω(x_c) equals the ℚ-linear combination
∑ cᵢ ω(dᵢ) for all c : ℕ →₀ ℚ simultaneously.
Uses countable intersection (eventually_countable_forall) since ℕ →₀ ℚ
is countable, plus linear_combination_ae for each individual c.
Bad set definitions for continuity from below #
The "bad set" for the concentration bound: the set of ω where some ℚ-linear combination of dense vectors violates the seminorm bound.
Equations
Instances For
The "restricted bad set" B_N: bad set restricted to ℚ-linear combinations
with support in {0, ..., N-1}.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The full bad set equals the union of the restricted bad sets.
Every c : ℕ →₀ ℚ has finite support contained in some Finset.range N.
If ν(B_N) ≤ δ for all N, then ν(full bad set) ≤ δ.
Uses continuity of measure from below (tendsto_measure_iUnion).
Seminorm Gram-Schmidt (proved) #
Gram-Schmidt for Hilbertian seminorms: given N vectors in F and a Hilbertian seminorm p, there exist k orthonormal vectors such that every element of the span of the original vectors decomposes as a p-ONB combination plus a kernel element (where p vanishes).
Per-N concentration bound #
For each N, the restricted bad set B_N has measure bounded by the tail probability of the squared evaluation norm on a p-ONB.
Key argument: on the a.e. set where all decompositions hold, Cauchy-Schwarz + Parseval gives |ω(x_c)| ≤ R · p(x_c) whenever Σ ω(eⱼ)² ≤ R². So B_N ⊆ {Σ ω(eⱼ)² > R²} ∪ (null set).
Nuclear cylindrical concentration #
Kernel evaluation a.e. bound #
Tail bound for evaluation on ONB (key step) #
Restricted bad set bound with kernel contribution #
Main theorem #
Nuclear cylindrical concentration (Gel'fand-Vilenkin Vol.4, Ch.IV §3.3).
Given Hilbertian seminorms with consecutive HS embeddings generating the topology,
a cylindrical probability measure with continuous CF, and any sequence of vectors,
there exist m, C : ℕ such that the concentration bound holds.
Main theorem #
Minlos concentration bound — wrapper around
nuclear_cylindrical_concentration.