`BookProof.SmHamiltonian.realCoeff_smMagW` (P : SmParams) (co : Fin 163 → Fin D) (m i : Fin 3) : RealCoeff (smMagW P co m i)

Proved

BookProof.SmHamiltonian.realCoeff_smMagW

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterSmHamiltonian.

BookProof.SmHamiltonian.realCoeff_smMagW (P : SmParams) (co : Fin 163 → Fin D) (m i : Fin 3) : RealCoeff (smMagW P co m i)

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

Preamble

-- Generated from ChapterSmHamiltonian.lean — theorem BookProof.SmHamiltonian.realCoeff_smMagW
import Definitions.Def_ChapterYangMillsFriedrichs
import Definitions.Def_ChapterHermiteProductCore
import Definitions.Def_ChapterFarisLavine
import Definitions.Def_ChapterFriedrichsExtension
import Mathlib
import Definitions.Def_ChapterSmHamiltonian
import Definitions.Def_ChapterSirkFinitePrecision
import Definitions.Def_ChapterSmOneParticle
import Definitions.Def_ChapterYangMillsHermite
open BookProof.SirkFinitePrecision
open BookProof.SirkFinitePrecision.CertInterval
open BookProof.SmOneParticle
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.realCoeff_smMagW (P : SmParams) (co : Fin 163 → Fin D) (m i : Fin 3) :
    RealCoeff (smMagW P co m i) := by sorry

View graph