OAI/NumberTheory/Ostmann/Arithmetic/BulkSmoothRootCuts.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.bulkSmoothFactors_root_cuts line 13

   Source documentation

   All cuts are constructed derivative roots of actual bulk polynomials. Their number depends on degree, never on coefficient height or prime values.

   theorem bulkSmoothFactors_root_cuts {σ : Type*} (value : σ → ℝ) (i : σ)
       {n : ℕ} (T : MovingSlotData σ n) (L R : Polynomial ℝ) (ψ : 𝓢(ℝ, ℂ))
       (X lo hi : ℝ) (hlo : 1 ≤ lo) (hhi : lo ≤ hi) (φ : ℝ → ℝ)
       (G : ℕ → ℝ) (B D : ℝ) (hB : 0 ≤ B) (hD : 0 ≤ D)
       (hφ : ∀ x, |φ x| ≤ B) (hlip : ∀ x y, |φ x - φ y| ≤ D * |x - y|)
       (d r e : ℕ) (hsize : T.SizeLE d) (hregular : T.RegularLengthLE r)
       (hL : L.natDegree ≤ e) (hR : R.natDegree ≤ e) :
       ∃ S : Finset ℝ,
         S.card ≤ (2 ^ n + (T.bulkNodePolynomials value i L R).length) * (2 * (n * d + e) + r) ∧
         ∀ j z, z ∈ (bulkSmoothFactors value i T L R ψ X lo hi hlo hhi φ G B D hB hD hφ hlip j).polynomial.derivative.roots → z ∈ S := by
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.bulkSmoothFactors