English
Let f be a continuous map between suitable normed spaces. Then the set of pairs (x, y) in E × E for which the line through x in direction y is differentiable at t = 0 is a measurable subset of E × E.
Русский
Пусть f — непрерывное отображение между подходящими нормированными пространствами. Тогда множество пар (x, y) ∈ E × E, для которых линейная траектория через x в направлении y дифференцируема при t = 0, является измеримой в σ-алгебре произведения.
LaTeX
$$$ \\MeasurableSet\\{(x,y) \\in E \\times E \\mid \\ LineDifferentiableAt 𝕜 f x y\\}$$$
Lean4
theorem measurableSet_lineDifferentiableAt_uncurry (hf : Continuous f) :
MeasurableSet {p : E × E | LineDifferentiableAt 𝕜 f p.1 p.2} :=
by
borelize 𝕜
let g : (E × E) → 𝕜 → F := fun p t ↦ f (p.1 + t • p.2)
have : Continuous g.uncurry :=
hf.comp <| (continuous_fst.comp continuous_fst).add <| continuous_snd.smul (continuous_snd.comp continuous_fst)
have M_meas : MeasurableSet {q : (E × E) × 𝕜 | DifferentiableAt 𝕜 (g q.1) q.2} :=
measurableSet_of_differentiableAt_with_param 𝕜 this
exact measurable_prodMk_right M_meas
