(U S : E →L[ℂ] E) (C Dmin h : ℝ) (m : ℕ) (hU : ∀ w : E, ‖U w‖ ≤ ‖w‖) (hS : ∀ w : E, ‖S w‖ ≤ ‖w‖) (hstep : ∀ w : E, ‖U w - S w‖ ≤ sirkBound C Dmin h 1 m *...
ProvedBookProof.ChapterSirkRestart.restart_error_accumulation_sirksirkspectral-theorytimepiece
Lean 4 theorem BookProof.ChapterSirkRestart.restart_error_accumulation_sirk (module BookProof.ChapterSirkRestart), source chapter BookProof/ChapterChapterSirkRestart.lean.
Preamble
-- Generated from ChapterSirkRestart.lean — theorem BookProof.ChapterSirkRestart.restart_error_accumulation_sirk
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.restart_error_accumulation_sirk (U S : E →L[ℂ] E) (C Dmin h : ℝ) (m : ℕ)
(hU : ∀ w : E, ‖U w‖ ≤ ‖w‖) (hS : ∀ w : E, ‖S w‖ ≤ ‖w‖)
(hstep : ∀ w : E, ‖U w - S w‖ ≤ sirkBound C Dmin h 1 m * ‖w‖)
(n : ℕ) (v : E) :
‖(U ^ n) v - (S ^ n) v‖ ≤ n * sirkBound C Dmin h 1 m * ‖v‖ := by sorrySource