SmoothSuffix.lean`

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Smoothness of the residual totient in an actual basic collision witness.

lemma OAI.TotientAsymptotic.largestPrimeFactor_le_of_prime_divisors line 12
lemma OAI.TotientAsymptotic.prime_dvd_le_largest line 20
lemma OAI.TotientAsymptotic.largestPrimeFactor_totient_le line 26
Source documentation
Taking a totient cannot introduce a prime larger than every prime of its argument. This also covers n = 0 under the existing largest-factor convention.
```
lemma largestPrimeFactor_totient_le (n : ℕ) :
    largestPrimeFactor n.totient ≤ largestPrimeFactor n := by
…
```
Mentions: OAI.TotientAsymptotic.largestPrimeFactor
lemma OAI.TotientAsymptotic.largestPrimeFactor_mul_le line 44
lemma OAI.TotientAsymptotic.largestPrimeFactor_prod_le line 53
lemma OAI.TotientAsymptotic.largestPrimeFactor_prime line 64
theorem OAI.TotientAsymptotic.basic_suffix_totient_smooth line 69
Source documentation
The actual residual integer after a cutoff is smooth below the next prime. The final cofactor may repeat the last displayed prime.
```
theorem basic_suffix_totient_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 ≤ remainderPrime η (j+1) := by
…
```
Mentions: OAI.TotientAsymptotic.RemainderDatum, OAI.TotientAsymptotic.L, OAI.TotientAsymptotic.IsBasicRemainder, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.largestPrimeFactor, OAI.TotientAsymptotic.suffixPreimage, OAI.TotientAsymptotic.remainderPrime