The Lean 4 theorem `isBand1_foPoly` in the `ChapterHermiteBandCalculus` chapter of the timepiece formalization
ProvedBookProof.HermiteBand.isBand1_foPolytimepiece
The Lean 4 theorem isBand1_foPoly in the ChapterHermiteBandCalculus chapter of the timepiece formalization.
Preamble
-- Generated from ChapterHermiteBandCalculus.lean — theorem BookProof.HermiteBand.isBand1_foPoly
import Mathlib
import Definitions.Def_ChapterHermiteBandCalculus
open BookProof.HermiteBand
noncomputable section
open MvPolynomial BookProof.HermiteProductCore BookProof.HermiteProductBasis
variable {d : ℕ}
open BookProof.NavierStokesFlow.DifferentialL2 BookProof.FullQuadraticFormal statement
theorem BookProof.HermiteBand.isBand1_foPoly (b b' : Fin d → ℝ) : IsBand1 (BookProof.HermiteRelative.foPoly b b') := by sorry
Source