SmallDegreeCorrections.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem335.rpow_one_sub_le_chord line 13
Source documentation
A convex chord controls the small-degree correction, without differentiating its logarithm.
```
theorem rpow_one_sub_le_chord (q z : ℝ) (hq : 0 < q)
    (hz : 0 ≤ z) (hz' : z ≤ 1 / 4) :
    q ^ (1 - z) ≤ q + 4 * z * q ^ ((3 : ℝ) / 4) := by
…
```

theorem OAI.Problem335.sum_rpow_one_sub_le_chord line 28

Source documentation

Sum version of the chord estimate.

theorem sum_rpow_one_sub_le_chord {ι : Type*} (I : Finset ι)
    (q : ℝ) (z : ι → ℝ) (hq : 0 < q)
    (hz : ∀ i ∈ I, 0 ≤ z i) (hz' : ∀ i ∈ I, z i ≤ 1 / 4) :
    ∑ i ∈ I, q ^ (1 - z i) ≤
      (I.card : ℝ) * q + 4 * (∑ i ∈ I, z i) * q ^ ((3 : ℝ) / 4) := by
…

theorem OAI.Problem335.sum_small_degree_corrections_le line 43

Source documentation

The total low-degree correction is O(sqrt n), uniformly in the number and sizes of factors. The degree variables may be real; natural degrees are a special case.

theorem sum_small_degree_corrections_le {ι : Type*} (I : Finset ι)
    (n s q : ℝ) (e : ι → ℝ)
    (hn : 0 < n) (hs : 0 ≤ s) (hs' : s ≤ Real.sqrt n)
    (hq : 0 < q) (hqone : q ≤ 1) (hqsmall : q ≤ 2 / Real.sqrt n)
    (he : ∀ i ∈ I, 1 ≤ e i)
    (helow : ∀ i ∈ I, s * e i / n ≤ 1 / 4)
    (hesum : ∑ i ∈ I, e i ≤ n) :
    ∑ i ∈ I, q ^ (1 - s * e i / n) ≤ 6 * Real.sqrt n := by
…