Prove2Me

(C Dmin h nv : ℝ) (hC : 0 ≤ C) (hD : 0 ≤ Dmin) (hnv : 0 ≤ nv) (hh : 0 ≤ h) : NestedBands (fun _ => (0 : ℝ)) (fun m => sirkBound C Dmin h nv m)

Open
BookProof.BandEnclosure.sirk_nestedBands

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

timepiece

Lean 4 theorem BookProof.BandEnclosure.sirk_nestedBands (module BookProof.BandEnclosure), source chapter BookProof/ChapterBandEnclosure.lean.

Preamble
-- Generated from ChapterBandEnclosure.lean — theorem BookProof.BandEnclosure.sirk_nestedBands
import Mathlib
import Definitions.Def_ChapterBandEnclosure
open BookProof.BandEnclosure










noncomputable section

open Filter Topology


open BookProof.FockOneParticleGap BookProof.FockSecondQuantization
open BookProof.ChapterH6 BookProof.ChapterH8
Formal statement
theorem BookProof.BandEnclosure.sirk_nestedBands (C Dmin h nv : ℝ)
    (hC : 0 ≤ C) (hD : 0 ≤ Dmin) (hnv : 0 ≤ nv) (hh : 0 ≤ h) :
    NestedBands (fun _ => (0 : ℝ)) (fun m => sirkBound C Dmin h nv m) := by sorry
Source
https://github.com/leonardopedrio/timepiece/blob/61595bc/BookProof/ChapterBandEnclosure.lean

View graph