OAI/NumberTheory/Ostmann/Quadratic/QuadraticFiniteDescent.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.quadraticDescentBudget line 11
2. theorem OAI.Ostmann.quadraticDescentBudget_nonneg line 15
3. theorem OAI.Ostmann.quadraticDescentBudget_bound line 21
4. theorem OAI.Ostmann.quadratic_rough_zero line 33
5. theorem OAI.Ostmann.quadratic_quotient_descent_cutoff line 37
6. theorem OAI.Ostmann.quadratic_rough_finite_descent line 50

   Source documentation

   Iterate the concrete n ↦ 2*n/D descent. The power condition proves that the last coefficient range is empty; no limiting or supremum argument occurs.

   theorem quadratic_rough_finite_descent {M N₀ K D : ℕ} {A B : ℝ}
       (hD : 2 ≤ D) (hA : 0 ≤ A) (hB : 0 ≤ B)
       (hstep : ∀ n : ℕ, 0 < n → n ≤ N₀ → ∀ T : ℝ, 0 ≤ T →
         QuadraticRoughBound M (2 * n / D) K T → QuadraticRoughBound M n K (A + B * T))
       (r n : ℕ) (hn : n ≤ N₀) (hcut : 2 ^ r * n < D ^ r) :
       QuadraticRoughBound M n K (quadraticDescentBudget A B r) := by
   …

   Mentions: OAI.Ostmann.QuadraticRoughBound, OAI.Ostmann.quadraticDescentBudget