Prove2Me

(p : MvPolynomial (Fin D) ℂ) : Real.sqrt ((D : ℝ) / 2) * ‖pgLp p‖ ≤ shiftNorm p

Proved
BookProof.GaussCoreQuadBounds.sqrt_dim_mul_norm_le_shiftNorm

by leonardopedro · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

timepiece

Lean 4 theorem BookProof.GaussCoreQuadBounds.sqrt_dim_mul_norm_le_shiftNorm (module BookProof.GaussCoreQuadBounds), source chapter BookProof/ChapterGaussCoreQuadBounds.lean.

Preamble
-- Generated from ChapterGaussCoreQuadBounds.lean — theorem BookProof.GaussCoreQuadBounds.sqrt_dim_mul_norm_le_shiftNorm
import Mathlib
import Definitions.Def_ChapterGaussCoreQuadBounds
open BookProof.GaussCoreQuadBounds








open Finset MvPolynomial
open BookProof.HermiteProductCore BookProof.QgHermiteCore BookProof.QgHermiteFriedrichs
open BookProof.FarisLavine

noncomputable section

variable {D : ℕ}
Formal statement
theorem BookProof.GaussCoreQuadBounds.sqrt_dim_mul_norm_le_shiftNorm (p : MvPolynomial (Fin D) ℂ) :
    Real.sqrt ((D : ℝ) / 2) * ‖pgLp p‖ ≤ shiftNorm p := by sorry
Source
https://github.com/leonardopedrio/timepiece/blob/61595bc/BookProof/ChapterGaussCoreQuadBounds.lean

View graph