OAI/NumberTheory/JointDickman/Arithmetic/PrimeIndicatorRegularity.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.bernoulli_prefix_violation_sum line 12
2. theorem OAI.JointDickman.bernoulli_tail_violation_sum line 31
3. def OAI.JointDickman.primeRegularityFailureProbability line 45
4. theorem OAI.JointDickman.bernoulli_regularity_failure_bound line 49
5. theorem OAI.JointDickman.independent_prime_regularity_loss line 77

   Source documentation

   The probability version of manuscript (9), uniform over all proper independent parameters with bounded total deviation from 1/(2p).

   theorem independent_prime_regularity_loss
       (hM : PublishedInputs.PrimeReciprocalMertensInput) {D : ℝ} (hD : 0 ≤ D) :
       ∃ K : ℝ, 0 < K ∧ ∀ (L : ℕ) (τ : ℝ), 0 < L → 0 < τ →
         ∃ ε : ℕ → ℝ, (∀ B, 0 ≤ ε B) ∧ Tendsto ε atTop (𝓝 0) ∧
           ∀ᶠ B : ℕ in atTop, ∀ (q : ℕ → ℝ) (C : ℝ), 0 ≤ C →
             (∀ p ∈ auxiliaryPrimes B, 0 ≤ q p ∧ q p ≤ 1) →
             (∑ p ∈ auxiliaryPrimes B, |q p - (1 / 2 : ℝ) / p|) ≤ D →
             primeRegularityFailureProbability B L τ C q ≤
               K * (ε B + Real.exp (-(1 / 10 : ℝ) * C)) := by
   …

   Mentions: OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.primeRegularityFailureProbability