Prove2Me

(C Dmin h nv : โ„) (n : โ„•) (hh : 0 < h) : Tendsto (fun m : โ„• => (n : โ„) * sirkBound C Dmin h nv m) atTop (๐“ 0)

Proved
BookProof.ChapterSirkRestart.restart_error_tendsto_zero

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

sirkspectral-theorytimepiece

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

Preamble
-- Generated from ChapterSirkRestart.lean โ€” theorem BookProof.ChapterSirkRestart.restart_error_tendsto_zero
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_tendsto_zero (C Dmin h nv : โ„) (n : โ„•) (hh : 0 < h) :
    Tendsto (fun m : โ„• => (n : โ„) * sirkBound C Dmin h nv m) atTop (๐“ 0) := by sorry
Source
https://github.com/leonardopedrio/timepiece/blob/61595bc/BookProof/ChapterChapterSirkRestart.lean

View graph