Theorems · Theorem · measure theory

exists_partition_approximatesLinearOn_of_hasFDerivWithinAt

∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : MeasurableSpace E] [BorelSpace E]
  [SecondCountableTopology F] (f : E → F) (s : Set E) (f' : E → E →L[ℝ] F),
  (∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) →
    ∀ (r : (E →L[ℝ] F) → NNReal),
      (∀ (A : E →L[ℝ] F), r A ≠ 0) →
        ∃ t A,
          Pairwise (Function.onFun Disjoint t) ∧
            (∀ (n : ℕ), MeasurableSet (t n)) ∧
              s ⊆ ⋃ n, t n ∧
                (∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (r (A n))) ∧
                  (s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y)

Assume that a function f has a derivative at every point of a set s. Then one may partition s into countably many disjoint relatively measurable sets (i.e., intersections of s with measurable sets t n) on which f is well approximated by linear maps A n.

Defined in

Mathlib.MeasureTheory.Function.Jacobian

Cited by

5 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceFiniteDimensionalNormedAddCommGroupNormedSpaceMeasurableSpaceBorelSpaceSecondCountableTopology