The Lean 4 theorem `mulHamiltonian_essentiallySelfAdjoint` in the `ChapterFarisLavine` chapter of the timepiece formalization

-- Generated from ChapterFarisLavine.lean — theorem BookProof.FarisLavine.mulHamiltonian_essentiallySelfAdjoint
import Mathlib
import Definitions.Def_ChapterFarisLavine
import Definitions.Def_ChapterNavierStokesFarisLavineLift
import Definitions.Def_ChapterFarisLavineCore
open BookProof.FarisLavine




variable {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℂ F]
variable {D : Submodule ℂ F}




open BookProof.NavierStokesFlow BookProof.NavierStokesFlow.LpNat




open scoped ENNReal

theorem BookProof.FarisLavine.mulHamiltonian_essentiallySelfAdjoint (lam : ℕ → ℝ) :
    EssentiallySelfAdjointOn (mulSymbolDomain lam) (mulHamiltonian lam) := by sorry