English
A monotone function is almost everywhere differentiable, with derivative equal to the Radon–Nikodym derivative of the associated Stieltjes measure with respect to Lebesgue measure.
Русский
У монотонной функции почти в точках дифференцируемость, производная равна радону-никодийской производной связанной меры Стилтьジェсу относительно Лебега.
LaTeX
$$$$ \text{aeHasDerivAt}(f) = rnDeriv(\text{stieltjes measure}) $$$$
Lean4
/-- A monotone function is almost everywhere differentiable, with derivative equal to the
Radon-Nikodym derivative of the associated Stieltjes measure with respect to Lebesgue. -/
theorem ae_hasDerivAt {f : ℝ → ℝ} (hf : Monotone f) :
∀ᵐ x, HasDerivAt f (rnDeriv hf.stieltjesFunction.measure volume x).toReal x := by
/- We already know that the Stieltjes function associated to `f` (i.e., `g : x ↦ f (x^+)`) is
differentiable almost everywhere. We reduce to this statement by sandwiching values of `f` with
values of `g`, by shifting with `(y - x)^2` (which has no influence on the relevant
scale `y - x`.) -/
filter_upwards [hf.stieltjesFunction.ae_hasDerivAt, hf.countable_not_continuousAt.ae_notMem volume] with x hx h'x
have A : hf.stieltjesFunction x = f x :=
by
rw [Classical.not_not, hf.continuousAt_iff_leftLim_eq_rightLim] at h'x
apply le_antisymm _ (hf.le_rightLim (le_refl _))
rw [← h'x]
exact hf.leftLim_le (le_refl _)
rw [hasDerivAt_iff_tendsto_slope, (nhdsLT_sup_nhdsGT x).symm, tendsto_sup, slope_fun_def_field, A] at hx
have L1 :
Tendsto (fun y => (f y - f x) / (y - x)) (𝓝[>] x) (𝓝 (rnDeriv hf.stieltjesFunction.measure volume x).toReal) := by
-- limit of a helper function, with a small shift compared to `g`
have :
Tendsto (fun y => (hf.stieltjesFunction (y + -1 * (y - x) ^ 2) - f x) / (y - x)) (𝓝[>] x)
(𝓝 (rnDeriv hf.stieltjesFunction.measure volume x).toReal) :=
by
apply tendsto_apply_add_mul_sq_div_sub (nhdsGT_le_nhdsNE x) hx.2
apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within
· apply Tendsto.mono_left _ nhdsWithin_le_nhds
have : Tendsto (fun y : ℝ => y + -↑1 * (y - x) ^ 2) (𝓝 x) (𝓝 (x + -↑1 * (x - x) ^ 2)) :=
tendsto_id.add (((tendsto_id.sub_const x).pow 2).const_mul (-1))
simpa using this
· filter_upwards [Ioo_mem_nhdsGT <| show x < x + 1 by simp]
rintro y ⟨hy : x < y, h'y : y < x + 1⟩
rw [mem_Ioi]
nlinarith
-- apply the sandwiching argument, with the helper function and `g`
apply tendsto_of_tendsto_of_tendsto_of_le_of_le' this hx.2
· filter_upwards [self_mem_nhdsWithin] with y hy
rw [mem_Ioi, ← sub_pos] at hy
gcongr
exact hf.rightLim_le (by nlinarith)
· filter_upwards [self_mem_nhdsWithin] with y hy
rw [mem_Ioi, ← sub_pos] at hy
gcongr
exact hf.le_rightLim le_rfl
have L2 :
Tendsto (fun y => (f y - f x) / (y - x)) (𝓝[<] x) (𝓝 (rnDeriv hf.stieltjesFunction.measure volume x).toReal) := by
-- limit of a helper function, with a small shift compared to `g`
have :
Tendsto (fun y => (hf.stieltjesFunction (y + -1 * (y - x) ^ 2) - f x) / (y - x)) (𝓝[<] x)
(𝓝 (rnDeriv hf.stieltjesFunction.measure volume x).toReal) :=
by
apply tendsto_apply_add_mul_sq_div_sub (nhdsLT_le_nhdsNE x) hx.1
apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within
· apply Tendsto.mono_left _ nhdsWithin_le_nhds
have : Tendsto (fun y : ℝ => y + -↑1 * (y - x) ^ 2) (𝓝 x) (𝓝 (x + -↑1 * (x - x) ^ 2)) :=
tendsto_id.add (((tendsto_id.sub_const x).pow 2).const_mul (-1))
simpa using this
· filter_upwards [Ioo_mem_nhdsLT <| show x - 1 < x by simp]
rintro y hy
rw [mem_Ioo] at hy
rw [mem_Iio]
nlinarith
-- apply the sandwiching argument, with `g` and the helper function
apply tendsto_of_tendsto_of_tendsto_of_le_of_le' hx.1 this
· filter_upwards [self_mem_nhdsWithin]
rintro y hy
rw [mem_Iio, ← sub_neg] at hy
apply div_le_div_of_nonpos_of_le hy.le
exact (sub_le_sub_iff_right _).2 (hf.le_rightLim (le_refl _))
· filter_upwards [self_mem_nhdsWithin]
rintro y hy
rw [mem_Iio, ← sub_neg] at hy
have : 0 < (y - x) ^ 2 := sq_pos_of_neg hy
apply div_le_div_of_nonpos_of_le hy.le
exact
(sub_le_sub_iff_right _).2
(hf.rightLim_le (by linarith))
-- conclude global differentiability
rw [hasDerivAt_iff_tendsto_slope, slope_fun_def_field, ← nhdsLT_sup_nhdsGT, tendsto_sup]
exact ⟨L2, L1⟩
