OAI/NumberTheory/TwoPoint/Bounds/PositivePrimeTilt.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Tilting the prime divisibility law by the positive majorant of one tuple of centered prime factors. Selected primes have parameter (1 + q)/2; every other prime keeps its original parameter.

  1. def OAI.TwoPointCorrelations.positiveCenterWeight line 17
  2. def OAI.TwoPointCorrelations.positiveCenterNormalizer line 21
  3. def OAI.TwoPointCorrelations.positiveCenterParameter line 24
  4. lemma OAI.TwoPointCorrelations.positiveCenterParameter_nonneg line 28
  5. lemma OAI.TwoPointCorrelations.positiveCenterParameter_le_one line 36
  6. def OAI.TwoPointCorrelations.positiveCenterLaw line 43
  7. lemma OAI.TwoPointCorrelations.positiveCenterWeight_eq line 48
  8. lemma OAI.TwoPointCorrelations.positiveCenterNormalizer_eq line 52
  9. lemma OAI.TwoPointCorrelations.positiveCenterNormalizer_nonneg line 56
  10. lemma OAI.TwoPointCorrelations.positive_center_tilt_weight line 65
  11. lemma OAI.TwoPointCorrelations.positive_center_tilt_average line 77
  12. lemma OAI.TwoPointCorrelations.positive_center_tilt_total line 88
  13. lemma OAI.TwoPointCorrelations.positiveCenterParameter_sum_le line 95
  14. theorem OAI.TwoPointCorrelations.positive_center_degree_tail line 112

    Source documentation

    The selected primes may be bounded simply by their number. The remaining Bernoulli mean is at most the original total reciprocal mass.

    theorem positive_center_degree_tail (q : ι → ℝ) (S : Finset ι)
    (hq0 : ∀ i, 0 ≤ q i) (hq1 : ∀ i, q i ≤ 1)
    (W : ℝ) (hW : 10 ≤ W) (hmass : (∑ i, q i) ≤ 2 * W * S.card) :
    (positiveCenterLaw q S hq0 hq1).probability
      (fun a => 6 * W * S.card < booleanCount a) ≤ Real.exp (-2 * W * S.card) := by
…

    Mentions: OAI.TwoPointCorrelations.positiveCenterLaw, OAI.TwoPointCorrelations.booleanCount

  15. theorem OAI.TwoPointCorrelations.positive_center_weighted_degree_tail line 134