The Lean 4 theorem `lagrangianCore_symmetricOn` in the `ChapterNavierStokesLagrangianKatoRellich` chapter of the timepiece formalization
ProvedBookProof.NavierStokesFlow.LagrangianKatoRellich.lagrangianCore_symmetricOntimepiece
The Lean 4 theorem lagrangianCore_symmetricOn in the ChapterNavierStokesLagrangianKatoRellich chapter of the timepiece formalization.
Preamble
-- Generated from ChapterNavierStokesLagrangianKatoRellich.lean — theorem BookProof.NavierStokesFlow.LagrangianKatoRellich.lagrangianCore_symmetricOn
import Mathlib
import Definitions.Def_ChapterNavierStokesLagrangianKatoRellich
import Definitions.Def_ChapterSirkBandLedger
open BookProof.NavierStokesFlow
open BookProof.NavierStokesFlow.LagrangianKatoRellich
open Filter Topology
open FullEsa LagrangianEsa BookProof.FarisLavine
open BookProof.EsaClosure BookProof.HashimotoShiftInvert BookProof.HermiteGalerkin
variable {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℂ F]
variable (L : LagrangianFullData F)Formal statement
theorem BookProof.NavierStokesFlow.LagrangianKatoRellich.lagrangianCore_symmetricOn : SymmetricOn L.D (lagrangianCore L) := by sorry
Source