SmoothLogCellProfile.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

A fixed smooth partition profile for the original logarithmic cells

def OAI.Ostmann.logCellProfile line 13
def OAI.Ostmann.logCellCentralLower line 16
theorem OAI.Ostmann.logCellCentralLower_pos line 19
theorem OAI.Ostmann.logCellProfile_nonneg line 23
theorem OAI.Ostmann.logCellProfile_le_one line 26
theorem OAI.Ostmann.logCellProfile_zero_outside line 30
theorem OAI.Ostmann.logCellProfile_central line 40
theorem OAI.Ostmann.logCellProfile_contDiff line 51
theorem OAI.Ostmann.logCellProfile_partition line 56
Source documentation
The two nonzero translates telescope to one on a unit logarithmic cell.
```
theorem logCellProfile_partition (x : ℝ) (hlo : 0 ≤ x) (hhi : x ≤ 1) :
    logCellProfile x + logCellProfile (x - 1) = 1 := by
…
```
Mentions: OAI.Ostmann.logCellProfile
theorem OAI.Ostmann.logCellProfile_partition_unity line 65
Source documentation
The full integer partition of unity specified for the logarithmic cells. Only the two translates adjacent to floor x can be nonzero.
```
theorem logCellProfile_partition_unity (x : ℝ) :
    (∑' n : ℤ, logCellProfile (x - n)) = 1 := by
…
```
Mentions: OAI.Ostmann.logCellProfile
theorem OAI.Ostmann.logCellProfile_compactSupport line 89
theorem OAI.Ostmann.logCellProfile_lipschitz line 98
Source documentation
One fixed finite Lipschitz constant supplies every later variation bound.
```
theorem logCellProfile_lipschitz : ∃ D : ℝ, 0 ≤ D ∧
    ∀ x y, |logCellProfile x - logCellProfile y| ≤ D * |x - y| := by
…
```
Mentions: OAI.Ostmann.logCellProfile

theorem OAI.Ostmann.PublishedProgressionInput.logCellProfile_normalizer_rate line 109

Source documentation

The fixed profile discharges the remaining bump premises in the smooth giant normalizer estimate.

theorem PublishedProgressionInput.logCellProfile_normalizer_rate
    (P : PublishedProgressionInput) (C : ℝ) :
    ∀ᶠ 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) logCellProfile G ∧
      smoothGiantLogNormalizer (smoothGiantPrimeRange G) logCellProfile G ≤ (C + 1 / 10) * L ∧
      (∑ p : smoothGiantPrimeRange G,
        smoothGiantPrior (smoothGiantPrimeRange G) logCellProfile G p) = 1 :=
…

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