NormalitySize.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Total factor counts and largest-factor locations for normal shifts.

lemma OAI.TotientAsymptotic.interval_count_partition line 12
lemma OAI.TotientAsymptotic.omegaIn_partition line 38
lemma OAI.TotientAsymptotic.normality_total_bound line 45
Source documentation
Ford normality controls the full number of prime occurrences of a shift.
```
lemma normality_total_bound {S : ℝ} {p : ℕ} (hp : IsNormalPrime S p)
    (hS : 1 < S) (hSn : S < (p-1 : ℕ)) (hBS : 0 ≤ B S) :
    (p-1).primeFactorsList.length ≤ 3*B (p-1 : ℕ) := by
…
```
Mentions: OAI.TotientAsymptotic.IsNormalPrime, OAI.TotientAsymptotic.B
lemma OAI.TotientAsymptotic.self_le_largest_pow_length line 62
lemma OAI.TotientAsymptotic.one_lt_largestPrimeFactor line 68
lemma OAI.TotientAsymptotic.largest_factor_doubleLog_lower line 78
Source documentation
A bound for Ω(n) puts the largest prime factor within a logarithmic distance of the double logarithm of n.
```
lemma largest_factor_doubleLog_lower {n : ℕ} {K : ℝ} (hn : 2 ≤ n) (hK : 0 < K)
    (hΩ : (n.primeFactorsList.length : ℝ) ≤ K) :
    B n - Real.log K ≤ B (largestPrimeFactor n) := by
…
```
Mentions: OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.largestPrimeFactor