OddDegreeThreshold.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform eventual smallness used to absorb the constant loss in the odd low-degree estimate. The threshold is independent of the factor degree and of the particular parameter q below its stated envelope.

theorem OAI.Problem335.eventually_small_power_of_envelope line 15

Source documentation

A polynomially decaying envelope absorbs every fixed positive power and fixed nonnegative multiplicative constant, uniformly below the envelope.

theorem eventually_small_power_of_envelope (a b C : ℝ)
    (ha : 0 < a) (hb : 0 < b) (hC : 0 ≤ C) :
    ∃ N : ℕ, ∀ n : ℕ, N ≤ n → ∀ q : ℝ, 0 ≤ q →
      q ≤ (n : ℝ) ^ (-a) → C * q ^ b ≤ 1 := by
…

theorem OAI.Problem335.eventually_odd_degree_smallness line 40

Source documentation

The exact eventual smallness hypothesis used for all low odd degrees.

theorem eventually_odd_degree_smallness :
    ∃ N : ℕ, ∀ n : ℕ, N ≤ n → ∀ q : ℝ, 0 ≤ q →
      q ≤ (n : ℝ) ^ (-(2 / 5 : ℝ)) →
      5 * q ^ (3 / 16 : ℝ) ≤ 1 := by
…