feat: define ContinuousMultilinearMap.linearDeriv and show it's the…

… `fderiv` (#9846)

Co-authored-by: Sophie Morel



Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
Co-authored-by: morel <smorel@math.princeton.edu>

Mathlib/Analysis/Analytic/Basic.lean

@@ -1297,7 +1297,6 @@ theorem changeOrigin_radius : p.radius - ‖x‖₊ ≤ (p.changeOrigin x).radiu
 
 /-- `derivSeries p` is a power series for `fderiv 𝕜 f` if `p` is a power series for `f`,
 see `HasFPowerSeriesOnBall.fderiv`. -/
-noncomputable
 def derivSeries : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F) :=
   (continuousMultilinearCurryFin1 𝕜 E F : (E[×1]→L[𝕜] F) →L[𝕜] E →L[𝕜] F)
     |>.compFormalMultilinearSeries (p.changeOriginSeries 1)

Mathlib/Analysis/Analytic/CPolynomial.lean

@@ -57,6 +57,16 @@ structure HasFiniteFPowerSeriesOnBall (f : E → F) (p : FormalMultilinearSeries
     (n : ℕ) (r : ℝ≥0∞) extends HasFPowerSeriesOnBall f p x r : Prop where
   finite : ∀ (m : ℕ), n ≤ m → p m = 0
 
+theorem HasFiniteFPowerSeriesOnBall.mk' {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E}
+    {n : ℕ} {r : ℝ≥0∞} (finite : ∀ (m : ℕ), n ≤ m → p m = 0) (pos : 0 < r)
+    (sum_eq : ∀ y ∈ EMetric.ball 0 r, (∑ i in Finset.range n, p i fun _ ↦ y) = f (x + y)) :
+    HasFiniteFPowerSeriesOnBall f p x n r where
+  r_le := p.radius_eq_top_of_eventually_eq_zero (Filter.eventually_atTop.mpr ⟨n, finite⟩) ▸ le_top
+  r_pos := pos
+  hasSum hy := sum_eq _ hy ▸ hasSum_sum_of_ne_finset_zero fun m hm ↦ by
+    rw [Finset.mem_range, not_lt] at hm; rw [finite m hm]; rfl
+  finite := finite
+
 /-- Given a function `f : E → F`, a formal multilinear series `p` and `n : ℕ`, we say that
 `f` has `p` as a finite power series around `x` if `f (x + y) = ∑' pₙ yⁿ` for all `y` in a
 neighborhood of `0`and `pₙ = 0` for `n ≤ m`.-/

Mathlib/Analysis/Calculus/FDeriv/Analytic.lean

@@ -291,6 +291,80 @@ theorem CPolynomialOn.iterated_deriv (h : CPolynomialOn 𝕜 f s) (n : ℕ) :
 
 end deriv
 
+namespace ContinuousMultilinearMap
+
+variable {ι : Type*} {E : ι → Type*} [∀ i, NormedAddCommGroup (E i)] [∀ i, NormedSpace 𝕜 (E i)]
+  [Fintype ι] (f : ContinuousMultilinearMap 𝕜 E F)
+
+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
+    simp_rw [FormalMultilinearSeries.changeOriginSeriesTerm,
+      toFormalMultilinearSeries, dif_neg h.symm, LinearIsometryEquiv.map_zero]
+
+variable {n : ℕ∞} (x : ∀ i, E i)
+
+open Finset in
+theorem changeOrigin_toFormalMultilinearSeries [DecidableEq ι] :
+    continuousMultilinearCurryFin1 𝕜 (∀ i, E i) F (f.toFormalMultilinearSeries.changeOrigin x 1) =
+    f.linearDeriv x := by
+  ext y
+  rw [continuousMultilinearCurryFin1_apply, linearDeriv_apply,
+      changeOrigin, FormalMultilinearSeries.sum]
+  cases isEmpty_or_nonempty ι
+  · have (l) : 1 + l ≠ Fintype.card ι := by
+      rw [add_comm, Fintype.card_eq_zero]; exact Nat.succ_ne_zero _
+    simp_rw [Fintype.sum_empty, changeOriginSeries_support _ (this _), zero_apply _, tsum_zero]; rfl
+  rw [tsum_eq_single (Fintype.card ι - 1), changeOriginSeries]; swap
+  · intro m hm
+    rw [Ne, eq_tsub_iff_add_eq_of_le (by exact Fintype.card_pos), add_comm] at hm
+    rw [f.changeOriginSeries_support hm, zero_apply]
+  rw [sum_apply, ContinuousMultilinearMap.sum_apply, Fin.snoc_zero]
+  simp_rw [changeOriginSeriesTerm_apply]
+  refine (Fintype.sum_bijective (?_ ∘ Fintype.equivFinOfCardEq (Nat.add_sub_of_le
+    Fintype.card_pos).symm) (.comp ?_ <| Equiv.bijective _) _ _ fun i ↦ ?_).symm
+  · exact (⟨{·}ᶜ, by
+      rw [card_compl, Fintype.card_fin, card_singleton, Nat.add_sub_cancel_left]⟩)
+  · use fun _ _ ↦ (singleton_injective <| compl_injective <| Subtype.ext_iff.mp ·)
+    intro ⟨s, hs⟩
+    have h : sᶜ.card = 1 := by rw [card_compl, hs, Fintype.card_fin, Nat.add_sub_cancel]
+    obtain ⟨a, ha⟩ := card_eq_one.mp h
+    refine ⟨a, Subtype.ext (compl_eq_comm.mp ha)⟩
+  rw [Function.comp_apply, Subtype.coe_mk, compl_singleton, piecewise_erase_univ,
+    toFormalMultilinearSeries, dif_pos (Nat.add_sub_of_le Fintype.card_pos).symm]
+  simp_rw [domDomCongr_apply, compContinuousLinearMap_apply, ContinuousLinearMap.proj_apply,
+    Function.update_apply, (Equiv.injective _).eq_iff, ite_apply]
+  congr; ext j
+  obtain rfl | hj := eq_or_ne j i
+  · rw [Function.update_same, if_pos rfl]
+  · rw [Function.update_noteq hj, if_neg hj]
+
+protected theorem hasFDerivAt [DecidableEq ι] : HasFDerivAt f (f.linearDeriv x) x := by
+  rw [← changeOrigin_toFormalMultilinearSeries]
+  convert f.hasFiniteFPowerSeriesOnBall.hasFDerivAt (y := x) ENNReal.coe_lt_top
+  rw [zero_add]
+
+lemma cPolynomialAt : CPolynomialAt 𝕜 f x :=
+  f.hasFiniteFPowerSeriesOnBall.cPolynomialAt_of_mem
+    (by simp only [Metric.emetric_ball_top, Set.mem_univ])
+
+lemma cPolyomialOn : CPolynomialOn 𝕜 f ⊤ := fun x _ ↦ f.cPolynomialAt x
+
+lemma contDiffAt : ContDiffAt 𝕜 n f x := (f.cPolynomialAt x).contDiffAt
+
+lemma contDiff : ContDiff 𝕜 n f := contDiff_iff_contDiffAt.mpr f.contDiffAt
+
+end ContinuousMultilinearMap
+
 namespace FormalMultilinearSeries
 
 variable (p : FormalMultilinearSeries 𝕜 E F)
@@ -320,7 +394,7 @@ theorem iteratedFDeriv_zero_apply_diag : iteratedFDeriv 𝕜 0 f x = p 0 := by
   ext
   convert (h.hasSum <| EMetric.mem_ball_self h.r_pos).tsum_eq.symm
   · rw [iteratedFDeriv_zero_apply, add_zero]
-  · rw [tsum_eq_single 0 <| fun n hn ↦ by haveI := NeZero.mk hn; exact (p n).map_zero]
+  · rw [tsum_eq_single 0 fun n hn ↦ by haveI := NeZero.mk hn; exact (p n).map_zero]
     exact congr(p 0 $(Subsingleton.elim _ _))
 
 open ContinuousLinearMap

Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean

@@ -35,7 +35,7 @@ variable {𝕜 : Type u} {𝕜' : Type u'} {E : Type v} {F : Type w} {G : Type x
 
 section
 
-variable [CommRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E]
+variable [Ring 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E]
   [ContinuousConstSMul 𝕜 E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F]
   [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] [AddCommGroup G] [Module 𝕜 G]
   [TopologicalSpace G] [TopologicalAddGroup G] [ContinuousConstSMul 𝕜 G]
@@ -59,11 +59,9 @@ instance : Inhabited (FormalMultilinearSeries 𝕜 E F) :=
 
 section Module
 
-/- `derive` is not able to find the module structure, probably because Lean is confused by the
-dependent types. We register it explicitly. -/
--- Porting note: rewrote with `inferInstanceAs`
-instance : Module 𝕜 (FormalMultilinearSeries 𝕜 E F) :=
-  inferInstanceAs <| Module 𝕜 <| ∀ n : ℕ, E[×n]→L[𝕜] F
+instance (𝕜') [Semiring 𝕜'] [Module 𝕜' F] [ContinuousConstSMul 𝕜' F] [SMulCommClass 𝕜 𝕜' F] :
+    Module 𝕜' (FormalMultilinearSeries 𝕜 E F) :=
+  inferInstanceAs <| Module 𝕜' <| ∀ n : ℕ, E[×n]→L[𝕜] F
 
 end Module
 
@@ -138,7 +136,7 @@ theorem compContinuousLinearMap_apply (p : FormalMultilinearSeries 𝕜 F G) (u
   rfl
 #align formal_multilinear_series.comp_continuous_linear_map_apply FormalMultilinearSeries.compContinuousLinearMap_apply
 
-variable (𝕜) [CommRing 𝕜'] [SMul 𝕜 𝕜']
+variable (𝕜) [Ring 𝕜'] [SMul 𝕜 𝕜']
 
 variable [Module 𝕜' E] [ContinuousConstSMul 𝕜' E] [IsScalarTower 𝕜 𝕜' E]
 
@@ -181,13 +179,15 @@ def unshift (q : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)) (z : F) : Form
 
 end FormalMultilinearSeries
 
-namespace ContinuousLinearMap
+section
 
-variable [CommRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E]
+variable [Ring 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E]
   [ContinuousConstSMul 𝕜 E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F]
   [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] [AddCommGroup G] [Module 𝕜 G]
   [TopologicalSpace G] [TopologicalAddGroup G] [ContinuousConstSMul 𝕜 G]
 
+namespace ContinuousLinearMap
+
 /-- Composing each term `pₙ` in a formal multilinear series with a continuous linear map `f` on the
 left gives a new formal multilinear series `f.compFormalMultilinearSeries p` whose general term
 is `f ∘ pₙ`. -/
@@ -208,11 +208,28 @@ theorem compFormalMultilinearSeries_apply' (f : F →L[𝕜] G) (p : FormalMulti
 
 end ContinuousLinearMap
 
+namespace ContinuousMultilinearMap
+
+variable {ι : Type*} {E : ι → Type*} [∀ i, AddCommGroup (E i)] [∀ i, Module 𝕜 (E i)]
+  [∀ i, TopologicalSpace (E i)] [∀ i, TopologicalAddGroup (E i)]
+  [∀ i, ContinuousConstSMul 𝕜 (E i)] [Fintype ι] (f : ContinuousMultilinearMap 𝕜 E F)
+
+/-- Realize a ContinuousMultilinearMap on `∀ i : ι, E i` as the evaluation of a
+FormalMultilinearSeries by choosing an arbitrary identification `ι ≃ Fin (Fintype.card ι)`. -/
+noncomputable def toFormalMultilinearSeries : FormalMultilinearSeries 𝕜 (∀ i, E i) F :=
+  fun n ↦ if h : Fintype.card ι = n then
+    (f.compContinuousLinearMap .proj).domDomCongr (Fintype.equivFinOfCardEq h)
+  else 0
+
+end ContinuousMultilinearMap
+
+end
+
 namespace FormalMultilinearSeries
 
 section Order
 
-variable [CommRing 𝕜] {n : ℕ} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E]
+variable [Ring 𝕜] {n : ℕ} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E]
   [TopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] [AddCommGroup F] [Module 𝕜 F]
   [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 F]
   {p : FormalMultilinearSeries 𝕜 E F}

Mathlib/Topology/Algebra/Module/Multilinear/Basic.lean

@@ -381,6 +381,23 @@ def domDomCongrEquiv {ι' : Type*} (e : ι ≃ ι') :
 #align continuous_multilinear_map.dom_dom_congr_equiv_apply ContinuousMultilinearMap.domDomCongrEquiv_apply
 #align continuous_multilinear_map.dom_dom_congr_equiv_symm_apply ContinuousMultilinearMap.domDomCongrEquiv_symm_apply
 
+section linearDeriv
+open scoped BigOperators
+variable [ContinuousAdd M₂] [DecidableEq ι] [Fintype ι] (x y : ∀ i, M₁ i)
+
+/-- The derivative of a continuous multilinear map, as a continuous linear map
+from `∀ i, M₁ i` to `M₂`; see `ContinuousMultilinearMap.hasFDerivAt`. -/
+def linearDeriv : (∀ i, M₁ i) →L[R] M₂ := ∑ i : ι, (f.toContinuousLinearMap x i).comp (.proj i)
+
+@[simp]
+lemma linearDeriv_apply : f.linearDeriv x y = ∑ i, f (Function.update x i (y i)) := by
+  unfold linearDeriv toContinuousLinearMap
+  simp only [ContinuousLinearMap.coe_sum', ContinuousLinearMap.coe_comp',
+    ContinuousLinearMap.coe_mk', LinearMap.coe_mk, LinearMap.coe_toAddHom, Finset.sum_apply]
+  rfl
+
+end linearDeriv
+
 /-- In the specific case of continuous multilinear maps on spaces indexed by `Fin (n+1)`, where one
 can build an element of `(i : Fin (n+1)) → M i` using `cons`, one can express directly the
 additivity of a multilinear map along the first variable. -/