shiftH_symmetricOn

Proved

BookProof.NavierStokesFlow.ShiftHamiltonian.ShiftData.shiftH_symmetricOn

by leonardopedro · Oct 2, 2026 · Mathlib 0df444a (Lean v4.33.1)

formalizationtimepiece

Formal statement of BookProof.NavierStokesFlow.ShiftHamiltonian.ShiftData.shiftH_symmetricOn from the timepiece Lean 4 formalization (source chapter BookProof/ChapterNavierStokesShiftHamiltonian.lean).

Preamble

-- Generated from ChapterNavierStokesShiftHamiltonian.lean — theorem BookProof.NavierStokesFlow.ShiftHamiltonian.ShiftData.shiftH_symmetricOn
import Mathlib
import Definitions.Def_ChapterNavierStokesShiftHamiltonian
import Definitions.Def_ChapterFarisLavineCore
import Definitions.Def_ChapterNavierStokesHermiteFarisLavine
import Definitions.Def_ChapterNavierStokesIkebeKato
import Definitions.Def_ChapterNavierStokesAffineFiberEsa
open BookProof.NavierStokesFlow.HermiteFarisLavine
open BookProof.NavierStokesFlow
open BookProof.NavierStokesFlow
open BookProof.NavierStokesFlow.ShiftHamiltonian

variable {ι : Type*} (S : ShiftData ι)


open scoped ENNReal



open LpNat BookProof.FarisLavine IkebeKato

Formal statement

theorem BookProof.NavierStokesFlow.ShiftHamiltonian.ShiftData.shiftH_symmetricOn : SymmetricOn (maxDom S.sym) (shiftH S) := by sorry

Source

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

View graph