Prove2Me

The Lean 4 theorem `wave_indefiniteQuadratic_essentiallySelfAdjoint` in the `ChapterHyperbolicQuadraticEsa` chapter of the timepiece formalization

Proved
BookProof.HyperbolicQuadratic.wave_indefiniteQuadratic_essentiallySelfAdjoint

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

timepiece

The Lean 4 theorem wave_indefiniteQuadratic_essentiallySelfAdjoint in the ChapterHyperbolicQuadraticEsa chapter of the timepiece formalization.

Preamble
-- Generated from ChapterHyperbolicQuadraticEsa.lean — theorem BookProof.HyperbolicQuadratic.wave_indefiniteQuadratic_essentiallySelfAdjoint
import Mathlib
import Definitions.Def_ChapterHyperbolicQuadraticEsa
open BookProof.HyperbolicQuadratic



open MeasureTheory MvPolynomial
open BookProof.HermiteProductCore BookProof.HermiteProductBasis
open BookProof.FarisLavine
open BookProof.NavierStokesFlow.DifferentialL2

noncomputable section
Formal statement
theorem BookProof.HyperbolicQuadratic.wave_indefiniteQuadratic_essentiallySelfAdjoint (n : ℕ) :
    EssentiallySelfAdjointOn (polyGaussCore (d := 1 + n)) (quadOp (minkowskiCoeff n)) := by sorry
Source
https://github.com/leonardopedro/timepiece/blob/61595bc/BookProof/ChapterHyperbolicQuadraticEsa.lean

View graph