Inner-product preservation (unquantized Gaussian-projection corollary)

Via the polarization identity ⟪u, v⟫ = (‖u+v‖² - ‖u-v‖²)/4, a linear map that preserves the squared norms of u+v and u-v to within a relative error ε also preserves the inner product ⟪u, v⟫:

|⟪f u, f v⟫ - ⟪u, v⟫| ≤ ε · (‖u‖² + ‖v‖²) / 2.

This is the unquantized inner-product corollary of full-precision Gaussian Johnson–Lindenstrauss: combined with the distributional norm-preservation bound applied to u+v and u-v, the Gaussian projection preserves inner products with high probability. It is the Dasgupta–Gupta baseline that quantized schemes (QJL / TurboQuant) are motivated by and compared against — it is not the mechanism behind QJL's one-bit guarantee, which instead rests on the asymmetric sign-product identity (JL/QJL.lean).

theorem JL.inner_product_preservation {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] (f : E →ₗ[ℝ] F) (u v : E) {ε : ℝ} (hplus : |‖f (u + v)‖ ^ 2 - ‖u + v‖ ^ 2| ≤ ε * ‖u + v‖ ^ 2) (hminus : |‖f (u - v)‖ ^ 2 - ‖u - v‖ ^ 2| ≤ ε * ‖u - v‖ ^ 2) : |inner ℝ (f u) (f v) - inner ℝ u v| ≤ ε * (‖u‖ ^ 2 + ‖v‖ ^ 2) / 2

Inner-product preservation via polarization. A linear map f preserving the squared norms of u+v and u-v within relative error ε preserves ⟪u, v⟫ within ε · (‖u‖² + ‖v‖²)/2.