(v : c.D) : (inner ℂ ((v : F)) ((c.comparison v : c.D) : F) : ℂ).re = (∑ i, ‖((c.mom i v : c.D) : F)‖ ^ 2) + (∑ i, ‖((c.drift i v : c.D) : F)‖ ^ 2) + ‖(v : F)‖ ^ 2

Proved

BookProof.NavierStokesFlow.FarisLavineLift.ComparisonData.comparison_inner_eq

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

navier-stokesoperator-algebrastimepiece

Lean 4 theorem BookProof.NavierStokesFlow.FarisLavineLift.ComparisonData.comparison_inner_eq (module BookProof.NavierStokesFlow), source chapter BookProof/ChapterNavierStokesFlow.lean.

Preamble

-- Generated from ChapterNavierStokesFarisLavineLift.lean — theorem BookProof.NavierStokesFlow.FarisLavineLift.ComparisonData.comparison_inner_eq
import Mathlib
import Definitions.Def_ChapterNavierStokesFarisLavineLift
open BookProof.NavierStokesFlow
open BookProof.NavierStokesFlow.FarisLavineLift
open BookProof.NavierStokesFlow.FarisLavineLift.ComparisonData













variable {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℂ F]






variable {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℂ F]



variable {d : ℕ} (c : ComparisonData F d)

Formal statement

theorem BookProof.NavierStokesFlow.FarisLavineLift.ComparisonData.comparison_inner_eq (v : c.D) :
    (inner ℂ ((v : F)) ((c.comparison v : c.D) : F) : ℂ).re
      = (∑ i, ‖((c.mom i v : c.D) : F)‖ ^ 2) + (∑ i, ‖((c.drift i v : c.D) : F)‖ ^ 2)
        + ‖(v : F)‖ ^ 2 := by sorry

Source

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

View graph