OAI/NumberTheory/TotientAsymptotic/PPTCancelCoordinates.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Cancel matching coordinates after the high-prime lists have been aligned. The first mismatch is retained, so the large-head condition is preserved. The canceled integer prime product is retained for the later reciprocal totient summation.

  1. def OAI.TotientAsymptotic.pptUnequalCoordinates line 19
  2. def OAI.TotientAsymptotic.pptEqualCoordinates line 22
  3. def OAI.TotientAsymptotic.pptCoordinateEmbedding line 25
  4. def OAI.TotientAsymptotic.pptCanceledPrimeProduct line 29
  5. lemma OAI.TotientAsymptotic.ppt_coordinate_embedding_mem line 32
  6. lemma OAI.TotientAsymptotic.ppt_product_coordinate_embedding line 37
  7. lemma OAI.TotientAsymptotic.ppt_shifted_product_coordinate_embedding line 52
  8. lemma OAI.TotientAsymptotic.ppt_canceled_prime_product_totient line 57
  9. lemma OAI.TotientAsymptotic.ppt_canceled_prime_product_split line 70
  10. lemma OAI.TotientAsymptotic.ppt_canceled_prime_product_pos line 77
  11. lemma OAI.TotientAsymptotic.ppt_canceled_totient_split line 81
  12. lemma OAI.TotientAsymptotic.ppt_canceled_comparison_size line 93

    Source documentation

    The same canceled factor which enters the reciprocal mass also supplies the divisor in the published comparison size bound.

    lemma ppt_canceled_comparison_size {k D : ℕ} (p q : Fin k → ℕ) {z : ℝ}
    (hp : ∀ i, (p i).Prime) (hinj : Function.Injective p)
    (hsize : ((D*shiftedProduct p : ℕ) : ℝ) ≤ z) :
    ((D*shiftedProduct (p ∘ pptCoordinateEmbedding p q) : ℕ) : ℝ) ≤
      z/(pptCanceledPrimeProduct p q).totient := by
…

    Mentions: OAI.TotientAsymptotic.D, OAI.TotientAsymptotic.shiftedProduct, OAI.TotientAsymptotic.pptCoordinateEmbedding, OAI.TotientAsymptotic.pptCanceledPrimeProduct

  13. lemma OAI.TotientAsymptotic.ppt_canceled_squarefreeAbove line 110
  14. lemma OAI.TotientAsymptotic.ppt_cancel_matching_coordinates line 118
  15. lemma OAI.TotientAsymptotic.ppt_coordinate_first_survives line 149
  16. lemma OAI.TotientAsymptotic.ppt_surviving_coordinates_unequal line 162
  17. lemma OAI.TotientAsymptotic.ppt_surviving_coordinates_strictAnti line 167