OAI/NumberTheory/JointDickman/Analysis/MellinSieveBudget.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.JointDickman.prime_survival_eventually_le line 11
2. lemma OAI.JointDickman.logarithmic_power_decay line 23
3. def OAI.JointDickman.mellinSparseBudget line 30
4. lemma OAI.JointDickman.mellinSparseBudget_tendsto line 33
5. lemma OAI.JointDickman.mellin_dyadic_count_le line 48
6. lemma OAI.JointDickman.mellin_sieve_remainder_ratio line 67
7. theorem OAI.JointDickman.mellin_sieve_remainder_absorption line 120

   Source documentation

   The complete remainder is smaller than the prime-density scale for sufficiently sparse samples and a correspondingly small sieve level.

   theorem mellin_sieve_remainder_absorption (A : ℝ) (hA : 0 ≤ A)
       {δ κ : ℝ} (hδ : 0 < δ) (hκ : κ ≤ 1/8) (hκδ : κ ≤ δ) :
       ∀ᶠ q : ℝ in atTop, ∀ N z s j : ℝ,
         q^10 ≤ N → N ≤ q^11 →
         0 ≤ z → z ≤ 2*q^κ → 0 ≤ s → s ≤ q^κ →
         0 ≤ j → j ≤ 8*Real.log q →
         z*(6*q^9+j*A*N^(1-δ))*s ≤ N/Real.log N := by
   …