PPTPreimageEquation.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The unequal-list normality argument applied to an actual chosen preimage. Its smooth factor is the totient of the low part of that preimage. The equation here is derived from the given totient identity, rather than imposed as an additional comparison hypothesis.

theorem OAI.TotientAsymptotic.ppt_actual_preimage_equation line 19

theorem OAI.TotientAsymptotic.ppt_actual_preimage_right_index line 40

Source documentation

A sufficiently high actual left coordinate forces the corresponding right prime to exist. No equality of the total list lengths is needed.

theorem ppt_actual_preimage_right_index {k d n : ℕ} (p : Fin k → ℕ)
    (j : Fin k) {S T ε : ℝ} (hd : 0 < d) (hn : 0 < n)
    (hS : 1 < S) (hBS : 0 ≤ B S)
    (hp : ∀ i, IsNormalPrime S (p i)) (hpa : StrictAnti p)
    (hvalue : n.totient = d*(∏ i, p i).totient)
    (hDS : (largestPrimeFactor d : ℝ) ≤ S)
    (hsq : SquarefreeAbove n S)
    (hnormal : ∀ r : ℕ, r.Prime → r ∣ n → IsNormalPrime S r)
    (hST : S < T) (hTp : T ≤ (p j-1 : ℕ))
    (hε : Real.sqrt (B S*B T) ≤ ε)
    (hgap : (2*(j.val : ℝ)+1)*ε < B T-B S) :
    ∃ (l : ℕ) (q : Fin l → ℕ) (E : ℕ),
…

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