`BookProof.CarlemanUnboundedHop.flux_identity` {a : ℕ → ℕ → ℂ} {u : ℕ → ℂ} {z : ℂ} (hherm : IsHermitianKernel a) (hrec : LadderRecInf a u z) (N : ℕ) : z.im * ∑ n ∈ range...

Proved

BookProof.CarlemanUnboundedHop.flux_identity

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterCarlemanUnboundedHop.

BookProof.CarlemanUnboundedHop.flux_identity {a : ℕ → ℕ → ℂ} {u : ℕ → ℂ} {z : ℂ} (hherm : IsHermitianKernel a) (hrec : LadderRecInf a u z) (N : ℕ) : z.im * ∑ n ∈ range (N + 1), ‖u n‖ ^ 2 = (flux a u N).im

Formalization note: Lean 4 identifier BookProof.CarlemanUnboundedHop.flux_identity.

Preamble

-- Generated from ChapterCarlemanUnboundedHop.lean — theorem BookProof.CarlemanUnboundedHop.flux_identity
import Mathlib
import Definitions.Def_ChapterCarlemanUnboundedHop
open BookProof.CarlemanUnboundedHop



open Finset

noncomputable section

Formal statement

theorem BookProof.CarlemanUnboundedHop.flux_identity {a : ℕ → ℕ → ℂ} {u : ℕ → ℂ} {z : ℂ} (hherm : IsHermitianKernel a)
    (hrec : LadderRecInf a u z) (N : ℕ) :
    z.im * ∑ n ∈ range (N + 1), ‖u n‖ ^ 2 = (flux a u N).im := by sorry

View graph