OAI/NumberTheory/JointDickman/Counting/CoefficientProbabilityLoss.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.coefficientPairFailureMass line 14
2. theorem OAI.JointDickman.auxiliaryHalfMass_nonneg line 20
3. theorem OAI.JointDickman.coefficientPairFailureMass_nonneg line 35
4. theorem OAI.JointDickman.coefficientPairFailureMass_le line 42
5. theorem OAI.JointDickman.coefficient_pair_loss_nonneg line 73
6. theorem OAI.JointDickman.coefficient_failure_box_bound line 82

   Source documentation

   The probability loss in one size-and-ratio box is O(B⁻²), with the same vanishing and tail-cutoff errors as the arithmetic regularity bound.

   theorem coefficient_failure_box_bound
       (hFord : PublishedInputs.FordUpperSieveInput)
       (hM : PublishedInputs.PrimeReciprocalMertensInput)
       {δ : ℝ} (hδ : 0 < δ) (hδ32 : δ ≤ 32) :
       ∃ K : ℝ, 0 < K ∧ ∀ (L : ℕ) (τ : ℝ), 0 < L → 0 < τ →
         ∃ ε : ℕ → ℝ, (∀ B, 0 ≤ ε B) ∧ Tendsto ε atTop (𝓝 0) ∧
           ∀ᶠ B : ℕ in atTop, ∀ (C : ℝ) (T X : ℕ), 0 ≤ C → 0 < T →
             Real.exp (δ * B) ≤ X →
             (4 * T * X : ℝ) ≤ Real.exp ((16 / 5 : ℝ) * B) →
             (∑ a ∈ Ico (T * X) (4 * T * X), ∑ c ∈ Ico X (2 * X),
               coefficientPairFailureMass B L τ C a c) ≤
               K / (B : ℝ)^2 * (ε B + Real.exp (-(1 / 10 : ℝ) * C)) := by
   …

   Mentions: OAI.JointDickman.PublishedInputs.FordUpperSieveInput, OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.coefficientPairFailureMass