The Lean 4 theorem `norm_basis` in the `ChapterNavierStokesDeficiency` chapter of the timepiece formalization

Proved

BookProof.NavierStokesFlow.DiagonalEsa.norm_basis

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

formalizationtimepiece

Formal statement of BookProof.NavierStokesFlow.DiagonalEsa.norm_basis from the timepiece Lean 4 formalization.

Preamble

-- Generated from ChapterNavierStokesDeficiency.lean — theorem BookProof.NavierStokesFlow.DiagonalEsa.norm_basis
import Mathlib
import Definitions.Def_ChapterNavierStokesDeficiency
open BookProof.NavierStokesFlow
open BookProof.NavierStokesFlow.DiagonalEsa









open scoped ENNReal











open LpNat





























open LpNat

Formal statement

theorem BookProof.NavierStokesFlow.DiagonalEsa.norm_basis (n : ℕ) : ‖basis n‖ = 1 := by sorry

Source

https://github.com/leonardopedro/timepiece

View graph