The Lean 4 theorem `two_re_inner_kin_harm_ge` in the `ChapterHermiteQuadraticEsa` chapter of the timepiece formalization

Proved

BookProof.HermiteQuadraticEsa.two_re_inner_kin_harm_ge

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

timepiece

The Lean 4 theorem two_re_inner_kin_harm_ge in the ChapterHermiteQuadraticEsa chapter of the timepiece formalization.

Preamble

-- Generated from ChapterHermiteQuadraticEsa.lean — theorem BookProof.HermiteQuadraticEsa.two_re_inner_kin_harm_ge
import Mathlib
import Definitions.Def_ChapterHermiteQuadraticEsa
open BookProof.HermiteQuadraticEsa














open MeasureTheory Complex MvPolynomial
open BookProof.HermiteProductCore BookProof.QgHermiteCore BookProof.QgHermiteFriedrichs
open BookProof.QgHermiteOscillator BookProof.FarisLavine BookProof.Starobinsky
open BookProof.StoneBridge BookProof.EsaClosure BookProof.ChapterStoneResolvent

noncomputable section

variable {d : ℕ}

Formal statement

theorem BookProof.HermiteQuadraticEsa.two_re_inner_kin_harm_ge (p : MvPolynomial (Fin d) ℂ) :
    -((d : ℝ) / 2) * ‖pgLp p‖ ^ 2
      ≤ 2 * (inner ℂ (pgLp (kinPoly p)) (pgLp (harmPoly * p)) : ℂ).re := by sorry

Source

https://github.com/leonardopedro/timepiece/blob/61595bc/BookProof/ChapterHermiteQuadraticEsa.lean

View graph