English
The derivative map on a measurable set is almost everywhere measurable with respect to restricted measure.
Русский
Производная на измеримом множестве измерима почти повсеместно относительно ограниченной меры.
LaTeX
$$$$ \text{ae-measurable}(f', \mu \restriction s). $$$$
Lean4
/-- The derivative of a function on a measurable set is almost everywhere measurable on this set
with respect to Lebesgue measure. Note that, in general, it is not genuinely measurable there,
as `f'` is not unique (but only on a set of measure `0`, as the argument shows). -/
theorem aemeasurable_fderivWithin (hs : MeasurableSet s) (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) :
AEMeasurable f' (μ.restrict s) := by
/- It suffices to show that `f'` can be uniformly approximated by a measurable function.
Fix `ε > 0`. Thanks to `exists_partition_approximatesLinearOn_of_hasFDerivWithinAt`, one
can find a countable measurable partition of `s` into sets `s ∩ t n` on which `f` is well
approximated by linear maps `A n`. On almost all of `s ∩ t n`, it follows from
`ApproximatesLinearOn.norm_fderiv_sub_le` that `f'` is uniformly approximated by `A n`, which
gives the conclusion. -/
-- fix a precision `ε`
refine aemeasurable_of_unif_approx fun ε εpos => ?_
let δ : ℝ≥0 := ⟨ε, le_of_lt εpos⟩
have δpos : 0 < δ := εpos
obtain ⟨t, A, t_disj, t_meas, t_cover, ht, _⟩ :
∃ (t : ℕ → Set E) (A : ℕ → E →L[ℝ] E),
Pairwise (Disjoint on t) ∧
(∀ n : ℕ, MeasurableSet (t n)) ∧
(s ⊆ ⋃ n : ℕ, t n) ∧
(∀ n : ℕ, ApproximatesLinearOn f (A n) (s ∩ t n) δ) ∧ (s.Nonempty → ∀ n, ∃ y ∈ s, A n = f' y) :=
exists_partition_approximatesLinearOn_of_hasFDerivWithinAt f s f' hf' (fun _ => δ) fun _ => δpos.ne'
obtain ⟨g, g_meas, hg⟩ : ∃ g : E → E →L[ℝ] E, Measurable g ∧ ∀ (n : ℕ) (x : E), x ∈ t n → g x = A n :=
exists_measurable_piecewise t t_meas (fun n _ => A n) (fun n => measurable_const) <|
t_disj.mono fun i j h => by simp only [h.inter_eq, eqOn_empty]
refine
⟨g, g_meas.aemeasurable, ?_⟩
-- reduce to checking that `f'` and `g` are close on almost all of `s ∩ t n`, for all `n`.
suffices H : ∀ᵐ x : E ∂sum fun n ↦ μ.restrict (s ∩ t n), dist (g x) (f' x) ≤ ε
by
have : μ.restrict s ≤ sum fun n => μ.restrict (s ∩ t n) :=
by
have : s = ⋃ n, s ∩ t n := by
rw [← inter_iUnion]
exact Subset.antisymm (subset_inter Subset.rfl t_cover) inter_subset_left
conv_lhs => rw [this]
exact restrict_iUnion_le
exact ae_mono this H
refine
ae_sum_iff.2 fun n =>
?_
-- on almost all `s ∩ t n`, `f' x` is close to `A n` thanks to
-- `ApproximatesLinearOn.norm_fderiv_sub_le`.
have E₁ : ∀ᵐ x : E ∂μ.restrict (s ∩ t n), ‖f' x - A n‖₊ ≤ δ :=
(ht n).norm_fderiv_sub_le μ (hs.inter (t_meas n)) f' fun x hx => (hf' x hx.1).mono inter_subset_left
have E₂ : ∀ᵐ x : E ∂μ.restrict (s ∩ t n), g x = A n :=
by
suffices H : ∀ᵐ x : E ∂μ.restrict (t n), g x = A n from ae_mono (restrict_mono inter_subset_right le_rfl) H
filter_upwards [ae_restrict_mem (t_meas n)]
exact hg n
filter_upwards [E₁, E₂] with x hx1 hx2
rw [← nndist_eq_nnnorm] at hx1
rw [hx2, dist_comm]
exact hx1
