ExpQuadratic.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.Problem313.quadratic_mul_exp_neg_eighth_le line 10
Source documentation
A deliberately generous quadratic-exponential estimate.
```
lemma quadratic_mul_exp_neg_eighth_le (t : ℝ) (ht : 0 ≤ t) :
    t ^ 2 * Real.exp (-t / 8) ≤ 256 := by
…
```

lemma OAI.Problem313.block_exponential_remainder_le line 32

Source documentation

The exponentially small term in the block argument, with ample constant slack.

lemma block_exponential_remainder_le (t ell : ℝ) (ht : 0 ≤ t)
    (hell : t / 2 - Real.log 2 ≤ ell) :
    (4 * Real.exp (-ell / 4)) * t ^ 2 ≤ 2048 := by
…

lemma OAI.Problem313.block_exponential_remainder_le_of_third line 48
Source documentation
A form requiring only the logarithmic lower bound used for the spectral tail.
```
lemma block_exponential_remainder_le_of_third (t ell : ℝ) (ht : 0 ≤ t)
    (hell : t / 3 ≤ ell) :
    (4 * Real.exp (-ell / 4)) * t ^ 2 ≤ 2304 := by
…
```

lemma OAI.Problem313.block_rpow_remainder_le line 60

Source documentation

The fractional-power form of the block remainder estimate.

lemma block_rpow_remainder_le (t m : ℝ) (ht : 0 ≤ t) (hm : 0 < m)
    (hm_log : t / 3 ≤ Real.log m) :
    (4 * m ^ (-1 / 4 : ℝ)) * t ^ 2 ≤ 2304 := by
…