The Lean 4 theorem `continuityHamiltonian_mem_finiteModes` in the `ChapterNavierStokesEsa` chapter of the timepiece formalization
ProvedBookProof.NavierStokesFlow.continuityHamiltonian_mem_finiteModestimepiece
The Lean 4 theorem continuityHamiltonian_mem_finiteModes in the ChapterNavierStokesEsa chapter of the timepiece formalization.
Preamble
-- Generated from ChapterNavierStokesEsa.lean — theorem BookProof.NavierStokesFlow.continuityHamiltonian_mem_finiteModes
import Mathlib
import Definitions.Def_ChapterNavierStokesEsa
open BookProof.NavierStokesFlow
open scoped Matrix
variable {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℂ F]
variable {ι : Type*}
open BookProof.ChapterContinuityUnitaryInfiniteFormal statement
theorem BookProof.NavierStokesFlow.continuityHamiltonian_mem_finiteModes (v : LinfZ) {f : L2Z} (hf : f ∈ finiteModes) :
continuityHamiltonian v f ∈ finiteModes := by sorrySource