Prove2Me

`BookProof.SmHamiltonian.smField_symmetricOn` (P : SmParams) (r : Fin 49) : SymmetricOn (polyGaussCore (d := 163)) ((polyGaussCore (d := 163)).subtype.comp (smField P r))

Proved
BookProof.SmHamiltonian.smField_symmetricOn

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterSmHamiltonian.

BookProof.SmHamiltonian.smField_symmetricOn (P : SmParams) (r : Fin 49) : SymmetricOn (polyGaussCore (d := 163)) ((polyGaussCore (d := 163)).subtype.comp (smField P r))

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

Preamble
-- Generated from ChapterSmHamiltonian.lean — theorem BookProof.SmHamiltonian.smField_symmetricOn
import Definitions.Def_ChapterSmOneParticle
import Definitions.Def_ChapterYangMillsFriedrichs
import Definitions.Def_ChapterFarisLavine
import Definitions.Def_ChapterFriedrichsExtension
import Mathlib
import Definitions.Def_ChapterSmHamiltonian
import Definitions.Def_ChapterF7
import Definitions.Def_ChapterFarisLavineCore
import Definitions.Def_ChapterHermiteProductCore
import Definitions.Def_ChapterYangMillsHermite
open BookProof.ChapterF7
open BookProof.HermiteProductCore
open BookProof.YangMillsHermite
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.smField_symmetricOn (P : SmParams) (r : Fin 49) :
    SymmetricOn (polyGaussCore (d := 163))
      ((polyGaussCore (d := 163)).subtype.comp (smField P r)) := by sorry

View graph