OAI/NumberTheory/TwoPoint/Bounds/ActualPrimeFamily.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The prohibited-word data are constructed from the actual prime bands, not assumed. Padding divisors have the requested degree cap, and the finite pair catalog can impose any numerical eligibility condition.

  1. def OAI.TwoPointCorrelations.centeredPrimeBands line 15
  2. def OAI.TwoPointCorrelations.centeredPrimePool line 18
  3. lemma OAI.TwoPointCorrelations.centeredPrimeBands_prime line 21
  4. lemma OAI.TwoPointCorrelations.centeredPrimeBands_disjoint line 25
  5. lemma OAI.TwoPointCorrelations.centeredPrimePool_disjoint_padding line 31
  6. def OAI.TwoPointCorrelations.actualProhibitedPrimeFamily line 40

    Source documentation

    The exclusion set need only contain prime divisors of the fixed shift. It may contain additional fixed primes, such as those dividing the modulus.

    noncomputable def actualProhibitedPrimeFamily (h J M : ℕ) (E : Finset ℕ)
    (A W L : ℝ) (eligible : ℕ → ℕ → Prop)
    (hA : 0 ≤ A) (hW : 0 ≤ W)
    (hE : ∀ p, p.Prime → p ∣ h → p ∈ E) : ProhibitedPrimeFamily h J M where
…

    Mentions: OAI.TwoPointCorrelations.ProhibitedPrimeFamily

  7. lemma OAI.TwoPointCorrelations.actualProhibitedPrimeFamily_pairs line 72
  8. lemma OAI.TwoPointCorrelations.centeredPrimeBand_subset_pool line 80
  9. lemma OAI.TwoPointCorrelations.centeredPrimePool_bounds line 85
  10. lemma OAI.TwoPointCorrelations.paddingPrimeSupply_bounds line 92
  11. lemma OAI.TwoPointCorrelations.actualProhibitedPrimeFamily_residue_bound line 96
  12. lemma OAI.TwoPointCorrelations.centeredPrimePool_lower_nat line 108
  13. lemma OAI.TwoPointCorrelations.shiftPrimeFactors_cover line 114

    Source documentation

    Taking E = h.primeFactors is sufficient for any nonzero fixed shift.

    lemma shiftPrimeFactors_cover {h : ℕ} (hh : h ≠ 0) :
    ∀ p, p.Prime → p ∣ h → p ∈ h.primeFactors :=
…