Prove2Me

The Lean 4 theorem `canH_eq_velH` in the `ChapterNavierStokesCanonicalVector` chapter of the timepiece formalization

Proved
BookProof.NavierStokesFlow.CanonicalVector.canH_eq_velH

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

formalizationtimepiece

Formal statement of BookProof.NavierStokesFlow.CanonicalVector.canH_eq_velH from the timepiece Lean 4 formalization.

Preamble
-- Generated from ChapterNavierStokesCanonicalVector.lean — theorem BookProof.NavierStokesFlow.CanonicalVector.canH_eq_velH
import Mathlib
import Definitions.Def_ChapterNavierStokesCanonicalVector
import Definitions.Def_ChapterNavierStokesEsa
import Definitions.Def_ChapterNavierStokesIkebeKato
import Definitions.Def_ChapterNavierStokesThreeComponent
import Definitions.Def_ChapterNavierStokesAffineFiberEsa
open BookProof.NavierStokesFlow
open BookProof.NavierStokesFlow
open BookProof.NavierStokesFlow
open BookProof.NavierStokesFlow.CanonicalVector


open scoped ENNReal



open LpNat BookProof.FarisLavine IkebeKato ThreeComponent ShiftHamiltonian SignedShift

variable (A : Matrix (Fin 3) (Fin 3) ℝ) (c : Fin 3 → ℝ)
Formal statement
theorem BookProof.NavierStokesFlow.CanonicalVector.canH_eq_velH :
    (lpFiniteModes Vel).subtype.comp (canH A c)
      = (velH A c).comp (Submodule.inclusion (finiteModes_le_maxDom (velSym (velMu A c)))) := by sorry
Source
https://github.com/leonardopedro/timepiece

View graph