chore: rename AnalyticOn to AnalyticOnNhd, and AnalyticWithinOn…

… to `AnalyticOn` (#17146)

For coherence with `ContinuousOn`, `DifferentiableOn` and so on. See Zulip https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/Integrate.20analytic.20functions.20in.20the.20smooth.20hierarchy/near/471899268

This is 90% renaming all `AnalyticOn` to `AnalyticOnNhd` and then `AnalyticWithinOn` to `AnalyticOn`, and then adding deprecations. The 10% remaining is, when adding a deprecation `alias AnalyticOn.foo := AnalyticOnNhd.foo`, I noticed that `AnalyticOn.foo` would definitely make sense (with the new meaning of `AnalyticOn`), so I added the lemma with the new meaning instead of deprecating the old one.

Archive/Hairer.lean

@@ -100,7 +100,7 @@ lemma inj_L : Injective (L ι) :=
         fun g hg _h2g g_supp ↦ by
           simpa [mul_comm (g _), L] using congr($hp ⟨g, g_supp.trans ball_subset_closedBall, hg⟩)
     simp_rw [MvPolynomial.funext_iff, map_zero]
-    refine fun x ↦ AnalyticOn.eval_linearMap (EuclideanSpace.equiv ι ℝ).toLinearMap p
+    refine fun x ↦ AnalyticOnNhd.eval_linearMap (EuclideanSpace.equiv ι ℝ).toLinearMap p
       |>.eqOn_zero_of_preconnected_of_eventuallyEq_zero
       (preconnectedSpace_iff_univ.mp inferInstance) (z₀ := 0) trivial
       (Filter.mem_of_superset (Metric.ball_mem_nhds 0 zero_lt_one) ?_) trivial

Mathlib/Analysis/Analytic/Basic.lean

@@ -49,13 +49,13 @@ Additionally, let `f` be a function from `E` to `F`.
 * `HasFPowerSeriesAt f p x`: on some ball of center `x` with positive radius, holds
   `HasFPowerSeriesOnBall f p x r`.
 * `AnalyticAt 𝕜 f x`: there exists a power series `p` such that holds `HasFPowerSeriesAt f p x`.
-* `AnalyticOn 𝕜 f s`: the function `f` is analytic at every point of `s`.
+* `AnalyticOnNhd 𝕜 f s`: the function `f` is analytic at every point of `s`.
 
-We also define versions of `HasFPowerSeriesOnBall`, `AnalyticAt`, and `AnalyticOn` restricted to a
-set, similar to `ContinuousWithinAt`. See `Mathlib.Analysis.Analytic.Within` for basic properties.
+We also define versions of `HasFPowerSeriesOnBall`, `AnalyticAt`, and `AnalyticOnNhd` restricted to
+a set, similar to `ContinuousWithinAt`. See `Mathlib.Analysis.Analytic.Within` for basic properties.
 
 * `AnalyticWithinAt 𝕜 f s x` means a power series at `x` converges to `f` on `𝓝[s ∪ {x}] x`.
-* `AnalyticWithinOn 𝕜 f s t` means `∀ x ∈ t, AnalyticWithinAt 𝕜 f s x`.
+* `AnalyticOn 𝕜 f s t` means `∀ x ∈ t, AnalyticWithinAt 𝕜 f s x`.
 
 We develop the basic properties of these notions, notably:
 * If a function admits a power series, it is continuous (see
@@ -384,14 +384,17 @@ def AnalyticWithinAt (f : E → F) (s : Set E) (x : E) : Prop :=
 
 /-- Given a function `f : E → F`, we say that `f` is analytic on a set `s` if it is analytic around
 every point of `s`. -/
-def AnalyticOn (f : E → F) (s : Set E) :=
+def AnalyticOnNhd (f : E → F) (s : Set E) :=
   ∀ x, x ∈ s → AnalyticAt 𝕜 f x
 
 /-- `f` is analytic within `s` if it is analytic within `s` at each point of `t`.  Note that
-this is weaker than `AnalyticOn 𝕜 f s`, as `f` is allowed to be arbitrary outside `s`. -/
-def AnalyticWithinOn (f : E → F) (s : Set E) : Prop :=
+this is weaker than `AnalyticOnNhd 𝕜 f s`, as `f` is allowed to be arbitrary outside `s`. -/
+def AnalyticOn (f : E → F) (s : Set E) : Prop :=
   ∀ x ∈ s, AnalyticWithinAt 𝕜 f s x
 
+@[deprecated (since := "2024-09-26")]
+alias AnalyticWithinOn := AnalyticOn
+
 /-!
 ### `HasFPowerSeriesOnBall` and `HasFPowerSeriesWithinOnBall`
 -/
@@ -612,9 +615,12 @@ theorem HasFPowerSeriesAt.coeff_zero (hf : HasFPowerSeriesAt f pf x) (v : Fin 0
     AnalyticWithinAt 𝕜 f univ x ↔ AnalyticAt 𝕜 f x := by
   simp [AnalyticWithinAt, AnalyticAt]
 
-@[simp] lemma analyticWithinOn_univ {f : E → F} :
-    AnalyticWithinOn 𝕜 f univ ↔ AnalyticOn 𝕜 f univ := by
-  simp only [AnalyticWithinOn, analyticWithinAt_univ, AnalyticOn]
+@[simp] lemma analyticOn_univ {f : E → F} :
+    AnalyticOn 𝕜 f univ ↔ AnalyticOnNhd 𝕜 f univ := by
+  simp only [AnalyticOn, analyticWithinAt_univ, AnalyticOnNhd]
+
+@[deprecated (since := "2024-09-26")]
+alias analyticWithinOn_univ := analyticOn_univ
 
 lemma AnalyticWithinAt.mono (hf : AnalyticWithinAt 𝕜 f s x) (h : t ⊆ s) :
     AnalyticWithinAt 𝕜 f t x := by
@@ -625,54 +631,79 @@ lemma AnalyticAt.analyticWithinAt (hf : AnalyticAt 𝕜 f x) : AnalyticWithinAt
   rw [← analyticWithinAt_univ] at hf
   apply hf.mono (subset_univ _)
 
-lemma AnalyticOn.analyticWithinOn (hf : AnalyticOn 𝕜 f s) : AnalyticWithinOn 𝕜 f s :=
+lemma AnalyticOnNhd.analyticOn (hf : AnalyticOnNhd 𝕜 f s) : AnalyticOn 𝕜 f s :=
   fun x hx ↦ (hf x hx).analyticWithinAt
 
+@[deprecated (since := "2024-09-26")]
+alias AnalyticOn.analyticWithinOn := AnalyticOnNhd.analyticOn
+
 lemma AnalyticWithinAt.congr_of_eventuallyEq {f g : E → F} {s : Set E} {x : E}
     (hf : AnalyticWithinAt 𝕜 f s x) (hs : g =ᶠ[𝓝[s] x] f) (hx : g x = f x) :
     AnalyticWithinAt 𝕜 g s x := by
   rcases hf with ⟨p, hp⟩
   exact ⟨p, hp.congr hs hx⟩
 
+lemma AnalyticWithinAt.congr_of_eventuallyEq_insert {f g : E → F} {s : Set E} {x : E}
+    (hf : AnalyticWithinAt 𝕜 f s x) (hs : g =ᶠ[𝓝[insert x s] x] f) :
+    AnalyticWithinAt 𝕜 g s x := by
+  apply hf.congr_of_eventuallyEq (nhdsWithin_mono x (subset_insert x s) hs)
+  apply mem_of_mem_nhdsWithin (mem_insert x s) hs
+
 lemma AnalyticWithinAt.congr {f g : E → F} {s : Set E} {x : E}
     (hf : AnalyticWithinAt 𝕜 f s x) (hs : EqOn g f s) (hx : g x = f x) :
     AnalyticWithinAt 𝕜 g s x :=
   hf.congr_of_eventuallyEq hs.eventuallyEq_nhdsWithin hx
 
-lemma AnalyticWithinOn.congr {f g : E → F} {s : Set E}
-    (hf : AnalyticWithinOn 𝕜 f s) (hs : EqOn g f s) :
-    AnalyticWithinOn 𝕜 g s :=
+lemma AnalyticOn.congr {f g : E → F} {s : Set E}
+    (hf : AnalyticOn 𝕜 f s) (hs : EqOn g f s) :
+    AnalyticOn 𝕜 g s :=
   fun x m ↦ (hf x m).congr hs (hs m)
 
+@[deprecated (since := "2024-09-26")]
+alias AnalyticWithinOn.congr := AnalyticOn.congr
+
 theorem AnalyticAt.congr (hf : AnalyticAt 𝕜 f x) (hg : f =ᶠ[𝓝 x] g) : AnalyticAt 𝕜 g x :=
   let ⟨_, hpf⟩ := hf
   (hpf.congr hg).analyticAt
 
 theorem analyticAt_congr (h : f =ᶠ[𝓝 x] g) : AnalyticAt 𝕜 f x ↔ AnalyticAt 𝕜 g x :=
   ⟨fun hf ↦ hf.congr h, fun hg ↦ hg.congr h.symm⟩
 
-theorem AnalyticOn.mono {s t : Set E} (hf : AnalyticOn 𝕜 f t) (hst : s ⊆ t) : AnalyticOn 𝕜 f s :=
+theorem AnalyticOnNhd.mono {s t : Set E} (hf : AnalyticOnNhd 𝕜 f t) (hst : s ⊆ t) :
+    AnalyticOnNhd 𝕜 f s :=
   fun z hz => hf z (hst hz)
 
-theorem AnalyticOn.congr' (hf : AnalyticOn 𝕜 f s) (hg : f =ᶠ[𝓝ˢ s] g) :
-    AnalyticOn 𝕜 g s :=
+theorem AnalyticOnNhd.congr' (hf : AnalyticOnNhd 𝕜 f s) (hg : f =ᶠ[𝓝ˢ s] g) :
+    AnalyticOnNhd 𝕜 g s :=
   fun z hz => (hf z hz).congr (mem_nhdsSet_iff_forall.mp hg z hz)
 
-theorem analyticOn_congr' (h : f =ᶠ[𝓝ˢ s] g) : AnalyticOn 𝕜 f s ↔ AnalyticOn 𝕜 g s :=
+@[deprecated (since := "2024-09-26")]
+alias AnalyticOn.congr' := AnalyticOnNhd.congr'
+
+theorem analyticOnNhd_congr' (h : f =ᶠ[𝓝ˢ s] g) : AnalyticOnNhd 𝕜 f s ↔ AnalyticOnNhd 𝕜 g s :=
   ⟨fun hf => hf.congr' h, fun hg => hg.congr' h.symm⟩
 
-theorem AnalyticOn.congr (hs : IsOpen s) (hf : AnalyticOn 𝕜 f s) (hg : s.EqOn f g) :
-    AnalyticOn 𝕜 g s :=
+@[deprecated (since := "2024-09-26")]
+alias analyticOn_congr' := analyticOnNhd_congr'
+
+theorem AnalyticOnNhd.congr (hs : IsOpen s) (hf : AnalyticOnNhd 𝕜 f s) (hg : s.EqOn f g) :
+    AnalyticOnNhd 𝕜 g s :=
   hf.congr' <| mem_nhdsSet_iff_forall.mpr
     (fun _ hz => eventuallyEq_iff_exists_mem.mpr ⟨s, hs.mem_nhds hz, hg⟩)
 
-theorem analyticOn_congr (hs : IsOpen s) (h : s.EqOn f g) : AnalyticOn 𝕜 f s ↔
-    AnalyticOn 𝕜 g s := ⟨fun hf => hf.congr hs h, fun hg => hg.congr hs h.symm⟩
+theorem analyticOnNhd_congr (hs : IsOpen s) (h : s.EqOn f g) : AnalyticOnNhd 𝕜 f s ↔
+    AnalyticOnNhd 𝕜 g s := ⟨fun hf => hf.congr hs h, fun hg => hg.congr hs h.symm⟩
 
-lemma AnalyticWithinOn.mono {f : E → F} {s t : Set E} (h : AnalyticWithinOn 𝕜 f t)
-    (hs : s ⊆ t) : AnalyticWithinOn 𝕜 f s :=
+@[deprecated (since := "2024-09-26")]
+alias analyticOn_congr := analyticOnNhd_congr
+
+lemma AnalyticOn.mono {f : E → F} {s t : Set E} (h : AnalyticOn 𝕜 f t)
+    (hs : s ⊆ t) : AnalyticOn 𝕜 f s :=
   fun _ m ↦ (h _ (hs m)).mono hs
 
+@[deprecated (since := "2024-09-26")]
+alias AnalyticWithinOn.mono := AnalyticOn.mono
+
 /-!
 ### Composition with linear maps
 -/
@@ -691,12 +722,16 @@ theorem ContinuousLinearMap.comp_hasFPowerSeriesOnBall (g : F →L[𝕜] G)
 
 /-- If a function `f` is analytic on a set `s` and `g` is linear, then `g ∘ f` is analytic
 on `s`. -/
-theorem ContinuousLinearMap.comp_analyticOn {s : Set E} (g : F →L[𝕜] G) (h : AnalyticOn 𝕜 f s) :
-    AnalyticOn 𝕜 (g ∘ f) s := by
+theorem ContinuousLinearMap.comp_analyticOnNhd
+    {s : Set E} (g : F →L[𝕜] G) (h : AnalyticOnNhd 𝕜 f s) :
+    AnalyticOnNhd 𝕜 (g ∘ f) s := by
   rintro x hx
   rcases h x hx with ⟨p, r, hp⟩
   exact ⟨g.compFormalMultilinearSeries p, r, g.comp_hasFPowerSeriesOnBall hp⟩
 
+@[deprecated (since := "2024-09-26")]
+alias ContinuousLinearMap.comp_analyticOn := ContinuousLinearMap.comp_analyticOnNhd
+
 /-!
 ### Relation between analytic function and the partial sums of its power series
 -/
@@ -1164,17 +1199,24 @@ protected theorem AnalyticAt.continuousAt (hf : AnalyticAt 𝕜 f x) : Continuou
   let ⟨_, hp⟩ := hf
   hp.continuousAt
 
-protected theorem AnalyticOn.continuousOn {s : Set E} (hf : AnalyticOn 𝕜 f s) : ContinuousOn f s :=
+protected theorem AnalyticOnNhd.continuousOn {s : Set E} (hf : AnalyticOnNhd 𝕜 f s) :
+    ContinuousOn f s :=
   fun x hx => (hf x hx).continuousAt.continuousWithinAt
 
-protected lemma AnalyticWithinOn.continuousOn {f : E → F} {s : Set E} (h : AnalyticWithinOn 𝕜 f s) :
+protected lemma AnalyticOn.continuousOn {f : E → F} {s : Set E} (h : AnalyticOn 𝕜 f s) :
     ContinuousOn f s :=
   fun x m ↦ (h x m).continuousWithinAt
 
+@[deprecated (since := "2024-09-26")]
+alias AnalyticWithinOn.continuousOn := AnalyticOn.continuousOn
+
 /-- Analytic everywhere implies continuous -/
-theorem AnalyticOn.continuous {f : E → F} (fa : AnalyticOn 𝕜 f univ) : Continuous f := by
+theorem AnalyticOnNhd.continuous {f : E → F} (fa : AnalyticOnNhd 𝕜 f univ) : Continuous f := by
   rw [continuous_iff_continuousOn_univ]; exact fa.continuousOn
 
+@[deprecated (since := "2024-09-26")]
+alias AnalyticOn.continuous := AnalyticOnNhd.continuous
+
 /-- In a complete space, the sum of a converging power series `p` admits `p` as a power series.
 This is not totally obvious as we need to check the convergence of the series. -/
 protected theorem FormalMultilinearSeries.hasFPowerSeriesOnBall [CompleteSpace F]

Mathlib/Analysis/Analytic/CPolynomial.lean

@@ -29,7 +29,7 @@ for `n : ℕ`, and let `f` be a function from `E` to `F`.
 We develop the basic properties of these notions, notably:
 * If a function is continuously polynomial, then it is analytic, see
   `HasFiniteFPowerSeriesOnBall.hasFPowerSeriesOnBall`, `HasFiniteFPowerSeriesAt.hasFPowerSeriesAt`,
-  `CPolynomialAt.analyticAt` and `CPolynomialOn.analyticOn`.
+  `CPolynomialAt.analyticAt` and `CPolynomialOn.analyticOnNhd`.
 * The sum of a finite formal power series with positive radius is well defined on the whole space,
   see `FormalMultilinearSeries.hasFiniteFPowerSeriesOnBall_of_finite`.
 * If a function admits a finite power series in a ball, then it is continuously polynomial at
@@ -116,9 +116,16 @@ theorem CPolynomialAt.analyticAt (hf : CPolynomialAt 𝕜 f x) : AnalyticAt 𝕜
   let ⟨p, _, hp⟩ := hf
   ⟨p, hp.toHasFPowerSeriesAt⟩
 
-theorem CPolynomialOn.analyticOn {s : Set E} (hf : CPolynomialOn 𝕜 f s) : AnalyticOn 𝕜 f s :=
+theorem CPolynomialAt.analyticWithinAt {s : Set E} (hf : CPolynomialAt 𝕜 f x) :
+    AnalyticWithinAt 𝕜 f s x :=
+  hf.analyticAt.analyticWithinAt
+
+theorem CPolynomialOn.analyticOnNhd {s : Set E} (hf : CPolynomialOn 𝕜 f s) : AnalyticOnNhd 𝕜 f s :=
   fun x hx ↦ (hf x hx).analyticAt
 
+theorem CPolynomialOn.analyticOn {s : Set E} (hf : CPolynomialOn 𝕜 f s) : AnalyticOn 𝕜 f s :=
+  hf.analyticOnNhd.analyticOn
+
 theorem HasFiniteFPowerSeriesOnBall.congr (hf : HasFiniteFPowerSeriesOnBall f p x n r)
     (hg : EqOn f g (EMetric.ball x r)) : HasFiniteFPowerSeriesOnBall g p x n r :=
   ⟨hf.1.congr hg, hf.finite⟩
@@ -335,7 +342,7 @@ protected theorem CPolynomialAt.continuousAt (hf : CPolynomialAt 𝕜 f x) : Con
 
 protected theorem CPolynomialOn.continuousOn {s : Set E} (hf : CPolynomialOn 𝕜 f s) :
     ContinuousOn f s :=
-  hf.analyticOn.continuousOn
+  hf.analyticOnNhd.continuousOn
 
 /-- Continuously polynomial everywhere implies continuous -/
 theorem CPolynomialOn.continuous {f : E → F} (fa : CPolynomialOn 𝕜 f univ) : Continuous f := by
@@ -571,10 +578,12 @@ lemma cpolynomialAt  : CPolynomialAt 𝕜 f x :=
 
 lemma cpolyomialOn : CPolynomialOn 𝕜 f s := fun _ _ ↦ f.cpolynomialAt
 
-lemma analyticOn : AnalyticOn 𝕜 f s := f.cpolyomialOn.analyticOn
+lemma analyticOnNhd : AnalyticOnNhd 𝕜 f s := f.cpolyomialOn.analyticOnNhd
+
+lemma analyticOn : AnalyticOn 𝕜 f s := f.analyticOnNhd.analyticOn
 
-lemma analyticWithinOn : AnalyticWithinOn 𝕜 f s :=
-  f.analyticOn.analyticWithinOn
+@[deprecated (since := "2024-09-26")]
+alias analyticWithinOn := analyticOn
 
 lemma analyticAt : AnalyticAt 𝕜 f x := f.cpolynomialAt.analyticAt
 
@@ -624,12 +633,16 @@ lemma cpolyomialOn_uncurry_of_multilinear :
     CPolynomialOn 𝕜 (fun (p : G × (Π i, Em i)) ↦ f p.1 p.2) s :=
   fun _ _ ↦ f.cpolynomialAt_uncurry_of_multilinear
 
-lemma analyticOn_uncurry_of_multilinear : AnalyticOn 𝕜 (fun (p : G × (Π i, Em i)) ↦ f p.1 p.2) s :=
-  f.cpolyomialOn_uncurry_of_multilinear.analyticOn
+lemma analyticOnNhd_uncurry_of_multilinear :
+    AnalyticOnNhd 𝕜 (fun (p : G × (Π i, Em i)) ↦ f p.1 p.2) s :=
+  f.cpolyomialOn_uncurry_of_multilinear.analyticOnNhd
+
+lemma analyticOn_uncurry_of_multilinear :
+    AnalyticOn 𝕜 (fun (p : G × (Π i, Em i)) ↦ f p.1 p.2) s :=
+  f.analyticOnNhd_uncurry_of_multilinear.analyticOn
 
-lemma analyticWithinOn_uncurry_of_multilinear :
-    AnalyticWithinOn 𝕜 (fun (p : G × (Π i, Em i)) ↦ f p.1 p.2) s :=
-  f.analyticOn_uncurry_of_multilinear.analyticWithinOn
+@[deprecated (since := "2024-09-26")]
+alias analyticWithinOn_uncurry_of_multilinear := analyticOn_uncurry_of_multilinear
 
 lemma analyticAt_uncurry_of_multilinear : AnalyticAt 𝕜 (fun (p : G × (Π i, Em i)) ↦ f p.1 p.2) x :=
   f.cpolynomialAt_uncurry_of_multilinear.analyticAt
@@ -640,11 +653,11 @@ lemma analyticWithinAt_uncurry_of_multilinear :
 
 lemma continuousOn_uncurry_of_multilinear :
     ContinuousOn (fun (p : G × (Π i, Em i)) ↦ f p.1 p.2) s :=
-  f.analyticOn_uncurry_of_multilinear.continuousOn
+  f.analyticOnNhd_uncurry_of_multilinear.continuousOn
 
 lemma continuous_uncurry_of_multilinear :
     Continuous (fun (p : G × (Π i, Em i)) ↦ f p.1 p.2) :=
-  f.analyticOn_uncurry_of_multilinear.continuous
+  f.analyticOnNhd_uncurry_of_multilinear.continuous
 
 lemma continuousAt_uncurry_of_multilinear :
     ContinuousAt (fun (p : G × (Π i, Em i)) ↦ f p.1 p.2) x :=

Mathlib/Analysis/Analytic/ChangeOrigin.lean

@@ -318,10 +318,13 @@ theorem HasFPowerSeriesOnBall.analyticAt_of_mem (hf : HasFPowerSeriesOnBall f p
   rw [add_sub_cancel] at this
   exact this.analyticAt
 
-theorem HasFPowerSeriesOnBall.analyticOn (hf : HasFPowerSeriesOnBall f p x r) :
-    AnalyticOn 𝕜 f (EMetric.ball x r) :=
+theorem HasFPowerSeriesOnBall.analyticOnNhd (hf : HasFPowerSeriesOnBall f p x r) :
+    AnalyticOnNhd 𝕜 f (EMetric.ball x r) :=
   fun _y hy => hf.analyticAt_of_mem hy
 
+@[deprecated (since := "2024-09-26")]
+alias HasFPowerSeriesOnBall.analyticOn := HasFPowerSeriesOnBall.analyticOnNhd
+
 variable (𝕜 f) in
 /-- For any function `f` from a normed vector space to a Banach space, the set of points `x` such
 that `f` is analytic at `x` is open. -/
@@ -334,13 +337,19 @@ theorem AnalyticAt.eventually_analyticAt (h : AnalyticAt 𝕜 f x) :
     ∀ᶠ y in 𝓝 x, AnalyticAt 𝕜 f y :=
   (isOpen_analyticAt 𝕜 f).mem_nhds h
 
-theorem AnalyticAt.exists_mem_nhds_analyticOn (h : AnalyticAt 𝕜 f x) :
-    ∃ s ∈ 𝓝 x, AnalyticOn 𝕜 f s :=
+theorem AnalyticAt.exists_mem_nhds_analyticOnNhd (h : AnalyticAt 𝕜 f x) :
+    ∃ s ∈ 𝓝 x, AnalyticOnNhd 𝕜 f s :=
   h.eventually_analyticAt.exists_mem
 
+@[deprecated (since := "2024-09-26")]
+alias AnalyticAt.exists_mem_nhds_analyticOn := AnalyticAt.exists_mem_nhds_analyticOnNhd
+
 /-- If we're analytic at a point, we're analytic in a nonempty ball -/
-theorem AnalyticAt.exists_ball_analyticOn (h : AnalyticAt 𝕜 f x) :
-    ∃ r : ℝ, 0 < r ∧ AnalyticOn 𝕜 f (Metric.ball x r) :=
+theorem AnalyticAt.exists_ball_analyticOnNhd (h : AnalyticAt 𝕜 f x) :
+    ∃ r : ℝ, 0 < r ∧ AnalyticOnNhd 𝕜 f (Metric.ball x r) :=
   Metric.isOpen_iff.mp (isOpen_analyticAt _ _) _ h
 
+@[deprecated (since := "2024-09-26")]
+alias AnalyticAt.exists_ball_analyticOn := AnalyticAt.exists_ball_analyticOnNhd
+
 end

Mathlib/Analysis/Analytic/Composition.lean

@@ -830,11 +830,14 @@ theorem AnalyticWithinAt.comp_of_eq {g : F → G} {f : E → F} {y : F} {x : E}
   rw [← hy] at hg
   exact hg.comp hf h
 
-lemma AnalyticWithinOn.comp {f : F → G} {g : E → F} {s : Set F}
-    {t : Set E} (hf : AnalyticWithinOn 𝕜 f s) (hg : AnalyticWithinOn 𝕜 g t) (h : Set.MapsTo g t s) :
-    AnalyticWithinOn 𝕜 (f ∘ g) t :=
+lemma AnalyticOn.comp {f : F → G} {g : E → F} {s : Set F}
+    {t : Set E} (hf : AnalyticOn 𝕜 f s) (hg : AnalyticOn 𝕜 g t) (h : Set.MapsTo g t s) :
+    AnalyticOn 𝕜 (f ∘ g) t :=
   fun x m ↦ (hf _ (h m)).comp (hg x m) h
 
+@[deprecated (since := "2024-09-26")]
+alias AnalyticWithinOn.comp := AnalyticOn.comp
+
 /-- If two functions `g` and `f` are analytic respectively at `f x` and `x`, then `g ∘ f` is
 analytic at `x`. -/
 theorem AnalyticAt.comp {g : F → G} {f : E → F} {x : E} (hg : AnalyticAt 𝕜 g (f x))
@@ -862,19 +865,26 @@ theorem AnalyticAt.comp_analyticWithinAt_of_eq {g : F → G} {f : E → F} {x :
 
 /-- If two functions `g` and `f` are analytic respectively on `s.image f` and `s`, then `g ∘ f` is
 analytic on `s`. -/
-theorem AnalyticOn.comp' {s : Set E} {g : F → G} {f : E → F} (hg : AnalyticOn 𝕜 g (s.image f))
-    (hf : AnalyticOn 𝕜 f s) : AnalyticOn 𝕜 (g ∘ f) s :=
+theorem AnalyticOnNhd.comp' {s : Set E} {g : F → G} {f : E → F} (hg : AnalyticOnNhd 𝕜 g (s.image f))
+    (hf : AnalyticOnNhd 𝕜 f s) : AnalyticOnNhd 𝕜 (g ∘ f) s :=
   fun z hz => (hg (f z) (Set.mem_image_of_mem f hz)).comp (hf z hz)
 
-theorem AnalyticOn.comp {s : Set E} {t : Set F} {g : F → G} {f : E → F} (hg : AnalyticOn 𝕜 g t)
-    (hf : AnalyticOn 𝕜 f s) (st : Set.MapsTo f s t) : AnalyticOn 𝕜 (g ∘ f) s :=
+@[deprecated (since := "2024-09-26")]
+alias AnalyticOn.comp' := AnalyticOnNhd.comp'
+
+theorem AnalyticOnNhd.comp {s : Set E} {t : Set F} {g : F → G} {f : E → F}
+    (hg : AnalyticOnNhd 𝕜 g t) (hf : AnalyticOnNhd 𝕜 f s) (st : Set.MapsTo f s t) :
+    AnalyticOnNhd 𝕜 (g ∘ f) s :=
   comp' (mono hg (Set.mapsTo'.mp st)) hf
 
-lemma AnalyticOn.comp_analyticWithinOn {f : F → G} {g : E → F} {s : Set F}
-    {t : Set E} (hf : AnalyticOn 𝕜 f s) (hg : AnalyticWithinOn 𝕜 g t) (h : Set.MapsTo g t s) :
-    AnalyticWithinOn 𝕜 (f ∘ g) t :=
+lemma AnalyticOnNhd.comp_analyticOn {f : F → G} {g : E → F} {s : Set F}
+    {t : Set E} (hf : AnalyticOnNhd 𝕜 f s) (hg : AnalyticOn 𝕜 g t) (h : Set.MapsTo g t s) :
+    AnalyticOn 𝕜 (f ∘ g) t :=
   fun x m ↦ (hf _ (h m)).comp_analyticWithinAt (hg x m)
 
+@[deprecated (since := "2024-09-26")]
+alias AnalyticOn.comp_analyticWithinOn := AnalyticOnNhd.comp_analyticOn
+
 /-!
 ### Associativity of the composition of formal multilinear series