OAI/NumberTheory/JointDickman/Probability/CompactTensorApproximation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Finite tensor approximation on the four-variable smooth support

  1. def OAI.JointDickman.supportPolynomialMap line 11
  2. theorem OAI.JointDickman.supportPolynomialMap_apply line 16
  3. theorem OAI.JointDickman.supportPolynomialMap_separates line 27
  4. theorem OAI.JointDickman.compact_support_polynomial_approximation line 43

    Source documentation

    The fourth coordinate can carry the external smooth parameter. Each polynomial is a finite sum of products of one-coordinate powers.

    theorem compact_support_polynomial_approximation (K : Set (Fin 4 → ℝ))
    (hK : IsCompact K) (f : C(K,ℝ)) {ε : ℝ} (hε : 0 < ε) :
    ∃ P : MvPolynomial (Fin 4) ℝ, ∀ x : K,
      |MvPolynomial.eval (x : Fin 4 → ℝ) P-f x| < ε := by
…