`sampledBudgetedCarrier`

definition

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.SampledTrace
domain: NumberTheory
line: 163 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.NumberTheory.SampledTrace on GitHub at line 163.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 160/-- Build a `BudgetedCarrier` from a `ZeroWindingCert` and carrier regularity data.
 161This replaces the synthetic `eulerBudgetedCarrier` with one built from actual
 162zero-winding certificates. -/
 163noncomputable def sampledBudgetedCarrier
 164    (cert : ZeroWindingCert)
 165    (logDerivBound : ℝ) (hM : 0 < logDerivBound)
 166    (R : ℝ) (hR : 0 < R) :
 167    BudgetedCarrier where
 168  logDerivBound := logDerivBound
 169  logDerivBound_pos := hM
 170  radius := R
 171  radius_pos := hR
 172  trace := sampledTraceToAnnularTrace cert
 173  trace_charge_zero := sampledTraceToAnnularTrace_charge_zero cert
 174  budgetConstant := 0
 175  budgetConstant_nonneg := le_refl 0
 176  excess_bound := by
 177    intro N
 178    have h := sampledTraceToAnnularTrace_excess_zero cert N
 179    rw [h]
 180    norm_num
 181
 182/-- The budget scale of a sampled carrier is 0. -/
 183theorem sampledBudgetedCarrier_scale_zero
 184    (cert : ZeroWindingCert)
 185    (logDerivBound : ℝ) (hM : 0 < logDerivBound)
 186    (R : ℝ) (hR : 0 < R) :
 187    carrierBudgetScale (sampledBudgetedCarrier cert logDerivBound hM R hR) = 0 := by
 188  simp [sampledBudgetedCarrier, carrierBudgetScale]
 189
 190end
 191
 192end SampledTrace
 193end NumberTheory

papers checked against this theorem

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