ResidualCutoff.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The residual smoothness cutoff follows from the actual coarse prime bands.

def OAI.TotientAsymptotic.residualCutoff line 13
Source documentation
The lower edge used for the residual integer in the comparison lemma.
```
def residualCutoff (x : ℝ) (j : ℕ) : ℝ :=
…
```
lemma OAI.TotientAsymptotic.next_band_below_residual_cutoff line 16
theorem OAI.TotientAsymptotic.basic_residual_smooth line 24
Source documentation
No normality or squarefreeness is needed for residual smoothness.
```
theorem basic_residual_smooth {x : ℝ} {H j : ℕ}
    {η : RemainderDatum (L x H)} (hη : IsBasicRemainder x H η)
    (hL : L x H < m x) (hj : j < L x H) :
    (largestPrimeFactor (suffixPreimage η j).totient : ℝ) < residualCutoff x j := by
…
```
Mentions: OAI.TotientAsymptotic.RemainderDatum, OAI.TotientAsymptotic.L, OAI.TotientAsymptotic.IsBasicRemainder, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.largestPrimeFactor, OAI.TotientAsymptotic.suffixPreimage, OAI.TotientAsymptotic.residualCutoff