[Merged by Bors] - feat: update the ContDiff definition to integrate analytic functions in the hierarchy

Archive/Hairer.lean

@@ -26,6 +26,7 @@ noncomputable section
 open Metric Set MeasureTheory
 open MvPolynomial hiding support
 open Function hiding eval
+open scoped ContDiff
 
 variable {ι : Type*} [Fintype ι]
 
@@ -110,7 +111,7 @@ lemma inj_L : Injective (L ι) :=
     apply subset_closure
 
 lemma hairer (N : ℕ) (ι : Type*) [Fintype ι] :
-    ∃ (ρ : EuclideanSpace ℝ ι → ℝ), tsupport ρ ⊆ closedBall 0 1 ∧ ContDiff ℝ ⊤ ρ ∧
+    ∃ (ρ : EuclideanSpace ℝ ι → ℝ), tsupport ρ ⊆ closedBall 0 1 ∧ ContDiff ℝ ∞ ρ ∧
     ∀ (p : MvPolynomial ι ℝ), p.totalDegree ≤ N →
     ∫ x : EuclideanSpace ℝ ι, eval x p • ρ x = eval 0 p := by
   have := (inj_L ι).comp (restrictTotalDegree ι ℝ N).injective_subtype

Mathlib.lean

@@ -977,6 +977,7 @@ import Mathlib.Analysis.Calculus.ContDiff.Basic
 import Mathlib.Analysis.Calculus.ContDiff.Bounds
 import Mathlib.Analysis.Calculus.ContDiff.Defs
 import Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
+import Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
 import Mathlib.Analysis.Calculus.ContDiff.FiniteDimension
 import Mathlib.Analysis.Calculus.ContDiff.RCLike
 import Mathlib.Analysis.Calculus.Darboux
@@ -1001,6 +1002,7 @@ import Mathlib.Analysis.Calculus.DiffContOnCl
 import Mathlib.Analysis.Calculus.Dslope
 import Mathlib.Analysis.Calculus.FDeriv.Add
 import Mathlib.Analysis.Calculus.FDeriv.Analytic
+import Mathlib.Analysis.Calculus.FDeriv.AnalyticIt
 import Mathlib.Analysis.Calculus.FDeriv.Basic
 import Mathlib.Analysis.Calculus.FDeriv.Bilinear
 import Mathlib.Analysis.Calculus.FDeriv.Comp

Mathlib/Analysis/Analytic/Basic.lean

@@ -301,6 +301,18 @@ theorem le_mul_pow_of_radius_pos (p : FormalMultilinearSeries 𝕜 E F) (h : 0 <
   rw [inv_pow, ← div_eq_mul_inv]
   exact hCp n
 
+lemma radius_le_of_le {𝕜' E' F' : Type*}
+    [NontriviallyNormedField 𝕜'] [NormedAddCommGroup E'] [NormedSpace 𝕜' E']
+    [NormedAddCommGroup F'] [NormedSpace 𝕜' F']
+    {p : FormalMultilinearSeries 𝕜 E F} {q : FormalMultilinearSeries 𝕜' E' F'}
+    (h : ∀ n, ‖p n‖ ≤ ‖q n‖) : q.radius ≤ p.radius := by
+  apply le_of_forall_nnreal_lt (fun r hr ↦ ?_)
+  rcases norm_mul_pow_le_of_lt_radius _ hr with ⟨C, -, hC⟩
+  apply le_radius_of_bound _ C (fun n ↦ ?_)
+  apply le_trans _ (hC n)
+  gcongr
+  exact h n
+
 /-- The radius of the sum of two formal series is at least the minimum of their two radii. -/
 theorem min_radius_le_radius_add (p q : FormalMultilinearSeries 𝕜 E F) :
     min p.radius q.radius ≤ (p + q).radius := by
@@ -478,6 +490,16 @@ lemma HasFPowerSeriesWithinOnBall.congr {f g : E → F} {p : FormalMultilinearSe
     refine ⟨hy, ?_⟩
     simpa [edist_eq_coe_nnnorm_sub] using h'y
 
+/-- Variant of `HasFPowerSeriesWithinOnBall.congr` where one does not separate the congruence
+property between `s` and `x`, requesting it instead of `insert x s`. -/
+lemma HasFPowerSeriesWithinOnBall.congr' {f g : E → F} {p : FormalMultilinearSeries 𝕜 E F}
+    {s : Set E} {x : E} {r : ℝ≥0∞} (h : HasFPowerSeriesWithinOnBall f p s x r)
+    (h' : EqOn g f (insert x s ∩ EMetric.ball x r)) :
+    HasFPowerSeriesWithinOnBall g p s x r := by
+  refine ⟨h.r_le, h.r_pos, fun {y} hy h'y ↦ ?_⟩
+  convert h.hasSum hy h'y using 1
+  exact h' ⟨hy, by simpa [edist_eq_coe_nnnorm_sub] using h'y⟩
+
 lemma HasFPowerSeriesWithinAt.congr {f g : E → F} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E}
     {x : E} (h : HasFPowerSeriesWithinAt f p s x) (h' : g =ᶠ[𝓝[s] x] f) (h'' : g x = f x) :
     HasFPowerSeriesWithinAt g p s x := by
@@ -581,6 +603,39 @@ lemma HasFPowerSeriesAt.hasFPowerSeriesWithinAt (hf : HasFPowerSeriesAt f p x) :
   rw [← hasFPowerSeriesWithinAt_univ] at hf
   apply hf.mono (subset_univ _)
 
+theorem HasFPowerSeriesWithinAt.mono_of_mem {f : E → F} {p : FormalMultilinearSeries 𝕜 E F}
+    {s t : Set E} {x : E} (h : HasFPowerSeriesWithinAt f p s x) (hst : s ∈ 𝓝[t] x) :
+    HasFPowerSeriesWithinAt f p t x := by
+  rcases h with ⟨r, hr⟩
+  rcases EMetric.mem_nhdsWithin_iff.1 hst with ⟨r', r'_pos, hr'⟩
+  refine ⟨min r r', ?_⟩
+  have Z := hr.of_le (by simp [r'_pos, hr.r_pos]) (min_le_left r r')
+  refine ⟨Z.r_le, Z.r_pos, fun {y} hy h'y ↦ ?_⟩
+  apply Z.hasSum ?_ h'y
+  simp only [mem_insert_iff, add_right_eq_self] at hy
+  rcases hy with rfl | hy
+  · simp
+  apply mem_insert_of_mem _ (hr' ?_)
+  simp only [EMetric.mem_ball, edist_eq_coe_nnnorm_sub, sub_zero, lt_min_iff, mem_inter_iff,
+    add_sub_cancel_left, hy, and_true] at h'y ⊢
+  exact h'y.2
+
+@[simp] lemma hasFPowerSeriesWithinOnBall_insert_self {f : E → F}
+    {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ℝ≥0∞} :
+    HasFPowerSeriesWithinOnBall f p (insert x s) x r ↔ HasFPowerSeriesWithinOnBall f p s x r := by
+  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩  <;>
+  exact ⟨h.r_le, h.r_pos, fun {y} ↦ by simpa only [insert_idem] using h.hasSum (y := y)⟩
+
+@[simp] theorem hasFPowerSeriesAt_insert {f : E → F} {p : FormalMultilinearSeries 𝕜 E F}
+    {s : Set E} {x y : E} :
+    HasFPowerSeriesWithinAt f p (insert y s) x ↔ HasFPowerSeriesWithinAt f p s x := by
+  rcases eq_or_ne x y with rfl | hy
+  · simp [HasFPowerSeriesWithinAt]
+  · refine ⟨fun h ↦ h.mono (subset_insert _ _), fun h ↦ ?_⟩
+    apply HasFPowerSeriesWithinAt.mono_of_mem h
+    rw [nhdsWithin_insert_of_ne hy]
+    exact self_mem_nhdsWithin
+
 theorem HasFPowerSeriesWithinOnBall.coeff_zero (hf : HasFPowerSeriesWithinOnBall f pf s x r)
     (v : Fin 0 → E) : pf 0 v = f x := by
   have v_eq : v = fun i => 0 := Subsingleton.elim _ _
@@ -697,28 +752,53 @@ theorem analyticOnNhd_congr (hs : IsOpen s) (h : s.EqOn f g) : AnalyticOnNhd 
 @[deprecated (since := "2024-09-26")]
 alias analyticOn_congr := analyticOnNhd_congr
 
+theorem AnalyticWithinAt.mono_of_mem {f : E → F} {s t : Set E} {x : E}
+    (h : AnalyticWithinAt 𝕜 f s x) (hst : s ∈ 𝓝[t] x) : AnalyticWithinAt 𝕜 f t x := by
+  rcases h with ⟨p, hp⟩
+  exact ⟨p, hp.mono_of_mem hst⟩
+
 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
 
+@[simp] theorem analyticWithinAt_insert {f : E → F} {s : Set E} {x y : E} :
+    AnalyticWithinAt 𝕜 f (insert y s) x ↔ AnalyticWithinAt 𝕜 f s x := by
+  simp [AnalyticWithinAt]
+
 /-!
 ### Composition with linear maps
 -/
 
+/-- If a function `f` has a power series `p` on a ball within a set and `g` is linear,
+then `g ∘ f` has the power series `g ∘ p` on the same ball. -/
+theorem ContinuousLinearMap.comp_hasFPowerSeriesWithinOnBall (g : F →L[𝕜] G)
+    (h : HasFPowerSeriesWithinOnBall f p s x r) :
+    HasFPowerSeriesWithinOnBall (g ∘ f) (g.compFormalMultilinearSeries p) s x r where
+  r_le := h.r_le.trans (p.radius_le_radius_continuousLinearMap_comp _)
+  r_pos := h.r_pos
+  hasSum := fun hy h'y => by
+    simpa only [ContinuousLinearMap.compFormalMultilinearSeries_apply,
+      ContinuousLinearMap.compContinuousMultilinearMap_coe, Function.comp_apply] using
+      g.hasSum (h.hasSum hy h'y)
+
 /-- If a function `f` has a power series `p` on a ball and `g` is linear, then `g ∘ f` has the
 power series `g ∘ p` on the same ball. -/
 theorem ContinuousLinearMap.comp_hasFPowerSeriesOnBall (g : F →L[𝕜] G)
     (h : HasFPowerSeriesOnBall f p x r) :
-    HasFPowerSeriesOnBall (g ∘ f) (g.compFormalMultilinearSeries p) x r :=
-  { r_le := h.r_le.trans (p.radius_le_radius_continuousLinearMap_comp _)
-    r_pos := h.r_pos
-    hasSum := fun hy => by
-      simpa only [ContinuousLinearMap.compFormalMultilinearSeries_apply,
-        ContinuousLinearMap.compContinuousMultilinearMap_coe, Function.comp_apply] using
-        g.hasSum (h.hasSum hy) }
+    HasFPowerSeriesOnBall (g ∘ f) (g.compFormalMultilinearSeries p) x r := by
+  rw [← hasFPowerSeriesWithinOnBall_univ] at h ⊢
+  exact g.comp_hasFPowerSeriesWithinOnBall h
+
+/-- 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
+  rintro x hx
+  rcases h x hx with ⟨p, r, hp⟩
+  exact ⟨g.compFormalMultilinearSeries p, r, g.comp_hasFPowerSeriesWithinOnBall hp⟩
 
 /-- If a function `f` is analytic on a set `s` and `g` is linear, then `g ∘ f` is analytic
 on `s`. -/
@@ -729,9 +809,6 @@ theorem ContinuousLinearMap.comp_analyticOnNhd
   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
 -/
@@ -747,6 +824,13 @@ theorem HasFPowerSeriesOnBall.tendsto_partialSum
     Tendsto (fun n => p.partialSum n y) atTop (𝓝 (f (x + y))) :=
   (hf.hasSum hy).tendsto_sum_nat
 
+theorem HasFPowerSeriesAt.tendsto_partialSum
+    (hf : HasFPowerSeriesAt f p x) :
+    ∀ᶠ y in 𝓝 0, Tendsto (fun n => p.partialSum n y) atTop (𝓝 (f (x + y))) := by
+  rcases hf with ⟨r, hr⟩
+  filter_upwards [EMetric.ball_mem_nhds (0 : E) hr.r_pos] with y hy
+  exact hr.tendsto_partialSum hy
+
 open Finset in
 /-- If a function admits a power series expansion within a ball, then the partial sums
 `p.partialSum n z` converge to `f (x + y)` as `n → ∞` and `z → y`. Note that `x + z` doesn't need
@@ -1228,6 +1312,10 @@ protected theorem FormalMultilinearSeries.hasFPowerSeriesOnBall [CompleteSpace F
       rw [zero_add]
       exact p.hasSum hy }
 
+theorem HasFPowerSeriesWithinOnBall.sum (h : HasFPowerSeriesWithinOnBall f p s x r) {y : E}
+    (h'y : x + y ∈ insert x s) (hy : y ∈ EMetric.ball (0 : E) r) : f (x + y) = p.sum y :=
+  (h.hasSum h'y hy).tsum_eq.symm
+
 theorem HasFPowerSeriesOnBall.sum (h : HasFPowerSeriesOnBall f p x r) {y : E}
     (hy : y ∈ EMetric.ball (0 : E) r) : f (x + y) = p.sum y :=
   (h.hasSum hy).tsum_eq.symm

Mathlib/Analysis/Analytic/ChangeOrigin.lean

@@ -226,6 +226,12 @@ def derivSeries : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F) :=
   (continuousMultilinearCurryFin1 𝕜 E F : (E[×1]→L[𝕜] F) →L[𝕜] E →L[𝕜] F)
     |>.compFormalMultilinearSeries (p.changeOriginSeries 1)
 
+theorem radius_le_radius_derivSeries : p.radius ≤ p.derivSeries.radius := by
+  apply (p.le_changeOriginSeries_radius 1).trans (radius_le_of_le (fun n ↦ ?_))
+  apply (ContinuousLinearMap.norm_compContinuousMultilinearMap_le _ _).trans
+  apply mul_le_of_le_one_left (norm_nonneg  _)
+  exact ContinuousLinearMap.opNorm_le_bound _ zero_le_one (by simp)
+
 end
 
 -- From this point on, assume that the space is complete, to make sure that series that converge
@@ -284,39 +290,69 @@ theorem analyticAt_changeOrigin (p : FormalMultilinearSeries 𝕜 E F) (rp : p.r
 
 end FormalMultilinearSeries
 
+
 section
 
-variable [CompleteSpace F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x y : E} {r : ℝ≥0∞}
+variable [CompleteSpace F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E}
+  {x y : E} {r : ℝ≥0∞}
+
+/-- If a function admits a power series expansion `p` within a set `s` on a ball `B (x, r)`, then
+it  also admits a power series on any subball of this ball (even with a different center provided
+it belongs to `s`), given by `p.changeOrigin`. -/
+theorem HasFPowerSeriesWithinOnBall.changeOrigin (hf : HasFPowerSeriesWithinOnBall f p s x r)
+    (h : (‖y‖₊ : ℝ≥0∞) < r) (hy : x + y ∈ insert x s) :
+    HasFPowerSeriesWithinOnBall f (p.changeOrigin y) s (x + y) (r - ‖y‖₊) where
+  r_le := by
+    apply le_trans _ p.changeOrigin_radius
+    exact tsub_le_tsub hf.r_le le_rfl
+  r_pos := by simp [h]
+  hasSum := fun {z} h'z hz => by
+    have : f (x + y + z) =
+        FormalMultilinearSeries.sum (FormalMultilinearSeries.changeOrigin p y) z := by
+      rw [mem_emetric_ball_zero_iff, lt_tsub_iff_right, add_comm] at hz
+      rw [p.changeOrigin_eval (hz.trans_le hf.r_le), add_assoc, hf.sum]
+      · have : insert (x + y) s ⊆ insert (x + y) (insert x s) := by
+          apply insert_subset_insert (subset_insert _ _)
+        rw [insert_eq_of_mem hy] at this
+        apply this
+        simpa [add_assoc] using h'z
+      refine mem_emetric_ball_zero_iff.2 (lt_of_le_of_lt ?_ hz)
+      exact mod_cast nnnorm_add_le y z
+    rw [this]
+    apply (p.changeOrigin y).hasSum
+    refine EMetric.ball_subset_ball (le_trans ?_ p.changeOrigin_radius) hz
+    exact tsub_le_tsub hf.r_le le_rfl
 
 /-- If a function admits a power series expansion `p` on a ball `B (x, r)`, then it also admits a
 power series on any subball of this ball (even with a different center), given by `p.changeOrigin`.
 -/
 theorem HasFPowerSeriesOnBall.changeOrigin (hf : HasFPowerSeriesOnBall f p x r)
-    (h : (‖y‖₊ : ℝ≥0∞) < r) : HasFPowerSeriesOnBall f (p.changeOrigin y) (x + y) (r - ‖y‖₊) :=
-  { r_le := by
-      apply le_trans _ p.changeOrigin_radius
-      exact tsub_le_tsub hf.r_le le_rfl
-    r_pos := by simp [h]
-    hasSum := fun {z} hz => by
-      have : f (x + y + z) =
-          FormalMultilinearSeries.sum (FormalMultilinearSeries.changeOrigin p y) z := by
-        rw [mem_emetric_ball_zero_iff, lt_tsub_iff_right, add_comm] at hz
-        rw [p.changeOrigin_eval (hz.trans_le hf.r_le), add_assoc, hf.sum]
-        refine mem_emetric_ball_zero_iff.2 (lt_of_le_of_lt ?_ hz)
-        exact mod_cast nnnorm_add_le y z
-      rw [this]
-      apply (p.changeOrigin y).hasSum
-      refine EMetric.ball_subset_ball (le_trans ?_ p.changeOrigin_radius) hz
-      exact tsub_le_tsub hf.r_le le_rfl }
+    (h : (‖y‖₊ : ℝ≥0∞) < r) : HasFPowerSeriesOnBall f (p.changeOrigin y) (x + y) (r - ‖y‖₊) := by
+  rw [← hasFPowerSeriesWithinOnBall_univ] at hf ⊢
+  exact hf.changeOrigin h (by simp)
+
+/-- If a function admits a power series expansion `p` on an open ball `B (x, r)`, then
+it is analytic at every point of this ball. -/
+theorem HasFPowerSeriesWithinOnBall.analyticWithinAt_of_mem
+    (hf : HasFPowerSeriesWithinOnBall f p s x r)
+    (h : y ∈ insert x s ∩ EMetric.ball x r) : AnalyticWithinAt 𝕜 f s y := by
+  have : (‖y - x‖₊ : ℝ≥0∞) < r := by simpa [edist_eq_coe_nnnorm_sub] using h.2
+  have := hf.changeOrigin this (by simpa using h.1)
+  rw [add_sub_cancel] at this
+  exact this.analyticWithinAt
 
 /-- If a function admits a power series expansion `p` on an open ball `B (x, r)`, then
 it is analytic at every point of this ball. -/
 theorem HasFPowerSeriesOnBall.analyticAt_of_mem (hf : HasFPowerSeriesOnBall f p x r)
     (h : y ∈ EMetric.ball x r) : AnalyticAt 𝕜 f y := by
-  have : (‖y - x‖₊ : ℝ≥0∞) < r := by simpa [edist_eq_coe_nnnorm_sub] using h
-  have := hf.changeOrigin this
-  rw [add_sub_cancel] at this
-  exact this.analyticAt
+  rw [← hasFPowerSeriesWithinOnBall_univ] at hf
+  rw [← analyticWithinAt_univ]
+  exact hf.analyticWithinAt_of_mem (by simpa using h)
+
+theorem HasFPowerSeriesWithinOnBall.analyticOn (hf : HasFPowerSeriesWithinOnBall f p s x r) :
+    AnalyticOn 𝕜 f (insert x s ∩ EMetric.ball x r) :=
+  fun _ hy ↦ ((analyticWithinAt_insert (y := x)).2 (hf.analyticWithinAt_of_mem hy)).mono
+    inter_subset_left
 
 theorem HasFPowerSeriesOnBall.analyticOnNhd (hf : HasFPowerSeriesOnBall f p x r) :
     AnalyticOnNhd 𝕜 f (EMetric.ball x r) :=