`BookProof.NavierStokesFlow.Carleman.wron_eq_sum` (c w : ℕ → ℂ) (z : ℂ) (hrec : ∀ n, tridiagFun c w n = z * w n) (N : ℕ) : wron c w N = (z - starRingEnd ℂ z) * ∑ n ∈ Finset.range (

Proved

BookProof.NavierStokesFlow.Carleman.wron_eq_sum

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterNavierStokesCarleman.

BookProof.NavierStokesFlow.Carleman.wron_eq_sum (c w : ℕ → ℂ) (z : ℂ) (hrec : ∀ n, tridiagFun c w n = z * w n) (N : ℕ) : wron c w N = (z - starRingEnd ℂ z) * ∑ n ∈ Finset.range (N + 1), starRingEnd ℂ (w n) * w n

Formalization note: Lean 4 identifier BookProof.NavierStokesFlow.Carleman.wron_eq_sum.

Preamble

-- Generated from ChapterNavierStokesCarleman.lean — theorem BookProof.NavierStokesFlow.Carleman.wron_eq_sum
import Mathlib
import Definitions.Def_ChapterNavierStokesCarleman
import Definitions.Def_ChapterNavierStokesAffineFiberEsa
open BookProof.NavierStokesFlow
open BookProof.NavierStokesFlow.Carleman


open scoped ENNReal



open LpNat DiagonalEsa FullEsa

Formal statement

theorem BookProof.NavierStokesFlow.Carleman.wron_eq_sum (c w : ℕ → ℂ) (z : ℂ)
    (hrec : ∀ n, tridiagFun c w n = z * w n) (N : ℕ) :
    wron c w N
      = (z - starRingEnd ℂ z) * ∑ n ∈ Finset.range (N + 1), starRingEnd ℂ (w n) * w n := by sorry

View graph