OAI/GroupTheory/PolycyclicRecognition/Analysis/UnivariateRemez.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

An elementary one-variable Remez bound

The constant is deliberately coarse. Only a fixed power of inverse length is needed in the subexponential geometric argument.

  1. theorem OAI.PolycyclicRecognition.univariate_remez_bound line 16
  2. theorem OAI.PolycyclicRecognition.exists_univariate_remez_constant line 66

    Source documentation

    The scalar interval sublevel estimate.

    theorem exists_univariate_remez_constant (D : ℕ) (hD : 1 ≤ D) :
    ∃ A : ℝ, 0 < A ∧
      ∀ (p : ℝ[X]), p.natDegree ≤ D → ∀ R : ℝ, 1 ≤ R →
      ∀ S : Set ℝ, S ⊆ closedBall 0 R → 0 < (volume S).toReal →
      ∀ η : ℝ, 0 ≤ η → (∀ x ∈ S, |p.eval x| ≤ η) →
      ∀ x ∈ closedBall 0 R,
        |p.eval x| ≤ (A * (1 + R) / (volume S).toReal) ^ D * η := by
…