feat: the composition of continuously polynomial functions is continuously polynomial (#30086)

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Author: sgouezel

Mathlib/Analysis/Analytic/Composition.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel, Johan Commelin
 -/
 import Mathlib.Analysis.Analytic.Basic
+import Mathlib.Analysis.Analytic.CPolynomialDef
 import Mathlib.Combinatorics.Enumerative.Composition
 
 /-!
@@ -808,7 +809,7 @@ theorem HasFPowerSeriesWithinAt.comp {g : F → G} {f : E → F} {q : FormalMult
   exact E
 
 /-- 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` within `s`. -/
+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) :
@@ -892,6 +893,79 @@ lemma AnalyticOnNhd.comp_analyticOn {f : F → G} {g : E → F} {s : Set F}
     AnalyticOn 𝕜 (f ∘ g) t :=
   fun x m ↦ (hf _ (h m)).comp_analyticWithinAt (hg x m)
 
+/-- If two functions `g` and `f` have finite power series `q` and `p` respectively at `f x` and `x`,
+then `g ∘ f` admits the finite power series `q.comp p` at `x`. -/
+theorem HasFiniteFPowerSeriesAt.comp {m n : ℕ} {g : F → G} {f : E → F}
+    {q : FormalMultilinearSeries 𝕜 F G} {p : FormalMultilinearSeries 𝕜 E F} {x : E}
+    (hg : HasFiniteFPowerSeriesAt g q (f x) m) (hf : HasFiniteFPowerSeriesAt f p x n) (hn : 0 < n) :
+    HasFiniteFPowerSeriesAt (g ∘ f) (q.comp p) x (m * n) := by
+  rcases hg.hasFPowerSeriesAt.comp hf.hasFPowerSeriesAt with ⟨r, hr⟩
+  refine ⟨r, hr, fun i hi ↦ ?_⟩
+  apply Finset.sum_eq_zero
+  rintro c -
+  ext v
+  simp only [compAlongComposition_apply, ContinuousMultilinearMap.zero_apply]
+  rcases le_or_gt m c.length with hc | hc
+  · simp [hg.finite _ hc]
+  obtain ⟨j, hj⟩ : ∃ j, n ≤ c.blocksFun j := by
+    contrapose! hi
+    rw [← c.sum_blocksFun]
+    rcases eq_zero_or_pos c.length with h'c | h'c
+    · have : ∑ j : Fin c.length, c.blocksFun j = 0 := by
+        apply Finset.sum_eq_zero (fun j hj ↦ ?_)
+        have := j.2
+        grind
+      rw [this]
+      exact mul_pos (by grind) hn
+    · calc ∑ j : Fin c.length, c.blocksFun j
+      _ < ∑ j : Fin c.length, n := by
+        apply Finset.sum_lt_sum (fun j hj ↦ (hi j).le)
+        exact ⟨⟨0, h'c⟩, Finset.mem_univ _, hi _⟩
+      _ = c.length * n := by simp
+      _ ≤ m * n := by gcongr
+  apply ContinuousMultilinearMap.map_coord_zero _ j
+  simp [applyComposition, hf.finite _ hj]
+
+/-- If two functions `g` and `f` are continuously polynomial respectively at `f x` and `x`,
+then `g ∘ f` is continuously polynomial at `x`. -/
+theorem CPolynomialAt.comp {g : F → G} {f : E → F} {x : E}
+    (hg : CPolynomialAt 𝕜 g (f x)) (hf : CPolynomialAt 𝕜 f x) :
+    CPolynomialAt 𝕜 (g ∘ f) x := by
+  rcases hg with ⟨q, m, hm⟩
+  rcases hf with ⟨p, n, hn⟩
+  refine ⟨q.comp p, m * (n + 1), ?_⟩
+  exact hm.comp (hn.of_le (Nat.le_succ n)) (Nat.zero_lt_succ n)
+
+/-- If two functions `g` and `f` are continuously polynomial respectively at `f x` and `x`,
+then `g ∘ f` is continuously polynomial at `x`. -/
+theorem CPolynomialAt.fun_comp {g : F → G} {f : E → F} {x : E}
+    (hg : CPolynomialAt 𝕜 g (f x)) (hf : CPolynomialAt 𝕜 f x) :
+    CPolynomialAt 𝕜 (fun z ↦ g (f z)) x :=
+  hg.comp hf
+
+/-- Version of `CPolynomialAt.comp` where point equality is a separate hypothesis. -/
+theorem CPolynomialAt.comp_of_eq {g : F → G} {f : E → F} {y : F} {x : E} (hg : CPolynomialAt 𝕜 g y)
+    (hf : CPolynomialAt 𝕜 f x) (hy : f x = y) : CPolynomialAt 𝕜 (g ∘ f) x := by
+  rw [← hy] at hg
+  exact hg.comp hf
+
+/-- Version of `CPolynomialAt.comp` where point equality is a separate hypothesis. -/
+theorem CPolynomialAt.fun_comp_of_eq {g : F → G} {f : E → F} {y : F} {x : E}
+    (hg : CPolynomialAt 𝕜 g y) (hf : CPolynomialAt 𝕜 f x) (hy : f x = y) :
+    CPolynomialAt 𝕜 (fun z ↦ g (f z)) x :=
+  hg.comp_of_eq hf hy
+
+/-- If two functions `g` and `f` are continuously polynomial respectively on `s.image f` and `s`,
+then `g ∘ f` is continuously polynomial on `s`. -/
+theorem CPolynomialOn.comp' {s : Set E} {g : F → G} {f : E → F} (hg : CPolynomialOn 𝕜 g (s.image f))
+    (hf : CPolynomialOn 𝕜 f s) : CPolynomialOn 𝕜 (g ∘ f) s :=
+  fun z hz => (hg (f z) (Set.mem_image_of_mem f hz)).comp (hf z hz)
+
+theorem CPolynomialOn.comp {s : Set E} {t : Set F} {g : F → G} {f : E → F}
+    (hg : CPolynomialOn 𝕜 g t) (hf : CPolynomialOn 𝕜 f s) (st : Set.MapsTo f s t) :
+    CPolynomialOn 𝕜 (g ∘ f) s :=
+  comp' (mono hg (Set.mapsTo_iff_image_subset.mp st)) hf
+
 /-!
 ### Associativity of the composition of formal multilinear series