OAI/NumberTheory/Ostmann/Arithmetic/MovingCutoffPolynomials.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.MovingSlotData.nodeCutoffPolynomials line 11
2. def OAI.Ostmann.movingRealNodeCutoff line 18
3. theorem OAI.Ostmann.MovingSlotData.nodeCutoffPolynomials_length line 26
4. theorem OAI.Ostmann.MovingSlotData.nodeCutoffPolynomials_degree line 36
5. theorem OAI.Ostmann.MovingSlotData.nodeCutoffPolynomials_value line 49
6. def OAI.Ostmann.movingNodeCutoffFactors line 61
7. theorem OAI.Ostmann.movingNodeCutoffFactors_value line 69
8. theorem OAI.Ostmann.movingNodeCutoffFactors_budget line 83
9. theorem OAI.Ostmann.movingNodeCutoffFactors_no_derivative_roots line 95

   Source documentation

   With either top giant fixed, all node cutoff polynomials are affine. Thus their derivatives have no roots and need no additional partition cuts.

   theorem movingNodeCutoffFactors_no_derivative_roots {σ : Type*} (value : σ → ℕ)
       {n : ℕ} (T : MovingSlotData σ n) (L R : Polynomial ℝ)
       (hL : L.natDegree ≤ 1) (hR : R.natDegree ≤ 1) (φ : ℝ → ℝ)
       (G : ℕ → ℝ) (B D : ℝ) (hB : 0 ≤ B) (hD : 0 ≤ D)
       (hφ : ∀ x, |φ x| ≤ B) (hlip : ∀ x y, |φ x - φ y| ≤ D * |x - y|)
       (i : Fin (T.nodeCutoffPolynomials value L R).length) :
       ((movingNodeCutoffFactors value T L R φ G B D hB hD hφ hlip i).polynomial.derivative).roots = 0 := by
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.movingNodeCutoffFactors