Special Functions · Lean source
MissingSuccess.lean
Selected results recorded Coverage and evidence
Compiler/replay evidence is reported for a subset or bounded block. No whole-work coverage is implied.
This viewer reads the retained source; it does not run Lean or assign new claim mappings.
Local imports (1)
guarded_majorant_controls/MissingSuccess.lean9 lines
Original source path
lean/guarded_majorant_controls/MissingSuccess.lean1 import CoupledGuardedMajorant
2 noncomputable section
3 open Komorebi.SpecialFunctions.Coupled.Scales
4
5 example (p : RationalScales) (hs : p.toReal.positive)
6 (hc : p.toReal.q < 1 ∧ p.toReal.r < 1 ∧ p.toReal.a < 1 ∧ p.toReal.b < 1)
7 (R B : ℚ) (hR : 0 ≤ R) (budget : ℕ) (fits : ℚ → Bool) (i : Fin 2)
8 (z : ℂ) (hz : ‖z‖ ≤ (R : ℝ)) : ‖p.toReal.complexComponent i z‖ ≤ (B : ℝ) := by
9 exact guarded_majorant_disk_bound p hs hc R B hR budget fits i z hz
Original file and source record
This copy matches the recorded source file. Its publication here does not change the work’s review status.
SHA-256: 7fc06fd8c21959132b8f9b57f4b6eeeb8da94edf875873926db88230e4be721d