DescentDepth.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.log_one_sub_reciprocal_lower line 8
Source documentation
A logarithmic estimate uniform over the moment orders used in the exceptional-set descent.
```
theorem log_one_sub_reciprocal_lower (r : ℝ) (hr : 2 ≤ r) :
    -(2 / r) ≤ Real.log (1 - 1 / r) := by
…
```
theorem OAI.Problem337.descent_power_lower line 28
Source documentation
A moment order at least eight times the logarithmic depth constant ensures that the repeated Hölder exponent loses at most a fourth power.
```
theorem descent_power_lower
    (r K S : ℝ) (d : ℕ) (hr : 2 ≤ r) (hKr : 8 * K ≤ r)
    (hS : 1 ≤ S) (hd : (d : ℝ) ≤ K * Real.log S) :
    S ^ (-(1 / 4 : ℝ)) ≤ (1 - 1 / r) ^ d := by
…
```

theorem OAI.Problem337.descent_density_exp_bound line 51

Source documentation

The explicit finite density estimate, before the final asymptotic comparison of the positive and negative terms in the exponent.

theorem descent_density_exp_bound
    (δ : ℕ → ℝ) (d : ℕ) (r K S c m : ℝ)
    (hr : 2 ≤ r) (hKr : 8 * K ≤ r) (hS : 1 ≤ S)
    (hc : 0 ≤ c) (hm : 0 ≤ m) (hd : (d : ℝ) ≤ K * Real.log S)
    (hδd : δ d = 0) (hδ : ∀ j ≤ d, 0 ≤ δ j)
    (hstep : ∀ j < d, δ j ≤ Real.exp (-c * m) +
      Real.exp (2 * S ^ (1 / 4 : ℝ)) * (δ (j + 1)) ^ (1 - 1 / r)) :
    δ 0 ≤ (d : ℝ) * Real.exp
      (2 * r * S ^ (1 / 4 : ℝ) - c * m * S ^ (-(1 / 4 : ℝ))) := by
…