feat(analysis/calculus/[f]deriv): derivative of pointwise composition…

…/application of continuous linear maps (#9174)

This introduces useful analogs to the product rule when working with derivatives in spaces of continuous linear maps.

src/analysis/calculus/deriv.lean

@@ -1566,6 +1566,88 @@ by simp only [div_eq_mul_inv, deriv_mul_const_field]
 
 end division
 
+section clm_comp_apply
+/-! ### Derivative of the pointwise composition/application of continuous linear maps -/
+
+open continuous_linear_map
+
+variables {G : Type*} [normed_group G] [normed_space 𝕜 G] {c : 𝕜 → F →L[𝕜] G} {c' : F →L[𝕜] G}
+  {d : 𝕜 → E →L[𝕜] F} {d' : E →L[𝕜] F} {u : 𝕜 → F} {u' : F}
+
+lemma has_strict_deriv_at.clm_comp (hc : has_strict_deriv_at c c' x)
+  (hd : has_strict_deriv_at d d' x) :
+  has_strict_deriv_at (λ y, (c y).comp (d y)) (c'.comp (d x) + (c x).comp d') x :=
+begin
+  have := (hc.has_strict_fderiv_at.clm_comp hd.has_strict_fderiv_at).has_strict_deriv_at,
+  rwa [add_apply, comp_apply, comp_apply, smul_right_apply, smul_right_apply, one_apply, one_smul,
+      one_smul, add_comm] at this,
+end
+
+lemma has_deriv_within_at.clm_comp (hc : has_deriv_within_at c c' s x)
+  (hd : has_deriv_within_at d d' s x) :
+  has_deriv_within_at (λ y, (c y).comp (d y)) (c'.comp (d x) + (c x).comp d') s x :=
+begin
+  have := (hc.has_fderiv_within_at.clm_comp hd.has_fderiv_within_at).has_deriv_within_at,
+  rwa [add_apply, comp_apply, comp_apply, smul_right_apply, smul_right_apply, one_apply, one_smul,
+      one_smul, add_comm] at this,
+end
+
+lemma has_deriv_at.clm_comp (hc : has_deriv_at c c' x) (hd : has_deriv_at d d' x) :
+  has_deriv_at (λ y, (c y).comp (d y))
+  (c'.comp (d x) + (c x).comp d') x :=
+begin
+  rw [← has_deriv_within_at_univ] at *,
+  exact hc.clm_comp hd
+end
+
+lemma deriv_within_clm_comp (hc : differentiable_within_at 𝕜 c s x)
+  (hd : differentiable_within_at 𝕜 d s x) (hxs : unique_diff_within_at 𝕜 s x):
+  deriv_within (λ y, (c y).comp (d y)) s x =
+    ((deriv_within c s x).comp (d x) + (c x).comp (deriv_within d s x)) :=
+(hc.has_deriv_within_at.clm_comp hd.has_deriv_within_at).deriv_within hxs
+
+lemma deriv_clm_comp (hc : differentiable_at 𝕜 c x) (hd : differentiable_at 𝕜 d x) :
+  deriv (λ y, (c y).comp (d y)) x =
+    ((deriv c x).comp (d x) + (c x).comp (deriv d x)) :=
+(hc.has_deriv_at.clm_comp hd.has_deriv_at).deriv
+
+lemma has_strict_deriv_at.clm_apply (hc : has_strict_deriv_at c c' x)
+  (hu : has_strict_deriv_at u u' x) :
+  has_strict_deriv_at (λ y, (c y) (u y)) (c' (u x) + c x u') x :=
+begin
+  have := (hc.has_strict_fderiv_at.clm_apply hu.has_strict_fderiv_at).has_strict_deriv_at,
+  rwa [add_apply, comp_apply, flip_apply, smul_right_apply, smul_right_apply, one_apply, one_smul,
+      one_smul, add_comm] at this,
+end
+
+lemma has_deriv_within_at.clm_apply (hc : has_deriv_within_at c c' s x)
+  (hu : has_deriv_within_at u u' s x) :
+  has_deriv_within_at (λ y, (c y) (u y)) (c' (u x) + c x u') s x :=
+begin
+  have := (hc.has_fderiv_within_at.clm_apply hu.has_fderiv_within_at).has_deriv_within_at,
+  rwa [add_apply, comp_apply, flip_apply, smul_right_apply, smul_right_apply, one_apply, one_smul,
+      one_smul, add_comm] at this,
+end
+
+lemma has_deriv_at.clm_apply (hc : has_deriv_at c c' x) (hu : has_deriv_at u u' x) :
+  has_deriv_at (λ y, (c y) (u y)) (c' (u x) + c x u') x :=
+begin
+  have := (hc.has_fderiv_at.clm_apply hu.has_fderiv_at).has_deriv_at,
+  rwa [add_apply, comp_apply, flip_apply, smul_right_apply, smul_right_apply, one_apply, one_smul,
+      one_smul, add_comm] at this,
+end
+
+lemma deriv_within_clm_apply (hxs : unique_diff_within_at 𝕜 s x)
+  (hc : differentiable_within_at 𝕜 c s x) (hu : differentiable_within_at 𝕜 u s x) :
+  deriv_within (λ y, (c y) (u y)) s x = (deriv_within c s x (u x) + c x (deriv_within u s x)) :=
+(hc.has_deriv_within_at.clm_apply hu.has_deriv_within_at).deriv_within hxs
+
+lemma deriv_clm_apply (hc : differentiable_at 𝕜 c x) (hu : differentiable_at 𝕜 u x) :
+  deriv (λ y, (c y) (u y)) x = (deriv c x (u x) + c x (deriv u x)) :=
+(hc.has_deriv_at.clm_apply hu.has_deriv_at).deriv
+
+end clm_comp_apply
+
 theorem has_strict_deriv_at.has_strict_fderiv_at_equiv {f : 𝕜 → 𝕜} {f' x : 𝕜}
   (hf : has_strict_deriv_at f f' x) (hf' : f' ≠ 0) :
   has_strict_fderiv_at f

src/analysis/calculus/fderiv.lean

@@ -2099,6 +2099,111 @@ h.continuous.comp (continuous_const.prod_mk continuous_id)
 
 end bilinear_map
 
+section clm_comp_apply
+/-! ### Derivative of the pointwise composition/application of continuous linear maps -/
+
+variables {H : Type*} [normed_group H] [normed_space 𝕜 H] {c : E → G →L[𝕜] H}
+  {c' : E →L[𝕜] G →L[𝕜] H} {d : E → F →L[𝕜] G} {d' : E →L[𝕜] F →L[𝕜] G} {u : E → G}
+  {u' : E →L[𝕜] G}
+
+lemma has_strict_fderiv_at.clm_comp (hc : has_strict_fderiv_at c c' x)
+  (hd : has_strict_fderiv_at d d' x) : has_strict_fderiv_at (λ y, (c y).comp (d y))
+  ((compL 𝕜 F G H (c x)).comp d' + ((compL 𝕜 F G H).flip (d x)).comp c') x :=
+begin
+  rw add_comm,
+  exact (is_bounded_bilinear_map_comp.has_strict_fderiv_at (d x, c x)).comp x (hd.prod hc)
+end
+
+lemma has_fderiv_within_at.clm_comp (hc : has_fderiv_within_at c c' s x)
+  (hd : has_fderiv_within_at d d' s x) : has_fderiv_within_at (λ y, (c y).comp (d y))
+  ((compL 𝕜 F G H (c x)).comp d' + ((compL 𝕜 F G H).flip (d x)).comp c') s x :=
+begin
+  rw add_comm,
+  exact (is_bounded_bilinear_map_comp.has_fderiv_at (d x, c x)).comp_has_fderiv_within_at x
+    (hd.prod hc)
+end
+
+lemma has_fderiv_at.clm_comp (hc : has_fderiv_at c c' x)
+  (hd : has_fderiv_at d d' x) : has_fderiv_at (λ y, (c y).comp (d y))
+  ((compL 𝕜 F G H (c x)).comp d' + ((compL 𝕜 F G H).flip (d x)).comp c') x :=
+begin
+  rw add_comm,
+  exact (is_bounded_bilinear_map_comp.has_fderiv_at (d x, c x)).comp x (hd.prod hc)
+end
+
+lemma differentiable_within_at.clm_comp
+  (hc : differentiable_within_at 𝕜 c s x) (hd : differentiable_within_at 𝕜 d s x) :
+  differentiable_within_at 𝕜 (λ y, (c y).comp (d y)) s x :=
+(hc.has_fderiv_within_at.clm_comp hd.has_fderiv_within_at).differentiable_within_at
+
+lemma differentiable_at.clm_comp (hc : differentiable_at 𝕜 c x)
+  (hd : differentiable_at 𝕜 d x) : differentiable_at 𝕜 (λ y, (c y).comp (d y)) x :=
+(hc.has_fderiv_at.clm_comp hd.has_fderiv_at).differentiable_at
+
+lemma differentiable_on.clm_comp (hc : differentiable_on 𝕜 c s) (hd : differentiable_on 𝕜 d s) :
+  differentiable_on 𝕜 (λ y, (c y).comp (d y)) s :=
+λx hx, (hc x hx).clm_comp (hd x hx)
+
+lemma differentiable.clm_comp (hc : differentiable 𝕜 c) (hd : differentiable 𝕜 d) :
+  differentiable 𝕜 (λ y, (c y).comp (d y)) :=
+λx, (hc x).clm_comp (hd x)
+
+lemma fderiv_within_clm_comp (hxs : unique_diff_within_at 𝕜 s x)
+  (hc : differentiable_within_at 𝕜 c s x) (hd : differentiable_within_at 𝕜 d s x) :
+  fderiv_within 𝕜 (λ y, (c y).comp (d y)) s x =
+    (compL 𝕜 F G H (c x)).comp (fderiv_within 𝕜 d s x) +
+    ((compL 𝕜 F G H).flip (d x)).comp (fderiv_within 𝕜 c s x) :=
+(hc.has_fderiv_within_at.clm_comp hd.has_fderiv_within_at).fderiv_within hxs
+
+lemma fderiv_clm_comp (hc : differentiable_at 𝕜 c x) (hd : differentiable_at 𝕜 d x) :
+  fderiv 𝕜 (λ y, (c y).comp (d y)) x =
+    (compL 𝕜 F G H (c x)).comp (fderiv 𝕜 d x) +
+    ((compL 𝕜 F G H).flip (d x)).comp (fderiv 𝕜 c x) :=
+(hc.has_fderiv_at.clm_comp hd.has_fderiv_at).fderiv
+
+lemma has_strict_fderiv_at.clm_apply (hc : has_strict_fderiv_at c c' x)
+  (hu : has_strict_fderiv_at u u' x) :
+  has_strict_fderiv_at (λ y, (c y) (u y)) ((c x).comp u' + c'.flip (u x)) x :=
+(is_bounded_bilinear_map_apply.has_strict_fderiv_at (c x, u x)).comp x (hc.prod hu)
+
+lemma has_fderiv_within_at.clm_apply (hc : has_fderiv_within_at c c' s x)
+  (hu : has_fderiv_within_at u u' s x) :
+  has_fderiv_within_at (λ y, (c y) (u y)) ((c x).comp u' + c'.flip (u x)) s x :=
+(is_bounded_bilinear_map_apply.has_fderiv_at (c x, u x)).comp_has_fderiv_within_at x (hc.prod hu)
+
+lemma has_fderiv_at.clm_apply (hc : has_fderiv_at c c' x) (hu : has_fderiv_at u u' x) :
+  has_fderiv_at (λ y, (c y) (u y)) ((c x).comp u' + c'.flip (u x)) x :=
+(is_bounded_bilinear_map_apply.has_fderiv_at (c x, u x)).comp x (hc.prod hu)
+
+lemma differentiable_within_at.clm_apply
+  (hc : differentiable_within_at 𝕜 c s x) (hu : differentiable_within_at 𝕜 u s x) :
+  differentiable_within_at 𝕜 (λ y, (c y) (u y)) s x :=
+(hc.has_fderiv_within_at.clm_apply hu.has_fderiv_within_at).differentiable_within_at
+
+lemma differentiable_at.clm_apply (hc : differentiable_at 𝕜 c x)
+  (hu : differentiable_at 𝕜 u x) : differentiable_at 𝕜 (λ y, (c y) (u y)) x :=
+(hc.has_fderiv_at.clm_apply hu.has_fderiv_at).differentiable_at
+
+lemma differentiable_on.clm_apply (hc : differentiable_on 𝕜 c s) (hu : differentiable_on 𝕜 u s) :
+  differentiable_on 𝕜 (λ y, (c y) (u y)) s :=
+λx hx, (hc x hx).clm_apply (hu x hx)
+
+lemma differentiable.clm_apply (hc : differentiable 𝕜 c) (hu : differentiable 𝕜 u) :
+  differentiable 𝕜 (λ y, (c y) (u y)) :=
+λx, (hc x).clm_apply (hu x)
+
+lemma fderiv_within_clm_apply (hxs : unique_diff_within_at 𝕜 s x)
+  (hc : differentiable_within_at 𝕜 c s x) (hu : differentiable_within_at 𝕜 u s x) :
+  fderiv_within 𝕜 (λ y, (c y) (u y)) s x =
+    ((c x).comp (fderiv_within 𝕜 u s x) + (fderiv_within 𝕜 c s x).flip (u x)) :=
+(hc.has_fderiv_within_at.clm_apply hu.has_fderiv_within_at).fderiv_within hxs
+
+lemma fderiv_clm_apply (hc : differentiable_at 𝕜 c x) (hu : differentiable_at 𝕜 u x) :
+  fderiv 𝕜 (λ y, (c y) (u y)) x = ((c x).comp (fderiv 𝕜 u x) + (fderiv 𝕜 c x).flip (u x)) :=
+(hc.has_fderiv_at.clm_apply hu.has_fderiv_at).fderiv
+
+end clm_comp_apply
+
 namespace continuous_linear_equiv
 
 /-!

src/topology/algebra/module.lean

@@ -386,6 +386,8 @@ def comp (g : M₂ →L[R] M₃) (f : M →L[R] M₂) : M →L[R] M₃ :=
 @[simp, norm_cast] lemma coe_comp : ((h.comp f) : (M →ₗ[R] M₃)) = (h : M₂ →ₗ[R] M₃) ∘ₗ ↑f := rfl
 @[simp, norm_cast] lemma coe_comp' : ((h.comp f) : (M → M₃)) = (h : M₂ → M₃) ∘ f := rfl
 
+lemma comp_apply (g : M₂ →L[R] M₃) (f : M →L[R] M₂) (x : M) : (g.comp f) x = g (f x) := rfl
+
 @[simp] theorem comp_id : f.comp (id R M) = f :=
 ext $ λ x, rfl