pith. machine review for the scientific record. sign in
theorem proved term proof

excess_bounded

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 648theorem excess_bounded (carrier : BudgetedCarrier) :
 649    ∃ K : ℝ, ∀ N : ℕ,
 650      annularExcess (carrier.trace.mesh N) ≤
 651        K * carrier.logDerivBound ^ 2 * carrier.radius ^ 2 := by

proof body

Term-mode proof.

 652  exact carrier_budget carrier
 653
 654end NumberTheory
 655end IndisputableMonolith

depends on (8)

Lean names referenced from this declaration's body.