PPTPreimageTerminal.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Match the chosen terminal prefix to the actual high-prime preimage list.

theorem OAI.TotientAsymptotic.ppt_preimage_terminal_prefix line 14

Source documentation

The unequal-list normality estimate gives every needed right index above the middle cutoff, while the right tail is smooth below it. The right list and first mismatch come from the actual preimage.

theorem ppt_preimage_terminal_prefix {k J d F : ℕ}
    (p : Fin k → ℕ) (hJ : 0 < J) (hJk : J ≤ k)
    {S U V T z ε ε' : ℝ}
    (hd : 0 < d) (hF : 0 < F)
    (hS : 2 ≤ S) (hBS : 0 ≤ B S)
    (hSU : S ≤ U) (hUV : U < V) (hVT : V < T)
    (hp : ∀ i, IsNormalPrime S (p i)) (hpa : StrictAnti p)
    (hvalue : F.totient = d*(∏ i, p i).totient)
    (hDS : (largestPrimeFactor d : ℝ) ≤ S)
    (hsq : SquarefreeAbove F S)
    (hnormal : ∀ q : ℕ, q.Prime → q ∣ F → IsNormalPrime S q)
    (hmismatch : largestPrimeFactor F ≠ p ⟨0,by omega⟩)
…

Mentions: OAI.TotientAsymptotic.V, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.IsNormalPrime, OAI.TotientAsymptotic.largestPrimeFactor, OAI.TotientAsymptotic.SquarefreeAbove