PrimeIndicatorErrors.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Stable prime-count estimates for the conditional indicator parameters

theorem OAI.JointDickman.restricted_indicator_mean_error line 13

Source documentation

Absolute errors in the inclusion probabilities control every restricted mean.

theorem restricted_indicator_mean_error (P Q : Finset ℕ) (q : ℕ → ℝ) {D : ℝ}
    (hD : (∑ p ∈ P, |q p - (1 / 2 : ℝ) / p|) ≤ D) :
    |(∑ p ∈ P ∩ Q, q p) - (1 / 2 : ℝ) * (∑ p ∈ P ∩ Q, 1 / (p : ℝ))| ≤ D := by
…

theorem OAI.JointDickman.exponential_mean_error line 31

Source documentation

A bounded total parameter error changes either signed exponential factor by at most exp D, uniformly for exp s <= 2.

theorem exponential_mean_error {m M s r D : ℝ} (_hD : 0 ≤ D)
    (hmean : |m - M / 2| ≤ D) (hs : Real.exp s ≤ 2) :
    Real.exp (-s * r + (Real.exp s - 1) * m) ≤
      Real.exp D * Real.exp (-s * r + ((Real.exp s - 1) / 2) * M) := by
…

theorem OAI.JointDickman.full_cutoff_prime_mass line 46
Source documentation
At the full cutoff the sieve mass is just the actual prime reciprocal mass, so the same Chernoff factors bound the indicator probabilities.
```
theorem full_cutoff_prime_mass (B : ℕ) (Q : Finset ℕ)
    (hP : 6 ≤ auxiliaryCutoff B) :
    tiltPrimeReciprocalMass (auxiliaryCutoff B) (sieveCutoff 4 B) Q =
      ∑ p ∈ auxiliaryPrimes B ∩ Q, 1 / (p : ℝ) := by
…
```
Mentions: OAI.JointDickman.auxiliaryCutoff, OAI.JointDickman.tiltPrimeReciprocalMass, OAI.JointDickman.sieveCutoff, OAI.JointDickman.auxiliaryPrimes
theorem OAI.JointDickman.bernoulli_count_tail_stable line 65