feat(src/analysis/normed_space): various improvements for continuous …

…bilinear maps (#14539)

* Add `simps` to `arrow_congrSL`
* `continuous_linear_map.flip (compSL F E H σ₂₁ σ₁₄)` takes almost 5 seconds to elaborate, but when giving the argument `(F →SL[σ₂₄] H)` for `G` explicitly, this goes down to 1 second.
* Reorder arguments of `is_bounded_bilinear_map_comp`
* Use `continuous_linear_map` results to prove `is_bounded_bilinear_map` results.
* Make arguments to `comp_continuous_multilinear_mapL` explicit
* Add `continuous[_on].clm_comp`, `cont_diff[_on].clm_comp` and `cont_diff.comp_cont_diff_on(₂|₃)`

src/analysis/calculus/cont_diff.lean

@@ -173,6 +173,7 @@ variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
 {E : Type*} [normed_group E] [normed_space 𝕜 E]
 {F : Type*} [normed_group F] [normed_space 𝕜 F]
 {G : Type*} [normed_group G] [normed_space 𝕜 G]
+{X : Type*} [normed_group X] [normed_space 𝕜 X]
 {s s₁ t u : set E} {f f₁ : E → F} {g : F → G} {x : E} {c : F}
 {b : E × F → G} {m n : with_top ℕ}
 
@@ -1628,7 +1629,7 @@ lemma has_ftaylor_series_up_to_on.continuous_linear_map_comp (g : F →L[𝕜] G
   has_ftaylor_series_up_to_on n (g ∘ f) (λ x k, g.comp_continuous_multilinear_map (p x k)) s :=
 begin
   set L : Π m : ℕ, (E [×m]→L[𝕜] F) →L[𝕜] (E [×m]→L[𝕜] G) :=
-    λ m, continuous_linear_map.comp_continuous_multilinear_mapL g,
+    λ m, continuous_linear_map.comp_continuous_multilinear_mapL 𝕜 (λ _, E) F G g,
   split,
   { exact λ x hx, congr_arg g (hf.zero_eq x hx) },
   { intros m hm x hx,
@@ -1650,14 +1651,12 @@ end
 
 /-- Composition by continuous linear maps on the left preserves `C^n` functions in a domain
 at a point. -/
-lemma cont_diff_at.continuous_linear_map_comp (g : F →L[𝕜] G)
-  (hf : cont_diff_at 𝕜 n f x) :
+lemma cont_diff_at.continuous_linear_map_comp (g : F →L[𝕜] G) (hf : cont_diff_at 𝕜 n f x) :
   cont_diff_at 𝕜 n (g ∘ f) x :=
 cont_diff_within_at.continuous_linear_map_comp g hf
 
 /-- Composition by continuous linear maps on the left preserves `C^n` functions on domains. -/
-lemma cont_diff_on.continuous_linear_map_comp (g : F →L[𝕜] G)
-  (hf : cont_diff_on 𝕜 n f s) :
+lemma cont_diff_on.continuous_linear_map_comp (g : F →L[𝕜] G) (hf : cont_diff_on 𝕜 n f s) :
   cont_diff_on 𝕜 n (g ∘ f) s :=
 λ x hx, (hf x hx).continuous_linear_map_comp g
 
@@ -1886,14 +1885,12 @@ begin
     { have A : cont_diff_on 𝕜 n (λ y, g' (f y)) w :=
         IH g'_diff ((hf.of_le (with_top.coe_le_coe.2 (nat.le_succ n))).mono ws) wv,
       have B : cont_diff_on 𝕜 n f' w := f'_diff.mono wu,
-      have C : cont_diff_on 𝕜 n (λ y, (f' y, g' (f y))) w :=
-        cont_diff_on.prod B A,
-      have D : cont_diff_on 𝕜 n (λ(p : (Eu →L[𝕜] Fu) × (Fu →L[𝕜] Gu)), p.2.comp p.1) univ :=
+      have C : cont_diff_on 𝕜 n (λ y, (g' (f y), f' y)) w := A.prod B,
+      have D : cont_diff_on 𝕜 n (λ p : (Fu →L[𝕜] Gu) × (Eu →L[𝕜] Fu), p.1.comp p.2) univ :=
         is_bounded_bilinear_map_comp.cont_diff.cont_diff_on,
       exact IH D C (subset_univ _) } },
   { rw cont_diff_on_top at hf hg ⊢,
-    assume n,
-    apply Itop n (hg n) (hf n) st }
+    exact λ n, Itop n (hg n) (hf n) st }
 end
 
 /-- The composition of `C^n` functions on domains is `C^n`. -/
@@ -2130,6 +2127,16 @@ lemma cont_diff.comp₃ {g : E₁ × E₂ × E₃ → G} {f₁ : F → E₁} {f
   (hf₃ : cont_diff 𝕜 n f₃) : cont_diff 𝕜 n (λ x, g (f₁ x, f₂ x, f₃ x)) :=
 hg.comp₂ hf₁ $ hf₂.prod hf₃
 
+lemma cont_diff.comp_cont_diff_on₂ {g : E₁ × E₂ → G} {f₁ : F → E₁} {f₂ : F → E₂} {s : set F}
+  (hg : cont_diff 𝕜 n g) (hf₁ : cont_diff_on 𝕜 n f₁ s) (hf₂ : cont_diff_on 𝕜 n f₂ s) :
+  cont_diff_on 𝕜 n (λ x, g (f₁ x, f₂ x)) s :=
+hg.comp_cont_diff_on $ hf₁.prod hf₂
+
+lemma cont_diff.comp_cont_diff_on₃ {g : E₁ × E₂ × E₃ → G} {f₁ : F → E₁} {f₂ : F → E₂} {f₃ : F → E₃}
+  {s : set F} (hg : cont_diff 𝕜 n g) (hf₁ : cont_diff_on 𝕜 n f₁ s) (hf₂ : cont_diff_on 𝕜 n f₂ s)
+  (hf₃ : cont_diff_on 𝕜 n f₃ s) : cont_diff_on 𝕜 n (λ x, g (f₁ x, f₂ x, f₃ x)) s :=
+hg.comp_cont_diff_on₂ hf₁ $ hf₂.prod hf₃
+
 end n_ary
 
 /--
@@ -2537,6 +2544,16 @@ cont_diff_const.prod cont_diff_id
 
 end prod_map
 
+lemma cont_diff.clm_comp {g : X → F →L[𝕜] G} {f : X → E →L[𝕜] F}
+  (hg : cont_diff 𝕜 n g) (hf : cont_diff 𝕜 n f) :
+  cont_diff 𝕜 n (λ x, (g x).comp (f x)) :=
+is_bounded_bilinear_map_comp.cont_diff.comp₂ hg hf
+
+lemma cont_diff_on.clm_comp {g : X → F →L[𝕜] G} {f : X → E →L[𝕜] F}
+  {s : set X} (hg : cont_diff_on 𝕜 n g s) (hf : cont_diff_on 𝕜 n f s) :
+  cont_diff_on 𝕜 n (λ x, (g x).comp (f x)) s :=
+is_bounded_bilinear_map_comp.cont_diff.comp_cont_diff_on₂ hg hf
+
 /-! ### Inversion in a complete normed algebra -/
 
 section algebra_inverse
@@ -2653,12 +2670,8 @@ begin
   rw this,
   -- `O₁` and `O₂` are `cont_diff`,
   -- so we reduce to proving that `ring.inverse` is `cont_diff`
-  have h₁ : cont_diff 𝕜 n O₁,
-    from is_bounded_bilinear_map_comp.cont_diff.comp
-      (cont_diff_const.prod cont_diff_id),
-  have h₂ : cont_diff 𝕜 n O₂,
-    from is_bounded_bilinear_map_comp.cont_diff.comp
-      (cont_diff_id.prod cont_diff_const),
+  have h₁ : cont_diff 𝕜 n O₁ := cont_diff_id.clm_comp cont_diff_const,
+  have h₂ : cont_diff 𝕜 n O₂ := cont_diff_const.clm_comp cont_diff_id,
   refine h₁.cont_diff_at.comp _ (cont_diff_at.comp _ _ h₂.cont_diff_at),
   convert cont_diff_at_ring_inverse 𝕜 (1 : (E →L[𝕜] E)ˣ),
   simp [O₂, one_def]

src/analysis/calculus/fderiv.lean

@@ -2147,27 +2147,17 @@ variables {H : Type*} [normed_group H] [normed_space 𝕜 H] {c : E → G →L[
 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
+(is_bounded_bilinear_map_comp.has_strict_fderiv_at (c x, d x)).comp x $ hc.prod hd
 
 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
+(is_bounded_bilinear_map_comp.has_fderiv_at (c x, d x)).comp_has_fderiv_within_at x $ hc.prod hd
 
 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
+(is_bounded_bilinear_map_comp.has_fderiv_at (c x, d x)).comp x $ hc.prod hd
 
 lemma differentiable_within_at.clm_comp
   (hc : differentiable_within_at 𝕜 c s x) (hd : differentiable_within_at 𝕜 d s x) :

src/analysis/normed_space/bounded_linear_maps.lean

@@ -406,81 +406,43 @@ lemma is_bounded_bilinear_map_smul {𝕜' : Type*} [normed_field 𝕜']
   [normed_algebra 𝕜 𝕜'] {E : Type*} [normed_group E] [normed_space 𝕜 E] [normed_space 𝕜' E]
   [is_scalar_tower 𝕜 𝕜' E] :
   is_bounded_bilinear_map 𝕜 (λ (p : 𝕜' × E), p.1 • p.2) :=
-{ add_left   := add_smul,
-  smul_left  := λ c x y, by simp [smul_assoc],
-  add_right  := smul_add,
-  smul_right := λ c x y, by simp [smul_assoc, smul_algebra_smul_comm],
-  bound      := ⟨1, zero_lt_one, λ x y, by simp [norm_smul] ⟩ }
+(lsmul 𝕜 𝕜' : 𝕜' →L[𝕜] E →L[𝕜] E).is_bounded_bilinear_map
 
 lemma is_bounded_bilinear_map_mul :
   is_bounded_bilinear_map 𝕜 (λ (p : 𝕜 × 𝕜), p.1 * p.2) :=
 by simp_rw ← smul_eq_mul; exact is_bounded_bilinear_map_smul
 
 lemma is_bounded_bilinear_map_comp :
-  is_bounded_bilinear_map 𝕜 (λ (p : (E →L[𝕜] F) × (F →L[𝕜] G)), p.2.comp p.1) :=
-{ add_left := λ x₁ x₂ y, begin
-      ext z,
-      change y (x₁ z + x₂ z) = y (x₁ z) + y (x₂ z),
-      rw y.map_add
-    end,
-  smul_left := λ c x y, begin
-      ext z,
-      change y (c • (x z)) = c • y (x z),
-      rw continuous_linear_map.map_smul
-    end,
-  add_right := λ x y₁ y₂, rfl,
-  smul_right := λ c x y, rfl,
-  bound := ⟨1, zero_lt_one, λ x y, calc
-    ∥continuous_linear_map.comp ((x, y).snd) ((x, y).fst)∥
-      ≤ ∥y∥ * ∥x∥ : continuous_linear_map.op_norm_comp_le _ _
-    ... = 1 * ∥x∥ * ∥ y∥ : by ring ⟩ }
+  is_bounded_bilinear_map 𝕜 (λ (p : (F →L[𝕜] G) × (E →L[𝕜] F)), p.1.comp p.2) :=
+(compL 𝕜 E F G).is_bounded_bilinear_map
 
 lemma continuous_linear_map.is_bounded_linear_map_comp_left (g : F →L[𝕜] G) :
   is_bounded_linear_map 𝕜 (λ (f : E →L[𝕜] F), continuous_linear_map.comp g f) :=
-is_bounded_bilinear_map_comp.is_bounded_linear_map_left _
+is_bounded_bilinear_map_comp.is_bounded_linear_map_right _
 
 lemma continuous_linear_map.is_bounded_linear_map_comp_right (f : E →L[𝕜] F) :
   is_bounded_linear_map 𝕜 (λ (g : F →L[𝕜] G), continuous_linear_map.comp g f) :=
-is_bounded_bilinear_map_comp.is_bounded_linear_map_right _
+is_bounded_bilinear_map_comp.is_bounded_linear_map_left _
 
 lemma is_bounded_bilinear_map_apply :
   is_bounded_bilinear_map 𝕜 (λ p : (E →L[𝕜] F) × E, p.1 p.2) :=
-{ add_left   := by simp,
-  smul_left  := by simp,
-  add_right  := by simp,
-  smul_right := by simp,
-  bound      := ⟨1, zero_lt_one, by simp [continuous_linear_map.le_op_norm]⟩ }
+(continuous_linear_map.flip (apply 𝕜 F : E →L[𝕜] (E →L[𝕜] F) →L[𝕜] F)).is_bounded_bilinear_map
 
 /-- The function `continuous_linear_map.smul_right`, associating to a continuous linear map
 `f : E → 𝕜` and a scalar `c : F` the tensor product `f ⊗ c` as a continuous linear map from `E` to
 `F`, is a bounded bilinear map. -/
 lemma is_bounded_bilinear_map_smul_right :
   is_bounded_bilinear_map 𝕜
     (λ p, (continuous_linear_map.smul_right : (E →L[𝕜] 𝕜) → F → (E →L[𝕜] F)) p.1 p.2) :=
-{ add_left   := λ m₁ m₂ f, by { ext z, simp [add_smul] },
-  smul_left  := λ c m f, by { ext z, simp [mul_smul] },
-  add_right  := λ m f₁ f₂, by { ext z, simp [smul_add] },
-  smul_right := λ c m f, by { ext z, simp [smul_smul, mul_comm] },
-  bound      := ⟨1, zero_lt_one, λ m f, by simp⟩ }
+(smul_rightL 𝕜 E F).is_bounded_bilinear_map
 
 /-- The composition of a continuous linear map with a continuous multilinear map is a bounded
 bilinear operation. -/
 lemma is_bounded_bilinear_map_comp_multilinear {ι : Type*} {E : ι → Type*}
 [decidable_eq ι] [fintype ι] [∀ i, normed_group (E i)] [∀ i, normed_space 𝕜 (E i)] :
   is_bounded_bilinear_map 𝕜 (λ p : (F →L[𝕜] G) × (continuous_multilinear_map 𝕜 E F),
     p.1.comp_continuous_multilinear_map p.2) :=
-{ add_left   := λ g₁ g₂ f, by { ext m, refl },
-  smul_left  := λ c g f, by { ext m, refl },
-  add_right  := λ g f₁ f₂, by { ext m, simp },
-  smul_right := λ c g f, by { ext m, simp },
-  bound      := ⟨1, zero_lt_one, λ g f, begin
-    apply continuous_multilinear_map.op_norm_le_bound _ _ (λ m, _),
-    { apply_rules [mul_nonneg, zero_le_one, norm_nonneg] },
-    calc ∥g (f m)∥ ≤ ∥g∥ * ∥f m∥ : g.le_op_norm _
-    ... ≤ ∥g∥ * (∥f∥ * ∏ i, ∥m i∥) :
-      mul_le_mul_of_nonneg_left (f.le_op_norm _) (norm_nonneg _)
-    ... = 1 * ∥g∥ * ∥f∥ * ∏ i, ∥m i∥ : by ring
-    end⟩ }
+(comp_continuous_multilinear_mapL 𝕜 E F G).is_bounded_bilinear_map
 
 /-- Definition of the derivative of a bilinear map `f`, given at a point `p` by
 `q ↦ f(p.1, q.2) + f(q.1, p.2)` as in the standard formula for the derivative of a product.
@@ -552,6 +514,16 @@ end
 
 end bilinear_map
 
+lemma continuous.clm_comp {X} [topological_space X] {g : X → F →L[𝕜] G} {f : X → E →L[𝕜] F}
+  (hg : continuous g) (hf : continuous f) :
+  continuous (λ x, (g x).comp (f x)) :=
+(compL 𝕜 E F G).continuous₂.comp₂ hg hf
+
+lemma continuous_on.clm_comp {X} [topological_space X] {g : X → F →L[𝕜] G} {f : X → E →L[𝕜] F}
+  {s : set X} (hg : continuous_on g s) (hf : continuous_on f s) :
+  continuous_on (λ x, (g x).comp (f x)) s :=
+(compL 𝕜 E F G).continuous₂.comp_continuous_on (hg.prod hf)
+
 namespace continuous_linear_equiv
 
 open set
@@ -568,7 +540,7 @@ begin
   rw [is_open_iff_mem_nhds, forall_range_iff],
   refine λ e, is_open.mem_nhds _ (mem_range_self _),
   let O : (E →L[𝕜] F) → (E →L[𝕜] E) := λ f, (e.symm : F →L[𝕜] E).comp f,
-  have h_O : continuous O := is_bounded_bilinear_map_comp.continuous_left,
+  have h_O : continuous O := is_bounded_bilinear_map_comp.continuous_right,
   convert units.is_open.preimage h_O using 1,
   ext f',
   split,

src/analysis/normed_space/multilinear.lean

@@ -817,6 +817,7 @@ continuous_multilinear_map.op_norm_le_bound _ (mul_nonneg (norm_nonneg _) (norm_
 calc ∥g (f m)∥ ≤ ∥g∥ * (∥f∥ * ∏ i, ∥m i∥) : g.le_op_norm_of_le $ f.le_op_norm _
            ... = _                        : (mul_assoc _ _ _).symm
 
+variables (𝕜 E G G')
 /-- `continuous_linear_map.comp_continuous_multilinear_map` as a bundled continuous bilinear map. -/
 def comp_continuous_multilinear_mapL :
   (G →L[𝕜] G') →L[𝕜] continuous_multilinear_map 𝕜 E G →L[𝕜] continuous_multilinear_map 𝕜 E G' :=
@@ -825,6 +826,8 @@ linear_map.mk_continuous₂
     (λ f g₁ g₂, by { ext1, apply f.map_add }) (λ c f g, by { ext1, simp }))
   1 $ λ f g, by { rw one_mul, exact f.norm_comp_continuous_multilinear_map_le g }
 
+variables {𝕜 E G G'}
+
 /-- Flip arguments in `f : G →L[𝕜] continuous_multilinear_map 𝕜 E G'` to get
 `continuous_multilinear_map 𝕜 E (G →L[𝕜] G')` -/
 def flip_multilinear (f : G →L[𝕜] continuous_multilinear_map 𝕜 E G') :

src/analysis/normed_space/operator_norm.lean

@@ -720,15 +720,25 @@ linear_map.mk_continuous₂
                                    function.comp_app, pi.smul_apply] }))
   1 $ λ f g, by simpa only [one_mul] using op_norm_comp_le f g
 
-variables {𝕜 E F G}
+variables {𝕜 σ₁₂ σ₂₃ E F G}
 
 include σ₁₃
 
 @[simp] lemma compSL_apply (f : F →SL[σ₂₃] G) (g : E →SL[σ₁₂] F) :
   compSL E F G σ₁₂ σ₂₃ f g = f.comp g := rfl
 
+lemma _root_.continuous.const_clm_comp {X} [topological_space X] {f : X → E →SL[σ₁₂] F}
+  (hf : continuous f) (g : F →SL[σ₂₃] G) : continuous (λ x, g.comp (f x) : X → E →SL[σ₁₃] G) :=
+(compSL E F G σ₁₂ σ₂₃ g).continuous.comp hf
+
+-- Giving the implicit argument speeds up elaboration significantly
+lemma _root_.continuous.clm_comp_const {X} [topological_space X] {g : X → F →SL[σ₂₃] G}
+  (hg : continuous g) (f : E →SL[σ₁₂] F) : continuous (λ x, (g x).comp f : X → E →SL[σ₁₃] G) :=
+(@continuous_linear_map.flip _ _ _ _ _ (E →SL[σ₁₃] G) _ _ _ _ _ _ _ _ _ _ _ _ _
+  (compSL E F G σ₁₂ σ₂₃) f).continuous.comp hg
+
 omit σ₁₃
-variables (𝕜 E Fₗ Gₗ)
+variables (𝕜 σ₁₂ σ₂₃ E Fₗ Gₗ)
 
 /-- Composition of continuous linear maps as a continuous bilinear map. -/
 def compL : (Fₗ →L[𝕜] Gₗ) →L[𝕜] (E →L[𝕜] Fₗ) →L[𝕜] (E →L[𝕜] Gₗ) :=
@@ -1767,18 +1777,20 @@ variables [ring_hom_isometric σ₁₃] [ring_hom_isometric σ₁₂]
 variables [ring_hom_isometric σ₃₄]
 
 include σ₂₁ σ₃₄ σ₁₃ σ₂₄
+
 /-- A pair of continuous (semi)linear equivalences generates an continuous (semi)linear equivalence
 between the spaces of continuous (semi)linear maps. -/
+@[simps apply symm_apply]
 def arrow_congrSL (e₁₂ : E ≃SL[σ₁₂] F) (e₄₃ : H ≃SL[σ₄₃] G) :
   (E →SL[σ₁₄] H) ≃SL[σ₄₃] (F →SL[σ₂₃] G) :=
-{ map_add' := λ f g, by simp only [equiv.to_fun_as_coe, add_comp, comp_add,
-    continuous_linear_equiv.arrow_congr_equiv_apply],
-  map_smul' := λ t f, by simp only [equiv.to_fun_as_coe, smul_comp, comp_smulₛₗ,
-    continuous_linear_equiv.arrow_congr_equiv_apply],
-  continuous_to_fun := (compSL F H G σ₂₄ σ₄₃ e₄₃).continuous.comp
-    (continuous_linear_map.flip (compSL F E H σ₂₁ σ₁₄) e₁₂.symm).continuous,
-  continuous_inv_fun := (compSL E G H σ₁₃ σ₃₄ e₄₃.symm).continuous.comp
-    (continuous_linear_map.flip (compSL E F G σ₁₂ σ₂₃) e₁₂).continuous,
+{ -- given explicitly to help `simps`
+  to_fun := λ L, (e₄₃ : H →SL[σ₄₃] G).comp (L.comp (e₁₂.symm : F →SL[σ₂₁] E)),
+  -- given explicitly to help `simps`
+  inv_fun := λ L, (e₄₃.symm : G →SL[σ₃₄] H).comp (L.comp (e₁₂ : E →SL[σ₁₂] F)),
+  map_add' := λ f g, by rw [add_comp, comp_add],
+  map_smul' := λ t f, by rw [smul_comp, comp_smulₛₗ],
+  continuous_to_fun := (continuous_id.clm_comp_const _).const_clm_comp _,
+  continuous_inv_fun := (continuous_id.clm_comp_const _).const_clm_comp _,
   .. e₁₂.arrow_congr_equiv e₄₃, }
 
 omit σ₂₁ σ₃₄ σ₁₃ σ₂₄