CoefficientCutoffRemoval.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Removing coefficient regularity in the normalized amplification mass

theorem OAI.JointDickman.coefficient_cutoff_removal line 14

Source documentation

The actual coefficient-support probability of a failed regularity cutoff, including the outside B normalization in manuscript (13).

theorem coefficient_cutoff_removal
    (hFord : PublishedInputs.FordUpperSieveInput)
    (hM : PublishedInputs.PrimeReciprocalMertensInput) :
    ∃ K : ℝ, 0 < K ∧ ∀ (L : ℕ) (τ : ℝ), 0 < L → 0 < τ →
      ∃ ε : ℕ → ℝ, (∀ B, 0 ≤ ε B) ∧ Tendsto ε atTop (𝓝 0) ∧
        ∀ᶠ B : ℕ in atTop, ∀ (C : ℝ) (T : ℕ), 0 ≤ C → 0 < T →
          (T : ℝ) ≤ Real.exp ((1 / 10 : ℝ) * B) →
          (B : ℝ) * (∑ ac ∈ amplificationCoefficientPairs B T,
            coefficientPairFailureMass B L τ C ac.1 ac.2) ≤
            K * (ε B + Real.exp (-(1 / 10 : ℝ) * C)) := by
…

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