The Lean 4 theorem `qgWeylProd_coord_mom_polySym` in the `ChapterQuantumGravity3DGauge` chapter of the timepiece formalization

Proved

BookProof.QuantumGravity3DGauge.qgWeylProd_coord_mom_polySym

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

formalizationtimepiece

Formal statement of BookProof.QuantumGravity3DGauge.qgWeylProd_coord_mom_polySym from the timepiece Lean 4 formalization.

Preamble

-- Generated from ChapterQuantumGravity3DGauge.lean — theorem BookProof.QuantumGravity3DGauge.qgWeylProd_coord_mom_polySym
import Mathlib
import Definitions.Def_ChapterQuantumGravity3DGauge
open BookProof.QuantumGravity3DGauge



open MeasureTheory Complex MvPolynomial Filter Topology
open BookProof.HermiteProductCore BookProof.YangMillsHermite BookProof.YangMillsFriedrichs
open BookProof.FarisLavine BookProof.FriedrichsExtension BookProof.HermiteGalerkin
open BookProof.HashimotoShiftInvert BookProof.QuantumGravityDensitized

noncomputable section

variable {d : ℕ}

Formal statement

theorem BookProof.QuantumGravity3DGauge.qgWeylProd_coord_mom_polySym (j k : Fin d) :
    PolySym (qgWeylProd (mulOp (X j)) (momOp k)) := by sorry

Source

https://github.com/leonardopedro/timepiece

View graph