`excess_bounded`

proved

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.AnnularCost
domain: NumberTheory
line: 648 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.NumberTheory.AnnularCost on GitHub at line 648.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 645/-- The excess cost: annular cost minus the topological floor.
 646    For a field F(s) = (s−ρ)^{−m} G(s) with G regular:
 647    excess = annularCost(F) − ∑ topologicalFloor(n, m) = O(R²). -/
 648theorem excess_bounded (carrier : BudgetedCarrier) :
 649    ∃ K : ℝ, ∀ N : ℕ,
 650      annularExcess (carrier.trace.mesh N) ≤
 651        K * carrier.logDerivBound ^ 2 * carrier.radius ^ 2 := by
 652  exact carrier_budget carrier
 653
 654end NumberTheory
 655end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.