VarianceConstants.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem313.variance_decay_constant line 10

Source documentation

A coarse bound sufficient for absorbing the low Fourier levels.

theorem variance_decay_constant {t m : ℝ} (ht : 0 < t) (hm : 0 < m)
    (hlog : t / 3 ≤ Real.log m) :
    4 * m ^ (-(1 : ℝ) / 4) ≤ 1152 / t ^ 2 := by
…

theorem OAI.Problem313.variance_tail_constant line 33

Source documentation

Cancellation of the bias and comparison of logarithms in the Fourier tail.

theorem variance_tail_constant {t m σ : ℝ} (ht : 0 < t)
    (hlog : t / 3 ≤ Real.log m) (hσ : 0 < σ) :
    2 * σ ^ 2 / (σ * Real.log m / 64) ^ 2 ≤ 73728 / t ^ 2 := by
…

theorem OAI.Problem313.variance_constant_bound line 50
Source documentation
A numerical bound for the sum of low-degree and spectral-tail contributions. Only the lower bound on log m is needed; no floor or exponential monotonicity arguments enter this estimate.
```
theorem variance_constant_bound {t m σ : ℝ} (ht : 0 < t) (hm : 0 < m)
    (hlog : t / 3 ≤ Real.log m) (hσ : 0 < σ) :
    4 * m ^ (-(1 : ℝ) / 4) + 2 * σ ^ 2 / (σ * Real.log m / 64) ^ 2 ≤
      (2 : ℝ) ^ 17 / t ^ 2 := by
…
```