UnbandedCubeCost.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The additive unit-box cost is uniformly comparable to one renewal coefficient.

lemma OAI.TotientAsymptotic.summable_shifted_square_geometric line 14
theorem OAI.TotientAsymptotic.prefixCubeCost_normalized_bound line 25
theorem OAI.TotientAsymptotic.prefixCubeCost_relative_bound line 83
Source documentation
For prefixes ending H coordinates before the natural dimension, the unit-box enlargement has a uniformly bounded relative volume cost.
```
theorem prefixCubeCost_relative_bound : ∃ C : ℝ, 0 < C ∧
    ∀ᶠ x : ℝ in atTop, ∀ N ≤ m x,
      (N:ℝ)*prefixCubeCost N/B x ≤ C*rho^(m x-N) := by
…
```
Mentions: OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.prefixCubeCost, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.rho