HarmonicPriorAtomDecay.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Actual harmonic prime priors have negligible point masses

theorem OAI.Ostmann.eventual_primeSubsetPrior_atom_decay line 12

Source documentation

A lower prime cutoff dominates the harmonic normalization uniformly in all selected cells, even after their permitted finite deletions.

theorem eventual_primeSubsetPrior_atom_decay (H z α c : ℝ)
    (hH : 0 ≤ H) (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 (H * (1 + m)) →
      (∀ q ∈ Q, Real.exp (c * Real.exp (α * L)) ≤ (q : ℝ)) →
      ∀ p : P, primeSubsetPrior P Q p ≤ Real.exp (-(c / 2) * Real.exp (α * L)) := by
…

Mentions: OAI.Ostmann.primeSubsetPrior

theorem OAI.Ostmann.eventual_prime_prior_guard_decay line 37

Source documentation

The extra unit and divisibility guards add a polynomially bounded multiple of the same actual point mass.

theorem eventual_prime_prior_guard_decay (H z α c : ℝ)
    (hH : 0 ≤ H) (hz : 0 ≤ z) (hα : 0 < α) (hc : 0 < c) :
    ∀ᶠ L : ℝ in atTop, ∀ m atom ratio : ℝ,
      0 ≤ m → m ≤ z * L → 0 ≤ atom →
      atom ≤ Real.exp (-c * Real.exp (α * L)) →
      ratio ≤ Real.exp (H * (1 + m)) →
      atom + ratio * atom ≤ Real.exp (-(c / 2) * Real.exp (α * L)) := by
…