Prove2Me

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

Proved
BookProof.ChapterH6.sirk_error_decay_exponential

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

timepiece

Lean 4 theorem BookProof.ChapterH6.sirk_error_decay_exponential (module BookProof.ChapterH6), source chapter BookProof/ChapterChapterH6.lean.

Preamble
-- Generated from ChapterH6.lean โ€” theorem BookProof.ChapterH6.sirk_error_decay_exponential
import Mathlib
import Definitions.Def_ChapterH6
open BookProof.ChapterH6
open Filter Topology

set_option maxHeartbeats 1000000 in
Formal statement
theorem BookProof.ChapterH6.sirk_error_decay_exponential (C Dmin h nv : โ„) (hh : 0 < h) :
    Tendsto (fun m : โ„• => sirkBound C Dmin h nv m) atTop (๐“ 0) := by sorry
Source
https://github.com/leonardopedrio/timepiece/blob/61595bc/BookProof/ChapterChapterH6.lean

View graph