PrimePriorDecay.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Actual harmonic-prime point masses on the separated scales

theorem OAI.Ostmann.primeSubsetPrior_le_exp line 13

theorem OAI.Ostmann.eventual_primeSubsetPrior_decay line 29

Source documentation

Polynomial exponential cell normalizers are absorbed by the lower prime scale. The bound is uniform over every actual role and every sampled prime.

theorem eventual_primeSubsetPrior_decay (K z α c : ℝ) (d : ℕ)
    (hK : 0 ≤ K) (hz : 0 ≤ z) (hα : 0 < α) (hc : 0 < c) :
    ∀ᶠ L : ℝ in atTop, ∀ (m : ℝ) (P Q : Finset ℕ), 0 ≤ m → m ≤ z * L →
      (∑ q ∈ Q, (q : ℝ)⁻¹)⁻¹ ≤ Real.exp (K * (1 + m) ^ d) →
      (∀ p ∈ P, Real.exp (c * Real.exp (α * L)) ≤ (p : ℝ)) →
      ∀ p : P, primeSubsetPrior P Q p ≤ Real.exp (-(c / 2) * Real.exp (α * L)) := by
…

Mentions: OAI.Ostmann.primeSubsetPrior