OAI/NumberTheory/Ostmann/Arithmetic/BulkFullSupportPolynomials.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.bulkFullSupportPolynomials line 12
2. theorem OAI.Ostmann.bulkFullSupportPolynomials_eval line 21
3. theorem OAI.Ostmann.bulkFullSupportPolynomials_degree line 53
4. theorem OAI.Ostmann.bulkFullSupport_root_cuts line 79

   Source documentation

   These roots include all node ranges and terminal windows. The count is uniform in all other real bulk values and both giant coefficients.

   theorem bulkFullSupport_root_cuts {σ : Type*} (value : σ → ℝ) (i : σ)
       (childBound pivotBound : ℕ → ℕ) {n : ℕ} (T : MovingSlotData σ n)
       (hT : T.CompensationAbsent i) (L R : Polynomial ℝ) (X lo hi : ℝ) (d r e : ℕ)
       (hsize : T.SizeLE d) (hregular : T.RegularLengthLE r)
       (hL : L.natDegree ≤ e) (hR : R.natDegree ≤ e) :
       ∃ S : Finset ℝ, S.card ≤ (3 * (2 ^ n - 1) + 2 * 2 ^ n) * (2 * (n * d + e) + r) ∧
         ∀ x y, rootCellCode S x = rootCellCode S y →
           realValueSupportFlag (Function.update value i x) childBound pivotBound T X lo hi (L.eval x) (R.eval x) =
           realValueSupportFlag (Function.update value i y) childBound pivotBound T X lo hi (L.eval y) (R.eval y) := by
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.rootCellCode, OAI.Ostmann.realValueSupportFlag