OAI/NumberTheory/TwoPoint/Bounds/PrimeTupleMass.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The centered divisor family is the actual image of one prime choice from each disjoint band. Its harmonic mass has no representation multiplicity and is exactly the product of the band masses.

  1. def OAI.TwoPointCorrelations.primeTupleDivisors line 16
  2. lemma OAI.TwoPointCorrelations.primeTupleDivisors_mass line 19
  3. lemma OAI.TwoPointCorrelations.centeredPrimeTuple_log_bound line 39
  4. lemma OAI.TwoPointCorrelations.centeredPrimeTuple_mass line 49
  5. lemma OAI.TwoPointCorrelations.primeTupleDivisors_mass_bounds line 61
  6. theorem OAI.TwoPointCorrelations.ModFiveThetaInput.eventually_primeTuple_bin_mass line 81

    Source documentation

    q:bin-mass for the actual prime families and the manuscript's scale choice. The assertion is uniform over the positive bin width.

    theorem ModFiveThetaInput.eventually_primeTuple_bin_mass (hP : ModFiveThetaInput)
    (E : Finset ℕ) (W : ℝ) (hW : 1 ≤ W) :
    ∀ᶠ L : ℝ in atTop, ∀ η : ℝ, 0 < η →
      let J := primeSupplyCount W L
…

    Mentions: OAI.TwoPointCorrelations.ModFiveThetaInput, OAI.TwoPointCorrelations.primeSupplyCount