NormalizedConcentration.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The full-dimensional band loss vanishes after both normalization and the entire discrete-cofactor cost.

def OAI.TotientAsymptotic.normalizedBandLoss line 15
lemma OAI.TotientAsymptotic.normalizedBandLoss_tendsto line 19
theorem OAI.TotientAsymptotic.normalized_retained_band_loss line 37
Source documentation
For every fixed cofactor exponent, Ford concentration removes all retained phase bands with an error tending to zero as the tail cut grows.
```
theorem normalized_retained_band_loss (hford : FordCoordinateConcentrationInput)
    (hren : FordRenewalInput) (K : ℝ) :
    ∃ δ : ℕ → ℝ, Tendsto δ atTop (nhds 0) ∧
      ∀ᶠ H : ℕ in atTop, ∀ᶠ x : ℝ in atTop,
        ∀ N : ℕ, L x H=N+2 → ∀ hRN : R x H ≤ N+2,
        Real.exp (K*cofactorScale H)*volume.real (retainedPhaseBad x H (N+2) hRN) /
          G x (m x) ≤ δ H := by
…
```
Mentions: OAI.TotientAsymptotic.FordCoordinateConcentrationInput, OAI.TotientAsymptotic.FordRenewalInput, OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.L, OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.cofactorScale, OAI.TotientAsymptotic.retainedPhaseBad, OAI.TotientAsymptotic.G, OAI.TotientAsymptotic.m