WeightedPrimeNormalization.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Normalizing the cutoff-weighted prime prior

A fixed positive lower bound for the cutoff on an interior unit log interval gives the required linear normalization cost.

theorem OAI.Ostmann.weighted_prime_interval_lower line 17

theorem OAI.Ostmann.PublishedProgressionInput.weighted_normalization_bound line 54

Source documentation

This applies to a smooth cutoff supported on a two-unit log interval and bounded below on its central unit interval. All endpoints and weights may depend on the log center.

theorem PublishedProgressionInput.weighted_normalization_bound (P : PublishedProgressionInput) :
    ∀ᶠ u : ℝ in atTop, ∀ (s t : ℝ) (w : ℝ → ℝ) (b : ℝ),
      s ≤ u → u + 1 ≤ t → 0 < b →
      (∀ y ∈ Set.Ioc s t, 0 ≤ w y) →
      (∀ y ∈ Set.Ioc u (u + 1), b ≤ w y) →
      0 < weightedReciprocalPrimeInterval 1 0 s t w ∧
        (weightedReciprocalPrimeInterval 1 0 s t w)⁻¹ ≤ 2 * (u + 1) / b := by
…

Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.weightedReciprocalPrimeInterval