OAI/NumberTheory/TotientAsymptotic/PPTPrefixEquation.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Truncate the two actual prime lists to the same high-prefix length. The left residual multiplier is exactly the seed times the totient of the removed prime tail; the right multiplier is the smooth factor already estimated in PPTTailAlignment.

  1. def OAI.TotientAsymptotic.pptPrimePrefix line 19
  2. def OAI.TotientAsymptotic.pptPrimeTailProduct line 22
  3. lemma OAI.TotientAsymptotic.ppt_prefix_product line 25
  4. lemma OAI.TotientAsymptotic.ppt_prime_prefix_tail_split line 39
  5. lemma OAI.TotientAsymptotic.ppt_shifted_prefix_tail_split line 49
  6. lemma OAI.TotientAsymptotic.ppt_prime_tail_totient line 55
  7. theorem OAI.TotientAsymptotic.ppt_equal_prefix_equation line 71

    Source documentation

    The fixed left tail enters the scalar D, exactly as required by the available l=0 specialization of Ford's comparison lemma.

    theorem ppt_equal_prefix_equation {k l J d E : ℕ}
    (p : Fin k → ℕ) (q : Fin l → ℕ) (hJp : J ≤ k) (hJq : J ≤ l)
    (hp : ∀ i, (p i).Prime) (hinj : Function.Injective p)
    (heq : d*shiftedProduct p = E*shiftedProduct q) :
    (d*(pptPrimeTailProduct p J).totient)*shiftedProduct (pptPrimePrefix p hJp) =
      pptRightLowFactor q E J*shiftedProduct (pptPrimePrefix q hJq) := by
…

    Mentions: OAI.TotientAsymptotic.shiftedProduct, OAI.TotientAsymptotic.pptPrimeTailProduct, OAI.TotientAsymptotic.pptPrimePrefix, OAI.TotientAsymptotic.pptRightLowFactor

  8. lemma OAI.TotientAsymptotic.ppt_prime_prefix_strictAnti line 87
  9. lemma OAI.TotientAsymptotic.ppt_prime_prefix_first line 92