Prove2Me

canFun_eq_ladFun

Open
BookProof.NavierStokesFlow.CanonicalVector.canFun_eq_ladFun

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

formalizationtimepiece

Formal statement of BookProof.NavierStokesFlow.CanonicalVector.canFun_eq_ladFun from the timepiece Lean 4 formalization (source chapter BookProof/ChapterNavierStokesCanonicalVector.lean).

Preamble
-- Generated from ChapterNavierStokesCanonicalVector.lean — theorem BookProof.NavierStokesFlow.CanonicalVector.canFun_eq_ladFun
import Mathlib
import Definitions.Def_ChapterNavierStokesCanonicalVector
import Definitions.Def_ChapterNavierStokesThreeComponent
import Definitions.Def_ChapterNavierStokesAffineFiberEsa
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.canFun_eq_ladFun (X : Vel → ℂ) (γ : Vel) :
    canFun A c X γ = ladFun A c X γ := by sorry
Source
https://github.com/leonardpedro/timepiece/blob/61595bc/BookProof/ChapterNavierStokesCanonicalVector.lean

View graph