Quantized Johnson–Lindenstrauss (QJL): unbiasedness of the 1-bit estimator

This file formalizes the unbiasedness theorem at the heart of QJL / TurboQuant's one-bit key quantization. It is built in three increasing layers:

1. Gaussian absolute moment (integral_abs_gaussianReal): E|Z| = √(2/π) for Z ~ N(0,1).

2. The asymmetric sign-product identity (sign_product_identity): for a standard Gaussian vector g in ℝ^d, a unit vector u, and an arbitrary v, E[ sign ⟪u,g⟫ · ⟪v,g⟫ ] = √(2/π) · ⟪u,v⟫. This is the asymmetric one-bit (one-sided, linear) analogue; it is not the symmetric Grothendieck arcsin identity E[ sign ⟪u,g⟫ · sign ⟪v,g⟫ ] = (2/π)·arcsin ⟪u,v⟫. The proof decomposes v = ⟪u,v⟫·u + v⊥ with v⊥ ⟂ u, uses that ⟪v⊥,g⟫ is independent of ⟪u,g⟫ (orthogonal linear functionals of a standard Gaussian are independent, via HasGaussianLaw.indepFun_of_covariance_eq_zero), and that the cross term vanishes because E⟪v⊥,g⟫ = 0.

3. QJL asymmetric estimator unbiasedness (qjlEstimator_unbiased): the 1-bit estimator estimator S key q = √(π/2)·(1/m)·Σᵢ sign ⟪key/‖key‖, sᵢ⟫ · ⟪q, sᵢ⟫ over an m × d i.i.d. standard-Gaussian sketch is unbiased for the normalized inner product: E[estimator] = ⟪key/‖key‖, q⟫.

Part 1: the Gaussian absolute moment E|Z| = √(2/π)

theorem JL.measurable_real_sign : Measurable Real.sign

Measurability of the real sign function.

theorem JL.sign_mul_self (r : ℝ) : r.sign * r = |r|

Real.sign r * r = |r|.

theorem JL.integral_Ioi_mul_exp : ∫ (x : ℝ) in Set.Ioi 0, x * Real.exp (-(1 / 2) * x ^ 2) = 1

The half-line first moment: ∫_{x>0} x·exp(-x²/2) dx = 1.

theorem JL.integral_abs_gaussianReal : ∫ (x : ℝ), |x| ∂ProbabilityTheory.gaussianReal 0 1 = √(2 / Real.pi)

Gaussian absolute moment. E|Z| = √(2/π) for Z ~ N(0,1).

Part 2: the asymmetric sign-product identity

theorem JL.integrable_inner_stdGaussian {d : ℕ} (w : EuclideanSpace ℝ (Fin d)) : MeasureTheory.Integrable (fun (g : EuclideanSpace ℝ (Fin d)) => inner ℝ w g) (ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin d)))

Integrability of a Gaussian linear functional g ↦ ⟪w, g⟫.

theorem JL.sign_product_identity {d : ℕ} (u v : EuclideanSpace ℝ (Fin d)) (hu : ‖u‖ = 1) : ∫ (g : EuclideanSpace ℝ (Fin d)), (inner ℝ u g).sign * inner ℝ v g ∂ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin d)) = √(2 / Real.pi) * inner ℝ u v

Asymmetric sign-product identity. For a standard Gaussian vector g in ℝ^d, a unit vector u and an arbitrary v, E[ sign ⟪u,g⟫ · ⟪v,g⟫ ] = √(2/π) · ⟪u,v⟫.

This is the asymmetric one-bit (one-sided, linear) identity; it is not the symmetric Grothendieck arcsin identity E[ sign ⟪u,g⟫ · sign ⟪v,g⟫ ] = (2/π)·arcsin ⟪u,v⟫.

The proof writes v = ⟪u,v⟫·u + v⊥ with v⊥ ⟂ u. The v⊥ part contributes E[ sign ⟪u,g⟫ · ⟪v⊥,g⟫ ] = E[sign ⟪u,g⟫]·E[⟪v⊥,g⟫] = 0 because the two orthogonal linear functionals are independent (HasGaussianLaw.indepFun_of_covariance_eq_zero) and E⟪v⊥,g⟫ = 0; the u part contributes ⟪u,v⟫·E|⟪u,g⟫| = ⟪u,v⟫·√(2/π).

Part 3: QJL asymmetric 1-bit estimator unbiasedness

theorem JL.integrable_sign_inner_mul {d : ℕ} (u w : EuclideanSpace ℝ (Fin d)) : MeasureTheory.Integrable (fun (g : EuclideanSpace ℝ (Fin d)) => (inner ℝ u g).sign * inner ℝ w g) (ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin d)))

Integrability of g ↦ sign ⟪u,g⟫ · ⟪w,g⟫ under a standard Gaussian: the sign factor is bounded by 1 and g ↦ ⟪w,g⟫ is integrable.

theorem JL.integral_eval_pi {m : ℕ} {E : Type u_1} [MeasurableSpace E] (P : MeasureTheory.Measure E) [MeasureTheory.IsProbabilityMeasure P] (i : Fin m) (f : E → ℝ) (hf : MeasureTheory.AEStronglyMeasurable f P) : (∫ (S : Fin m → E), f (S i) ∂MeasureTheory.Measure.pi fun (x : Fin m) => P) = ∫ (x : E), f x ∂P

Marginalization: integrating a function of a single coordinate against a product of i.i.d. probability measures equals the single-coordinate integral.

noncomputable def JL.qjlEstimator {m d : ℕ} (key q : EuclideanSpace ℝ (Fin d)) (S : Fin m → EuclideanSpace ℝ (Fin d)) : ℝ

The QJL asymmetric 1-bit estimator. Given an m × d sketch S whose rows S i are i.i.d. standard Gaussian vectors, a key and a query q, estimator = √(π/2) · (1/m) · Σᵢ sign ⟪key/‖key‖, sᵢ⟫ · ⟪q, sᵢ⟫.

Equations

• JL.qjlEstimator key q S = √(Real.pi / 2) * ((↑m)⁻¹ * ∑ i : Fin m, (inner ℝ (‖key‖⁻¹ • key) (S i)).sign * inner ℝ q (S i))

theorem JL.qjlEstimator_unbiased {m d : ℕ} (hm : 0 < m) (key q : EuclideanSpace ℝ (Fin d)) (hkey : key ≠ 0) : (∫ (S : Fin m → EuclideanSpace ℝ (Fin d)), qjlEstimator key q S ∂MeasureTheory.Measure.pi fun (x : Fin m) => ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin d))) = inner ℝ (‖key‖⁻¹ • key) q

QJL unbiasedness. Over an m × d i.i.d. standard-Gaussian sketch, the asymmetric 1-bit estimator is unbiased for the normalized inner product ⟪key/‖key‖, q⟫.

theorem JL.qjlEstimator_unbiased_inner {m d : ℕ} (hm : 0 < m) (key q : EuclideanSpace ℝ (Fin d)) (hkey : key ≠ 0) : (‖key‖ * ∫ (S : Fin m → EuclideanSpace ℝ (Fin d)), qjlEstimator key q S ∂MeasureTheory.Measure.pi fun (x : Fin m) => ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin d))) = inner ℝ key q

QJL unbiasedness, un-normalized form. ‖key‖ · E[estimator] = ⟪key, q⟫.