OAI/NumberTheory/Ostmann/Arithmetic/BulkLeafPolynomials.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Terminal moduli as polynomials in a bulk-prime coordinate

  1. def OAI.Ostmann.MovingSlotData.bulkLeafPolynomials line 12
  2. theorem OAI.Ostmann.MovingSlotData.bulkLeafPolynomials_eval line 22
  3. theorem OAI.Ostmann.MovingSlotData.bulkLeafPolynomials_degree line 39

    Source documentation

    Degree grows with the fixed tree depth and the actual list lengths; the size of a prime and every coefficient are irrelevant.

    theorem MovingSlotData.bulkLeafPolynomials_degree {σ : Type*} (value : σ → ℝ) (i : σ)
    {n : ℕ} (T : MovingSlotData σ n) (L R : Polynomial ℝ) (d D e : ℕ)
    (hsize : T.SizeLE d) (hregular : T.RegularLengthLE D)
    (hL : L.natDegree ≤ e) (hR : R.natDegree ≤ e) (j : TreeLeafIndex n) :
    (T.bulkLeafPolynomials value i L R j).natDegree ≤ 2 * (n * d + e) + D := by
…

    Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.TreeLeafIndex