NormalizedShell.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Additive boundary slices vanish after the smooth-cofactor cost.

def OAI.TotientAsymptotic.normalizedShellLoss line 14
lemma OAI.TotientAsymptotic.normalizedShellLoss_tendsto line 18
theorem OAI.TotientAsymptotic.normalized_additive_shell_loss line 31
Source documentation
All retained boundary slices have negligible normalized volume, even after paying for every admissible smooth cofactor.
```
theorem normalized_additive_shell_loss (hren : FordRenewalInput) (K : ℝ) :
    ∃ δ : ℕ → ℝ, Tendsto δ atTop (nhds 0) ∧
      ∀ᶠ H : ℕ in atTop, ∀ᶠ x : ℝ in atTop,
      ∀ hRN : R x H ≤ L x H,
      Real.exp (K*cofactorScale H)*
        volume.real (additiveBoxShell x (R x H) (L x H) hRN)/G x (m x) ≤ δ H := by
…
```
Mentions: OAI.TotientAsymptotic.FordRenewalInput, OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.L, OAI.TotientAsymptotic.cofactorScale, OAI.TotientAsymptotic.additiveBoxShell, OAI.TotientAsymptotic.G, OAI.TotientAsymptotic.m