OAI/NumberTheory/TwoPoint/Bounds/PrimeDegreeTail.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The prime-degree deletion under the literal full residue law. The positive tuple majorant has mean 2^omega(d)/d, and its tilted degree tail is exponentially small in W * omega(d).

  1. def OAI.TwoPointCorrelations.primeSelection line 16
  2. lemma OAI.TwoPointCorrelations.primeSelection_card line 19
  3. def OAI.TwoPointCorrelations.positivePrimeWeight line 26
  4. def OAI.TwoPointCorrelations.positivePrimeNormalizer line 29
  5. lemma OAI.TwoPointCorrelations.positivePrimeWeight_nonneg line 32
  6. lemma OAI.TwoPointCorrelations.abs_centeredTuple_le_positivePrimeWeight line 38
  7. lemma OAI.TwoPointCorrelations.positivePrimeWeight_eq_selection line 49
  8. lemma OAI.TwoPointCorrelations.positivePrimeNormalizer_eq_selection line 62
  9. lemma OAI.TwoPointCorrelations.positivePrimeNormalizer_squarefree line 73
  10. lemma OAI.TwoPointCorrelations.actualPrimeDegree_eq_count line 80
  11. lemma OAI.TwoPointCorrelations.ProhibitedPrimeFamily.residue_average_prime_availability line 92

    Source documentation

    Every prime coordinate retains its Bernoulli divisibility law under the full tuple-and-padding law, also at a translated CRT origin.

    lemma residue_average_prime_availability
    (hB : ∀ p ∈ data.P ∪ data.Q, p ≤ B) (site : ℤ)
    (F : (data.P → Bool) → ℝ) :
    (data.residueLaw B hB).average (fun x =>
      F (fun p : data.P => decide ((p.val : ℤ) ∣ data.residueOrigin x + site))) =
      (paddingOriginalLaw data.P (fun p hp => (data.primeP p hp).two_le)).average F := by
…

    Mentions: OAI.TwoPointCorrelations.paddingOriginalLaw

  12. lemma OAI.TwoPointCorrelations.ProhibitedPrimeFamily.positive_prime_mean line 123
  13. theorem OAI.TwoPointCorrelations.ProhibitedPrimeFamily.positive_prime_degree_tail line 141

    Source documentation

    The positive centered-prime majorant, with a prime-degree failure, is bounded by its exact mean times exp(-2W * #S).

    theorem positive_prime_degree_tail (hB : ∀ p ∈ data.P ∪ data.Q, p ≤ B)
    (S : Finset ℕ) (hSP : S ⊆ data.P) (W : ℝ) (hW : 10 ≤ W)
    (hmass : (∑ p ∈ data.P, 1 / (p : ℝ)) ≤ 2 * W * S.card) (site : ℤ) :
    (data.residueLaw B hB).average (fun x =>
      positivePrimeWeight S (data.residueOrigin x + site) *
        if 6 * W * S.card < (actualPaddingDegree data.P (data.residueOrigin x + site) : ℝ)
          then 1 else 0) ≤
      positivePrimeNormalizer S * Real.exp (-2 * W * S.card) := by
…

    Mentions: OAI.TwoPointCorrelations.positivePrimeWeight, OAI.TwoPointCorrelations.actualPaddingDegree, OAI.TwoPointCorrelations.positivePrimeNormalizer

  14. theorem OAI.TwoPointCorrelations.ProhibitedPrimeFamily.positive_tuple_degree_tail line 177