SuffixSize.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Deterministic size estimates for the complete remainder of a basic witness.

lemma OAI.TotientAsymptotic.basic_prime_log_le line 13
lemma OAI.TotientAsymptotic.log_suffixPreimage line 23
theorem OAI.TotientAsymptotic.basic_suffix_log_bound line 38
Source documentation
All factors after a cutoff are bounded by the first band after it. This keeps the cofactor separate and permits repetitions of the last prime.
```
theorem basic_suffix_log_bound {x : ℝ} {H j : ℕ}
    {η : RemainderDatum (L x H)} (hη : IsBasicRemainder x H η) :
    Real.log (suffixPreimage η j : ℝ) ≤
      (L x H-j : ℕ)*Real.exp ((11/10 : ℝ)*bandScale x (j+1))+
        Real.exp (2*bandScale x (L x H)) := by
…
```
Mentions: OAI.TotientAsymptotic.RemainderDatum, OAI.TotientAsymptotic.L, OAI.TotientAsymptotic.IsBasicRemainder, OAI.TotientAsymptotic.suffixPreimage, OAI.TotientAsymptotic.bandScale
lemma OAI.TotientAsymptotic.m_le_log_B line 58
theorem OAI.TotientAsymptotic.basic_remainder_log_small line 70
Source documentation
The total logarithmic size of a basic remainder is uniformly smaller than the largest-prime scale.
```
theorem basic_remainder_log_small (H : ℕ) :
    ∀ᶠ x : ℝ in atTop, ∀ η : RemainderDatum (L x H), IsBasicRemainder x H η →
      Real.log (suffixPreimage η 0 : ℝ) ≤ (Real.log x)^(4/5 : ℝ) := by
…
```
Mentions: OAI.TotientAsymptotic.RemainderDatum, OAI.TotientAsymptotic.L, OAI.TotientAsymptotic.IsBasicRemainder, OAI.TotientAsymptotic.suffixPreimage