English
If f is differentiable on a punctured neighborhood and dslope f c is differentiable almost everywhere, then dslope behaves as a Schwarz-type estimate on the ball.
Русский
Если f дифференцируема на окрестности с вычитанием точки, и dslope f c дифференцируема почти везде, то dslope удовлетворяет неравенству типа Шварца на шаре.
LaTeX
$$$\forall c,\ R>0,\ \text{ DifferentiableOn } f \text{ on } B(c,R) \Rightarrow \text{ дифференцируемость dslope } f c \text{ на } B(c,R).$$$
Lean4
theorem differentiableOn_dslope {f : ℂ → E} {s : Set ℂ} {c : ℂ} (hc : s ∈ 𝓝 c) :
DifferentiableOn ℂ (dslope f c) s ↔ DifferentiableOn ℂ f s :=
⟨fun h => h.of_dslope, fun h =>
(differentiableOn_compl_singleton_and_continuousAt_iff hc).mp <|
⟨Iff.mpr (differentiableOn_dslope_of_notMem fun h => h.2 rfl) (h.mono diff_subset),
continuousAt_dslope_same.2 <| h.differentiableAt hc⟩⟩
