English
The set of right differentiability points is a Borel-measurable set.
Русский
Множество точек правой дифференциации является борелевским измеримым.
LaTeX
$$MeasurableSet {x | DifferentiableWithinAt ℝ f (Ici x) x}$$
Lean4
@[measurability, fun_prop]
theorem measurable_derivWithin_Ici [MeasurableSpace F] [BorelSpace F] : Measurable fun x => derivWithin f (Ici x) x :=
by
refine measurable_of_isClosed fun s hs => ?_
have :
(fun x => derivWithin f (Ici x) x) ⁻¹' s =
{x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ s} ∪
{x | ¬DifferentiableWithinAt ℝ f (Ici x) x} ∩ {_x | (0 : F) ∈ s} :=
Set.ext fun x => mem_preimage.trans derivWithin_mem_iff
rw [this]
exact
(measurableSet_of_differentiableWithinAt_Ici_of_isComplete _ hs.isComplete).union
((measurableSet_of_differentiableWithinAt_Ici _).compl.inter (MeasurableSet.const _))
