nnnorm_approxOn_le — Mathlib

English

Norm-based bound: the NN-norm distance between approxOn and f is bounded by the distance to y0.

Русский

Граневая неравенство по норме: отношение НН-нормы между approxOn и f ограничено расстоянием до y0.

LaTeX

$$$\\|approxOn\\ f\\ hf\\ s\\ y_0\\ h_0\\ n\\ x - f\\ x\\|_{nn} \\le \\|f\\ x - y_0\\|_{nn}.$$$

Lean4

theorem nnnorm_approxOn_le [OpensMeasurableSpace E] {f : β → E} (hf : Measurable f) {s : Set E} {y₀ : E} (h₀ : y₀ ∈ s)
    [SeparableSpace s] (x : β) (n : ℕ) : ‖approxOn f hf s y₀ h₀ n x - f x‖₊ ≤ ‖f x - y₀‖₊ :=
  by
  have := edist_approxOn_le hf h₀ x n
  rw [edist_comm y₀] at this
  simp only [edist_nndist, nndist_eq_nnnorm] at this
  exact mod_cast this

Похожие утверждения