FullOmegaMoment.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The sharp three-halves moment needed for the small-prime-factor excess.

lemma OAI.TotientAsymptotic.omegaIn_all_factors line 10
theorem OAI.TotientAsymptotic.full_omega_moment_bound line 22
Source documentation
The exponent three used in coarse extraction bounds is sharpened to three halves here, as required by the normality exception estimate.
```
theorem full_omega_moment_bound : ∃ C : ℝ, 0<C ∧ ∀ N : ℕ, 2≤N →
    ∀ Q : Finset ℕ, (∀ n ∈ Q,0<n ∧ n≤N) →
      (∑ n ∈ Q,omegaReciprocal n) ≤ C*(Real.log N)^(3/2:ℝ) := by
…
```
Mentions: OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.omegaReciprocal