Lean4
/-- 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). -/
theorem exists_decomposition_of_monotoneOn_hasDerivWithinAt (hs : MeasurableSet s) (hf : MonotoneOn f s)
(hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x) :
∃ (a b c : Set ℝ),
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) ∧ InjOn f c :=
by
let a := {x ∈ s | 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x ∈ s | 𝓝[s ∩ Iio x] x = ⊥}
have a_count : a.Countable := countable_setOf_isolated_right_within.union countable_setOf_isolated_left_within
let s₁ := s \ a
have hs₁ : MeasurableSet s₁ := hs.diff a_count.measurableSet
let u : Set ℝ := {c | ∃ x y, x ∈ s₁ ∧ y ∈ s₁ ∧ x < y ∧ f x = c ∧ f y = c}
have hu : Set.Countable u := MonotoneOn.countable_setOf_two_preimages (hf.mono diff_subset)
let b := s₁ ∩ f ⁻¹' u
have hb : MeasurableSet b := by
have : b = ⋃ z ∈ u, s₁ ∩ f ⁻¹' { z } := by ext; simp [b]
rw [this]
apply MeasurableSet.biUnion hu (fun z hz ↦ ?_)
obtain ⟨v, hv, tv⟩ : ∃ v, OrdConnected v ∧ (s \ a) ∩ f ⁻¹' { z } = (s \ a) ∩ v :=
ordConnected_singleton.preimage_monotoneOn (hf.mono diff_subset)
exact tv ▸ (hs.diff a_count.measurableSet).inter hv.measurableSet
let c := s₁ \ b
have hc : MeasurableSet c := hs₁.diff hb
refine ⟨a, b, c, ?_, a_count.measurableSet, hb, hc, ?_, ?_, a_count, ?_, ?_, ?_, ?_⟩
· ext x
simp only [diff_self_inter, inter_union_diff, union_diff_self, mem_union, mem_setOf_eq, or_iff_right_iff_imp, a, b,
s₁, c]
tauto
· simpa [b, c, s₁] using disjoint_sdiff_right
· simpa [c] using disjoint_sdiff_right
· exact hu.mono (by simp [b])
· /- We have to show that the derivative is `0` at `x ∈ b`. For that, we use that there is another
point `p` with `f p = f x`, by definition of `b`. If `p < x`, then `f` is locally constant to
the left of `x`. As `x` is not isolated to its left (since we are not in the set `a`), it
follows that `f' x = 0`. The same argument works if `x < p`, using the right neighborhood
instead. -/
intro x hx
obtain ⟨p, ps₁, px, fpx⟩ : ∃ p ∈ s₁, p ≠ x ∧ f p = f x :=
by
rcases hx.2 with ⟨p, q, ps₁, qs₁, pq, hp, hq⟩
rcases eq_or_ne p x with h'p | h'p
· exact ⟨q, qs₁, (h'p.symm.le.trans_lt pq).ne', hq⟩
·
exact
⟨p, ps₁, h'p, hp⟩
-- we treat separately the cases `p < x` and `x < p` as we couldn't unify their proofs nicely
rcases lt_or_gt_of_ne px with px | px
· have K : HasDerivWithinAt f 0 (s ∩ Ioo p x) x :=
by
have E (y) (hy : y ∈ s ∩ Ioo p x) : f y = f x :=
by
apply le_antisymm (hf hy.1 hx.1.1 hy.2.2.le)
rw [← fpx]
exact hf ps₁.1 hy.1 hy.2.1.le
have : HasDerivWithinAt (fun y ↦ f x) 0 (s ∩ Ioo p x) x := hasDerivWithinAt_const x (s ∩ Ioo p x) (f x)
exact this.congr E rfl
have K' : HasDerivWithinAt f (f' x) (s ∩ Ioo p x) x := (hf' x hx.1.1).mono inter_subset_left
apply UniqueDiffWithinAt.eq_deriv _ _ K' K
have J1 : (s ∩ Ioo p x) \ { x } = s ∩ Ioo p x := by simp
have J2 : 𝓝[s ∩ Ioo p x] x = 𝓝[s ∩ Iio x] x := by simp [nhdsWithin_inter, nhdsWithin_Ioo_eq_nhdsLT px]
rw [uniqueDiffWithinAt_iff_accPt, accPt_principal_iff_nhdsWithin, J1, J2]
simp only [mem_inter_iff, mem_diff, hx.1.1, mem_union, mem_setOf_eq, true_and, not_or, mem_preimage, b, s₁,
a] at hx
exact neBot_iff.2 hx.1.2
· have K : HasDerivWithinAt f 0 (s ∩ Ioo x p) x :=
by
have E (y) (hy : y ∈ s ∩ Ioo x p) : f y = f x :=
by
apply le_antisymm _ (hf hx.1.1 hy.1 hy.2.1.le)
rw [← fpx]
exact hf hy.1 ps₁.1 hy.2.2.le
have : HasDerivWithinAt (fun y ↦ f x) 0 (s ∩ Ioo x p) x := hasDerivWithinAt_const x (s ∩ Ioo x p) (f x)
exact this.congr E rfl
have K' : HasDerivWithinAt f (f' x) (s ∩ Ioo x p) x := (hf' x hx.1.1).mono inter_subset_left
apply UniqueDiffWithinAt.eq_deriv _ _ K' K
have J1 : (s ∩ Ioo x p) \ { x } = (s ∩ Ioo x p) := by simp
have J2 : 𝓝[s ∩ Ioo x p] x = 𝓝[s ∩ Ioi x] x := by simp [nhdsWithin_inter, nhdsWithin_Ioo_eq_nhdsGT px]
rw [uniqueDiffWithinAt_iff_accPt, accPt_principal_iff_nhdsWithin, J1, J2]
simp only [mem_inter_iff, mem_diff, hx.1.1, mem_union, mem_setOf_eq, true_and, not_or, mem_preimage, b, s₁,
a] at hx
exact neBot_iff.2 hx.1.1
· /- We have to show that the derivative is nonnegative at points of `c`. As these points are
not isolated in `s`, this follows from the fact that `f` is monotone on `s`. -/
intro x hx
apply (hf' x hx.1.1).nonneg_of_monotoneOn _ hf
simp only [mem_diff, hx.1.1, mem_union, mem_setOf_eq, true_and, not_or, c, s₁, a, b] at hx
rw [accPt_principal_iff_nhdsWithin]
have : (𝓝[s ∩ Iio x] x).NeBot := neBot_iff.2 hx.1.2
apply this.mono
apply nhdsWithin_mono
rintro y ⟨yt, yx : y < x⟩
exact ⟨yt, by simpa using yx.ne⟩
· intro x hx y hy hxy
contrapose! hxy
wlog H : x < y generalizing x y with h
· have : y < x := by order
exact (h hy hx hxy.symm this).symm
refine fun h ↦ hx.2 ⟨hx.1, ?_⟩
exact
⟨x, y, hx.1, hy.1, H, rfl, h.symm⟩
/- Change of variable formula for differentiable functions: if a real function `f` is
monotone and differentiable on a measurable set `s`, then the Lebesgue integral of a function
`u : ℝ → ℝ≥0∞` on `f '' s` coincides with the integral of `(f' x) * u ∘ f` on `s`.
Note that the measurability of `f '' s` is given by `MeasurableSet.image_of_monotoneOn`. -/
