PolynomialCellVariation.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Actual interval pieces and smooth polynomial weights

theorem OAI.Ostmann.exists_rootCell_partition line 15

Source documentation

Root comparisons give an exact interval decomposition of any increasing integer sampling grid. Equality endpoints retain their own code.

theorem exists_rootCell_partition (S : Finset ℝ) (N : ℕ) (u : ℕ → ℝ)
    (hu : Monotone u) :
    ∃ (a K : (S → Ordering) → ℕ) (e : Fin N ≃ Σ i, Fin (K i)),
      (∀ i (j : Fin (K i)), (e.symm ⟨i, j⟩).val = a i + j.val) ∧
      (∀ i (j : Fin (K i)), rootCellCode S (u (a i + j.val)) = i) := by
…

Mentions: OAI.Ostmann.rootCellCode

theorem OAI.Ostmann.discreteVariation_polynomial_cell line 26

Source documentation

Including derivative roots among the cuts proves the required variation bound for a compactly supported smooth factor evaluated on the polynomial.

theorem discreteVariation_polynomial_cell (P : Polynomial ℝ) (S : Finset ℝ)
    (hroots : ∀ r ∈ P.derivative.roots, r ∈ S)
    (u : ℕ → ℝ) (hu : Monotone u) (N : ℕ)
    (hcode : rootCellCode S (u 0) = rootCellCode S (u (N - 1)))
    (Φ : ℝ → ℂ) (lo hi B D : ℝ) (hlohi : lo ≤ hi) (hD : 0 ≤ D)
    (hbound : ∀ x, ‖Φ x‖ ≤ B)
    (hlip : ∀ x y, ‖Φ x - Φ y‖ ≤ D * |x - y|)
    (hlo : Φ lo = 0) (hhi : Φ hi = 0)
    (hout : ∀ x, x < lo ∨ hi < x → Φ x = 0) :
    discreteVariation (fun j => Φ (P.eval (u j))) N ≤ B + D * (hi - lo) := by
…

Mentions: OAI.Ostmann.rootCellCode, OAI.Ostmann.discreteVariation

theorem OAI.Ostmann.discreteVariation_polynomial_product_cell line 49

Source documentation

The same explicit root set works simultaneously for all smooth factors.

theorem discreteVariation_polynomial_product_cell (n : ℕ) (P : Fin n → Polynomial ℝ)
    (S : Finset ℝ) (hroots : ∀ i r, r ∈ (P i).derivative.roots → r ∈ S)
    (u : ℕ → ℝ) (hu : Monotone u) (N : ℕ)
    (hcode : rootCellCode S (u 0) = rootCellCode S (u (N - 1)))
    (Φ : Fin n → ℝ → ℂ) (lo hi B D : Fin n → ℝ)
    (hlohi : ∀ i, lo i ≤ hi i) (hB : ∀ i, 0 ≤ B i) (hD : ∀ i, 0 ≤ D i)
    (hbound : ∀ i x, ‖Φ i x‖ ≤ B i)
    (hlip : ∀ i x y, ‖Φ i x - Φ i y‖ ≤ D i * |x - y|)
    (hlo : ∀ i, Φ i (lo i) = 0) (hhi : ∀ i, Φ i (hi i) = 0)
    (hout : ∀ i x, x < lo i ∨ hi i < x → Φ i x = 0) :
    discreteVariation (fun j => ∏ i, Φ i ((P i).eval (u j))) N ≤
      ∏ i, (2 * B i + D i * (hi i - lo i)) := by
…

Mentions: OAI.Ostmann.rootCellCode, OAI.Ostmann.discreteVariation

theorem OAI.Ostmann.polynomial_nonneg_iff_of_root_cell line 74

Source documentation

On a root cell, polynomial inequality supports really are constant.

theorem polynomial_nonneg_iff_of_root_cell (P : Polynomial ℝ) (S : Finset ℝ)
    (hroots : ∀ r ∈ P.roots, r ∈ S) {x y : ℝ}
    (hcode : rootCellCode S x = rootCellCode S y) :
    0 ≤ P.eval x ↔ 0 ≤ P.eval y := by
…

Mentions: OAI.Ostmann.rootCellCode