The Lean 4 theorem `sirk_bands_tendsto_zero` in the `ChapterH8` chapter of the timepiece formalization

Proved

BookProof.ChapterH8.sirk_bands_tendsto_zero

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

timepiece

The Lean 4 theorem sirk_bands_tendsto_zero in the ChapterH8 chapter of the timepiece formalization.

Preamble

-- Generated from ChapterH8.lean — theorem BookProof.ChapterH8.sirk_bands_tendsto_zero
import Mathlib
import Definitions.Def_ChapterH8
open BookProof.ChapterH8


noncomputable section


open BookProof.ChapterH4 BookProof.ChapterH5 BookProof.ChapterH6

Formal statement

theorem BookProof.ChapterH8.sirk_bands_tendsto_zero (C Dmin h nv : ℝ) (hh : 0 < h) :
    Filter.Tendsto (fun n : ℕ => sirkBound C Dmin h nv n) Filter.atTop (nhds 0) := by sorry

Source

https://github.com/leonardopedro/timepiece/blob/61595bc/BookProof/ChapterH8.lean

View graph