PolynomialInterpolationBound.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Elementary interpolation estimates on measurable sets

Positive length supplies separated interpolation nodes. Lagrange interpolation then bounds a polynomial on an interval in terms of its values on these nodes. These bounds give the scalar Remez estimate on measurable sets.

theorem OAI.PolycyclicRecognition.exists_separated_finset_of_length line 23

Source documentation

A set of length greater than 2*n*δ contains n points separated by δ. No regularity of the set is needed.

theorem exists_separated_finset_of_length (S : Set ℝ) (δ : ℝ) (hδ : 0 < δ)
    (n : ℕ) (hm : 2 * (n : ℝ) * δ < (volume S).toReal) :
    ∃ s : Finset ℝ, s.card = n ∧ (↑s : Set ℝ) ⊆ S ∧
      ∀ x ∈ s, ∀ y ∈ s, x ≠ y → δ ≤ |x - y| := by
…

theorem OAI.PolycyclicRecognition.polynomial_bound_of_separated_nodes line 73

Source documentation

Explicit interpolation bound, with the separation and interval radius visible. The degree may be strictly smaller than the number of nodes.

theorem polynomial_bound_of_separated_nodes (p : ℝ[X]) (s : Finset ℝ)
    (hdeg : p.degree < s.card) (δ R η : ℝ) (hδ : 0 < δ)
    (hR : 0 ≤ R) (hη : 0 ≤ η)
    (hsep : ∀ a ∈ s, ∀ b ∈ s, a ≠ b → δ ≤ |a - b|)
    (hs : ∀ a ∈ s, |a| ≤ R) (hp : ∀ a ∈ s, |p.eval a| ≤ η)
    (x : ℝ) (hx : |x| ≤ R) :
    |p.eval x| ≤ (s.card : ℝ) * η * (2 * R / δ) ^ (s.card - 1) := by
…