ResidualFactorCount.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Prime-factor counts in actual residual totients, including a repeated last prime in the cofactor.

lemma OAI.TotientAsymptotic.omega_count_mul line 14
lemma OAI.TotientAsymptotic.omega_count_prod line 18
lemma OAI.TotientAsymptotic.omega_count_le_log line 30
lemma OAI.TotientAsymptotic.totient_prime_factor_count line 43
lemma OAI.TotientAsymptotic.basic_suffix_factor_count line 58
Source documentation
Only one extra occurrence is paid for possible overlap at the last prime; every other shifted-prime factor is exact.
```
lemma basic_suffix_factor_count {x : ℝ} {H k : ℕ}
    {η : RemainderDatum (L x H)} (hη : IsBasicRemainder x H η)
    (hL : L x H < m x) (hk : k < L x H) :
    ((suffixPreimage η k).totient.primeFactorsList.length : ℝ) ≤
      2*Real.log (η.cofactor : ℝ)+1+
        ∑ j ∈ Finset.Icc (k+1) (L x H), ((remainderPrime η j-1).primeFactorsList.length : ℝ) := by
…
```
Mentions: OAI.TotientAsymptotic.RemainderDatum, OAI.TotientAsymptotic.L, OAI.TotientAsymptotic.IsBasicRemainder, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.suffixPreimage, OAI.TotientAsymptotic.remainderPrime