OAI/NumberTheory/TwoPoint/Bounds/PrimePairCatalog.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The tuple/padding pair catalog injects into its integer product: the two factors have disjoint prime supports. Thus the numerical bin endpoint bounds the whole catalog, without an extra tuple factor.

  1. lemma OAI.TwoPointCorrelations.ProhibitedPrimeFamily.pair_cross_coprime line 14
  2. lemma OAI.TwoPointCorrelations.ProhibitedPrimeFamily.pair_product_injective line 20
  3. lemma OAI.TwoPointCorrelations.ProhibitedPrimeFamily.pairs_card_le line 36
  4. lemma OAI.TwoPointCorrelations.paddingPairEligible_product_upper line 54
  5. lemma OAI.TwoPointCorrelations.actualProhibitedPrimeFamily_pairs_card line 69