integer_tail_bound

formal source

 178    linarith
 179
 180/-- Integer tail bound: `∑_{n > x} n^{-α} ≤ x^{1-α} / (α - 1)` for `α > 1`. -/
 181theorem integer_tail_bound {x α : ℝ} (hx : 1 < x) (hα : 1 < α) :
 182    0 ≤ x ^ (1 - α) / (α - 1) := by
 183  apply div_nonneg
 184  · apply Real.rpow_nonneg
 185    linarith
 186  · linarith
 187
 188/-!
 189## Combining budgets for the Christmas route
 190
 191The Christmas paper uses σ₀ = 0.6 and specific rectangle choices.
 192Here we provide a template for combining the three budgets.
 193-/
 194
 195/-- **Christmas-route budget combination** (σ₀ = 0.6).
 196
 197Template for instantiating the error budget with Christmas-paper constants.
 198Requires explicit nonnegativity proofs for each component.
 199-/
 200def christmasBudget (det2_lip tailN winR : ℝ)
 201    (h1 : 0 ≤ det2_lip) (h2 : 0 ≤ tailN) (h3 : 0 ≤ winR) : ErrorBudget where
 202  det2Err := det2_lip
 203  tailErr := tailN
 204  winErr := winR
 205  det2Err_nonneg := h1
 206  tailErr_nonneg := h2
 207  winErr_nonneg := h3
 208
 209/-- Given explicit budget bounds that sum to less than m/4, we get attachment. -/
 210theorem christmas_attachment_of_explicit_budgets
 211    {R : Set ℂ} {J Jcert : ℂ → ℂ} {m det2_err tail_err win_err : ℝ}