HeavyOmegaTail.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The excessive-prime-factor exception at the five-log-log threshold.

lemma OAI.TotientAsymptotic.log_fifteen_eighths_lower line 12
lemma OAI.TotientAsymptotic.heavy_factor_tail_weight line 17
theorem OAI.TotientAsymptotic.heavy_factor_tail_count line 32
Source documentation
In particular, the excessive-Omega exception is smaller than N / log(N)^(1+1/6), the largest saving required for the nice-value count.
```
theorem heavy_factor_tail_count : ∃ C : ℝ,0 < C ∧ ∀ N : ℕ,4 ≤ N →
    ∀ Q : Finset ℕ,(∀ n ∈ Q,0 < n ∧ n ≤ N ∧ 5*B N ≤ (n.primeFactorsList.length:ℝ)) →
    (Q.card:ℝ) ≤ C*N*(Real.log N)^(-5/4:ℝ) := by
…
```
Mentions: OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.B