Theorems · Theorem · measure theory

ApproximatesLinearOn.norm_fderiv_sub_le

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E}
  {f : E → E} [inst_3 : MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure]
  {A : E →L[ℝ] E} {δ : NNReal},
  ApproximatesLinearOn f A s δ →
    MeasurableSet s →
      ∀ (f' : E → E →L[ℝ] E), (∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) → ∀ᵐ (x : E) ∂μ.restrict s, ‖f' x - A‖₊ ≤ δ

If a differentiable function f is approximated by a linear map A on a set s, up to δ, then at almost every x in s one has ‖f' x - A‖ ≤ δ.

Defined in

Mathlib.MeasureTheory.Function.Jacobian

Cited by

3 results in Mathlib

Foundations

Depth 268 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceFiniteDimensionalMeasurableSpaceBorelSpaceMeasureTheory.Measure.IsAddHaarMeasure