English
Analogous to the right-derivative result, if f is differentiable on the left of a, continuous at a, and the left-hand derivative converges, then f has a left-hand derivative at a with the corresponding limit.
Русский
Аналогично правилу правой производной: если f дифференцируема слева от a, непрерывна в a, и лево-градиент сходится, то у f существует левая производная в a с соответствующим пределом.
LaTeX
$$$$ \\text{HasDerivWithinAt } f e (I_i c a) a, $$$$
Lean4
/-- If a function is differentiable on the left of a point `a : ℝ`, continuous at `a`, and
its derivative also converges at `a`, then `f` is differentiable on the left at `a`. -/
theorem hasDerivWithinAt_Iic_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 (Iic 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 = (b, a)`. Then, we check all the assumptions of this theorem and we
apply it. -/
obtain ⟨b, ba, sab⟩ : ∃ b ∈ Iio a, Ico b a ⊆ s := mem_nhdsLT_iff_exists_Ico_subset.1 hs
let t := Ioo b a
have ts : t ⊆ s := Subset.trans Ioo_subset_Ico_self sab
have t_diff : DifferentiableOn ℝ f t := f_diff.mono ts
have t_conv : Convex ℝ t := convex_Ioo b a
have t_open : IsOpen t := isOpen_Ioo
have t_closure : closure t = Icc b a := closure_Ioo (ne_of_lt ba)
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 ⟨hy.1, lt_of_le_of_ne hy.2 h⟩
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_Iio_self f_lim')
-- now we can apply `hasFDerivWithinAt_closure_of_tendsto_fderiv`
have : HasDerivWithinAt f e (Icc b a) 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_nhdsLE ba)
