QJL distortion / concentration bound

This file proves the distortion (concentration) bound for the QJL asymmetric 1-bit estimator defined in JL/QJL.lean. With m sign-bits, the estimator is close to the true normalized inner product ⟪key/‖key‖, q⟫ with high probability. It is built in three layers:

1. Per-row variance (qjl_perrow_variance_le): for a single standard-Gaussian g, unit u and arbitrary q, Var[sign ⟪u,g⟫ · ⟪q,g⟫] ≤ ‖q‖² (and, with the √(π/2) scaling, the per-row estimator term has variance ≤ (π/2)‖q‖²).

2. Estimator variance (qjlEstimator_variance_le): the m per-row terms are i.i.d. under the product measure, so by additivity of variance over independent summands Var[qjlEstimator] ≤ (π/2)‖q‖² / m. The cross-row independence is supplied by mathlib's ProbabilityTheory.variance_sum_pi.

3. Chebyshev concentration (qjlEstimator_concentration): combining the variance bound with Chebyshev's inequality gives P(|qjlEstimator − ⟪key/‖key‖,q⟫| ≥ ε) ≤ (π/2)‖q‖² / (m·ε²), so m = O(‖q‖²/(ε²δ)) sign-bits suffice for additive error ε with probability 1−δ.

Part 1: per-row second moment / variance of the sign-product term

theorem JL.integral_inner_sq_stdGaussian {d : ℕ} (q : EuclideanSpace ℝ (Fin d)) : ∫ (g : EuclideanSpace ℝ (Fin d)), inner ℝ q g ^ 2 ∂ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin d)) = ‖q‖ ^ 2

Second moment of a Gaussian linear functional: E⟪q,g⟫² = ‖q‖². This is the variance of the (mean-zero) dual functional innerSL ℝ q.

theorem JL.memLp_inner {d : ℕ} (q : EuclideanSpace ℝ (Fin d)) : MeasureTheory.MemLp (fun (g : EuclideanSpace ℝ (Fin d)) => inner ℝ q g) 2 (ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin d)))

The Gaussian linear functional g ↦ ⟪q,g⟫ is in L².

theorem JL.memLp_sign_inner {d : ℕ} (u q : EuclideanSpace ℝ (Fin d)) : MeasureTheory.MemLp (fun (g : EuclideanSpace ℝ (Fin d)) => (inner ℝ u g).sign * inner ℝ q g) 2 (ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin d)))

The sign-product term g ↦ sign ⟪u,g⟫ · ⟪q,g⟫ is in L² (dominated by ⟪q,g⟫).

theorem JL.qjl_perrow_variance_le {d : ℕ} (u q : EuclideanSpace ℝ (Fin d)) : ProbabilityTheory.variance (fun (g : EuclideanSpace ℝ (Fin d)) => (inner ℝ u g).sign * inner ℝ q g) (ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin d))) ≤ ‖q‖ ^ 2

Per-row variance bound. For a single standard-Gaussian g, unit u and arbitrary q, Var[sign ⟪u,g⟫ · ⟪q,g⟫] ≤ ‖q‖².

The proof uses Var X ≤ E[X²], bounds (sign ⟪u,g⟫ · ⟪q,g⟫)² ≤ ⟪q,g⟫² pointwise (since (sign r)² ≤ 1), and evaluates E⟪q,g⟫² = ‖q‖².

Part 2: variance of the m-row estimator via cross-row independence

theorem JL.qjlEstimator_variance_le {m d : ℕ} (hm : 0 < m) (key q : EuclideanSpace ℝ (Fin d)) : ProbabilityTheory.variance (fun (S : Fin m → EuclideanSpace ℝ (Fin d)) => qjlEstimator key q S) (MeasureTheory.Measure.pi fun (x : Fin m) => ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin d))) ≤ Real.pi / 2 * ‖q‖ ^ 2 / ↑m

Estimator variance bound. Over an m × d i.i.d. standard-Gaussian sketch, the variance of the asymmetric 1-bit estimator is ≤ (π/2)‖q‖² / m.

The m per-row terms are i.i.d. functions of distinct coordinates of the product measure, so ProbabilityTheory.variance_sum_pi gives Var[Σ row] = Σ Var[row] = m·Var[row]; pulling out the (√(π/2)/m) scaling and applying the per-row bound finishes it.

Part 3: Chebyshev distortion / concentration bound

theorem JL.qjlEstimator_memLp {m d : ℕ} (key q : EuclideanSpace ℝ (Fin d)) : MeasureTheory.MemLp (fun (S : Fin m → EuclideanSpace ℝ (Fin d)) => qjlEstimator key q S) 2 (MeasureTheory.Measure.pi fun (x : Fin m) => ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin d)))

The estimator is in L² under the product measure (a constant times a finite sum of i.i.d. per-row terms, each L²).

theorem JL.qjlEstimator_concentration {m d : ℕ} (hm : 0 < m) (key q : EuclideanSpace ℝ (Fin d)) (hkey : key ≠ 0) {ε : ℝ} (hε : 0 < ε) : (MeasureTheory.Measure.pi fun (x : Fin m) => ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin d))).real {S : Fin m → EuclideanSpace ℝ (Fin d) | ε ≤ |qjlEstimator key q S - inner ℝ (‖key‖⁻¹ • key) q|} ≤ Real.pi / 2 * ‖q‖ ^ 2 / (↑m * ε ^ 2)

QJL distortion / concentration bound (Chebyshev). With m sign-bits, the asymmetric 1-bit estimator deviates from the true normalized inner product ⟪key/‖key‖, q⟫ by at least ε with probability at most (π/2)‖q‖² / (m·ε²). Hence m = O(‖q‖²/(ε²δ)) sign-bits suffice for additive error ε with probability 1 − δ.

Part 4: exponential (sub-Gaussian) distortion bound

The Chebyshev bound above decays only polynomially in m. The classical QJL guarantee is an exponential tail, obtained by showing the per-row sign-product term is sub-Gaussian and summing over the m independent rows.

The crux is the per-row sub-Gaussian moment-generating-function bound: bounding E[exp(t·(√(π/2)·sign⟪u,g⟫·⟪q,g⟫))] sharply requires a folded-normal sub-Gaussian estimate for |⟪u,g⟫| (the crude exp(t|x|) ≤ exp(tx)+exp(-tx) route loses a factor 2 per row, which is fatal for m rows). That estimate is not in mathlib, so we build it from scratch in JL/GaussianTail.lean (foldedNormal_subgaussian) and assemble the per-row bound here in isPerRowSubgaussian_of_unit / isPerRowSubgaussian_normalized. With this in hand the entire exponential bound — per-row MGF, coordinate independence under Measure.pi, additivity of the sub-Gaussian parameter over independent rows, the 1/m rescaling, and the two-sided Chernoff bound — is proved fully and unconditionally.

@[reducible]

def JL.IsPerRowSubgaussian {d : ℕ} (u q : EuclideanSpace ℝ (Fin d)) : Prop

The centered, √(π/2)-scaled per-row sign-product term g ↦ √(π/2)·sign⟪u,g⟫·⟪q,g⟫ − ⟪u,q⟫ has a sub-Gaussian moment generating function with variance proxy (π/2)·‖q‖² under the standard Gaussian.

This is proved unconditionally for the normalized key direction by isPerRowSubgaussian_normalized (and for any unit u by isPerRowSubgaussian_of_unit); the named predicate is kept as a convenient abbreviation used by the exponential distortion bound below.

Equations

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

theorem JL.gaussianReal_mgf_id (r : ℝ) (v : NNReal) : ∫ (b : ℝ), Real.exp (r * b) ∂ProbabilityTheory.gaussianReal 0 v = Real.exp (↑v * r ^ 2 / 2)

The moment generating function of a centered real Gaussian: ∫ exp(r·b) d(N(0,v)) = exp(v·r²/2).

theorem JL.isPerRowSubgaussian_of_unit {d : ℕ} (u q : EuclideanSpace ℝ (Fin d)) (hu : ‖u‖ = 1) : IsPerRowSubgaussian u q

Per-row sub-Gaussian MGF bound (unit u), proved unconditionally. For a unit vector u and arbitrary q, the centered √(π/2)-scaled sign-product term g ↦ √(π/2)·sign⟪u,g⟫·⟪q,g⟫ − ⟪u,q⟫ is sub-Gaussian with variance proxy (π/2)·‖q‖² under the standard Gaussian.

The proof decomposes q = ⟪u,q⟫·u + w with w ⟂ u. Under the standard Gaussian, a := ⟪u,g⟫ and b := ⟪w,g⟫ are independent, with a ~ N(0,1) and b ~ N(0,‖w‖²). Pushing forward to the product law N(0,1) ⊗ N(0,‖w‖²) and integrating in b first (Gaussian MGF) leaves a folded-normal integral in a, controlled by foldedNormal_subgaussian. The two variance proxies combine to (π/2)(⟪u,q⟫² + ‖w‖²) = (π/2)‖q‖² by Pythagoras.

theorem JL.isPerRowSubgaussian_normalized {d : ℕ} (key q : EuclideanSpace ℝ (Fin d)) : IsPerRowSubgaussian (‖key‖⁻¹ • key) q

Per-row sub-Gaussian MGF bound for the normalized key, proved unconditionally. For any key and q, the normalized direction ‖key‖⁻¹ • key satisfies IsPerRowSubgaussian. When key ≠ 0 this is the unit case isPerRowSubgaussian_of_unit; when key = 0 the normalized direction is 0, the per-row term is identically 0, and the bound is trivial.

theorem JL.qjlEstimator_centered_hasSubgaussianMGF {m d : ℕ} (hm : 0 < m) (key q : EuclideanSpace ℝ (Fin d)) : ProbabilityTheory.HasSubgaussianMGF (fun (S : Fin m → EuclideanSpace ℝ (Fin d)) => qjlEstimator key q S - inner ℝ (‖key‖⁻¹ • key) q) ⟨Real.pi / 2 * ‖q‖ ^ 2 / ↑m, ⋯⟩ (MeasureTheory.Measure.pi fun (x : Fin m) => ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin d)))

Centered estimator is sub-Gaussian. The centered estimator qjlEstimator − ⟪key/‖key‖, q⟫ is sub-Gaussian with variance proxy (π/2)·‖q‖² / m under the m-fold product Gaussian, by summing the m i.i.d. per-row terms (independent coordinates of Measure.pi) and rescaling by 1/m. The per-row sub-Gaussian bound is supplied unconditionally by isPerRowSubgaussian_normalized.

theorem JL.qjlEstimator_concentration_exp {m d : ℕ} (hm : 0 < m) (key q : EuclideanSpace ℝ (Fin d)) {ε : ℝ} (hε : 0 < ε) : (MeasureTheory.Measure.pi fun (x : Fin m) => ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin d))).real {S : Fin m → EuclideanSpace ℝ (Fin d) | ε ≤ |qjlEstimator key q S - inner ℝ (‖key‖⁻¹ • key) q|} ≤ 2 * Real.exp (-(↑m * ε ^ 2) / (Real.pi * ‖q‖ ^ 2))

QJL exponential distortion bound (sub-Gaussian / Chernoff). The asymmetric 1-bit estimator deviates from the true normalized inner product ⟪key/‖key‖, q⟫ by at least ε with probability at most 2 · exp(-m·ε² / (π·‖q‖²)), an exponential (rather than polynomial) improvement over the Chebyshev bound qjlEstimator_concentration. Hence m = O(‖q‖²·log(1/δ)/ε²) sign-bits suffice for additive error ε with probability 1 − δ.