feat: a continuous linear map into continuous multilinear maps is ana…

…lytic (#16844)

Also move the fact that continuous linear maps are analytic to the proper place, i.e., in `Analytic.CPolynomial` instead of `Calculus.FDeriv.Analytic`.

Mathlib/Analysis/Analytic/CPolynomial.lean

@@ -34,9 +34,13 @@ We develop the basic properties of these notions, notably:
 * If a function admits a finite power series in a ball, then it is continuously polynomial at
   any point `y` of this ball, and the power series there can be expressed in terms of the initial
   power series `p` as `p.changeOrigin y`, which is finite (with the same bound as `p`) by
-  `changeOrigin_finite_of_finite`. See `HasFiniteFPowerSeriesOnBall.changeOrigin `. It follows in
+  `changeOrigin_finite_of_finite`. See `HasFiniteFPowerSeriesOnBall.changeOrigin`. It follows in
   particular that the set of points at which a given function is continuously polynomial is open,
   see `isOpen_cPolynomialAt`.
+
+We prove in particular that continuous multilinear maps are continuously polynomial, and so
+are continuous linear maps into continuous multilinear maps. In particular, such maps are
+analytic.
 -/
 
 variable {𝕜 E F G : Type*} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E]
@@ -539,3 +543,114 @@ theorem CPolynomialAt.exists_ball_cPolynomialOn {f : E → F} {x : E} (h : CPoly
   Metric.isOpen_iff.mp (isOpen_cPolynomialAt _ _) _ h
 
 end
+
+/-!
+### Continuous multilinear maps
+
+We show that continuous multilinear maps are continuously polynomial, and therefore analytic.
+-/
+
+namespace ContinuousMultilinearMap
+
+variable {ι : Type*} {Em : ι → Type*} [∀ i, NormedAddCommGroup (Em i)] [∀ i, NormedSpace 𝕜 (Em i)]
+  [Fintype ι] (f : ContinuousMultilinearMap 𝕜 Em F) {x : Π i, Em i} {s : Set (Π i, Em i)}
+
+open FormalMultilinearSeries
+
+protected theorem hasFiniteFPowerSeriesOnBall :
+    HasFiniteFPowerSeriesOnBall f f.toFormalMultilinearSeries 0 (Fintype.card ι + 1) ⊤ :=
+  .mk' (fun m hm ↦ dif_neg (Nat.succ_le_iff.mp hm).ne) ENNReal.zero_lt_top fun y _ ↦ by
+    rw [Finset.sum_eq_single_of_mem _ (Finset.self_mem_range_succ _), zero_add]
+    · rw [toFormalMultilinearSeries, dif_pos rfl]; rfl
+    · intro m _ ne; rw [toFormalMultilinearSeries, dif_neg ne.symm]; rfl
+
+lemma cpolynomialAt  : CPolynomialAt 𝕜 f x :=
+  f.hasFiniteFPowerSeriesOnBall.cPolynomialAt_of_mem
+    (by simp only [Metric.emetric_ball_top, Set.mem_univ])
+
+lemma cpolyomialOn : CPolynomialOn 𝕜 f s := fun _ _ ↦ f.cpolynomialAt
+
+lemma analyticOn : AnalyticOn 𝕜 f s := f.cpolyomialOn.analyticOn
+
+lemma analyticWithinOn : AnalyticWithinOn 𝕜 f s :=
+  f.analyticOn.analyticWithinOn
+
+lemma analyticAt : AnalyticAt 𝕜 f x := f.cpolynomialAt.analyticAt
+
+lemma analyticWithinAt : AnalyticWithinAt 𝕜 f s x := f.analyticAt.analyticWithinAt
+
+end ContinuousMultilinearMap
+
+
+/-!
+### Continuous linear maps into continuous multilinear maps
+
+We show that a continuous linear map into continuous multilinear maps is continuously polynomial
+(as a function of two variables, i.e., uncurried). Therefore, it is also analytic.
+-/
+
+namespace ContinuousLinearMap
+
+variable {ι : Type*} {Em : ι → Type*} [∀ i, NormedAddCommGroup (Em i)] [∀ i, NormedSpace 𝕜 (Em i)]
+  [Fintype ι] (f : G →L[𝕜] ContinuousMultilinearMap 𝕜 Em F)
+  {s : Set (G × (Π i, Em i))} {x : G × (Π i, Em i)}
+
+/-- Formal multilinear series associated to a linear map into multilinear maps. -/
+noncomputable def toFormalMultilinearSeriesOfMultilinear :
+    FormalMultilinearSeries 𝕜 (G × (Π i, Em i)) F :=
+  fun n ↦ if h : Fintype.card (Option ι) = n then
+    (f.continuousMultilinearMapOption).domDomCongr (Fintype.equivFinOfCardEq h)
+  else 0
+
+protected theorem hasFiniteFPowerSeriesOnBall_uncurry_of_multilinear :
+    HasFiniteFPowerSeriesOnBall (fun (p : G × (Π i, Em i)) ↦ f p.1 p.2)
+      f.toFormalMultilinearSeriesOfMultilinear 0 (Fintype.card (Option ι) + 1) ⊤ := by
+  apply HasFiniteFPowerSeriesOnBall.mk' ?_ ENNReal.zero_lt_top  ?_
+  · intro m hm
+    apply dif_neg
+    exact Nat.ne_of_lt hm
+  · intro y _
+    rw [Finset.sum_eq_single_of_mem _ (Finset.self_mem_range_succ _), zero_add]
+    · rw [toFormalMultilinearSeriesOfMultilinear, dif_pos rfl]; rfl
+    · intro m _ ne; rw [toFormalMultilinearSeriesOfMultilinear, dif_neg ne.symm]; rfl
+
+lemma cpolynomialAt_uncurry_of_multilinear :
+    CPolynomialAt 𝕜 (fun (p : G × (Π i, Em i)) ↦ f p.1 p.2) x :=
+  f.hasFiniteFPowerSeriesOnBall_uncurry_of_multilinear.cPolynomialAt_of_mem
+    (by simp only [Metric.emetric_ball_top, Set.mem_univ])
+
+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 analyticWithinOn_uncurry_of_multilinear :
+    AnalyticWithinOn 𝕜 (fun (p : G × (Π i, Em i)) ↦ f p.1 p.2) s :=
+  f.analyticOn_uncurry_of_multilinear.analyticWithinOn
+
+lemma analyticAt_uncurry_of_multilinear : AnalyticAt 𝕜 (fun (p : G × (Π i, Em i)) ↦ f p.1 p.2) x :=
+  f.cpolynomialAt_uncurry_of_multilinear.analyticAt
+
+lemma analyticWithinAt_uncurry_of_multilinear :
+    AnalyticWithinAt 𝕜 (fun (p : G × (Π i, Em i)) ↦ f p.1 p.2) s x :=
+  f.analyticAt_uncurry_of_multilinear.analyticWithinAt
+
+lemma continuousOn_uncurry_of_multilinear :
+    ContinuousOn (fun (p : G × (Π i, Em i)) ↦ f p.1 p.2) s :=
+  f.analyticOn_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
+
+lemma continuousAt_uncurry_of_multilinear :
+    ContinuousAt (fun (p : G × (Π i, Em i)) ↦ f p.1 p.2) x :=
+  f.analyticAt_uncurry_of_multilinear.continuousAt
+
+lemma continuousWithinAt_uncurry_of_multilinear :
+    ContinuousWithinAt (fun (p : G × (Π i, Em i)) ↦ f p.1 p.2) s x :=
+  f.analyticWithinAt_uncurry_of_multilinear.continuousWithinAt
+
+end ContinuousLinearMap

Mathlib/Analysis/Calculus/FDeriv/Analytic.lean

@@ -278,13 +278,6 @@ variable {ι : Type*} {E : ι → Type*} [∀ i, NormedAddCommGroup (E i)] [∀
 
 open FormalMultilinearSeries
 
-protected theorem hasFiniteFPowerSeriesOnBall :
-    HasFiniteFPowerSeriesOnBall f f.toFormalMultilinearSeries 0 (Fintype.card ι + 1) ⊤ :=
-  .mk' (fun m hm ↦ dif_neg (Nat.succ_le_iff.mp hm).ne) ENNReal.zero_lt_top fun y _ ↦ by
-    rw [Finset.sum_eq_single_of_mem _ (Finset.self_mem_range_succ _), zero_add]
-    · rw [toFormalMultilinearSeries, dif_pos rfl]; rfl
-    · intro m _ ne; rw [toFormalMultilinearSeries, dif_neg ne.symm]; rfl
-
 theorem changeOriginSeries_support {k l : ℕ} (h : k + l ≠ Fintype.card ι) :
     f.toFormalMultilinearSeries.changeOriginSeries k l = 0 :=
   Finset.sum_eq_zero fun _ _ ↦ by

Mathlib/Analysis/NormedSpace/Multilinear/Curry.lean

@@ -603,3 +603,58 @@ theorem curryFinFinset_apply_const (hk : s.card = k) (hl : sᶜ.card = l) (f : G
 end
 
 end ContinuousMultilinearMap
+
+namespace ContinuousLinearMap
+
+variable {F G : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
+  [NormedAddCommGroup G] [NormedSpace 𝕜 G]
+
+/-- Given a linear map into continuous multilinear maps
+`B : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F`, one can not always uncurry it as `G` and `E` might
+live in a different universe. However, one can always lift it to a continuous multilinear map
+on `(G × (Π i, E i)) ^ (1 + n)`, which maps `(v_0, ..., v_n)` to `B (g_0) (u_1, ..., u_n)` where
+`g_0` is the `G`-coordinate of `v_0` and `u_i` is the `E_i` coordinate of `v_i`. -/
+noncomputable def continuousMultilinearMapOption (B : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F) :
+    ContinuousMultilinearMap 𝕜 (fun (_ : Option ι) ↦ (G × (Π i, E i))) F :=
+  MultilinearMap.mkContinuous
+  { toFun := fun p ↦ B (p none).1 (fun i ↦ (p i).2 i)
+    map_add' := by
+      intro inst v j x y
+      match j with
+      | none => simp
+      | some j =>
+        classical
+        have B z : (fun i ↦ (Function.update v (some j) z (some i)).2 i) =
+            Function.update (fun (i : ι) ↦ (v i).2 i) j (z.2 j) := by
+          ext i
+          rcases eq_or_ne i j with rfl | hij
+          · simp
+          · simp [hij]
+        simp [B]
+    map_smul' := by
+      intro inst v j c x
+      match j with
+      | none => simp
+      | some j =>
+        classical
+        have B z : (fun i ↦ (Function.update v (some j) z (some i)).2 i) =
+            Function.update (fun (i : ι) ↦ (v i).2 i) j (z.2 j) := by
+          ext i
+          rcases eq_or_ne i j with rfl | hij
+          · simp
+          · simp [hij]
+        simp [B] } (‖B‖) <| by
+  intro b
+  simp only [MultilinearMap.coe_mk, Fintype.prod_option]
+  apply (ContinuousMultilinearMap.le_opNorm _ _).trans
+  rw [← mul_assoc]
+  gcongr with i _
+  · apply (B.le_opNorm _).trans
+    gcongr
+    exact norm_fst_le _
+  · exact (norm_le_pi_norm _ _).trans (norm_snd_le _)
+
+lemma continuousMultilinearMapOption_apply_eq_self (B : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F)
+    (a : G) (v : Π i, E i) : B.continuousMultilinearMapOption (fun _ ↦ (a, v)) = B a v := rfl
+
+end ContinuousLinearMap