chore(Analysis/Calculus/FDeriv/Extend): use Lean 4 naming scheme (#14632)

Most of the declarations in this file are still named according to the Lean 3 naming scheme.

Author: dupuisf

Mathlib/Analysis/Calculus/FDeriv/Extend.lean

@@ -12,13 +12,12 @@ import Mathlib.Analysis.Calculus.MeanValue
 
 We investigate how differentiable functions inside a set extend to differentiable functions
 on the boundary. For this, it suffices that the function and its derivative admit limits there.
-A general version of this statement is given in `has_fderiv_at_boundary_of_tendsto_fderiv`.
+A general version of this statement is given in `hasFDerivWithinAt_closure_of_tendsto_fderiv`.
 
 One-dimensional versions, in which one wants to obtain differentiability at the left endpoint or
-the right endpoint of an interval, are given in
-`has_deriv_at_interval_left_endpoint_of_tendsto_deriv` and
-`has_deriv_at_interval_right_endpoint_of_tendsto_deriv`. These versions are formulated in terms
-of the one-dimensional derivative `deriv ℝ f`.
+the right endpoint of an interval, are given in `hasDerivWithinAt_Ici_of_tendsto_deriv` and
+`hasDerivWithinAt_Iic_of_tendsto_deriv`.  These versions are formulated in terms of the
+one-dimensional derivative `deriv ℝ f`.
 -/
 
 
@@ -32,7 +31,7 @@ open scoped Topology
 /-- If a function `f` is differentiable in a convex open set and continuous on its closure, and its
 derivative converges to a limit `f'` at a point on the boundary, then `f` is differentiable there
 with derivative `f'`. -/
-theorem has_fderiv_at_boundary_of_tendsto_fderiv {f : E → F} {s : Set E} {x : E} {f' : E →L[ℝ] F}
+theorem hasFDerivWithinAt_closure_of_tendsto_fderiv {f : E → F} {s : Set E} {x : E} {f' : E →L[ℝ] F}
     (f_diff : DifferentiableOn ℝ f s) (s_conv : Convex ℝ s) (s_open : IsOpen s)
     (f_cont : ∀ y ∈ closure s, ContinuousWithinAt f s y)
     (h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')) :
@@ -102,16 +101,20 @@ theorem has_fderiv_at_boundary_of_tendsto_fderiv {f : E → F} {s : Set E} {x :
       exact
         tendsto_const_nhds.mul
           (Tendsto.comp continuous_norm.continuousAt <| tendsto_snd.sub tendsto_fst)
-#align has_fderiv_at_boundary_of_tendsto_fderiv has_fderiv_at_boundary_of_tendsto_fderiv
+#align has_fderiv_at_boundary_of_tendsto_fderiv hasFDerivWithinAt_closure_of_tendsto_fderiv
+
+@[deprecated (since := "2024-07-10")] alias has_fderiv_at_boundary_of_tendsto_fderiv :=
+  hasFDerivWithinAt_closure_of_tendsto_fderiv
 
 /-- 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 has_deriv_at_interval_left_endpoint_of_tendsto_deriv {s : Set ℝ} {e : E} {a : ℝ} {f : ℝ → E}
+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 `has_fderiv_at_boundary_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. -/
+  /- 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_nhdsWithin_Ioi_iff_exists_Ioc_subset.1 hs
   let t := Ioo a b
   have ts : t ⊆ s := Subset.trans Ioo_subset_Ioc_self sab
@@ -131,22 +134,26 @@ theorem has_deriv_at_interval_left_endpoint_of_tendsto_deriv {s : Set ℝ} {e :
     exact Tendsto.comp
       (isBoundedBilinearMap_smulRight : IsBoundedBilinearMap ℝ _).continuous_right.continuousAt
       (tendsto_nhdsWithin_mono_left Ioo_subset_Ioi_self f_lim')
-  -- now we can apply `has_fderiv_at_boundary_of_differentiable`
+  -- 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 has_fderiv_at_boundary_of_tendsto_fderiv t_diff t_conv t_open t_cont t_diff'
+    exact hasFDerivWithinAt_closure_of_tendsto_fderiv t_diff t_conv t_open t_cont t_diff'
   exact this.mono_of_mem (Icc_mem_nhdsWithin_Ici <| left_mem_Ico.2 ab)
-#align has_deriv_at_interval_left_endpoint_of_tendsto_deriv has_deriv_at_interval_left_endpoint_of_tendsto_deriv
+#align has_deriv_at_interval_left_endpoint_of_tendsto_deriv hasDerivWithinAt_Ici_of_tendsto_deriv
+
+@[deprecated (since := "2024-07-10")] alias has_deriv_at_interval_left_endpoint_of_tendsto_deriv :=
+  hasDerivWithinAt_Ici_of_tendsto_deriv
 
 /-- 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 has_deriv_at_interval_right_endpoint_of_tendsto_deriv {s : Set ℝ} {e : E} {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 `has_fderiv_at_boundary_of_differentiable`. 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. -/
+  /- 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_nhdsWithin_Iio_iff_exists_Ico_subset.1 hs
   let t := Ioo b a
   have ts : t ⊆ s := Subset.trans Ioo_subset_Ico_self sab
@@ -166,12 +173,15 @@ theorem has_deriv_at_interval_right_endpoint_of_tendsto_deriv {s : Set ℝ} {e :
     exact Tendsto.comp
       (isBoundedBilinearMap_smulRight : IsBoundedBilinearMap ℝ _).continuous_right.continuousAt
       (tendsto_nhdsWithin_mono_left Ioo_subset_Iio_self f_lim')
-  -- now we can apply `has_fderiv_at_boundary_of_differentiable`
+  -- 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 has_fderiv_at_boundary_of_tendsto_fderiv t_diff t_conv t_open t_cont t_diff'
+    exact hasFDerivWithinAt_closure_of_tendsto_fderiv t_diff t_conv t_open t_cont t_diff'
   exact this.mono_of_mem (Icc_mem_nhdsWithin_Iic <| right_mem_Ioc.2 ba)
-#align has_deriv_at_interval_right_endpoint_of_tendsto_deriv has_deriv_at_interval_right_endpoint_of_tendsto_deriv
+#align has_deriv_at_interval_right_endpoint_of_tendsto_deriv hasDerivWithinAt_Iic_of_tendsto_deriv
+
+@[deprecated (since := "2024-07-10")] alias has_deriv_at_interval_right_endpoint_of_tendsto_deriv :=
+  hasDerivWithinAt_Iic_of_tendsto_deriv
 
 /-- 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. -/
@@ -184,7 +194,7 @@ theorem hasDerivAt_of_hasDerivAt_of_ne {f g : ℝ → E} {x : ℝ}
     -- next line is the nontrivial bit of this proof, appealing to differentiability
     -- extension results.
     apply
-      has_deriv_at_interval_left_endpoint_of_tendsto_deriv diff hf.continuousWithinAt
+      hasDerivWithinAt_Ici_of_tendsto_deriv diff hf.continuousWithinAt
         self_mem_nhdsWithin
     have : Tendsto g (𝓝[>] x) (𝓝 (g x)) := tendsto_inf_left hg
     apply this.congr' _
@@ -197,7 +207,7 @@ theorem hasDerivAt_of_hasDerivAt_of_ne {f g : ℝ → E} {x : ℝ}
     -- next line is the nontrivial bit of this proof, appealing to differentiability
     -- extension results.
     apply
-      has_deriv_at_interval_right_endpoint_of_tendsto_deriv diff hf.continuousWithinAt
+      hasDerivWithinAt_Iic_of_tendsto_deriv diff hf.continuousWithinAt
         self_mem_nhdsWithin
     have : Tendsto g (𝓝[<] x) (𝓝 (g x)) := tendsto_inf_left hg
     apply this.congr' _