feat: fderiv of ContinuousMultilinearMap applied to const; use for Sc…

…hwartzMap.iteratedPDeriv (#9576)

add `ContinuousMultilinearMap.apply`; use for `fderiv`, `iteratedFDeriv`, `SchwartzMap.iteratedPDeriv`

Defining `ContinuousMultilinearMap.apply` as a CLM (using existing proof of continuity) enables the proof that the application of a `ContinuousMultilinearMap` to a constant commutes with differentiation.

This closes a todo in `Mathlib/Analysis/Distribution/SchwartzSpace.lean`.



Co-authored-by: Jack Valmadre <jvlmdr@users.noreply.github.com>

Mathlib/Analysis/Calculus/ContDiff/Basic.lean

@@ -907,6 +907,40 @@ theorem ContDiff.smulRight {f : E → F →L[𝕜] 𝕜} {g : E → G} {n : ℕ
 
 end SpecificBilinearMaps
 
+section ClmApplyConst
+
+/-- Application of a `ContinuousLinearMap` to a constant commutes with `iteratedFDerivWithin`. -/
+theorem iteratedFDerivWithin_clm_apply_const_apply
+    {s : Set E} (hs : UniqueDiffOn 𝕜 s) {n : ℕ∞} {c : E → F →L[𝕜] G} (hc : ContDiffOn 𝕜 n c s)
+    {i : ℕ} (hi : i ≤ n) {x : E} (hx : x ∈ s) {u : F} {m : Fin i → E} :
+    (iteratedFDerivWithin 𝕜 i (fun y ↦ (c y) u) s x) m = (iteratedFDerivWithin 𝕜 i c s x) m u := by
+  induction i generalizing x with
+  | zero => simp
+  | succ i ih =>
+    replace hi : i < n := lt_of_lt_of_le (by norm_cast; simp) hi
+    have h_deriv_apply : DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 i (fun y ↦ (c y) u) s) s :=
+      (hc.clm_apply contDiffOn_const).differentiableOn_iteratedFDerivWithin hi hs
+    have h_deriv : DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 i c s) s :=
+      hc.differentiableOn_iteratedFDerivWithin hi hs
+    simp only [iteratedFDerivWithin_succ_apply_left]
+    rw [← fderivWithin_continuousMultilinear_apply_const_apply (hs x hx) (h_deriv_apply x hx)]
+    rw [fderivWithin_congr' (fun x hx ↦ ih hi.le hx) hx]
+    rw [fderivWithin_clm_apply (hs x hx) (h_deriv.continuousMultilinear_apply_const _ x hx)
+      (differentiableWithinAt_const u)]
+    rw [fderivWithin_const_apply _ (hs x hx)]
+    simp only [ContinuousLinearMap.flip_apply, ContinuousLinearMap.comp_zero, zero_add]
+    rw [fderivWithin_continuousMultilinear_apply_const_apply (hs x hx) (h_deriv x hx)]
+
+/-- Application of a `ContinuousLinearMap` to a constant commutes with `iteratedFDeriv`. -/
+theorem iteratedFDeriv_clm_apply_const_apply
+    {n : ℕ∞} {c : E → F →L[𝕜] G} (hc : ContDiff 𝕜 n c)
+    {i : ℕ} (hi : i ≤ n) {x : E} {u : F} {m : Fin i → E} :
+    (iteratedFDeriv 𝕜 i (fun y ↦ (c y) u) x) m = (iteratedFDeriv 𝕜 i c x) m u := by
+  simp only [← iteratedFDerivWithin_univ]
+  exact iteratedFDerivWithin_clm_apply_const_apply uniqueDiffOn_univ hc.contDiffOn hi (mem_univ _)
+
+end ClmApplyConst
+
 /-- The natural equivalence `(E × F) × G ≃ E × (F × G)` is smooth.
 
 Warning: if you think you need this lemma, it is likely that you can simplify your proof by

Mathlib/Analysis/Calculus/FDeriv/Mul.lean

@@ -159,6 +159,69 @@ theorem fderiv_clm_apply (hc : DifferentiableAt 𝕜 c x) (hu : DifferentiableAt
 
 end CLMCompApply
 
+section ContinuousMultilinearApplyConst
+
+/-! ### Derivative of the application of continuous multilinear maps to a constant -/
+
+variable {ι : Type*} [Fintype ι]
+  {M : ι → Type*} [∀ i, NormedAddCommGroup (M i)] [∀ i, NormedSpace 𝕜 (M i)]
+  {H : Type*} [NormedAddCommGroup H] [NormedSpace 𝕜 H]
+  {c : E → ContinuousMultilinearMap 𝕜 M H}
+  {c' : E →L[𝕜] ContinuousMultilinearMap 𝕜 M H}
+
+theorem HasStrictFDerivAt.continuousMultilinear_apply_const (hc : HasStrictFDerivAt c c' x)
+    (u : ∀ i, M i) : HasStrictFDerivAt (fun y ↦ (c y) u) (c'.flipMultilinear u) x :=
+  (ContinuousMultilinearMap.apply 𝕜 M H u).hasStrictFDerivAt.comp x hc
+
+theorem HasFDerivWithinAt.continuousMultilinear_apply_const (hc : HasFDerivWithinAt c c' s x)
+    (u : ∀ i, M i) :
+    HasFDerivWithinAt (fun y ↦ (c y) u) (c'.flipMultilinear u) s x :=
+  (ContinuousMultilinearMap.apply 𝕜 M H u).hasFDerivAt.comp_hasFDerivWithinAt x hc
+
+theorem HasFDerivAt.continuousMultilinear_apply_const (hc : HasFDerivAt c c' x) (u : ∀ i, M i) :
+    HasFDerivAt (fun y ↦ (c y) u) (c'.flipMultilinear u) x :=
+  (ContinuousMultilinearMap.apply 𝕜 M H u).hasFDerivAt.comp x hc
+
+theorem DifferentiableWithinAt.continuousMultilinear_apply_const
+    (hc : DifferentiableWithinAt 𝕜 c s x) (u : ∀ i, M i) :
+    DifferentiableWithinAt 𝕜 (fun y ↦ (c y) u) s x :=
+  (hc.hasFDerivWithinAt.continuousMultilinear_apply_const u).differentiableWithinAt
+
+theorem DifferentiableAt.continuousMultilinear_apply_const (hc : DifferentiableAt 𝕜 c x)
+    (u : ∀ i, M i) :
+    DifferentiableAt 𝕜 (fun y ↦ (c y) u) x :=
+  (hc.hasFDerivAt.continuousMultilinear_apply_const u).differentiableAt
+
+theorem DifferentiableOn.continuousMultilinear_apply_const (hc : DifferentiableOn 𝕜 c s)
+    (u : ∀ i, M i) : DifferentiableOn 𝕜 (fun y ↦ (c y) u) s :=
+  fun x hx ↦ (hc x hx).continuousMultilinear_apply_const u
+
+theorem Differentiable.continuousMultilinear_apply_const (hc : Differentiable 𝕜 c) (u : ∀ i, M i) :
+    Differentiable 𝕜 fun y ↦ (c y) u := fun x ↦ (hc x).continuousMultilinear_apply_const u
+
+theorem fderivWithin_continuousMultilinear_apply_const (hxs : UniqueDiffWithinAt 𝕜 s x)
+    (hc : DifferentiableWithinAt 𝕜 c s x) (u : ∀ i, M i) :
+    fderivWithin 𝕜 (fun y ↦ (c y) u) s x = ((fderivWithin 𝕜 c s x).flipMultilinear u) :=
+  (hc.hasFDerivWithinAt.continuousMultilinear_apply_const u).fderivWithin hxs
+
+theorem fderiv_continuousMultilinear_apply_const (hc : DifferentiableAt 𝕜 c x) (u : ∀ i, M i) :
+    (fderiv 𝕜 (fun y ↦ (c y) u) x) = (fderiv 𝕜 c x).flipMultilinear u :=
+  (hc.hasFDerivAt.continuousMultilinear_apply_const u).fderiv
+
+/-- Application of a `ContinuousMultilinearMap` to a constant commutes with `fderivWithin`. -/
+theorem fderivWithin_continuousMultilinear_apply_const_apply (hxs : UniqueDiffWithinAt 𝕜 s x)
+    (hc : DifferentiableWithinAt 𝕜 c s x) (u : ∀ i, M i) (m : E) :
+    (fderivWithin 𝕜 (fun y ↦ (c y) u) s x) m = (fderivWithin 𝕜 c s x) m u := by
+  simp [fderivWithin_continuousMultilinear_apply_const hxs hc]
+
+/-- Application of a `ContinuousMultilinearMap` to a constant commutes with `fderiv`. -/
+theorem fderiv_continuousMultilinear_apply_const_apply (hc : DifferentiableAt 𝕜 c x)
+    (u : ∀ i, M i) (m : E) :
+    (fderiv 𝕜 (fun y ↦ (c y) u) x) m = (fderiv 𝕜 c x) m u := by
+  simp [fderiv_continuousMultilinear_apply_const hc]
+
+end ContinuousMultilinearApplyConst
+
 section SMul
 
 /-! ### Derivative of the product of a scalar-valued function and a vector-valued function

Mathlib/Analysis/Distribution/SchwartzSpace.lean

@@ -957,7 +957,16 @@ theorem iteratedPDeriv_succ_right {n : ℕ} (m : Fin (n + 1) → E) (f : 𝓢(E,
       simp only [hmtail, iteratedPDeriv_succ_left, hmzero, Fin.tail_init_eq_init_tail]
 #align schwartz_map.iterated_pderiv_succ_right SchwartzMap.iteratedPDeriv_succ_right
 
--- Todo: `iteratedPDeriv 𝕜 m f x = iteratedFDeriv ℝ f x m`
+theorem iteratedPDeriv_eq_iteratedFDeriv {n : ℕ} {m : Fin n → E} {f : 𝓢(E, F)} {x : E} :
+    iteratedPDeriv 𝕜 m f x = iteratedFDeriv ℝ n f x m := by
+  induction n generalizing x with
+  | zero => simp
+  | succ n ih =>
+    simp only [iteratedPDeriv_succ_left, iteratedFDeriv_succ_apply_left]
+    rw [← fderiv_continuousMultilinear_apply_const_apply]
+    · simp [← ih]
+    · exact f.smooth'.differentiable_iteratedFDeriv (WithTop.coe_lt_top n) _
+
 end Derivatives
 
 section BoundedContinuousFunction

Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean

@@ -789,6 +789,21 @@ theorem hasSum_eval {α : Type*} {p : α → ContinuousMultilinearMap 𝕜 E G}
   simp
 #align continuous_multilinear_map.has_sum_eval ContinuousMultilinearMap.hasSum_eval
 
+variable (𝕜 E G)
+
+/-- The application of a multilinear map as a `ContinuousLinearMap`. -/
+def apply (m : ∀ i, E i) : ContinuousMultilinearMap 𝕜 E G →L[𝕜] G where
+  toFun c := c m
+  map_add' _ _ := rfl
+  map_smul' _ _ := rfl
+  cont := continuous_eval_left m
+
+variable {𝕜 E G}
+
+@[simp]
+lemma apply_apply {m : ∀ i, E i} {c : ContinuousMultilinearMap 𝕜 E G} :
+    (apply 𝕜 E G m) c = c m := rfl
+
 end ContinuousMultilinearMap
 
 /-- If a continuous multilinear map is constructed from a multilinear map via the constructor