SmoothGiantMassEstimate.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The smooth giant normalizer from the published progression estimate

theorem OAI.Ostmann.central_harmonic_interval_lower line 12
theorem OAI.Ostmann.PublishedProgressionInput.smoothGiantMass_lower line 27
Source documentation
A fixed positive part of the bump supplies a genuine lower bound for its original prime mass; the only analytic input is the published progression estimate at modulus one.
```
theorem PublishedProgressionInput.smoothGiantMass_lower
    (P : PublishedProgressionInput) (φ : ℝ → ℝ) (G b : ℝ)
    (hG : 2 ≤ G) (hb : 0 < b) (hφ : ∀ x, 0 ≤ φ x)
    (hcentral : ∀ x, |x| ≤ 1 / 2 → b ≤ φ x)
    (herr : bulkPrimeErrorFactor P 2 (G - 1 / 2) ≤ (4 * G)⁻¹) :
    b / (4 * G) ≤ smoothGiantMass (smoothGiantPrimeRange G) φ G := by
…
```
Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.bulkPrimeErrorFactor, OAI.Ostmann.smoothGiantMass, OAI.Ostmann.smoothGiantPrimeRange

theorem OAI.Ostmann.PublishedProgressionInput.smoothGiant_normalizer_rate line 68

Source documentation

The loss of every admissible giant shell is linear in L, uniformly in its center. This derives both positivity and normalization from the published progression estimate, rather than assuming a prime in the shell.

theorem PublishedProgressionInput.smoothGiant_normalizer_rate
    (P : PublishedProgressionInput) (C b : ℝ) (hb : 0 < b)
    (φ : ℝ → ℝ) (hφ : ∀ x, 0 ≤ φ x)
    (hcentral : ∀ x, |x| ≤ 1 / 2 → b ≤ φ x) :
    ∀ᶠ L : ℝ in atTop, ∀ G : ℝ,
      2 ≤ G → Real.exp ((39 / 10000 : ℝ) * L) ≤ G - 1 / 2 →
      G ≤ Real.exp (C * L) →
      Real.exp (-(C + 1 / 10) * L) ≤ smoothGiantMass (smoothGiantPrimeRange G) φ G ∧
      smoothGiantLogNormalizer (smoothGiantPrimeRange G) φ G ≤ (C + 1 / 10) * L ∧
      (∑ p : smoothGiantPrimeRange G, smoothGiantPrior (smoothGiantPrimeRange G) φ G p) = 1 := by
…

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