DescentPolynomialLoss.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.DescentDecay.tendsto_linear_mul_exp_neg_quarter line 11
Source documentation
Linear losses are negligible compared to the quarter-power exponential.
```
theorem tendsto_linear_mul_exp_neg_quarter (A B : ℝ) :
    Tendsto (fun S : ℝ => (A * S + B) * Real.exp (-(S ^ (1 / 4 : ℝ))))
      atTop (𝓝 0) := by
…
```
theorem OAI.Problem337.DescentDecay.eventually_linear_le_exp_quarter line 30
Source documentation
A useful pointwise eventual version, with an absolute rather than relative error.
```
theorem eventually_linear_le_exp_quarter (A B : ℝ) :
    ∀ᶠ S : ℝ in atTop, A * S + B ≤ Real.exp (S ^ (1 / 4 : ℝ)) := by
…
```

theorem OAI.Problem337.DescentDecay.eventually_polynomial_loss_absorbed line 40

Source documentation

The polynomial loss from a localized Fourier packet fits the original descent budget.

theorem eventually_polynomial_loss_absorbed (A B r : ℝ)
    (hA : 0 ≤ A) (hB : 0 ≤ B) (hr : 1 ≤ r) :
    ∀ᶠ S : ℝ in atTop,
      1 + (A * S + B) * Real.exp (S ^ (1 / 4 : ℝ) / r) ≤
        Real.exp (2 * S ^ (1 / 4 : ℝ)) := by
…

theorem OAI.Problem337.DescentDecay.eventually_polynomial_loss_absorbed_of_le line 65

Source documentation

Variable polynomial coefficients can be dominated uniformly before absorption.

theorem eventually_polynomial_loss_absorbed_of_le (A B r : ℝ)
    (hA : 0 ≤ A) (hB : 0 ≤ B) (hr : 1 ≤ r) :
    ∀ᶠ S : ℝ in atTop, ∀ P : ℝ, P ≤ A * S + B →
      1 + P * Real.exp (S ^ (1 / 4 : ℝ) / r) ≤
        Real.exp (2 * S ^ (1 / 4 : ℝ)) := by
…