PPTTailAlignment.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The right-tail smoothness argument following Ford (5.35). If the left tail is smooth, an additional right prime with a large predecessor factor would force too many normal shifts across the intervening interval.

theorem OAI.TotientAsymptotic.ppt_right_tail_smooth line 16
def OAI.TotientAsymptotic.pptRightLowFactor line 55

lemma OAI.TotientAsymptotic.ppt_right_low_factor_smooth line 60

Source documentation

The actual remaining shifted product, not an additional smoothness hypothesis for an unrelated integer.

lemma ppt_right_low_factor_smooth {l E J : ℕ} (q : Fin l → ℕ) {V : ℝ}
    (hV : 1 ≤ V) (hE : (largestPrimeFactor E : ℝ) ≤ V)
    (htail : ∀ i : Fin l, J ≤ i.val → (largestPrimeFactor (q i-1) : ℝ) ≤ V) :
    (largestPrimeFactor (pptRightLowFactor q E J) : ℝ) ≤ V := by
…

Mentions: OAI.TotientAsymptotic.V, OAI.TotientAsymptotic.largestPrimeFactor, OAI.TotientAsymptotic.pptRightLowFactor

lemma OAI.TotientAsymptotic.ppt_right_low_factor_equation line 73
Source documentation
Splitting the right list at J preserves the exact shifted-product equation with pptRightLowFactor as its residual multiplier.
```
lemma ppt_right_low_factor_equation {k l D E J : ℕ}
    (p : Fin k → ℕ) (q : Fin l → ℕ)
    (heq : D*shiftedProduct p = E*shiftedProduct q) :
    D*shiftedProduct p = pptRightLowFactor q E J *
      ∏ i ∈ Finset.univ.filter (fun i : Fin l => i.val < J), (q i-1) := by
…
```
Mentions: OAI.TotientAsymptotic.D, OAI.TotientAsymptotic.shiftedProduct, OAI.TotientAsymptotic.pptRightLowFactor