Prove2Me

(s : Finset (Fin d)) (v : Fin d → lpFiniteModes (Occ d)) (α : Occ d) : (((∑ i ∈ s, v i : lpFiniteModes (Occ d)) : L2I (Occ d)) : Occ d → ℂ) α = ∑ i ∈ s, (((v i : lpFiniteModes...

Proved
BookProof.NavierStokesFlow.FockCanonical.coe_sum_apply

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

navier-stokesoperator-algebrastimepiece

Lean 4 theorem BookProof.NavierStokesFlow.FockCanonical.coe_sum_apply (module BookProof.NavierStokesFlow), source chapter BookProof/ChapterNavierStokesFlow.lean.

Preamble
-- Generated from ChapterNavierStokesFockCanonical.lean — theorem BookProof.NavierStokesFlow.FockCanonical.coe_sum_apply
import Mathlib
import Definitions.Def_ChapterNavierStokesFockCanonical
import Definitions.Def_ChapterNavierStokesEsa
import Definitions.Def_ChapterNavierStokesFockManyMode
import Definitions.Def_ChapterNavierStokesAffineFiberEsa
open BookProof.NavierStokesFlow
open BookProof.NavierStokesFlow
open BookProof.NavierStokesFlow.FockCanonical

variable {d : ℕ} {κ : Fin d → ℝ}


open scoped ENNReal



open LpNat BookProof.FarisLavine IkebeKato ShiftHamiltonian FockManyMode HermiteCanonical
Formal statement
theorem BookProof.NavierStokesFlow.FockCanonical.coe_sum_apply (s : Finset (Fin d)) (v : Fin d → lpFiniteModes (Occ d)) (α : Occ d) :
    (((∑ i ∈ s, v i : lpFiniteModes (Occ d)) : L2I (Occ d)) : Occ d → ℂ) α
      = ∑ i ∈ s, (((v i : lpFiniteModes (Occ d)) : L2I (Occ d)) : Occ d → ℂ) α := by sorry
Source
https://github.com/leonardopedrio/timepiece/blob/61595bc/BookProof/ChapterNavierStokesFlow.lean

View graph