Sazonov Tightness

This module establishes that Sazonov-continuous characteristic functions imply tightness of finite-dimensional marginals via Gaussian averaging, spectral decomposition, and Chebyshev inequalities.

Main definitions

• SazonovContinuousAt: Characteristic function continuity in the Sazonov topology
• marginalFun: Finite-dimensional marginal characteristic function

Main statements

• marginalFun_isPositiveDefinite: Marginals of PD functions are PD
• sazonov_tight_marginals: Sazonov CF continuity implies tight marginals
• sazonov_tight_marginals_apply: Explicit tightness bound via Gaussian averaging

Sazonov Continuity

def SazonovContinuousAt {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (φ : H → ℂ) : Prop

Sazonov continuity at 0: for every ε > 0, there exists a positive trace-class operator S such that ⟪x, Sx⟫ < 1 implies |1 - φ(x)| < ε.

Equations

• SazonovContinuousAt φ = ∀ ε > 0, ∃ (S : SazonovIndex H), ∀ (x : H), quadForm S.op x < 1 → ‖1 - φ x‖ < ε

Finite-Dimensional Marginals

def marginalFun {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (φ : H → ℂ) {n : ℕ} (v : Fin n → H) : EuclideanSpace ℝ (Fin n) → ℂ

For a family v : Fin n → H, the marginal function φ_v(t) = φ(∑ i, t i • v i).

Equations

• marginalFun φ v t = φ (∑ i : Fin n, t.ofLp i • v i)

theorem marginalFun_isPositiveDefinite {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (φ : H → ℂ) (hpd : IsPositiveDefinite φ) {n : ℕ} (v : Fin n → H) : IsPositiveDefinite (marginalFun φ v)

The marginal function of a PD function is PD.

Tail Bound Algebra

theorem one_sub_exp_neg_pos {t : ℝ} (ht : 0 < t) : 0 < 1 - Real.exp (-t)

1 - exp(-t) > 0 for t > 0.

theorem exp_neg_le_exp_neg {a b : ℝ} (hab : a ≤ b) : Real.exp (-b) ≤ Real.exp (-a)

exp(-b) ≤ exp(-a) when a ≤ b.

theorem one_sub_exp_half_sq_pos (R : ℝ) (hR : 0 < R) : 0 < 1 - Real.exp (-(R ^ 2 / 2))

The denominator 1 - exp(-R²/2) is positive for R > 0.

theorem tail_bound_from_exp_integral {V : Type u_2} [NormedAddCommGroup V] [MeasurableSpace V] [BorelSpace V] (μ : MeasureTheory.ProbabilityMeasure V) (σ : ℝ) (hσ : 0 < σ) (C : ℝ) (_hC0 : 0 ≤ C) (hC : ∫ (y : V), 1 - Real.exp (-(σ ^ 2 * ‖y‖ ^ 2 / 2)) ∂↑μ ≤ C) (R : ℝ) (hR : 0 < R) : (↑μ {y : V | R ≤ ‖y‖}).toReal ≤ C / (1 - Real.exp (-(σ ^ 2 * R ^ 2 / 2)))

Chebyshev/Markov bound with scaling: if ∫ (1 - exp(-σ²‖y‖²/2)) dμ ≤ C, then μ({‖y‖ ≥ R}) ≤ C / (1 - exp(-σ²R²/2)).

The Gaussian Averaging Bound (with scaling parameter)

Gaussian Averaging Infrastructure

@[reducible, inline]

noncomputable abbrev gaussDensity {V : Type u_2} [NormedAddCommGroup V] (σ : ℝ) (x : V) : ℝ

Centered Gaussian density profile with scale σ.

Equations

• gaussDensity σ x = Real.exp (-(1 / (2 * σ ^ 2)) * ‖x‖ ^ 2)

theorem gaussDensity_nonneg' {V : Type u_2} [NormedAddCommGroup V] (σ : ℝ) (x : V) : 0 ≤ gaussDensity σ x

theorem gaussDensity_continuous' {V : Type u_2} [NormedAddCommGroup V] (σ : ℝ) : Continuous (gaussDensity σ)

theorem gaussDensity_integrable' {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (σ : ℝ) (hσ : 0 < σ) : MeasureTheory.Integrable (gaussDensity σ) MeasureTheory.volume

theorem gaussDensity_integral_pos' {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (σ : ℝ) (hσ : 0 < σ) : 0 < ∫ (x : V), gaussDensity σ x

theorem gaussDensity_mul_charFun_re_integrable' {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] [SecondCountableTopology V] (μ : MeasureTheory.ProbabilityMeasure V) (φ : V → ℂ) (hφ : ∀ (t : V), MeasureTheory.charFun (↑μ) t = φ t) (σ : ℝ) (hσ : 0 < σ) : MeasureTheory.Integrable (fun (x : V) => gaussDensity σ x * (φ x).re) MeasureTheory.volume

theorem fubini_gaussian_charFun {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] [SecondCountableTopology V] (μ : MeasureTheory.ProbabilityMeasure V) (φ : V → ℂ) (hφ : ∀ (t : V), MeasureTheory.charFun (↑μ) t = φ t) (σ : ℝ) (hσ : 0 < σ) : ∫ (y : V), 1 - Real.exp (-(σ ^ 2 * ‖y‖ ^ 2 / 2)) ∂↑μ = (∫ (x : V), gaussDensity σ x)⁻¹ * ∫ (x : V), gaussDensity σ x * (1 - (φ x).re)

Fubini identity for Gaussian averaging: ∫_μ (1-exp(-σ²‖y‖²/2)) = C⁻¹ ∫ exp(-b‖x‖²) Re(1-φ(x)) dx.

theorem gaussian_quadForm_integral_le {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] [SecondCountableTopology V] (σ : ℝ) (hσ : 0 < σ) (S : V →L[ℝ] V) (hS : S.IsPositive) (T : ℝ) (_hT : 0 ≤ T) (h_trace : ∀ (ι : Type u_3) [inst : Fintype ι] (b : OrthonormalBasis ι ℝ V), ∑ i : ι, inner ℝ (b i) (S (b i)) ≤ T) : (∫ (x : V), gaussDensity σ x)⁻¹ * ∫ (x : V), gaussDensity σ x * quadForm S x ≤ σ ^ 2 * T

Gaussian second moment bound: C⁻¹ ∫ exp(-b‖x‖²) ⟪x,Sx⟫ dx ≤ σ²·Tr(S). Uses spectral decomposition to reduce to single-direction bounds.

theorem gaussDensity_mul_quadForm_integrable' {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (σ : ℝ) (hσ : 0 < σ) (S : V →L[ℝ] V) : MeasureTheory.Integrable (fun (x : V) => gaussDensity σ x * quadForm S x) MeasureTheory.volume

theorem gaussian_averaging_bound {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] [SecondCountableTopology V] (μ : MeasureTheory.ProbabilityMeasure V) (φ : V → ℂ) (hφ : ∀ (t : V), MeasureTheory.charFun (↑μ) t = φ t) (ε : ℝ) (hε : 0 < ε) (σ : ℝ) (hσ : 0 < σ) (S : V →L[ℝ] V) (hS : S.IsPositive) (h_bound : ∀ (x : V), quadForm S x < 1 → ‖1 - φ x‖ < ε) (T : ℝ) (hT : 0 ≤ T) (h_trace : ∀ (ι : Type u_3) [inst : Fintype ι] (b : OrthonormalBasis ι ℝ V), ∑ i : ι, inner ℝ (b i) (S (b i)) ≤ T) : ∫ (y : V), 1 - Real.exp (-(σ ^ 2 * ‖y‖ ^ 2 / 2)) ∂↑μ ≤ ε + 2 * σ ^ 2 * T

The Gaussian averaging bound with scaling parameter σ > 0:

∫ (1 - exp(-σ²‖y‖²/2)) dμ(y) ≤ ε + 2σ²·T

Here exp(-σ²‖y‖²/2) is the characteristic function of N(0, σ²I). The bound follows from Fubini + pointwise bound Re(1-φ) ≤ ε + 2·qf

• Gaussian second moment E_γ[⟨x,Sx⟩] ≤ σ²·Tr(S).

theorem scaled_tail_bound {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] [SecondCountableTopology V] (μ : MeasureTheory.ProbabilityMeasure V) (φ : V → ℂ) (hφ : ∀ (t : V), MeasureTheory.charFun (↑μ) t = φ t) (ε : ℝ) (hε : 0 < ε) (σ : ℝ) (hσ : 0 < σ) (S : V →L[ℝ] V) (hS : S.IsPositive) (h_bound : ∀ (x : V), quadForm S x < 1 → ‖1 - φ x‖ < ε) (T : ℝ) (hT : 0 ≤ T) (h_trace : ∀ (ι : Type u_3) [inst : Fintype ι] (b : OrthonormalBasis ι ℝ V), ∑ i : ι, inner ℝ (b i) (S (b i)) ≤ T) (R : ℝ) (hR : 0 < R) : (↑μ {y : V | R ≤ ‖y‖}).toReal ≤ (ε + 2 * σ ^ 2 * T) / (1 - Real.exp (-(σ ^ 2 * R ^ 2 / 2)))

Scaled Chebyshev: combining Gaussian averaging with the tail bound.

Restriction of Operators to Marginal Subspaces

noncomputable def restrictOp {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (S : H →L[ℝ] H) {n : ℕ} (v : Fin n → H) : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n)

Restriction of an operator S on H to a finite-dimensional subspace spanned by an orthonormal family v : Fin n → H. Defined as π ∘ S ∘ ι where ι embeds and π projects. Matrix: (S_v)_{ij} = ⟪vᵢ, S(vⱼ)⟫.

Equations

• restrictOp S v = LinearMap.toContinuousLinearMap (projON✝ v ∘ₗ ↑S ∘ₗ embedON✝ v)

theorem restrictOp_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (S : H →L[ℝ] H) {n : ℕ} (v : Fin n → H) (t : EuclideanSpace ℝ (Fin n)) (i : Fin n) : ((restrictOp S v) t).ofLp i = inner ℝ (v i) (S (∑ j : Fin n, t.ofLp j • v j))

Coordinate formula for restrictOp.

theorem restrictOp_quadForm {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (S : H →L[ℝ] H) {n : ℕ} (v : Fin n → H) (t : EuclideanSpace ℝ (Fin n)) : quadForm (restrictOp S v) t = quadForm S (∑ i : Fin n, t.ofLp i • v i)

The quadratic form of the restricted operator equals the original.

theorem restrictOp_isPositive {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (S : H →L[ℝ] H) (hS : S.IsPositive) {n : ℕ} (v : Fin n → H) : (restrictOp S v).IsPositive

The restriction of a positive operator is positive.

theorem orthonormal_diag_le_hilbert_trace {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (S : H →L[ℝ] H) (hS : S.IsPositive) {n : ℕ} (v : Fin n → H) (hv : Orthonormal ℝ v) {ι : Type} (b : HilbertBasis ι ℝ H) (hsum : Summable fun (i : ι) => inner ℝ (b i) (S (b i))) : ∑ j : Fin n, inner ℝ (v j) (S (v j)) ≤ ∑' (i : ι), inner ℝ (b i) (S (b i))

For a finite orthonormal set in a Hilbert space, the sum of diagonal entries ∑ⱼ ⟪vⱼ, S(vⱼ)⟫ is bounded by the trace ∑' k ⟪bₖ, S(bₖ)⟫. Proof: decompose bₖ = P(bₖ) + Q(bₖ) via the projection P onto span(v). The cross term ∑' k ⟪Q(bₖ), S(P(bₖ))⟫ vanishes by Parseval + orthonormality, so the difference = ∑' k ⟪Q(bₖ), S(Q(bₖ))⟫ ≥ 0 by positivity of S.

theorem restrictOp_trace_eq_diag {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (S : H →L[ℝ] H) {n : ℕ} (v : Fin n → H) (_hv : Orthonormal ℝ v) (ι' : Type u_2) [Fintype ι'] (b' : OrthonormalBasis ι' ℝ (EuclideanSpace ℝ (Fin n))) : ∑ i : ι', inner ℝ (b' i) ((restrictOp S v) (b' i)) = ∑ j : Fin n, inner ℝ (v j) (S (v j))

The trace of restrictOp in any ONB of EuclideanSpace equals ∑ⱼ ⟪vⱼ, S(vⱼ)⟫. Uses LinearMap.trace_eq_sum_inner for basis independence on finite-dimensional EuclideanSpace, then computes the standard basis entries.

theorem restrictOp_trace_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (S : H →L[ℝ] H) (hS : S.IsPositive) {n : ℕ} (v : Fin n → H) (hv : Orthonormal ℝ v) {ι : Type} (b : HilbertBasis ι ℝ H) (hsum : Summable fun (i : ι) => inner ℝ (b i) (S (b i))) (ι' : Type) [Fintype ι'] (b' : OrthonormalBasis ι' ℝ (EuclideanSpace ℝ (Fin n))) : ∑ i : ι', inner ℝ (b' i) ((restrictOp S v) (b' i)) ≤ ∑' (i : ι), inner ℝ (b i) (S (b i))

The trace of the restricted operator is bounded by the trace of the original on any Hilbert basis. Combines trace basis independence on EuclideanSpace with the diagonal bound.

Main Tightness Theorem

theorem exists_R_for_tail_bound (C η σ : ℝ) (hC : 0 < C) (hCη : C < η) (hσ : 0 < σ) : ∃ R > 0, C / (1 - Real.exp (-(σ ^ 2 * R ^ 2 / 2))) < η

For any C < η and σ > 0, there exists R > 0 such that C / (1 - exp(-σ²R²/2)) < η.

theorem sazonov_tightness {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (φ : H → ℂ) (_hpd : IsPositiveDefinite φ) (_hnorm : φ 0 = 1) (_hcont : Continuous φ) (hsaz : SazonovContinuousAt φ) (η : ℝ) : η > 0 → ∃ R > 0, ∀ (n : ℕ) (v : Fin n → H), Orthonormal ℝ v → ∀ (μ : MeasureTheory.ProbabilityMeasure (EuclideanSpace ℝ (Fin n))), (∀ (t : EuclideanSpace ℝ (Fin n)), MeasureTheory.charFun (↑μ) t = marginalFun φ v t) → (↑μ {y : EuclideanSpace ℝ (Fin n) | R ≤ ‖y‖}).toReal < η

Sazonov Tightness Theorem. If φ : H → ℂ is positive definite, normalized, and Sazonov-continuous at 0, then the family of all finite-dimensional marginal measures is uniformly tight.