SmoothGiantLossBudget.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The actual giant normalization fits the iteration reserve

theorem OAI.Ostmann.PublishedProgressionInput.smoothGiant_iteration_budget line 15

Source documentation

Taking the positive part only enlarges the transfer loss. For every center in the paper's range, the sum of these actual losses fits the even bulk count, including the factor two reserved at each step.

theorem PublishedProgressionInput.smoothGiant_iteration_budget
    (P : PublishedProgressionInput) (k : ℕ) (hk : 2 ≤ k) :
    ∀ᶠ L : ℝ in atTop, ∀ G : ℕ → ℝ,
      (∀ j < k, 2 ≤ G j) →
      (∀ j < k, Real.exp ((39 / 10000 : ℝ) * L) ≤ G j - 1 / 2) →
      (∀ j < k, G j ≤ Real.exp ((9 / 10 : ℝ) * L)) →
      ∑ j ∈ Finset.range k,
        (max 0 (smoothGiantLogNormalizer (smoothGiantPrimeRange (G j)) logCellProfile (G j)) +
          Real.log 2) ≤ (spectatorBulkCount k L : ℝ) := by
…

Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.smoothGiantLogNormalizer, OAI.Ostmann.smoothGiantPrimeRange, OAI.Ostmann.logCellProfile, OAI.Ostmann.spectatorBulkCount