Theorems · Theorem · measure theory

MeasureTheory.exists_decomposition_of_monotoneOn_hasDerivWithinAt

∀ {s : Set ℝ} {f f' : ℝ → ℝ},
  MeasurableSet s →
    MonotoneOn f s →
      (∀ x ∈ s, HasDerivWithinAt f (f' x) s x) →
        ∃ a b c,
          a ∪ (b ∪ c) = s ∧
            MeasurableSet a ∧
              MeasurableSet b ∧
                MeasurableSet c ∧
                  Disjoint a (b ∪ c) ∧
                    Disjoint b c ∧
                      a.Countable ∧ (f '' b).Countable ∧ (∀ x ∈ b, f' x = 0) ∧ (∀ x ∈ c, 0 ≤ f' x) ∧ Set.InjOn f c

Technical structure theorem for monotone differentiable functions. If a function f is monotone on a measurable set and has a derivative f', one can decompose the set as a disjoint union a ∪ b ∪ c of measurable sets where a is countable (the points which are isolated on the left or on the right, where f' is not well controlled), f is locally constant on b and f' = 0 there (the preimages of the countably many points with several preimages), and f is injective on c with nonnegative derivative (the other points).

Defined in

Mathlib.MeasureTheory.Function.JacobianOneDim

Cited by

3 results in Mathlib

Foundations

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