ShellCost.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Simultaneous summation of the unit-box slack-shell costs.

lemma OAI.TotientAsymptotic.uniform_slice_bound line 14
lemma OAI.TotientAsymptotic.sum_reverse_prefix line 41
def OAI.TotientAsymptotic.quadraticShellTail line 62
lemma OAI.TotientAsymptotic.quadraticShellTail_tendsto line 65
theorem OAI.TotientAsymptotic.prefix_cube_shell_cost line 72
Source documentation
Summing the slice bounds for all unit-box boundary errors has a vanishing tail uniform in the moving dimension and phase.
```
theorem prefix_cube_shell_cost (hford : FordRenewalInput) :
    ∃ C : ℝ, 0 < C ∧ ∀ᶠ x : ℝ in atTop, ∀ H ≤ m x,
      (R x H : ℝ)/B x * (∑ i : Fin (R x H),
        g (i.val+1)*((m x-(i.val+1) : ℕ) : ℝ)^2) ≤ C*quadraticShellTail H := by
…
```
Mentions: OAI.TotientAsymptotic.FordRenewalInput, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.g, OAI.TotientAsymptotic.quadraticShellTail