The Lean 4 theorem `kinetic_posSemidef` in the `ChapterNavierStokesFlow` chapter of the timepiece formalization

Proved

BookProof.NavierStokesFlow.LagrangianNS.kinetic_posSemidef

by leonardopedro · Sep 18, 2026 · Mathlib 0df444a (Lean v4.33.1)

timepiece

The Lean 4 theorem kinetic_posSemidef in the ChapterNavierStokesFlow chapter of the timepiece formalization.

Preamble

-- Generated from ChapterNavierStokesFlow.lean — theorem BookProof.NavierStokesFlow.LagrangianNS.kinetic_posSemidef
import Mathlib
import Definitions.Def_ChapterNavierStokesFlow
open BookProof.NavierStokesFlow
open BookProof.NavierStokesFlow.LagrangianNS


open scoped BigOperators Matrix Kronecker ComplexOrder TensorProduct

variable {n : ℕ} (L : LagrangianNS n)

Formal statement

theorem BookProof.NavierStokesFlow.LagrangianNS.kinetic_posSemidef : L.kinetic.PosSemidef := by sorry

Source

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

View graph