The Lean 4 theorem `isBand1_mulXPoly` in the `ChapterHermiteBandCalculus` chapter of the timepiece formalization

Proved

BookProof.HermiteBand.isBand1_mulXPoly

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

timepiece

The Lean 4 theorem isBand1_mulXPoly in the ChapterHermiteBandCalculus chapter of the timepiece formalization.

Preamble

-- Generated from ChapterHermiteBandCalculus.lean — theorem BookProof.HermiteBand.isBand1_mulXPoly
import Mathlib
import Definitions.Def_ChapterHermiteBandCalculus
open BookProof.HermiteBand







noncomputable section

open MvPolynomial BookProof.HermiteProductCore BookProof.HermiteProductBasis

variable {d : ℕ}

























open BookProof.NavierStokesFlow.DifferentialL2 BookProof.FullQuadratic

Formal statement

theorem BookProof.HermiteBand.isBand1_mulXPoly (i : Fin d) : IsBand1 (mulXPoly i) := by sorry

Source

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

View graph