`BookProof.SmHamiltonian.smHamiltonian_quadForm` (P : SmParams) (x : polyGaussCore (d := 163)) : quadForm (smHamiltonian P) x = 1 / 2 * (∑ m, ‖((smPi m x : polyGaussCore (d := 163)

Proved

BookProof.SmHamiltonian.smHamiltonian_quadForm

by leonardopedro · Oct 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

theoremstimepiece

Prove the following Lean 4 theorem from ChapterSmHamiltonian.

BookProof.SmHamiltonian.smHamiltonian_quadForm (P : SmParams) (x : polyGaussCore (d := 163)) : quadForm (smHamiltonian P) x = 1 / 2 * (∑ m, ‖((smPi m x : polyGaussCore (d := 163)) : L2d 163)‖ ^ 2) + 1 / 2 * ∑ r, ‖((smField P r x : polyGaussCore (d := 163)) : L2d 163)‖ ^ 2

Formalization note: Lean 4 identifier BookProof.SmHamiltonian.smHamiltonian_quadForm.

Preamble

-- Generated from ChapterSmHamiltonian.lean — theorem BookProof.SmHamiltonian.smHamiltonian_quadForm
import Definitions.Def_ChapterSmOneParticle
import Definitions.Def_ChapterYangMillsHermite
import Definitions.Def_ChapterFarisLavine
import Definitions.Def_ChapterFriedrichsExtension
import Mathlib
import Definitions.Def_ChapterSmHamiltonian
import Definitions.Def_ChapterFarisLavineCore
import Definitions.Def_ChapterHermiteProductCore
import Definitions.Def_ChapterYangMillsFriedrichs
open BookProof.HermiteProductCore
open BookProof.YangMillsFriedrichs
open BookProof.SmHamiltonian



open MvPolynomial
open BookProof.SmOneParticle
open BookProof.YangMillsHermite BookProof.YangMillsFriedrichs
open BookProof.HermiteProductCore BookProof.FarisLavine
open BookProof.FriedrichsExtension

noncomputable section

variable {D : ℕ}

Formal statement

theorem BookProof.SmHamiltonian.smHamiltonian_quadForm (P : SmParams) (x : polyGaussCore (d := 163)) :
    quadForm (smHamiltonian P) x
      = 1 / 2 * (∑ m, ‖((smPi m x : polyGaussCore (d := 163)) : L2d 163)‖ ^ 2)
        + 1 / 2 * ∑ r, ‖((smField P r x : polyGaussCore (d := 163)) : L2d 163)‖ ^ 2 := by sorry

View graph