`BookProof.CarlemanUnboundedHop.inner_block_im_eq_zero` (a : ℕ → ℕ → ℂ) (u : ℕ → ℂ) (hherm : IsHermitianKernel a) (N : ℕ) : (∑ n ∈ range (N + 1), (starRingEnd ℂ) (u n) *...

Proved

BookProof.CarlemanUnboundedHop.inner_block_im_eq_zero

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterCarlemanUnboundedHop.

BookProof.CarlemanUnboundedHop.inner_block_im_eq_zero (a : ℕ → ℕ → ℂ) (u : ℕ → ℂ) (hherm : IsHermitianKernel a) (N : ℕ) : (∑ n ∈ range (N + 1), (starRingEnd ℂ) (u n) * ∑ k ∈ range (N + 1), a n k * u k).im = 0

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

Preamble

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



open Finset

noncomputable section

Formal statement

theorem BookProof.CarlemanUnboundedHop.inner_block_im_eq_zero (a : ℕ → ℕ → ℂ) (u : ℕ → ℂ) (hherm : IsHermitianKernel a)
    (N : ℕ) :
    (∑ n ∈ range (N + 1), (starRingEnd ℂ) (u n) *
        ∑ k ∈ range (N + 1), a n k * u k).im = 0 := by sorry

View graph