From 2eceb4dde52957962c3179ab5b5f468f772378ef Mon Sep 17 00:00:00 2001
From: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Date: Sat, 28 Sep 2024 12:33:15 +0200
Subject: [PATCH 1/5] more on derivatives

---
 .../Analysis/Calculus/FDeriv/Analytic.lean    | 240 +++++++++++++++++-
 .../NormedSpace/OperatorNorm/NormedSpace.lean |   9 +
 2 files changed, 236 insertions(+), 13 deletions(-)

diff --git a/Mathlib/Analysis/Calculus/FDeriv/Analytic.lean b/Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
index 896125484853c..4596b843e760e 100644
--- a/Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
+++ b/Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
@@ -8,6 +8,7 @@ import Mathlib.Analysis.Analytic.Within
 import Mathlib.Analysis.Calculus.Deriv.Basic
 import Mathlib.Analysis.Calculus.ContDiff.Defs
 import Mathlib.Analysis.Calculus.FDeriv.Add
+import Mathlib.Analysis.Normed.Module.Completion
 
 /-!
 # Frechet derivatives of analytic functions.
@@ -21,7 +22,7 @@ iterated derivatives, in `ContinuousMultilinearMap.iteratedFDeriv_eq`.
 
 open Filter Asymptotics Set
 
-open scoped ENNReal
+open scoped ENNReal Topology
 
 universe u v
 
@@ -34,26 +35,58 @@ section fderiv
 variable {p : FormalMultilinearSeries 𝕜 E F} {r : ℝ≥0∞}
 variable {f : E → F} {x : E} {s : Set E}
 
-theorem HasFPowerSeriesAt.hasStrictFDerivAt (h : HasFPowerSeriesAt f p x) :
-    HasStrictFDerivAt f (continuousMultilinearCurryFin1 𝕜 E F (p 1)) x := by
+/-- A function which is analytic within a set is strictly differentiable there. Since we
+don't have a predicate `HasStrictFDerivWithinAt`, we spell out what it would mean. -/
+theorem HasFPowerSeriesWithinAt.hasStrictFDerivWithinAt (h : HasFPowerSeriesWithinAt f p s x) :
+    (fun y ↦ f y.1 - f y.2 - ((continuousMultilinearCurryFin1 𝕜 E F) (p 1)) (y.1 - y.2))
+      =o[𝓝[insert x s ×ˢ insert x s] (x, x)] fun y ↦ y.1 - y.2 := by
   refine h.isBigO_image_sub_norm_mul_norm_sub.trans_isLittleO (IsLittleO.of_norm_right ?_)
   refine isLittleO_iff_exists_eq_mul.2 ⟨fun y => ‖y - (x, x)‖, ?_, EventuallyEq.rfl⟩
+  apply Tendsto.mono_left _ nhdsWithin_le_nhds
   refine (continuous_id.sub continuous_const).norm.tendsto' _ _ ?_
   rw [_root_.id, sub_self, norm_zero]
 
+theorem HasFPowerSeriesAt.hasStrictFDerivAt (h : HasFPowerSeriesAt f p x) :
+    HasStrictFDerivAt f (continuousMultilinearCurryFin1 𝕜 E F (p 1)) x := by
+  simpa only [Set.insert_eq_of_mem, Set.mem_univ, Set.univ_prod_univ, nhdsWithin_univ]
+    using (h.hasFPowerSeriesWithinAt (s := Set.univ)).hasStrictFDerivWithinAt
+
+theorem HasFPowerSeriesWithinAt.hasFDerivWithinAt (h : HasFPowerSeriesWithinAt f p s x) :
+    HasFDerivWithinAt f (continuousMultilinearCurryFin1 𝕜 E F (p 1)) (insert x s) x := by
+  rw [HasFDerivWithinAt, hasFDerivAtFilter_iff_isLittleO, isLittleO_iff]
+  intro c hc
+  have : Tendsto (fun y ↦ (y, x)) (𝓝[insert x s] x) (𝓝[insert x s ×ˢ insert x s] (x, x)) := by
+    rw [nhdsWithin_prod_eq]
+    exact Tendsto.prod_mk tendsto_id (tendsto_const_nhdsWithin (by simp))
+  exact this (isLittleO_iff.1 h.hasStrictFDerivWithinAt hc)
+
 theorem HasFPowerSeriesAt.hasFDerivAt (h : HasFPowerSeriesAt f p x) :
     HasFDerivAt f (continuousMultilinearCurryFin1 𝕜 E F (p 1)) x :=
   h.hasStrictFDerivAt.hasFDerivAt
 
+theorem HasFPowerSeriesWithinAt.differentiableWithinAt (h : HasFPowerSeriesWithinAt f p s x) :
+    DifferentiableWithinAt 𝕜 f (insert x s) x :=
+  h.hasFDerivWithinAt.differentiableWithinAt
+
 theorem HasFPowerSeriesAt.differentiableAt (h : HasFPowerSeriesAt f p x) : DifferentiableAt 𝕜 f x :=
   h.hasFDerivAt.differentiableAt
 
+theorem AnalyticWithinAt.differentiableWithinAt (h : AnalyticWithinAt 𝕜 f s x) :
+    DifferentiableWithinAt 𝕜 f (insert x s) x := by
+  obtain ⟨p, hp⟩ := h
+  exact hp.differentiableWithinAt
+
 theorem AnalyticAt.differentiableAt : AnalyticAt 𝕜 f x → DifferentiableAt 𝕜 f x
   | ⟨_, hp⟩ => hp.differentiableAt
 
 theorem AnalyticAt.differentiableWithinAt (h : AnalyticAt 𝕜 f x) : DifferentiableWithinAt 𝕜 f s x :=
   h.differentiableAt.differentiableWithinAt
 
+theorem HasFPowerSeriesWithinAt.fderivWithin_eq
+    (h : HasFPowerSeriesWithinAt f p s x) (hu : UniqueDiffWithinAt 𝕜 (insert x s) x) :
+    fderivWithin 𝕜 f (insert x s) x = continuousMultilinearCurryFin1 𝕜 E F (p 1) :=
+  h.hasFDerivWithinAt.fderivWithin hu
+
 theorem HasFPowerSeriesAt.fderiv_eq (h : HasFPowerSeriesAt f p x) :
     fderiv 𝕜 f x = continuousMultilinearCurryFin1 𝕜 E F (p 1) :=
   h.hasFDerivAt.fderiv
@@ -64,29 +97,62 @@ theorem AnalyticAt.hasStrictFDerivAt (h : AnalyticAt 𝕜 f x) :
   rw [hp.fderiv_eq]
   exact hp.hasStrictFDerivAt
 
+theorem HasFPowerSeriesWithinOnBall.differentiableOn [CompleteSpace F]
+    (h : HasFPowerSeriesWithinOnBall f p s x r) :
+    DifferentiableOn 𝕜 f (insert x s ∩ EMetric.ball x r) := by
+  intro y hy
+  have Z := (h.analyticWithinAt_of_mem hy).differentiableWithinAt
+  rcases eq_or_ne y x with rfl | hy
+  · exact Z.mono inter_subset_left
+  · apply (Z.mono (subset_insert _ _)).mono_of_mem
+    suffices s ∈ 𝓝[insert x s] y from nhdsWithin_mono _ inter_subset_left this
+    rw [nhdsWithin_insert_of_ne hy]
+    exact self_mem_nhdsWithin
+
 theorem HasFPowerSeriesOnBall.differentiableOn [CompleteSpace F]
     (h : HasFPowerSeriesOnBall f p x r) : DifferentiableOn 𝕜 f (EMetric.ball x r) := fun _ hy =>
   (h.analyticAt_of_mem hy).differentiableWithinAt
 
-theorem AnalyticOnNhd.differentiableOn (h : AnalyticOnNhd 𝕜 f s) :
-    DifferentiableOn 𝕜 f s := fun y hy =>
-  (h y hy).differentiableWithinAt
+theorem AnalyticOn.differentiableOn (h : AnalyticOn 𝕜 f s) : DifferentiableOn 𝕜 f s :=
+  fun y hy ↦  (h y hy).differentiableWithinAt.mono (by simp)
 
-@[deprecated (since := "2024-09-26")]
-alias AnalyticOn.differentiableOn := AnalyticOnNhd.differentiableOn
+theorem AnalyticOnNhd.differentiableOn (h : AnalyticOnNhd 𝕜 f s) : DifferentiableOn 𝕜 f s :=
+  fun y hy ↦ (h y hy).differentiableWithinAt
+
+theorem HasFPowerSeriesWithinOnBall.hasFDerivWithinAt [CompleteSpace F]
+    (h : HasFPowerSeriesWithinOnBall f p s x r)
+    {y : E} (hy : (‖y‖₊ : ℝ≥0∞) < r) (h'y : x + y ∈ insert x s) :
+    HasFDerivWithinAt f (continuousMultilinearCurryFin1 𝕜 E F (p.changeOrigin y 1))
+      (insert x s) (x + y) := by
+  rcases eq_or_ne y 0 with rfl | h''y
+  · convert (h.changeOrigin hy h'y).hasFPowerSeriesWithinAt.hasFDerivWithinAt
+    simp
+  · have Z := (h.changeOrigin hy h'y).hasFPowerSeriesWithinAt.hasFDerivWithinAt
+    apply (Z.mono (subset_insert _ _)).mono_of_mem
+    rw [nhdsWithin_insert_of_ne]
+    · exact self_mem_nhdsWithin
+    · simpa using h''y
 
 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
 
+theorem HasFPowerSeriesWithinOnBall.fderivWithin_eq [CompleteSpace F]
+    (h : HasFPowerSeriesWithinOnBall f p s x r)
+    {y : E} (hy : (‖y‖₊ : ℝ≥0∞) < r) (h'y : x + y ∈ insert x s) (hu : UniqueDiffOn 𝕜 (insert x s)) :
+    fderivWithin 𝕜 f (insert x s) (x + y) =
+      continuousMultilinearCurryFin1 𝕜 E F (p.changeOrigin y 1) :=
+  (h.hasFDerivWithinAt hy h'y).fderivWithin (hu _ h'y)
+
 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
 
 /-- 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) :
+protected theorem HasFPowerSeriesOnBall.fderiv [CompleteSpace F]
+    (h : HasFPowerSeriesOnBall f p x r) :
     HasFPowerSeriesOnBall (fderiv 𝕜 f) p.derivSeries x r := by
   refine .congr (f := fun z ↦ continuousMultilinearCurryFin1 𝕜 E F (p.changeOrigin (z - x) 1)) ?_
     fun z hz ↦ ?_
@@ -98,13 +164,34 @@ theorem HasFPowerSeriesOnBall.fderiv [CompleteSpace F] (h : HasFPowerSeriesOnBal
   rw [← h.fderiv_eq, add_sub_cancel]
   simpa only [edist_eq_coe_nnnorm_sub, EMetric.mem_ball] using hz
 
+
+/-- If a function has a power series within a set on a ball, then so does its derivative. -/
+protected theorem HasFPowerSeriesWithinOnBall.fderivWithin [CompleteSpace F]
+    (h : HasFPowerSeriesWithinOnBall f p s x r) (hu : UniqueDiffOn 𝕜 (insert x s)) :
+    HasFPowerSeriesWithinOnBall (fderivWithin 𝕜 f (insert x s)) p.derivSeries s x r := by
+  refine .congr' (f := fun z ↦ continuousMultilinearCurryFin1 𝕜 E F (p.changeOrigin (z - x) 1)) ?_
+    (fun z hz ↦ ?_)
+  · refine continuousMultilinearCurryFin1 𝕜 E F
+      |>.toContinuousLinearEquiv.toContinuousLinearMap.comp_hasFPowerSeriesWithinOnBall ?_
+    apply HasFPowerSeriesOnBall.hasFPowerSeriesWithinOnBall
+    simpa using ((p.hasFPowerSeriesOnBall_changeOrigin 1
+      (h.r_pos.trans_le h.r_le)).mono h.r_pos h.r_le).comp_sub x
+  · dsimp only
+    rw [← h.fderivWithin_eq _ _ hu, add_sub_cancel]
+    · simpa only [edist_eq_coe_nnnorm_sub, EMetric.mem_ball] using hz.2
+    · simpa using hz.1
+
 /-- If a function is analytic on a set `s`, so is its Fréchet derivative. -/
-theorem AnalyticOnNhd.fderiv [CompleteSpace F] (h : AnalyticOnNhd 𝕜 f s) :
-    AnalyticOnNhd 𝕜 (fderiv 𝕜 f) s := by
-  intro y hy
-  rcases h y hy with ⟨p, r, hp⟩
+protected theorem AnalyticAt.fderiv [CompleteSpace F] (h : AnalyticAt 𝕜 f x) :
+    AnalyticAt 𝕜 (fderiv 𝕜 f) x := by
+  rcases h with ⟨p, r, hp⟩
   exact hp.fderiv.analyticAt
 
+/-- If a function is analytic on a set `s`, so is its Fréchet derivative. -/
+protected theorem AnalyticOnNhd.fderiv [CompleteSpace F] (h : AnalyticOnNhd 𝕜 f s) :
+    AnalyticOnNhd 𝕜 (fderiv 𝕜 f) s :=
+  fun y hy ↦ AnalyticAt.fderiv (h y hy)
+
 @[deprecated (since := "2024-09-26")]
 alias AnalyticOn.fderiv := AnalyticOnNhd.fderiv
 
@@ -125,6 +212,15 @@ theorem AnalyticOnNhd.iteratedFDeriv [CompleteSpace F] (h : AnalyticOnNhd 𝕜 f
 @[deprecated (since := "2024-09-26")]
 alias AnalyticOn.iteratedFDeriv := AnalyticOnNhd.iteratedFDeriv
 
+lemma AnalyticOnNhd.hasFTaylorSeriesUpToOn [CompleteSpace F]
+    (n : ℕ∞) (h : AnalyticOnNhd 𝕜 f s) :
+    HasFTaylorSeriesUpToOn n f (ftaylorSeries 𝕜 f) s := by
+  refine ⟨fun x _hx ↦ rfl, fun m _hm x hx ↦ ?_, fun m _hm x hx ↦ ?_⟩
+  · apply HasFDerivAt.hasFDerivWithinAt
+    exact ((h.iteratedFDeriv m x hx).differentiableAt).hasFDerivAt
+  · apply (DifferentiableAt.continuousAt (𝕜 := 𝕜) ?_).continuousWithinAt
+    exact (h.iteratedFDeriv m x hx).differentiableAt
+
 /-- An analytic function is infinitely differentiable. -/
 theorem AnalyticOnNhd.contDiffOn [CompleteSpace F] (h : AnalyticOnNhd 𝕜 f s) {n : ℕ∞} :
     ContDiffOn 𝕜 n f s :=
@@ -155,6 +251,124 @@ lemma AnalyticOn.contDiffOn [CompleteSpace F] {f : E → F} {s : Set E}
 @[deprecated (since := "2024-09-26")]
 alias AnalyticWithinOn.contDiffOn := AnalyticOn.contDiffOn
 
+lemma AnalyticWithinAt.exists_hasFTaylorSeriesUpToOn [CompleteSpace F]
+    (n : ℕ∞) (h : AnalyticWithinAt 𝕜 f s x) :
+    ∃ u ∈ 𝓝[insert x s] x, ∃ (p : E → FormalMultilinearSeries 𝕜 E F),
+    HasFTaylorSeriesUpToOn n f p u ∧ ∀ i, AnalyticOn 𝕜 (fun x ↦ p x i) u := by
+  rcases h.exists_analyticAt with ⟨g, -, fg, hg⟩
+  rcases hg.exists_mem_nhds_analyticOnNhd with ⟨v, vx, hv⟩
+  refine ⟨insert x s ∩ v, inter_mem_nhdsWithin _ vx, ftaylorSeries 𝕜 g, ?_, fun i ↦ ?_⟩
+  · suffices HasFTaylorSeriesUpToOn n g (ftaylorSeries 𝕜 g) (insert x s ∩ v) from
+      this.congr (fun y hy ↦ fg hy.1)
+    exact AnalyticOnNhd.hasFTaylorSeriesUpToOn _ (hv.mono Set.inter_subset_right)
+  · exact (hv.iteratedFDeriv i).analyticOn.mono Set.inter_subset_right
+
+/-- If a function has a power series `p` within a set of unique differentiability, inside a ball,
+and is differentiable at a point, then the derivative series of `p` is summable at a point, with
+sum the given differential. Note that this theorem does not require completeness of the space.-/
+theorem HasFPowerSeriesWithinOnBall.hasSum_derivSeries_of_hasFDerivWithinAt
+    (h : HasFPowerSeriesWithinOnBall f p s x r)
+    {f' : E →L[𝕜] F}
+    {y : E} (hy : (‖y‖₊ : ℝ≥0∞) < r) (h'y : x + y ∈ insert x s)
+    (hf' : HasFDerivWithinAt f f' (insert x s) (x + y))
+    (hu : UniqueDiffOn 𝕜 (insert x s)) :
+    HasSum (fun n ↦ p.derivSeries n (fun _ ↦ y)) f' := by
+  /- In the completion of the space, the derivative series is summable, and its sum is a derivative
+  of the function. Therefore, by uniqueness of derivatives, its sum is the image of `f'` under
+  the canonical embedding. As this is an embedding, it means that there was also convergence in
+  the original space, to `f'`. -/
+  let F' := UniformSpace.Completion F
+  let a : F →L[𝕜] F' := UniformSpace.Completion.toComplL
+  let b : (E →L[𝕜] F) →ₗᵢ[𝕜] (E →L[𝕜] F') := UniformSpace.Completion.toComplₗᵢ.postcomp
+  rw [← b.embedding.hasSum_iff]
+  have : HasFPowerSeriesWithinOnBall (a ∘ f) (a.compFormalMultilinearSeries p) s x r :=
+    a.comp_hasFPowerSeriesWithinOnBall h
+  have Z := (this.fderivWithin hu).hasSum h'y (by simpa [edist_eq_coe_nnnorm] using hy)
+  have : fderivWithin 𝕜 (a ∘ f) (insert x s) (x + y) = a ∘L f' := by
+    apply HasFDerivWithinAt.fderivWithin _ (hu _ h'y)
+    exact a.hasFDerivAt.comp_hasFDerivWithinAt (x + y) hf'
+  rw [this] at Z
+  convert Z with n
+  ext v
+  simp only [FormalMultilinearSeries.derivSeries,
+    ContinuousLinearMap.compFormalMultilinearSeries_apply,
+    FormalMultilinearSeries.changeOriginSeries,
+    ContinuousLinearMap.compContinuousMultilinearMap_coe, ContinuousLinearEquiv.coe_coe,
+    LinearIsometryEquiv.coe_coe, Function.comp_apply, ContinuousMultilinearMap.sum_apply, map_sum,
+    ContinuousLinearMap.coe_sum', Finset.sum_apply,
+    Matrix.zero_empty]
+  rfl
+
+/-- If a function is analytic within a set with unique differentials, then so is its derivative.
+Note that this theorem does not require completeness of the space. -/
+theorem AnalyticOn.fderivWithin (h : AnalyticOn 𝕜 f s) (hu : UniqueDiffOn 𝕜 s) :
+    AnalyticOn 𝕜 (fderivWithin 𝕜 f s) s := by
+  intro x hx
+  rcases h x hx with ⟨p, r, hr⟩
+  refine ⟨p.derivSeries, r, ?_⟩
+  refine ⟨hr.r_le.trans p.radius_le_radius_derivSeries, hr.r_pos, fun {y} hy h'y ↦ ?_⟩
+  apply hr.hasSum_derivSeries_of_hasFDerivWithinAt (by simpa [edist_eq_coe_nnnorm] using h'y) hy
+  rw [insert_eq_of_mem hx] at hy ⊢
+  apply DifferentiableWithinAt.hasFDerivWithinAt
+  · exact h.differentiableOn _ hy
+  · rwa [insert_eq_of_mem hx]
+
+/-- If a function is analytic on a set `s`, so are its successive Fréchet derivative within this
+set. Note that this theorem does not require completeness of the space. -/
+theorem AnalyticOn.iteratedFDerivWithin (h : AnalyticOn 𝕜 f s)
+    (hu : UniqueDiffOn 𝕜 s) (n : ℕ) :
+    AnalyticOn 𝕜 (iteratedFDerivWithin 𝕜 n f s) s := by
+  induction n with
+  | zero =>
+    rw [iteratedFDerivWithin_zero_eq_comp]
+    exact ((continuousMultilinearCurryFin0 𝕜 E F).symm : F →L[𝕜] E[×0]→L[𝕜] F)
+      |>.comp_analyticOn h
+  | succ n IH =>
+    rw [iteratedFDerivWithin_succ_eq_comp_left]
+    apply AnalyticOnNhd.comp_analyticOn _ (IH.fderivWithin hu) (mapsTo_univ _ _)
+    apply LinearIsometryEquiv.analyticOnNhd
+
+lemma AnalyticOn.exists_hasFTaylorSeriesUpToOn
+    (h : AnalyticOn 𝕜 f s) (hu : UniqueDiffOn 𝕜 s) :
+    ∃ (p : E → FormalMultilinearSeries 𝕜 E F),
+    HasFTaylorSeriesUpToOn ⊤ f p s ∧ ∀ i, AnalyticOn 𝕜 (fun x ↦ p x i) s := by
+  refine ⟨ftaylorSeriesWithin 𝕜 f s, ?_, fun i ↦ ?_⟩
+  · refine ⟨fun x _hx ↦ rfl, fun m _hm x hx ↦ ?_, fun m _hm x hx ↦ ?_⟩
+    · have := (h.iteratedFDerivWithin hu m x hx).differentiableWithinAt.hasFDerivWithinAt
+      rwa [insert_eq_of_mem hx] at this
+    · exact (h.iteratedFDerivWithin hu m x hx).continuousWithinAt
+  · apply h.iteratedFDerivWithin hu
+
+theorem AnalyticOnNhd.fderiv_of_isOpen (h : AnalyticOnNhd 𝕜 f s) (hs : IsOpen s) :
+    AnalyticOnNhd 𝕜 (fderiv 𝕜 f) s := by
+  rw [← hs.analyticOn_iff_analyticOnNhd] at h ⊢
+  exact (h.fderivWithin hs.uniqueDiffOn).congr (fun x hx ↦ (fderivWithin_of_isOpen hs hx).symm)
+
+theorem AnalyticOnNhd.iteratedFDeriv_of_isOpen (h : AnalyticOnNhd 𝕜 f s) (hs : IsOpen s) (n : ℕ) :
+    AnalyticOnNhd 𝕜 (iteratedFDeriv 𝕜 n f) s := by
+  rw [← hs.analyticOn_iff_analyticOnNhd] at h ⊢
+  exact (h.iteratedFDerivWithin hs.uniqueDiffOn n).congr
+    (fun x hx ↦ (iteratedFDerivWithin_of_isOpen n hs hx).symm)
+
+/-- If a partial homeomorphism `f` is analytic at a point `a`, with invertible derivative, then
+its inverse is analytic at `f a`. -/
+theorem PartialHomeomorph.analyticAt_symm' (f : PartialHomeomorph E F) {a : E}
+    {i : E ≃L[𝕜] F} (h0 : a ∈ f.source) (h : AnalyticAt 𝕜 f a) (h' : fderiv 𝕜 f a = i) :
+    AnalyticAt 𝕜 f.symm (f a) := by
+  rcases h with ⟨p, hp⟩
+  have : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm i := by simp [← h', hp.fderiv_eq]
+  exact (f.hasFPowerSeriesAt_symm h0 hp this).analyticAt
+
+/-- If a partial homeomorphism `f` is analytic at a point `a`, with invertible derivative, then
+its inverse is analytic at `f a`. -/
+theorem PartialHomeomorph.analyticAt_symm (f : PartialHomeomorph E F) {a : F}
+    {i : E ≃L[𝕜] F} (h0 : a ∈ f.target) (h : AnalyticAt 𝕜 f (f.symm a))
+    (h' : fderiv 𝕜 f (f.symm a) = i) :
+    AnalyticAt 𝕜 f.symm a := by
+  have : a = f (f.symm a) := by simp [h0]
+  rw [this]
+  exact f.analyticAt_symm' (by simp [h0]) h h'
+
 end fderiv
 
 section deriv
diff --git a/Mathlib/Analysis/NormedSpace/OperatorNorm/NormedSpace.lean b/Mathlib/Analysis/NormedSpace/OperatorNorm/NormedSpace.lean
index 85edc3f7a843e..253805834044d 100644
--- a/Mathlib/Analysis/NormedSpace/OperatorNorm/NormedSpace.lean
+++ b/Mathlib/Analysis/NormedSpace/OperatorNorm/NormedSpace.lean
@@ -165,6 +165,15 @@ theorem norm_toContinuousLinearMap_comp [RingHomIsometric σ₁₂] (f : F →
   opNorm_ext (f.toContinuousLinearMap.comp g) g fun x => by
     simp only [norm_map, coe_toContinuousLinearMap, coe_comp', Function.comp_apply]
 
+/-- Composing on the left with a linear isometry gives a linear isometry between spaces of
+continuous linear maps. -/
+def postcomp [RingHomIsometric σ₁₂] [RingHomIsometric σ₁₃] (a : F →ₛₗᵢ[σ₂₃] G) :
+    (E →SL[σ₁₂] F) →ₛₗᵢ[σ₂₃] (E →SL[σ₁₃] G) where
+  toFun f := a.toContinuousLinearMap.comp f
+  map_add' f g := by simp
+  map_smul' c f := by simp
+  norm_map' f := by simp [a.norm_toContinuousLinearMap_comp]
+
 end LinearIsometry
 
 end

From d723e13e6b7f8b92588125ff5087bd43f1c26148 Mon Sep 17 00:00:00 2001
From: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Date: Sat, 28 Sep 2024 13:15:55 +0200
Subject: [PATCH 2/5] missing file

---
 Mathlib/Analysis/Calculus/FDeriv/Analytic.lean       | 1 +
 Mathlib/Analysis/Normed/Operator/LinearIsometry.lean | 2 ++
 2 files changed, 3 insertions(+)

diff --git a/Mathlib/Analysis/Calculus/FDeriv/Analytic.lean b/Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
index 4596b843e760e..05cf61c29fa61 100644
--- a/Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
+++ b/Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
 import Mathlib.Analysis.Analytic.CPolynomial
+import Mathlib.Analysis.Analytic.Inverse
 import Mathlib.Analysis.Analytic.Within
 import Mathlib.Analysis.Calculus.Deriv.Basic
 import Mathlib.Analysis.Calculus.ContDiff.Defs
diff --git a/Mathlib/Analysis/Normed/Operator/LinearIsometry.lean b/Mathlib/Analysis/Normed/Operator/LinearIsometry.lean
index 578fd81859e6d..77c5f4cf43a72 100644
--- a/Mathlib/Analysis/Normed/Operator/LinearIsometry.lean
+++ b/Mathlib/Analysis/Normed/Operator/LinearIsometry.lean
@@ -205,6 +205,8 @@ theorem nnnorm_map (x : E) : ‖f x‖₊ = ‖x‖₊ :=
 protected theorem isometry : Isometry f :=
   AddMonoidHomClass.isometry_of_norm f.toLinearMap (norm_map _)
 
+protected lemma embedding (f : F →ₛₗᵢ[σ₁₂] E₂) : Embedding f := f.isometry.embedding
+
 -- Should be `@[simp]` but it doesn't fire due to `lean4#3107`.
 theorem isComplete_image_iff [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕) {s : Set E} :
     IsComplete (f '' s) ↔ IsComplete s :=

From ff29b573a6be567ee9dfb1e38d42d7df1a2b6286 Mon Sep 17 00:00:00 2001
From: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Date: Sat, 28 Sep 2024 14:02:38 +0200
Subject: [PATCH 3/5] progress

---
 .../Analysis/Calculus/FDeriv/Analytic.lean    | 109 ++++++++++++++++--
 1 file changed, 102 insertions(+), 7 deletions(-)

diff --git a/Mathlib/Analysis/Calculus/FDeriv/Analytic.lean b/Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
index 05cf61c29fa61..dbccd8412ac13 100644
--- a/Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
+++ b/Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
@@ -9,6 +9,7 @@ import Mathlib.Analysis.Analytic.Within
 import Mathlib.Analysis.Calculus.Deriv.Basic
 import Mathlib.Analysis.Calculus.ContDiff.Defs
 import Mathlib.Analysis.Calculus.FDeriv.Add
+import Mathlib.Analysis.Calculus.FDeriv.Prod
 import Mathlib.Analysis.Normed.Module.Completion
 
 /-!
@@ -197,7 +198,7 @@ protected theorem AnalyticOnNhd.fderiv [CompleteSpace F] (h : AnalyticOnNhd 𝕜
 alias AnalyticOn.fderiv := AnalyticOnNhd.fderiv
 
 /-- If a function is analytic on a set `s`, so are its successive Fréchet derivative. -/
-theorem AnalyticOnNhd.iteratedFDeriv [CompleteSpace F] (h : AnalyticOnNhd 𝕜 f s) (n : ℕ) :
+protected theorem AnalyticOnNhd.iteratedFDeriv [CompleteSpace F] (h : AnalyticOnNhd 𝕜 f s) (n : ℕ) :
     AnalyticOnNhd 𝕜 (iteratedFDeriv 𝕜 n f) s := by
   induction n with
   | zero =>
@@ -223,7 +224,7 @@ lemma AnalyticOnNhd.hasFTaylorSeriesUpToOn [CompleteSpace F]
     exact (h.iteratedFDeriv m x hx).differentiableAt
 
 /-- An analytic function is infinitely differentiable. -/
-theorem AnalyticOnNhd.contDiffOn [CompleteSpace F] (h : AnalyticOnNhd 𝕜 f s) {n : ℕ∞} :
+protected theorem AnalyticOnNhd.contDiffOn [CompleteSpace F] (h : AnalyticOnNhd 𝕜 f s) {n : ℕ∞} :
     ContDiffOn 𝕜 n f s :=
   let t := { x | AnalyticAt 𝕜 f x }
   suffices ContDiffOn 𝕜 n f t from this.mono h
@@ -235,17 +236,17 @@ theorem AnalyticOnNhd.contDiffOn [CompleteSpace F] (h : AnalyticOnNhd 𝕜 f s)
     (fun m _ ↦ (H.iteratedFDeriv m).differentiableOn.congr
       fun _ hx ↦ iteratedFDerivWithin_of_isOpen _ t_open hx)
 
-theorem AnalyticAt.contDiffAt [CompleteSpace F] (h : AnalyticAt 𝕜 f x) {n : ℕ∞} :
+protected theorem AnalyticAt.contDiffAt [CompleteSpace F] (h : AnalyticAt 𝕜 f x) {n : ℕ∞} :
     ContDiffAt 𝕜 n f x := by
   obtain ⟨s, hs, hf⟩ := h.exists_mem_nhds_analyticOnNhd
   exact hf.contDiffOn.contDiffAt hs
 
-lemma AnalyticWithinAt.contDiffWithinAt [CompleteSpace F] {f : E → F} {s : Set E} {x : E}
+protected lemma AnalyticWithinAt.contDiffWithinAt [CompleteSpace F] {f : E → F} {s : Set E} {x : E}
     (h : AnalyticWithinAt 𝕜 f s x) {n : ℕ∞} : ContDiffWithinAt 𝕜 n f s x := by
   rcases h.exists_analyticAt with ⟨g, fx, fg, hg⟩
   exact hg.contDiffAt.contDiffWithinAt.congr (fg.mono (subset_insert _ _)) fx
 
-lemma AnalyticOn.contDiffOn [CompleteSpace F] {f : E → F} {s : Set E}
+protected lemma AnalyticOn.contDiffOn [CompleteSpace F] {f : E → F} {s : Set E}
     (h : AnalyticOn 𝕜 f s) {n : ℕ∞} : ContDiffOn 𝕜 n f s :=
   fun x m ↦ (h x m).contDiffWithinAt
 
@@ -302,7 +303,7 @@ theorem HasFPowerSeriesWithinOnBall.hasSum_derivSeries_of_hasFDerivWithinAt
 
 /-- If a function is analytic within a set with unique differentials, then so is its derivative.
 Note that this theorem does not require completeness of the space. -/
-theorem AnalyticOn.fderivWithin (h : AnalyticOn 𝕜 f s) (hu : UniqueDiffOn 𝕜 s) :
+protected theorem AnalyticOn.fderivWithin (h : AnalyticOn 𝕜 f s) (hu : UniqueDiffOn 𝕜 s) :
     AnalyticOn 𝕜 (fderivWithin 𝕜 f s) s := by
   intro x hx
   rcases h x hx with ⟨p, r, hr⟩
@@ -316,7 +317,7 @@ theorem AnalyticOn.fderivWithin (h : AnalyticOn 𝕜 f s) (hu : UniqueDiffOn 
 
 /-- If a function is analytic on a set `s`, so are its successive Fréchet derivative within this
 set. Note that this theorem does not require completeness of the space. -/
-theorem AnalyticOn.iteratedFDerivWithin (h : AnalyticOn 𝕜 f s)
+protected theorem AnalyticOn.iteratedFDerivWithin (h : AnalyticOn 𝕜 f s)
     (hu : UniqueDiffOn 𝕜 s) (n : ℕ) :
     AnalyticOn 𝕜 (iteratedFDerivWithin 𝕜 n f s) s := by
   induction n with
@@ -576,6 +577,30 @@ protected theorem hasFDerivAt [DecidableEq ι] : HasFDerivAt f (f.linearDeriv x)
   convert f.hasFiniteFPowerSeriesOnBall.hasFDerivAt (y := x) ENNReal.coe_lt_top
   rw [zero_add]
 
+/-- Given `f` a multilinear map, then the derivative of `x ↦ f (g₁ x, ..., gₙ x)` at `x` applied
+to a vector `v` is given by `∑ i, f (g₁ x, ..., g'ᵢ v, ..., gₙ x)`. Version inside a set. -/
+theorem _root_.HasFDerivWithinAt.multilinear_comp
+    [DecidableEq ι] {G : Type*} [NormedAddCommGroup G] [NormedSpace 𝕜 G]
+    {g : ∀ i, G → E i} {g' : ∀ i, G →L[𝕜] E i} {s : Set G} {x : G}
+    (hg : ∀ i, HasFDerivWithinAt (g i) (g' i) s x) :
+    HasFDerivWithinAt (fun x ↦ f (fun i ↦ g i x))
+      ((∑ i : ι, (f.toContinuousLinearMap (fun j ↦ g j x) i) ∘L (g' i))) s x := by
+  convert (f.hasFDerivAt (fun j ↦ g j x)).comp_hasFDerivWithinAt x (hasFDerivWithinAt_pi.2 hg)
+  ext v
+  simp [linearDeriv]
+
+/-- Given `f` a multilinear map, then the derivative of `x ↦ f (g₁ x, ..., gₙ x)` at `x` applied
+to a vector `v` is given by `∑ i, f (g₁ x, ..., g'ᵢ v, ..., gₙ x)`. -/
+theorem _root_.HasFDerivAt.multilinear_comp
+    [DecidableEq ι] {G : Type*} [NormedAddCommGroup G] [NormedSpace 𝕜 G]
+    {g : ∀ i, G → E i} {g' : ∀ i, G →L[𝕜] E i} {x : G}
+    (hg : ∀ i, HasFDerivAt (g i) (g' i) x) :
+    HasFDerivAt (fun x ↦ f (fun i ↦ g i x))
+      ((∑ i : ι, (f.toContinuousLinearMap (fun j ↦ g j x) i) ∘L (g' i))) x := by
+  convert (f.hasFDerivAt (fun j ↦ g j x)).comp x (hasFDerivAt_pi.2 hg)
+  ext v
+  simp [linearDeriv]
+
 /-- Technical lemma used in the proof of `hasFTaylorSeriesUpTo_iteratedFDeriv`, to compare sums
 over embedding of `Fin k` and `Fin (k + 1)`. -/
 private lemma _root_.Equiv.succ_embeddingFinSucc_fst_symm_apply {ι : Type*} [DecidableEq ι]
@@ -730,3 +755,73 @@ theorem hasSum_iteratedFDeriv [CharZero 𝕜] {y : E} (hy : y ∈ EMetric.ball 0
     mul_inv_cancel₀ <| cast_ne_zero.mpr n.factorial_ne_zero, one_smul]
 
 end HasFPowerSeriesOnBall
+
+/-!
+### Derivative of a linear map into multilinear maps
+-/
+
+namespace ContinuousLinearMap
+
+variable {ι : Type*} {G : ι → Type*} [∀ i, NormedAddCommGroup (G i)] [∀ i, NormedSpace 𝕜 (G i)]
+  [Fintype ι]  {H : Type*} [NormedAddCommGroup H]
+  [NormedSpace 𝕜 H]
+
+theorem hasFDerivAt_uncurry_of_multilinear [DecidableEq ι]
+    (f : E →L[𝕜] ContinuousMultilinearMap 𝕜 G F) (v : E × Π i, G i) :
+    HasFDerivAt (fun (p : E × Π i, G i) ↦ f p.1 p.2)
+      ((f.flipMultilinear v.2) ∘L (.fst _ _ _) +
+        ∑ i : ι, ((f v.1).toContinuousLinearMap v.2 i) ∘L (.proj _) ∘L (.snd _ _ _)) v := by
+  convert HasFDerivAt.multilinear_comp (f.continuousMultilinearMapOption)
+    (g := fun (_ : Option ι) p ↦ p) (g' := fun _ ↦ ContinuousLinearMap.id _ _) (x := v)
+    (fun _ ↦ hasFDerivAt_id _)
+  have I : f.continuousMultilinearMapOption.toContinuousLinearMap (fun _ ↦ v) none =
+      (f.flipMultilinear v.2) ∘L (.fst _ _ _) := by
+    simp [ContinuousMultilinearMap.toContinuousLinearMap, continuousMultilinearMapOption]
+    apply ContinuousLinearMap.ext (fun w ↦ ?_)
+    simp
+  have J : ∀ (i : ι), f.continuousMultilinearMapOption.toContinuousLinearMap (fun _ ↦ v) (some i)
+      = ((f v.1).toContinuousLinearMap v.2 i) ∘L (.proj _) ∘L (.snd _ _ _) := by
+    intro i
+    apply ContinuousLinearMap.ext (fun w ↦ ?_)
+    simp only [ContinuousMultilinearMap.toContinuousLinearMap, continuousMultilinearMapOption,
+      coe_mk', MultilinearMap.toLinearMap_apply, ContinuousMultilinearMap.coe_coe,
+      MultilinearMap.coe_mkContinuous, MultilinearMap.coe_mk, ne_eq, reduceCtorEq,
+      not_false_eq_true, Function.update_noteq, coe_comp', coe_snd', Function.comp_apply,
+      proj_apply]
+    congr
+    ext j
+    rcases eq_or_ne j i with rfl | hij
+    · simp
+    · simp [hij]
+  simp [I, J]
+
+/-- Given `f` a linear map into multilinear maps, then the derivative
+of `x ↦ f (a x) (b₁ x, ..., bₙ x)` at `x` applied to a vector `v` is given by
+`f (a' v) (b₁ x, ...., bₙ x) + ∑ i, f a (b₁ x, ..., b'ᵢ v, ..., bₙ x)`. Version inside a set. -/
+theorem _root_.HasFDerivWithinAt.linear_multilinear_comp
+    [DecidableEq ι] {a : H → E} {a' : H →L[𝕜] E}
+    {b : ∀ i, H → G i} {b' : ∀ i, H →L[𝕜] G i} {s : Set H} {x : H}
+    (ha : HasFDerivWithinAt a a' s x) (hb : ∀ i, HasFDerivWithinAt (b i) (b' i) s x)
+    (f : E →L[𝕜] ContinuousMultilinearMap 𝕜 G F) :
+    HasFDerivWithinAt (fun y ↦ f (a y) (fun i ↦ b i y))
+      ((f.flipMultilinear (fun i ↦ b i x)) ∘L a' +
+        ∑ i, ((f (a x)).toContinuousLinearMap (fun j ↦ b j x) i) ∘L (b' i)) s x := by
+  convert (hasFDerivAt_uncurry_of_multilinear f (a x, fun i ↦ b i x)).comp_hasFDerivWithinAt x
+    (ha.prod (hasFDerivWithinAt_pi.mpr hb))
+  ext v
+  simp
+
+/-- Given `f` a linear map into multilinear maps, then the derivative
+of `x ↦ f (a x) (b₁ x, ..., bₙ x)` at `x` applied to a vector `v` is given by
+`f (a' v) (b₁ x, ...., bₙ x) + ∑ i, f a (b₁ x, ..., b'ᵢ v, ..., bₙ x)`. -/
+theorem _root_.HasFDerivAt.linear_multilinear_comp [DecidableEq ι] {a : H → E} {a' : H →L[𝕜] E}
+    {b : ∀ i, H → G i} {b' : ∀ i, H →L[𝕜] G i} {x : H}
+    (ha : HasFDerivAt a a' x) (hb : ∀ i, HasFDerivAt (b i) (b' i) x)
+    (f : E →L[𝕜] ContinuousMultilinearMap 𝕜 G F) :
+    HasFDerivAt (fun y ↦ f (a y) (fun i ↦ b i y))
+      ((f.flipMultilinear (fun i ↦ b i x)) ∘L a' +
+        ∑ i, ((f (a x)).toContinuousLinearMap (fun j ↦ b j x) i) ∘L (b' i)) x := by
+  simp_rw [← hasFDerivWithinAt_univ] at ha hb ⊢
+  exact HasFDerivWithinAt.linear_multilinear_comp ha hb f
+
+end ContinuousLinearMap

From 602348a95d518283233806f771346d4320b4eb56 Mon Sep 17 00:00:00 2001
From: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Date: Sat, 28 Sep 2024 16:04:25 +0200
Subject: [PATCH 4/5] docstrings

---
 Mathlib/Analysis/Calculus/FDeriv/Analytic.lean | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Analysis/Calculus/FDeriv/Analytic.lean b/Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
index dbccd8412ac13..276a1587ae939 100644
--- a/Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
+++ b/Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
@@ -166,7 +166,6 @@ protected theorem HasFPowerSeriesOnBall.fderiv [CompleteSpace F]
   rw [← h.fderiv_eq, add_sub_cancel]
   simpa only [edist_eq_coe_nnnorm_sub, EMetric.mem_ball] using hz
 
-
 /-- If a function has a power series within a set on a ball, then so does its derivative. -/
 protected theorem HasFPowerSeriesWithinOnBall.fderivWithin [CompleteSpace F]
     (h : HasFPowerSeriesWithinOnBall f p s x r) (hu : UniqueDiffOn 𝕜 (insert x s)) :
@@ -189,7 +188,9 @@ protected theorem AnalyticAt.fderiv [CompleteSpace F] (h : AnalyticAt 𝕜 f x)
   rcases h with ⟨p, r, hp⟩
   exact hp.fderiv.analyticAt
 
-/-- If a function is analytic on a set `s`, so is its Fréchet derivative. -/
+/-- If a function is analytic on a set `s`, so is its Fréchet derivative. See also
+`AnalyticOnNhd.fderiv_of_isOpen`, removing the completeness assumption but requiring the set
+to be open. -/
 protected theorem AnalyticOnNhd.fderiv [CompleteSpace F] (h : AnalyticOnNhd 𝕜 f s) :
     AnalyticOnNhd 𝕜 (fderiv 𝕜 f) s :=
   fun y hy ↦ AnalyticAt.fderiv (h y hy)
@@ -197,7 +198,9 @@ protected theorem AnalyticOnNhd.fderiv [CompleteSpace F] (h : AnalyticOnNhd 𝕜
 @[deprecated (since := "2024-09-26")]
 alias AnalyticOn.fderiv := AnalyticOnNhd.fderiv
 
-/-- If a function is analytic on a set `s`, so are its successive Fréchet derivative. -/
+/-- If a function is analytic on a set `s`, so are its successive Fréchet derivative. See also
+`AnalyticOnNhd.iteratedFDeruv_of_isOpen`, removing the completeness assumption but requiring the set
+to be open.-/
 protected theorem AnalyticOnNhd.iteratedFDeriv [CompleteSpace F] (h : AnalyticOnNhd 𝕜 f s) (n : ℕ) :
     AnalyticOnNhd 𝕜 (iteratedFDeriv 𝕜 n f) s := by
   induction n with

From c021d921535517993264873976e6bebcd2d24241 Mon Sep 17 00:00:00 2001
From: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Date: Sun, 29 Sep 2024 09:40:57 +0200
Subject: [PATCH 5/5] docstrings

---
 .../Analysis/Calculus/FDeriv/Analytic.lean    | 74 ++++++++++++++++---
 1 file changed, 62 insertions(+), 12 deletions(-)

diff --git a/Mathlib/Analysis/Calculus/FDeriv/Analytic.lean b/Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
index 276a1587ae939..10a992f7280df 100644
--- a/Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
+++ b/Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
@@ -20,6 +20,45 @@ Also the special case in terms of `deriv` when the domain is 1-dimensional.
 
 As an application, we show that continuous multilinear maps are smooth. We also compute their
 iterated derivatives, in `ContinuousMultilinearMap.iteratedFDeriv_eq`.
+
+## Main definitions and results
+
+* `AnalyticAt.differentiableAt` : an analytic function at a point is differentiable there.
+* `AnalyticOnNhd.fderiv` : in a complete space, if a function is analytic on a
+  neighborhood of a set `s`, so is its derivative.
+* `AnalyticOnNhd.fderiv_of_isOpen` : if a function is analytic on a neighborhood of an
+  open set `s`, so is its derivative.
+* `AnalyticOn.fderivWithin` : if a function is analytic on a set of unique differentiability,
+  so is its derivative within this set.
+* `PartialHomeomorph.analyticAt_symm` : if a partial homeomorphism `f` is analytic at a
+  point `f.symm a`, with invertible derivative, then its inverse is analytic at `a`.
+
+## Comments on completeness
+
+Some theorems need a complete space, some don't, for the following reason.
+
+(1) If a function is analytic at a point `x`, then it is differentiable there (with derivative given
+by the first term in the power series). There is no issue of convergence here.
+
+(2) If a function has a power series on a ball `B (x, r)`, there is no guarantee that the power
+series for the derivative will converge at `y ≠ x`, if the space is not complete. So, to deduce
+that `f` is differentiable at `y`, one needs completeness in general.
+
+(3) However, if a function `f` has a power series on a ball `B (x, r)`, and is a priori known to be
+differentiable at some point `y ≠ x`, then the power series for the derivative of `f` will
+automatically converge at `y`, towards the given derivative: this follows from the facts that this
+is true in the completion (thanks to the previous point) and that the map to the completion is
+an embedding.
+
+(4) Therefore, if one assumes `AnalyticOn 𝕜 f s` where `s` is an open set, then `f` is analytic
+therefore differentiable at every point of `s`, by (1), so by (3) the power series for its
+derivative converges on whole balls. Therefore, the derivative of `f` is also analytic on `s`. The
+same holds if `s` is merely a set with unique differentials.
+
+(5) However, this does not work for `AnalyticOnNhd 𝕜 f s`, as we don't get for free
+differentiability at points in a neighborhood of `s`. Therefore, the theorem that deduces
+`AnalyticOnNhd 𝕜 (fderiv 𝕜 f) s` from `AnalyticOnNhd 𝕜 f s` requires completeness of the space.
+
 -/
 
 open Filter Asymptotics Set
@@ -152,7 +191,6 @@ theorem HasFPowerSeriesOnBall.fderiv_eq [CompleteSpace F] (h : HasFPowerSeriesOn
     fderiv 𝕜 f (x + y) = continuousMultilinearCurryFin1 𝕜 E F (p.changeOrigin y 1) :=
   (h.hasFDerivAt hy).fderiv
 
-/-- If a function has a power series on a ball, then so does its derivative. -/
 protected theorem HasFPowerSeriesOnBall.fderiv [CompleteSpace F]
     (h : HasFPowerSeriesOnBall f p x r) :
     HasFPowerSeriesOnBall (fderiv 𝕜 f) p.derivSeries x r := by
@@ -217,6 +255,10 @@ protected theorem AnalyticOnNhd.iteratedFDeriv [CompleteSpace F] (h : AnalyticOn
 @[deprecated (since := "2024-09-26")]
 alias AnalyticOn.iteratedFDeriv := AnalyticOnNhd.iteratedFDeriv
 
+/-- If a function is analytic on a neighborhood of a set `s`, then it has a Taylor series given
+by the sequence of its derivatives. Note that, if the function were just analytic on `s`, then
+one would have to use instead the sequence of derivatives inside the set, as in
+`AnalyticOn.hasFTaylorSeriesUpToOn`. -/
 lemma AnalyticOnNhd.hasFTaylorSeriesUpToOn [CompleteSpace F]
     (n : ℕ∞) (h : AnalyticOnNhd 𝕜 f s) :
     HasFTaylorSeriesUpToOn n f (ftaylorSeries 𝕜 f) s := by
@@ -333,16 +375,19 @@ protected theorem AnalyticOn.iteratedFDerivWithin (h : AnalyticOn 𝕜 f s)
     apply AnalyticOnNhd.comp_analyticOn _ (IH.fderivWithin hu) (mapsTo_univ _ _)
     apply LinearIsometryEquiv.analyticOnNhd
 
+lemma AnalyticOn.hasFTaylorSeriesUpToOn {n : ℕ∞}
+    (h : AnalyticOn 𝕜 f s) (hu : UniqueDiffOn 𝕜 s) :
+    HasFTaylorSeriesUpToOn n f (ftaylorSeriesWithin 𝕜 f s) s := by
+  refine ⟨fun x _hx ↦ rfl, fun m _hm x hx ↦ ?_, fun m _hm x hx ↦ ?_⟩
+  · have := (h.iteratedFDerivWithin hu m x hx).differentiableWithinAt.hasFDerivWithinAt
+    rwa [insert_eq_of_mem hx] at this
+  · exact (h.iteratedFDerivWithin hu m x hx).continuousWithinAt
+
 lemma AnalyticOn.exists_hasFTaylorSeriesUpToOn
     (h : AnalyticOn 𝕜 f s) (hu : UniqueDiffOn 𝕜 s) :
     ∃ (p : E → FormalMultilinearSeries 𝕜 E F),
-    HasFTaylorSeriesUpToOn ⊤ f p s ∧ ∀ i, AnalyticOn 𝕜 (fun x ↦ p x i) s := by
-  refine ⟨ftaylorSeriesWithin 𝕜 f s, ?_, fun i ↦ ?_⟩
-  · refine ⟨fun x _hx ↦ rfl, fun m _hm x hx ↦ ?_, fun m _hm x hx ↦ ?_⟩
-    · have := (h.iteratedFDerivWithin hu m x hx).differentiableWithinAt.hasFDerivWithinAt
-      rwa [insert_eq_of_mem hx] at this
-    · exact (h.iteratedFDerivWithin hu m x hx).continuousWithinAt
-  · apply h.iteratedFDerivWithin hu
+      HasFTaylorSeriesUpToOn ⊤ f p s ∧ ∀ i, AnalyticOn 𝕜 (fun x ↦ p x i) s :=
+  ⟨ftaylorSeriesWithin 𝕜 f s, h.hasFTaylorSeriesUpToOn hu, h.iteratedFDerivWithin hu⟩
 
 theorem AnalyticOnNhd.fderiv_of_isOpen (h : AnalyticOnNhd 𝕜 f s) (hs : IsOpen s) :
     AnalyticOnNhd 𝕜 (fderiv 𝕜 f) s := by
@@ -364,8 +409,8 @@ theorem PartialHomeomorph.analyticAt_symm' (f : PartialHomeomorph E F) {a : E}
   have : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm i := by simp [← h', hp.fderiv_eq]
   exact (f.hasFPowerSeriesAt_symm h0 hp this).analyticAt
 
-/-- If a partial homeomorphism `f` is analytic at a point `a`, with invertible derivative, then
-its inverse is analytic at `f a`. -/
+/-- If a partial homeomorphism `f` is analytic at a point `f.symm a`, with invertible derivative,
+then its inverse is analytic at `a`. -/
 theorem PartialHomeomorph.analyticAt_symm (f : PartialHomeomorph E F) {a : F}
     {i : E ≃L[𝕜] F} (h0 : a ∈ f.target) (h : AnalyticAt 𝕜 f (f.symm a))
     (h' : fderiv 𝕜 f (f.symm a) = i) :
@@ -393,14 +438,19 @@ protected theorem HasFPowerSeriesAt.deriv (h : HasFPowerSeriesAt f p x) :
     deriv f x = p 1 fun _ => 1 :=
   h.hasDerivAt.deriv
 
-/-- If a function is analytic on a set `s`, so is its derivative. -/
-theorem AnalyticOnNhd.deriv [CompleteSpace F] (h : AnalyticOnNhd 𝕜 f s) :
+/-- If a function is analytic on a set `s` in a complete space, so is its derivative. -/
+protected theorem AnalyticOnNhd.deriv [CompleteSpace F] (h : AnalyticOnNhd 𝕜 f s) :
     AnalyticOnNhd 𝕜 (deriv f) s :=
   (ContinuousLinearMap.apply 𝕜 F (1 : 𝕜)).comp_analyticOnNhd h.fderiv
 
 @[deprecated (since := "2024-09-26")]
 alias AnalyticOn.deriv := AnalyticOnNhd.deriv
 
+/-- If a function is analytic on an open set `s`, so is its derivative. -/
+theorem AnalyticOnNhd.deriv_of_isOpen (h : AnalyticOnNhd 𝕜 f s) (hs : IsOpen s) :
+    AnalyticOnNhd 𝕜 (deriv f) s :=
+  (ContinuousLinearMap.apply 𝕜 F (1 : 𝕜)).comp_analyticOnNhd (h.fderiv_of_isOpen hs)
+
 /-- If a function is analytic on a set `s`, so are its successive derivatives. -/
 theorem AnalyticOnNhd.iterated_deriv [CompleteSpace F] (h : AnalyticOnNhd 𝕜 f s) (n : ℕ) :
     AnalyticOnNhd 𝕜 (_root_.deriv^[n] f) s := by