bump to nightly-2023-06-01-18

mathlib commit leanprover-community/mathlib@cca4078

Mathbin/Analysis/Analytic/Composition.lean

@@ -770,9 +770,9 @@ open FormalMultilinearSeries
 
 /-- If two functions `g` and `f` have power series `q` and `p` respectively at `f x` and `x`, then
 `g ∘ f` admits the power series `q.comp p` at `x`. -/
-theorem HasFpowerSeriesAt.comp {g : F → G} {f : E → F} {q : FormalMultilinearSeries 𝕜 F G}
-    {p : FormalMultilinearSeries 𝕜 E F} {x : E} (hg : HasFpowerSeriesAt g q (f x))
-    (hf : HasFpowerSeriesAt f p x) : HasFpowerSeriesAt (g ∘ f) (q.comp p) x :=
+theorem HasFPowerSeriesAt.comp {g : F → G} {f : E → F} {q : FormalMultilinearSeries 𝕜 F G}
+    {p : FormalMultilinearSeries 𝕜 E F} {x : E} (hg : HasFPowerSeriesAt g q (f x))
+    (hf : HasFPowerSeriesAt f p x) : HasFPowerSeriesAt (g ∘ f) (q.comp p) x :=
   by
   /- Consider `rf` and `rg` such that `f` and `g` have power series expansion on the disks
     of radius `rf` and `rg`. -/
@@ -899,7 +899,7 @@ theorem HasFpowerSeriesAt.comp {g : F → G} {f : E → F} {q : FormalMultilinea
     simp only [ContinuousMultilinearMap.sum_apply]
     rfl
   exact E
-#align has_fpower_series_at.comp HasFpowerSeriesAt.comp
+#align has_fpower_series_at.comp HasFPowerSeriesAt.comp
 
 /-- If two functions `g` and `f` are analytic respectively at `f x` and `x`, then `g ∘ f` is
 analytic at `x`. -/

Mathbin/Analysis/Analytic/IsolatedZeros.lean

@@ -73,39 +73,39 @@ theorem exists_hasSum_smul_of_apply_eq_zero (hs : HasSum (fun m => z ^ m • a m
 
 end HasSum
 
-namespace HasFpowerSeriesAt
+namespace HasFPowerSeriesAt
 
-theorem hasFpowerSeriesDslopeFslope (hp : HasFpowerSeriesAt f p z₀) :
-    HasFpowerSeriesAt (dslope f z₀) p.fslope z₀ :=
+theorem has_fpower_series_dslope_fslope (hp : HasFPowerSeriesAt f p z₀) :
+    HasFPowerSeriesAt (dslope f z₀) p.fslope z₀ :=
   by
   have hpd : deriv f z₀ = p.coeff 1 := hp.deriv
   have hp0 : p.coeff 0 = f z₀ := hp.coeff_zero 1
-  simp only [hasFpowerSeriesAt_iff, apply_eq_pow_smul_coeff, coeff_fslope] at hp ⊢
+  simp only [hasFPowerSeriesAt_iff, apply_eq_pow_smul_coeff, coeff_fslope] at hp ⊢
   refine' hp.mono fun x hx => _
   by_cases h : x = 0
   · convert hasSum_single 0 _ <;> intros <;> simp [*]
   · have hxx : ∀ n : ℕ, x⁻¹ * x ^ (n + 1) = x ^ n := fun n => by field_simp [h, pow_succ']
     suffices HasSum (fun n => x⁻¹ • x ^ (n + 1) • p.coeff (n + 1)) (x⁻¹ • (f (z₀ + x) - f z₀)) by
       simpa [dslope, slope, h, smul_smul, hxx] using this
     · simpa [hp0] using ((hasSum_nat_add_iff' 1).mpr hx).const_smul x⁻¹
-#align has_fpower_series_at.has_fpower_series_dslope_fslope HasFpowerSeriesAt.hasFpowerSeriesDslopeFslope
+#align has_fpower_series_at.has_fpower_series_dslope_fslope HasFPowerSeriesAt.has_fpower_series_dslope_fslope
 
-theorem hasFpowerSeriesIterateDslopeFslope (n : ℕ) (hp : HasFpowerSeriesAt f p z₀) :
-    HasFpowerSeriesAt ((swap dslope z₀^[n]) f) ((fslope^[n]) p) z₀ :=
+theorem has_fpower_series_iterate_dslope_fslope (n : ℕ) (hp : HasFPowerSeriesAt f p z₀) :
+    HasFPowerSeriesAt ((swap dslope z₀^[n]) f) ((fslope^[n]) p) z₀ :=
   by
   induction' n with n ih generalizing f p
   · exact hp
   · simpa using ih (has_fpower_series_dslope_fslope hp)
-#align has_fpower_series_at.has_fpower_series_iterate_dslope_fslope HasFpowerSeriesAt.hasFpowerSeriesIterateDslopeFslope
+#align has_fpower_series_at.has_fpower_series_iterate_dslope_fslope HasFPowerSeriesAt.has_fpower_series_iterate_dslope_fslope
 
-theorem iterate_dslope_fslope_ne_zero (hp : HasFpowerSeriesAt f p z₀) (h : p ≠ 0) :
+theorem iterate_dslope_fslope_ne_zero (hp : HasFPowerSeriesAt f p z₀) (h : p ≠ 0) :
     (swap dslope z₀^[p.order]) f z₀ ≠ 0 :=
   by
   rw [← coeff_zero (has_fpower_series_iterate_dslope_fslope p.order hp) 1]
   simpa [coeff_eq_zero] using apply_order_ne_zero h
-#align has_fpower_series_at.iterate_dslope_fslope_ne_zero HasFpowerSeriesAt.iterate_dslope_fslope_ne_zero
+#align has_fpower_series_at.iterate_dslope_fslope_ne_zero HasFPowerSeriesAt.iterate_dslope_fslope_ne_zero
 
-theorem eq_pow_order_mul_iterate_dslope (hp : HasFpowerSeriesAt f p z₀) :
+theorem eq_pow_order_mul_iterate_dslope (hp : HasFPowerSeriesAt f p z₀) :
     ∀ᶠ z in 𝓝 z₀, f z = (z - z₀) ^ p.order • (swap dslope z₀^[p.order]) f z :=
   by
   have hq := has_fpower_series_at_iff'.mp (has_fpower_series_iterate_dslope_fslope p.order hp)
@@ -116,22 +116,22 @@ theorem eq_pow_order_mul_iterate_dslope (hp : HasFpowerSeriesAt f p z₀) :
   convert hs1.symm
   simp only [coeff_iterate_fslope] at hx1 
   exact hx1.unique hs2
-#align has_fpower_series_at.eq_pow_order_mul_iterate_dslope HasFpowerSeriesAt.eq_pow_order_mul_iterate_dslope
+#align has_fpower_series_at.eq_pow_order_mul_iterate_dslope HasFPowerSeriesAt.eq_pow_order_mul_iterate_dslope
 
-theorem locally_ne_zero (hp : HasFpowerSeriesAt f p z₀) (h : p ≠ 0) : ∀ᶠ z in 𝓝[≠] z₀, f z ≠ 0 :=
+theorem locally_ne_zero (hp : HasFPowerSeriesAt f p z₀) (h : p ≠ 0) : ∀ᶠ z in 𝓝[≠] z₀, f z ≠ 0 :=
   by
   rw [eventually_nhdsWithin_iff]
   have h2 := (has_fpower_series_iterate_dslope_fslope p.order hp).ContinuousAt
   have h3 := h2.eventually_ne (iterate_dslope_fslope_ne_zero hp h)
   filter_upwards [eq_pow_order_mul_iterate_dslope hp, h3]with z e1 e2 e3
   simpa [e1, e2, e3] using pow_ne_zero p.order (sub_ne_zero.mpr e3)
-#align has_fpower_series_at.locally_ne_zero HasFpowerSeriesAt.locally_ne_zero
+#align has_fpower_series_at.locally_ne_zero HasFPowerSeriesAt.locally_ne_zero
 
-theorem locally_zero_iff (hp : HasFpowerSeriesAt f p z₀) : (∀ᶠ z in 𝓝 z₀, f z = 0) ↔ p = 0 :=
+theorem locally_zero_iff (hp : HasFPowerSeriesAt f p z₀) : (∀ᶠ z in 𝓝 z₀, f z = 0) ↔ p = 0 :=
   ⟨fun hf => hp.eq_zero_of_eventually hf, fun h => eventually_eq_zero (by rwa [h] at hp )⟩
-#align has_fpower_series_at.locally_zero_iff HasFpowerSeriesAt.locally_zero_iff
+#align has_fpower_series_at.locally_zero_iff HasFPowerSeriesAt.locally_zero_iff
 
-end HasFpowerSeriesAt
+end HasFPowerSeriesAt
 
 namespace AnalyticAt
 
@@ -143,7 +143,7 @@ theorem eventually_eq_zero_or_eventually_ne_zero (hf : AnalyticAt 𝕜 f z₀) :
   by
   rcases hf with ⟨p, hp⟩
   by_cases h : p = 0
-  · exact Or.inl (HasFpowerSeriesAt.eventually_eq_zero (by rwa [h] at hp ))
+  · exact Or.inl (HasFPowerSeriesAt.eventually_eq_zero (by rwa [h] at hp ))
   · exact Or.inr (hp.locally_ne_zero h)
 #align analytic_at.eventually_eq_zero_or_eventually_ne_zero AnalyticAt.eventually_eq_zero_or_eventually_ne_zero
 

Mathbin/Analysis/Analytic/Linear.lean

@@ -49,21 +49,21 @@ theorem fpowerSeries_radius (f : E →L[𝕜] F) (x : E) : (f.fpowerSeries x).ra
   (f.fpowerSeries x).radius_eq_top_of_forall_image_add_eq_zero 2 fun n => rfl
 #align continuous_linear_map.fpower_series_radius ContinuousLinearMap.fpowerSeries_radius
 
-protected theorem hasFpowerSeriesOnBall (f : E →L[𝕜] F) (x : E) :
-    HasFpowerSeriesOnBall f (f.fpowerSeries x) x ∞ :=
+protected theorem hasFPowerSeriesOnBall (f : E →L[𝕜] F) (x : E) :
+    HasFPowerSeriesOnBall f (f.fpowerSeries x) x ∞ :=
   { r_le := by simp
     r_pos := ENNReal.coe_lt_top
     HasSum := fun y _ =>
       (hasSum_nat_add_iff' 2).1 <| by simp [Finset.sum_range_succ, ← sub_sub, hasSum_zero] }
-#align continuous_linear_map.has_fpower_series_on_ball ContinuousLinearMap.hasFpowerSeriesOnBall
+#align continuous_linear_map.has_fpower_series_on_ball ContinuousLinearMap.hasFPowerSeriesOnBall
 
-protected theorem hasFpowerSeriesAt (f : E →L[𝕜] F) (x : E) :
-    HasFpowerSeriesAt f (f.fpowerSeries x) x :=
-  ⟨∞, f.HasFpowerSeriesOnBall x⟩
-#align continuous_linear_map.has_fpower_series_at ContinuousLinearMap.hasFpowerSeriesAt
+protected theorem hasFPowerSeriesAt (f : E →L[𝕜] F) (x : E) :
+    HasFPowerSeriesAt f (f.fpowerSeries x) x :=
+  ⟨∞, f.HasFPowerSeriesOnBall x⟩
+#align continuous_linear_map.has_fpower_series_at ContinuousLinearMap.hasFPowerSeriesAt
 
 protected theorem analyticAt (f : E →L[𝕜] F) (x : E) : AnalyticAt 𝕜 f x :=
-  (f.HasFpowerSeriesAt x).AnalyticAt
+  (f.HasFPowerSeriesAt x).AnalyticAt
 #align continuous_linear_map.analytic_at ContinuousLinearMap.analyticAt
 
 /-- Reinterpret a bilinear map `f : E →L[𝕜] F →L[𝕜] G` as a multilinear map
@@ -97,8 +97,8 @@ theorem fpowerSeriesBilinear_radius (f : E →L[𝕜] F →L[𝕜] G) (x : E ×
   (f.fpowerSeriesBilinear x).radius_eq_top_of_forall_image_add_eq_zero 3 fun n => rfl
 #align continuous_linear_map.fpower_series_bilinear_radius ContinuousLinearMap.fpowerSeriesBilinear_radius
 
-protected theorem hasFpowerSeriesOnBallBilinear (f : E →L[𝕜] F →L[𝕜] G) (x : E × F) :
-    HasFpowerSeriesOnBall (fun x : E × F => f x.1 x.2) (f.fpowerSeriesBilinear x) x ∞ :=
+protected theorem hasFPowerSeriesOnBall_bilinear (f : E →L[𝕜] F →L[𝕜] G) (x : E × F) :
+    HasFPowerSeriesOnBall (fun x : E × F => f x.1 x.2) (f.fpowerSeriesBilinear x) x ∞ :=
   { r_le := by simp
     r_pos := ENNReal.coe_lt_top
     HasSum := fun y _ =>
@@ -107,16 +107,16 @@ protected theorem hasFpowerSeriesOnBallBilinear (f : E →L[𝕜] F →L[𝕜] G
         simp only [Finset.sum_range_succ, Finset.sum_range_one, Prod.fst_add, Prod.snd_add,
           f.map_add_add]
         dsimp; simp only [add_comm, sub_self, hasSum_zero] }
-#align continuous_linear_map.has_fpower_series_on_ball_bilinear ContinuousLinearMap.hasFpowerSeriesOnBallBilinear
+#align continuous_linear_map.has_fpower_series_on_ball_bilinear ContinuousLinearMap.hasFPowerSeriesOnBall_bilinear
 
-protected theorem hasFpowerSeriesAtBilinear (f : E →L[𝕜] F →L[𝕜] G) (x : E × F) :
-    HasFpowerSeriesAt (fun x : E × F => f x.1 x.2) (f.fpowerSeriesBilinear x) x :=
-  ⟨∞, f.hasFpowerSeriesOnBallBilinear x⟩
-#align continuous_linear_map.has_fpower_series_at_bilinear ContinuousLinearMap.hasFpowerSeriesAtBilinear
+protected theorem hasFPowerSeriesAt_bilinear (f : E →L[𝕜] F →L[𝕜] G) (x : E × F) :
+    HasFPowerSeriesAt (fun x : E × F => f x.1 x.2) (f.fpowerSeriesBilinear x) x :=
+  ⟨∞, f.hasFPowerSeriesOnBall_bilinear x⟩
+#align continuous_linear_map.has_fpower_series_at_bilinear ContinuousLinearMap.hasFPowerSeriesAt_bilinear
 
 protected theorem analyticAt_bilinear (f : E →L[𝕜] F →L[𝕜] G) (x : E × F) :
     AnalyticAt 𝕜 (fun x : E × F => f x.1 x.2) x :=
-  (f.hasFpowerSeriesAtBilinear x).AnalyticAt
+  (f.hasFPowerSeriesAt_bilinear x).AnalyticAt
 #align continuous_linear_map.analytic_at_bilinear ContinuousLinearMap.analyticAt_bilinear
 
 end ContinuousLinearMap

Mathbin/Analysis/Analytic/Uniqueness.lean

@@ -55,7 +55,7 @@ theorem eqOn_zero_of_preconnected_of_eventuallyEq_zero_aux [CompleteSpace F] {f
   obtain ⟨y, yu, hxy⟩ : ∃ y ∈ u, edist x y < r / 2
   exact EMetric.mem_closure_iff.1 xu (r / 2) (ENNReal.half_pos hp.r_pos.ne')
   let q := p.change_origin (y - x)
-  have has_series : HasFpowerSeriesOnBall f q y (r / 2) :=
+  have has_series : HasFPowerSeriesOnBall f q y (r / 2) :=
     by
     have A : (‖y - x‖₊ : ℝ≥0∞) < r / 2 := by rwa [edist_comm, edist_eq_coe_nnnorm_sub] at hxy 
     have := hp.change_origin (A.trans_le ENNReal.half_le_self)
@@ -69,7 +69,7 @@ theorem eqOn_zero_of_preconnected_of_eventuallyEq_zero_aux [CompleteSpace F] {f
   have A : HasSum (fun n : ℕ => q n fun i : Fin n => z - y) (f z) := has_series.has_sum_sub hz
   have B : HasSum (fun n : ℕ => q n fun i : Fin n => z - y) 0 :=
     by
-    have : HasFpowerSeriesAt 0 q y := has_series.has_fpower_series_at.congr yu
+    have : HasFPowerSeriesAt 0 q y := has_series.has_fpower_series_at.congr yu
     convert hasSum_zero
     ext n
     exact this.apply_eq_zero n _

Mathbin/Analysis/Calculus/FderivAnalytic.lean

@@ -36,23 +36,23 @@ variable {p : FormalMultilinearSeries 𝕜 E F} {r : ℝ≥0∞}
 
 variable {f : E → F} {x : E} {s : Set E}
 
-theorem HasFpowerSeriesAt.hasStrictFDerivAt (h : HasFpowerSeriesAt f p x) :
+theorem HasFPowerSeriesAt.hasStrictFDerivAt (h : HasFPowerSeriesAt f p x) :
     HasStrictFDerivAt f (continuousMultilinearCurryFin1 𝕜 E F (p 1)) x :=
   by
   refine' h.is_O_image_sub_norm_mul_norm_sub.trans_is_o (is_o.of_norm_right _)
   refine' is_o_iff_exists_eq_mul.2 ⟨fun y => ‖y - (x, x)‖, _, eventually_eq.rfl⟩
   refine' (continuous_id.sub continuous_const).norm.tendsto' _ _ _
   rw [_root_.id, sub_self, norm_zero]
-#align has_fpower_series_at.has_strict_fderiv_at HasFpowerSeriesAt.hasStrictFDerivAt
+#align has_fpower_series_at.has_strict_fderiv_at HasFPowerSeriesAt.hasStrictFDerivAt
 
-theorem HasFpowerSeriesAt.hasFDerivAt (h : HasFpowerSeriesAt f p x) :
+theorem HasFPowerSeriesAt.hasFDerivAt (h : HasFPowerSeriesAt f p x) :
     HasFDerivAt f (continuousMultilinearCurryFin1 𝕜 E F (p 1)) x :=
   h.HasStrictFDerivAt.HasFDerivAt
-#align has_fpower_series_at.has_fderiv_at HasFpowerSeriesAt.hasFDerivAt
+#align has_fpower_series_at.has_fderiv_at HasFPowerSeriesAt.hasFDerivAt
 
-theorem HasFpowerSeriesAt.differentiableAt (h : HasFpowerSeriesAt f p x) : DifferentiableAt 𝕜 f x :=
+theorem HasFPowerSeriesAt.differentiableAt (h : HasFPowerSeriesAt f p x) : DifferentiableAt 𝕜 f x :=
   h.HasFDerivAt.DifferentiableAt
-#align has_fpower_series_at.differentiable_at HasFpowerSeriesAt.differentiableAt
+#align has_fpower_series_at.differentiable_at HasFPowerSeriesAt.differentiableAt
 
 theorem AnalyticAt.differentiableAt : AnalyticAt 𝕜 f x → DifferentiableAt 𝕜 f x
   | ⟨p, hp⟩ => hp.DifferentiableAt
@@ -62,42 +62,42 @@ theorem AnalyticAt.differentiableWithinAt (h : AnalyticAt 𝕜 f x) : Differenti
   h.DifferentiableAt.DifferentiableWithinAt
 #align analytic_at.differentiable_within_at AnalyticAt.differentiableWithinAt
 
-theorem HasFpowerSeriesAt.fderiv_eq (h : HasFpowerSeriesAt f p x) :
+theorem HasFPowerSeriesAt.fderiv_eq (h : HasFPowerSeriesAt f p x) :
     fderiv 𝕜 f x = continuousMultilinearCurryFin1 𝕜 E F (p 1) :=
   h.HasFDerivAt.fderiv
-#align has_fpower_series_at.fderiv_eq HasFpowerSeriesAt.fderiv_eq
+#align has_fpower_series_at.fderiv_eq HasFPowerSeriesAt.fderiv_eq
 
-theorem HasFpowerSeriesOnBall.differentiableOn [CompleteSpace F]
-    (h : HasFpowerSeriesOnBall f p x r) : DifferentiableOn 𝕜 f (EMetric.ball x r) := fun y hy =>
+theorem HasFPowerSeriesOnBall.differentiableOn [CompleteSpace F]
+    (h : HasFPowerSeriesOnBall f p x r) : DifferentiableOn 𝕜 f (EMetric.ball x r) := fun y hy =>
   (h.analyticAt_of_mem hy).DifferentiableWithinAt
-#align has_fpower_series_on_ball.differentiable_on HasFpowerSeriesOnBall.differentiableOn
+#align has_fpower_series_on_ball.differentiable_on HasFPowerSeriesOnBall.differentiableOn
 
 theorem AnalyticOn.differentiableOn (h : AnalyticOn 𝕜 f s) : DifferentiableOn 𝕜 f s := fun y hy =>
   (h y hy).DifferentiableWithinAt
 #align analytic_on.differentiable_on AnalyticOn.differentiableOn
 
-theorem HasFpowerSeriesOnBall.hasFDerivAt [CompleteSpace F] (h : HasFpowerSeriesOnBall f p x r)
+theorem HasFPowerSeriesOnBall.hasFDerivAt [CompleteSpace F] (h : HasFPowerSeriesOnBall f p x r)
     {y : E} (hy : (‖y‖₊ : ℝ≥0∞) < r) :
     HasFDerivAt f (continuousMultilinearCurryFin1 𝕜 E F (p.changeOrigin y 1)) (x + y) :=
-  (h.changeOrigin hy).HasFpowerSeriesAt.HasFDerivAt
-#align has_fpower_series_on_ball.has_fderiv_at HasFpowerSeriesOnBall.hasFDerivAt
+  (h.changeOrigin hy).HasFPowerSeriesAt.HasFDerivAt
+#align has_fpower_series_on_ball.has_fderiv_at HasFPowerSeriesOnBall.hasFDerivAt
 
-theorem HasFpowerSeriesOnBall.fderiv_eq [CompleteSpace F] (h : HasFpowerSeriesOnBall f p x r)
+theorem HasFPowerSeriesOnBall.fderiv_eq [CompleteSpace F] (h : HasFPowerSeriesOnBall f p x r)
     {y : E} (hy : (‖y‖₊ : ℝ≥0∞) < r) :
     fderiv 𝕜 f (x + y) = continuousMultilinearCurryFin1 𝕜 E F (p.changeOrigin y 1) :=
   (h.HasFDerivAt hy).fderiv
-#align has_fpower_series_on_ball.fderiv_eq HasFpowerSeriesOnBall.fderiv_eq
+#align has_fpower_series_on_ball.fderiv_eq HasFPowerSeriesOnBall.fderiv_eq
 
 /-- If a function has a power series on a ball, then so does its derivative. -/
-theorem HasFpowerSeriesOnBall.fderiv [CompleteSpace F] (h : HasFpowerSeriesOnBall f p x r) :
-    HasFpowerSeriesOnBall (fderiv 𝕜 f)
+theorem HasFPowerSeriesOnBall.fderiv [CompleteSpace F] (h : HasFPowerSeriesOnBall f p x r) :
+    HasFPowerSeriesOnBall (fderiv 𝕜 f)
       ((continuousMultilinearCurryFin1 𝕜 E F :
             (E[×1]→L[𝕜] F) →L[𝕜] E →L[𝕜] F).compFormalMultilinearSeries
         (p.changeOriginSeries 1))
       x r :=
   by
   suffices A :
-    HasFpowerSeriesOnBall
+    HasFPowerSeriesOnBall
       (fun z => continuousMultilinearCurryFin1 𝕜 E F (p.change_origin (z - x) 1))
       ((continuousMultilinearCurryFin1 𝕜 E F :
             (E[×1]→L[𝕜] F) →L[𝕜] E →L[𝕜] F).compFormalMultilinearSeries
@@ -109,16 +109,16 @@ theorem HasFpowerSeriesOnBall.fderiv [CompleteSpace F] (h : HasFpowerSeriesOnBal
     rw [← h.fderiv_eq, add_sub_cancel'_right]
     simpa only [edist_eq_coe_nnnorm_sub, EMetric.mem_ball] using hz
   suffices B :
-    HasFpowerSeriesOnBall (fun z => p.change_origin (z - x) 1) (p.change_origin_series 1) x r
+    HasFPowerSeriesOnBall (fun z => p.change_origin (z - x) 1) (p.change_origin_series 1) x r
   exact
     (continuousMultilinearCurryFin1 𝕜 E
-              F).toContinuousLinearEquiv.toContinuousLinearMap.compHasFpowerSeriesOnBall
+              F).toContinuousLinearEquiv.toContinuousLinearMap.comp_hasFPowerSeriesOnBall
       B
   simpa using
     ((p.has_fpower_series_on_ball_change_origin 1 (h.r_pos.trans_le h.r_le)).mono h.r_pos
           h.r_le).comp_sub
       x
-#align has_fpower_series_on_ball.fderiv HasFpowerSeriesOnBall.fderiv
+#align has_fpower_series_on_ball.fderiv HasFPowerSeriesOnBall.fderiv
 
 /-- If a function is analytic on a set `s`, so is its Fréchet derivative. -/
 theorem AnalyticOn.fderiv [CompleteSpace F] (h : AnalyticOn 𝕜 f s) : AnalyticOn 𝕜 (fderiv 𝕜 f) s :=
@@ -168,20 +168,20 @@ variable {p : FormalMultilinearSeries 𝕜 𝕜 F} {r : ℝ≥0∞}
 
 variable {f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜}
 
-protected theorem HasFpowerSeriesAt.hasStrictDerivAt (h : HasFpowerSeriesAt f p x) :
+protected theorem HasFPowerSeriesAt.hasStrictDerivAt (h : HasFPowerSeriesAt f p x) :
     HasStrictDerivAt f (p 1 fun _ => 1) x :=
   h.HasStrictFDerivAt.HasStrictDerivAt
-#align has_fpower_series_at.has_strict_deriv_at HasFpowerSeriesAt.hasStrictDerivAt
+#align has_fpower_series_at.has_strict_deriv_at HasFPowerSeriesAt.hasStrictDerivAt
 
-protected theorem HasFpowerSeriesAt.hasDerivAt (h : HasFpowerSeriesAt f p x) :
+protected theorem HasFPowerSeriesAt.hasDerivAt (h : HasFPowerSeriesAt f p x) :
     HasDerivAt f (p 1 fun _ => 1) x :=
   h.HasStrictDerivAt.HasDerivAt
-#align has_fpower_series_at.has_deriv_at HasFpowerSeriesAt.hasDerivAt
+#align has_fpower_series_at.has_deriv_at HasFPowerSeriesAt.hasDerivAt
 
-protected theorem HasFpowerSeriesAt.deriv (h : HasFpowerSeriesAt f p x) :
+protected theorem HasFPowerSeriesAt.deriv (h : HasFPowerSeriesAt f p x) :
     deriv f x = p 1 fun _ => 1 :=
   h.HasDerivAt.deriv
-#align has_fpower_series_at.deriv HasFpowerSeriesAt.deriv
+#align has_fpower_series_at.deriv HasFPowerSeriesAt.deriv
 
 /-- If a function is analytic on a set `s`, so is its derivative. -/
 theorem AnalyticOn.deriv [CompleteSpace F] (h : AnalyticOn 𝕜 f s) : AnalyticOn 𝕜 (deriv f) s :=