SmoothCellRate.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform normalization after the two prescribed nongiant deletions

theorem OAI.Ostmann.PublishedProgressionInput.deletedSmoothCell_normalizer_rate line 15

Source documentation

Removing either Page-exceptional prime costs less than half the cell mass. The bound is uniform over the chosen centres and over the deleted set.

theorem PublishedProgressionInput.deletedSmoothCell_normalizer_rate
    (P : PublishedProgressionInput) (C b : ℝ) (hb : 0 < b)
    (φ : ℝ → ℝ) (hφ : ∀ x, 0 ≤ φ x) (hφone : ∀ x, φ x ≤ 1)
    (hout : ∀ x, 1 ≤ |x| → φ x = 0)
    (hcentral : ∀ x, |x| ≤ 1 / 2 → b ≤ φ x) :
    ∀ᶠ L : ℝ in atTop, ∀ (G : ℝ) (E : Finset ℕ),
      2 ≤ G → Real.exp ((39 / 10000 : ℝ) * L) ≤ G - 1 / 2 →
      G ≤ Real.exp (C * L) → E.card ≤ 2 →
      Real.exp (-(C + 1 / 5) * L) ≤
        smoothGiantMass (smoothGiantPrimeRange G \ E) φ G ∧
      smoothGiantLogNormalizer (smoothGiantPrimeRange G \ E) φ G ≤ (C + 1 / 5) * L ∧
      (∑ p : smoothGiantPrimeRange G,
…

Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.smoothGiantMass, OAI.Ostmann.smoothGiantPrimeRange, OAI.Ostmann.smoothGiantLogNormalizer

theorem OAI.Ostmann.PublishedProgressionInput.logCellProfile_deleted_rate line 77

theorem OAI.Ostmann.PublishedProgressionInput.logCellProfile_deleted_atom_rate line 93

Source documentation

All role centres share one threshold. Both the repeated-sample loss and the maximum atom are computed from the actual deleted smooth prior.

theorem PublishedProgressionInput.logCellProfile_deleted_atom_rate
    (P : PublishedProgressionInput) (C : ℝ) :
    ∀ᶠ L : ℝ in atTop, ∀ (G : ℝ) (E : Finset ℕ),
      2 ≤ G → Real.exp ((39 / 10000 : ℝ) * L) ≤ G - 1 / 2 →
      G ≤ Real.exp (C * L) → E.card ≤ 2 →
      (∑ p : smoothGiantPrimeRange G,
        deletedSmoothCellPrior (smoothGiantPrimeRange G) E logCellProfile G p) = 1 ∧
      ∀ p : smoothGiantPrimeRange G,
        (p : ℝ) * deletedSmoothCellPrior (smoothGiantPrimeRange G) E logCellProfile G p ≤
          Real.exp ((C + 1 / 5) * L) ∧
        deletedSmoothCellPrior (smoothGiantPrimeRange G) E logCellProfile G p ≤
          Real.exp ((C + 1 / 5) * L - (G - 1)) := by
…

Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.smoothGiantPrimeRange, OAI.Ostmann.deletedSmoothCellPrior, OAI.Ostmann.logCellProfile