English
If a function f is differentiable on the right of a, continuous at a, and its derivative converges from the right to a limit, then f has a right-hand derivative at a with that limit as derivative.
Русский
Если функция f дифференцируема справа от a, непрерывна в a и производная сходится справа к пределу, тогда у f существует правая производная в a с этим пределом как производной.
LaTeX
$$$$ \\text{HasDerivWithinAt } f e (I_c i a) a, \\text{ where } e=\\lim_{x\\downarrow a} f'(x). $$$$
Lean4
/-- If a function is differentiable on the right of a point `a : ℝ`, continuous at `a`, and
its derivative also converges at `a`, then `f` is differentiable on the right at `a`. -/
theorem hasDerivWithinAt_Ici_of_tendsto_deriv {s : Set ℝ} {e : E} {a : ℝ} {f : ℝ → E} (f_diff : DifferentiableOn ℝ f s)
(f_lim : ContinuousWithinAt f s a) (hs : s ∈ 𝓝[>] a) (f_lim' : Tendsto (fun x => deriv f x) (𝓝[>] a) (𝓝 e)) :
HasDerivWithinAt f e (Ici a) a := by
/- This is a specialization of `hasFDerivWithinAt_closure_of_tendsto_fderiv`. To be in the
setting of this theorem, we need to work on an open interval with closure contained in
`s ∪ {a}`, that we call `t = (a, b)`. Then, we check all the assumptions of this theorem and
we apply it. -/
obtain ⟨b, ab : a < b, sab : Ioc a b ⊆ s⟩ := mem_nhdsGT_iff_exists_Ioc_subset.1 hs
let t := Ioo a b
have ts : t ⊆ s := Subset.trans Ioo_subset_Ioc_self sab
have t_diff : DifferentiableOn ℝ f t := f_diff.mono ts
have t_conv : Convex ℝ t := convex_Ioo a b
have t_open : IsOpen t := isOpen_Ioo
have t_closure : closure t = Icc a b := closure_Ioo ab.ne
have t_cont : ∀ y ∈ closure t, ContinuousWithinAt f t y :=
by
rw [t_closure]
intro y hy
by_cases h : y = a
· rw [h]; exact f_lim.mono ts
· have : y ∈ s := sab ⟨lt_of_le_of_ne hy.1 (Ne.symm h), hy.2⟩
exact (f_diff.continuousOn y this).mono ts
have t_diff' : Tendsto (fun x => fderiv ℝ f x) (𝓝[t] a) (𝓝 (smulRight (1 : ℝ →L[ℝ] ℝ) e)) :=
by
simp only [deriv_fderiv.symm]
exact
Tendsto.comp (isBoundedBilinearMap_smulRight : IsBoundedBilinearMap ℝ _).continuous_right.continuousAt
(tendsto_nhdsWithin_mono_left Ioo_subset_Ioi_self f_lim')
-- now we can apply `hasFDerivWithinAt_closure_of_tendsto_fderiv`
have : HasDerivWithinAt f e (Icc a b) a :=
by
rw [hasDerivWithinAt_iff_hasFDerivWithinAt, ← t_closure]
exact hasFDerivWithinAt_closure_of_tendsto_fderiv t_diff t_conv t_open t_cont t_diff'
exact this.mono_of_mem_nhdsWithin (Icc_mem_nhdsGE ab)
