OAI/NumberTheory/CubicMoment/Estimates/PrimaryPrimePNTProofLogCount.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Unweight a prime logarithmic mean using a moving power cutoff.

  1. def OAI.CubicFirstMoment.selectedRationalPrimes line 12
  2. def OAI.CubicFirstMoment.selectedRationalTheta line 15
  3. def OAI.CubicFirstMoment.selectedRationalCount line 18
  4. lemma OAI.CubicFirstMoment.selectedRationalTheta_le line 21
  5. lemma OAI.CubicFirstMoment.selectedRationalCount_upper line 32
  6. lemma OAI.CubicFirstMoment.power_log_remainder_tendsto_zero line 83
  7. theorem OAI.CubicFirstMoment.selectedRationalCount_limit line 95

    Source documentation

    A positive logarithmic prime mean gives the ordinary natural-density count.

    theorem selectedRationalCount_limit (P : ℕ → Prop) {c : ℝ} (hc : 0 < c)
    (hθ : Tendsto (fun X => selectedRationalTheta P X / X) atTop (𝓝 c)) :
    Tendsto (fun X => selectedRationalCount P X * Real.log X / X) atTop (𝓝 c) := by
…

    Mentions: OAI.CubicFirstMoment.selectedRationalTheta, OAI.CubicFirstMoment.selectedRationalCount