OAI/NumberTheory/Ostmann/Arithmetic/BulkNodeSupportPolynomials.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.MovingSlotReversal.bulkCompositePolynomial line 12
2. theorem OAI.Ostmann.MovingSlotReversal.bulkCompositePolynomial_eval line 16
3. theorem OAI.Ostmann.MovingSlotReversal.bulkCompositePolynomial_degree line 23
4. def OAI.Ostmann.MovingSlotData.bulkNodeSupportPolynomials line 29
5. theorem OAI.Ostmann.MovingSlotData.bulkNodeSupportPolynomials_eval line 43
6. theorem OAI.Ostmann.MovingSlotData.bulkNodeSupportPolynomials_length line 61
7. theorem OAI.Ostmann.MovingSlotData.bulkNodeSupportPolynomials_degree line 75

   Source documentation

   Every inequality has degree bounded by the depth times the actual slot length. No coefficient-size assumption is needed.

   theorem MovingSlotData.bulkNodeSupportPolynomials_degree {σ : Type*}
       (value : σ → ℝ) (i : σ) (childBound pivotBound : ℕ → ℕ)
       {n : ℕ} (T : MovingSlotData σ n) (L R : Polynomial ℝ) (d e : ℕ)
       (hsize : T.SizeLE d) (hL : L.natDegree ≤ e) (hR : R.natDegree ≤ e) :
       ∀ P ∈ T.bulkNodeSupportPolynomials value i childBound pivotBound L R, P.natDegree ≤ n * d + e := by
   …

   Mentions: OAI.Ostmann.MovingSlotData