`BookProof.NavierStokesFlow.FockOfFock.lpDiag_inner_self` {ι : Type*} (c : ι → ℝ) (v : lpFiniteModes ι) : (inner ℂ ((v : lp (fun _ : ι => ℂ) 2)) (((lpDiag c v : lpFiniteModes ι) :

Proved

BookProof.NavierStokesFlow.FockOfFock.lpDiag_inner_self

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterNavierStokesFockEsa.

BookProof.NavierStokesFlow.FockOfFock.lpDiag_inner_self {ι : Type*} (c : ι → ℝ) (v : lpFiniteModes ι) : (inner ℂ ((v : lp (fun _ : ι => ℂ) 2)) (((lpDiag c v : lpFiniteModes ι) : lp (fun _ : ι => ℂ) 2)) : ℂ) = ((∑ i ∈ v.2.toFinset, c i * ‖((v : lp (fun _ : ι => ℂ) 2) : ι → ℂ) i‖ ^ 2 : ℝ) : ℂ)

Formalization note: Lean 4 identifier BookProof.NavierStokesFlow.FockOfFock.lpDiag_inner_self.

Preamble

-- Generated from ChapterNavierStokesFockEsa.lean — theorem BookProof.NavierStokesFlow.FockOfFock.lpDiag_inner_self
import Mathlib
import Definitions.Def_ChapterNavierStokesFockEsa
import Definitions.Def_ChapterNavierStokesEsa
import Definitions.Def_ChapterNavierStokesFockSpace
import Definitions.Def_ChapterNavierStokesAffineFiberEsa
open BookProof.NavierStokesFlow.FockOfFock
open BookProof.NavierStokesFlow


open MeasureTheory



open FullEsa LagrangianEsa

variable {M : Type*} [DecidableEq M]
variable {M : Type*} [DecidableEq M] {Ω : Type*} [MeasurableSpace Ω]

Formal statement

theorem BookProof.NavierStokesFlow.FockOfFock.lpDiag_inner_self {ι : Type*} (c : ι → ℝ) (v : lpFiniteModes ι) :
    (inner ℂ ((v : lp (fun _ : ι => ℂ) 2))
        (((lpDiag c v : lpFiniteModes ι) : lp (fun _ : ι => ℂ) 2)) : ℂ)
      = ((∑ i ∈ v.2.toFinset, c i * ‖((v : lp (fun _ : ι => ℂ) 2) : ι → ℂ) i‖ ^ 2 : ℝ) : ℂ) := by sorry

View graph