Prove2Me

(U Om : E →L[ℂ] E) (hcomm : Om.comp U = U.comp Om) (n : ℕ) (v : E) (hv : Om v = 0) : Om ((U ^ n) v) = 0

Proved
BookProof.ChapterSirkRestart.brst_leakage_zero_of_exact

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

sirkspectral-theorytimepiece

Lean 4 theorem BookProof.ChapterSirkRestart.brst_leakage_zero_of_exact (module BookProof.ChapterSirkRestart), source chapter BookProof/ChapterChapterSirkRestart.lean.

Preamble
-- Generated from ChapterSirkRestart.lean — theorem BookProof.ChapterSirkRestart.brst_leakage_zero_of_exact
import Mathlib
import Definitions.Def_ChapterSirkRestart
open BookProof.ChapterSirkRestart







noncomputable section

open Filter Topology


open BookProof.ChapterH6

variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℂ E]
Formal statement
theorem BookProof.ChapterSirkRestart.brst_leakage_zero_of_exact (U Om : E →L[ℂ] E)
    (hcomm : Om.comp U = U.comp Om) (n : ℕ) (v : E) (hv : Om v = 0) :
    Om ((U ^ n) v) = 0 := by sorry
Source
https://github.com/leonardopedrio/timepiece/blob/61595bc/BookProof/ChapterChapterSirkRestart.lean

View graph