English
If f is the derivative and there exists a bounded linear map h representing the derivative, then the derivative within s at x equals that linear map h, provided a suitable differentiability hypothesis holds.
Русский
Если производная существует и существует ограниченная линейная карта h, представляющая производную, то во внутренности s в x производная равна этой линейной карте h при условии соответствующего предположения о дифференцируемости.
LaTeX
$$$$ fderivWithin\\,\\mathbb{K}\\,f\\,s\\,x \\\\= h.toContinuousLinearMap $$$$
Lean4
/-- If a real function `f` has a derivative `g` everywhere but at a point, and `f` and `g` are
continuous at this point, then `g` is also the derivative of `f` at this point. -/
theorem hasDerivAt_of_hasDerivAt_of_ne {f g : ℝ → E} {x : ℝ} (f_diff : ∀ y ≠ x, HasDerivAt f (g y) y)
(hf : ContinuousAt f x) (hg : ContinuousAt g x) : HasDerivAt f (g x) x :=
by
have A : HasDerivWithinAt f (g x) (Ici x) x :=
by
have diff : DifferentiableOn ℝ f (Ioi x) := fun y hy =>
(f_diff y (ne_of_gt hy)).differentiableAt.differentiableWithinAt
apply hasDerivWithinAt_Ici_of_tendsto_deriv diff hf.continuousWithinAt self_mem_nhdsWithin
have : Tendsto g (𝓝[>] x) (𝓝 (g x)) := tendsto_inf_left hg
apply this.congr' _
apply mem_of_superset self_mem_nhdsWithin fun y hy => _
intro y hy
exact (f_diff y (ne_of_gt hy)).deriv.symm
have B : HasDerivWithinAt f (g x) (Iic x) x :=
by
have diff : DifferentiableOn ℝ f (Iio x) := fun y hy =>
(f_diff y (ne_of_lt hy)).differentiableAt.differentiableWithinAt
apply hasDerivWithinAt_Iic_of_tendsto_deriv diff hf.continuousWithinAt self_mem_nhdsWithin
have : Tendsto g (𝓝[<] x) (𝓝 (g x)) := tendsto_inf_left hg
apply this.congr' _
apply mem_of_superset self_mem_nhdsWithin fun y hy => _
intro y hy
exact (f_diff y (ne_of_lt hy)).deriv.symm
simpa using B.union A
