PrimePairDecay.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Numerical decay with all range, unit and large-prime support costs

theorem OAI.Ostmann.eventual_ranged_word_pair_decay line 13

theorem OAI.Ostmann.eventual_prime_support_decay line 59

Source documentation

Point-mass and polynomial history losses remain negligible alongside the already proved one-sided character error.

theorem eventual_prime_support_decay (K z α c : ℝ) (d : ℕ)
    (hK : 0 ≤ K) (hz : 0 ≤ z) (hα : 0 < α) (hc : 0 < c) :
    ∀ᶠ L : ℝ in atTop, ∀ (m δ loss atom value : ℝ),
      0 ≤ m → m ≤ z * L → 0 ≤ loss →
      loss ≤ Real.exp (K * (1 + m) ^ d) →
      atom ≤ Real.exp (-c * Real.exp (α * L)) →
      δ ≤ Real.exp (-(c / 4) * Real.exp (α * L)) →
      value ≤ δ + loss * atom → value ≤ Real.exp (-(c / 8) * Real.exp (α * L)) := by
…