`BookProof.HermiteExpWall.l2_gaussPoly_le_of_gint_le` {q : Polynomial ℝ} {K : ℝ} (hK : 0 ≤ K) (N : ℕ) (h : gint (q * q) ≤ K ^ 2 * gaussMoment (2 * N)) : l2 (gaussPoly q) ≤ K * l2 (

Initializing...

`BookProof.HermiteExpWall.l2_gaussPoly_le_of_gint_le` {q : Polynomial ℝ} {K : ℝ} (hK : 0 ≤ K) (N : ℕ) (h : gint (q * q) ≤ K ^ 2 * gaussMoment (2 * N)) : l2 (gaussPoly q) ≤ K * l2 ( · Prove2Me