CoefficientRegularization.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Removing all three coefficient regularity cutoffs from the signed sum

def OAI.JointDickman.regularizedAmplificationArithmeticSum line 12
theorem OAI.JointDickman.amplification_regularization_error line 19

theorem OAI.JointDickman.amplification_coefficient_regularization line 42

Source documentation

The three coefficient regularity restrictions cost the published vanishing error plus the explicit tail, uniformly for bounded site tests.

theorem amplification_coefficient_regularization
    (hFord : PublishedInputs.FordUpperSieveInput)
    (hM : PublishedInputs.PrimeReciprocalMertensInput) :
    ∃ K : ℝ, 0 < K ∧ ∀ L : ℕ, ∀ τ : ℝ, 0 < L → 0 < τ →
      ∃ ε : ℕ → ℝ, (∀ B, 0 ≤ ε B) ∧ Tendsto ε atTop (𝓝 0) ∧
        ∀ᶠ B : ℕ in atTop, ∀ T : ℝ, 1 ≤ T → Real.log T ≤ (B : ℝ)/10 →
          ∀ (C : ℝ) (j U V : ℕ), 0 ≤ C → j ≠ 0 →
          (∀ k ∈ dyadicBoxIndices (dyadicBoxLower B T) (dyadicBoxUpper B T),
            ⌊(17/4 : ℝ)*Real.exp ((k : ℝ)*Real.log 2)⌋₊ ≤ U) →
          (∀ k ∈ dyadicBoxIndices (dyadicBoxLower B T) (dyadicBoxUpper B T),
            ⌊(17/4 : ℝ)*(Real.exp ((k : ℝ)*Real.log 2)/T)⌋₊ ≤ V) →
          ∀ g h : (auxiliaryPrimes B → Bool) → ℝ,
…

Mentions: OAI.JointDickman.PublishedInputs.FordUpperSieveInput, OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.dyadicBoxIndices, OAI.JointDickman.dyadicBoxLower, OAI.JointDickman.dyadicBoxUpper, OAI.JointDickman.auxiliaryPrimes