English
The derivative within Ici x is measurable (strongly, AE) as a function of x.
Русский
Производная внутри Ici x является измеримой функцией по x (сильная/AE).
LaTeX
$$Measurable (fun x => derivWithin f (Ici x) x)$$
Lean4
theorem stronglyMeasurable_derivWithin_Ici : StronglyMeasurable (fun x ↦ derivWithin f (Ici x) x) :=
by
borelize F
apply stronglyMeasurable_iff_measurable_separable.2 ⟨measurable_derivWithin_Ici f, ?_⟩
obtain ⟨t, t_count, ht⟩ : ∃ t : Set ℝ, t.Countable ∧ Dense t := exists_countable_dense ℝ
suffices H : range (fun x ↦ derivWithin f (Ici x) x) ⊆ closure (Submodule.span ℝ (f '' t)) from
IsSeparable.mono (t_count.image f).isSeparable.span.closure H
rintro - ⟨x, rfl⟩
suffices H' : range (fun y ↦ derivWithin f (Ici x) y) ⊆ closure (Submodule.span ℝ (f '' t)) from H' (mem_range_self _)
apply range_derivWithin_subset_closure_span_image
calc
Ici x = closure (Ioi x ∩ closure t) := by simp [dense_iff_closure_eq.1 ht]
_ ⊆ closure (closure (Ioi x ∩ t)) := by
apply closure_mono
simpa [inter_comm] using (isOpen_Ioi (a := x)).closure_inter (s := t)
_ ⊆ closure (Ici x ∩ t) := by
rw [closure_closure]
exact closure_mono (inter_subset_inter_left _ Ioi_subset_Ici_self)
