English
Under suitable hypotheses, the set of points where DifferentiableAt holds with a derivative in K is measurable.
Русский
При разумных предположениях множество точек, где выполняется DifferentiableAt с производной в K, измеримо.
LaTeX
$$MeasurableSet {p : α × E | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ K}$$
Lean4
theorem measurableSet_of_differentiableAt_of_isComplete_with_param (hf : Continuous f.uncurry) {K : Set (E →L[𝕜] F)}
(hK : IsComplete K) : MeasurableSet {p : α × E | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ K} :=
by
have : {p : α × E | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ K} = {p : α × E | p.2 ∈ D (f p.1) K} := by
simp [← differentiable_set_eq_D K hK]
rw [this]
simp only [D, mem_iInter, mem_iUnion]
simp only [setOf_forall, setOf_exists]
refine MeasurableSet.iInter (fun _ ↦ ?_)
refine MeasurableSet.iUnion (fun _ ↦ ?_)
refine MeasurableSet.iInter (fun _ ↦ ?_)
refine MeasurableSet.iInter (fun _ ↦ ?_)
refine MeasurableSet.iInter (fun _ ↦ ?_)
refine MeasurableSet.iInter (fun _ ↦ ?_)
have : ProperSpace E := .of_locallyCompactSpace 𝕜
exact (isOpen_B_with_param hf K).measurableSet
