NormalHeadBand.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The first shifted prime has its largest factor above height 0.9.

lemma OAI.TotientAsymptotic.head_logarithmic_loss line 13
theorem OAI.TotientAsymptotic.normal_head_largest_factor line 28
Source documentation
This handles the largest-prime coordinate, whose band convention is u₀ = B x rather than B p.
```
theorem normal_head_largest_factor : ∀ᶠ x : ℝ in atTop, ∀ S : ℝ, ∀ p : ℕ,
    IsNormalPrime S p → 1 < S → 0 ≤ B S → S ≤ x →
    x^(9/10 : ℝ) ≤ p → (p-1 : ℕ) ≤ x →
    (9/10 : ℝ)*B x ≤ B (largestPrimeFactor (p-1)) := by
…
```
Mentions: OAI.TotientAsymptotic.IsNormalPrime, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.largestPrimeFactor