feat(analysis/calculus/times_cont_diff): smoothness of f : E → Π i, F i (#6674)

Also add helper lemmas/definitions about multilinear maps.

Author: urkud

src/analysis/calculus/times_cont_diff.lean

@@ -232,9 +232,7 @@ begin
   refine ⟨λ H, ⟨H.continuous_on, H.zero_eq⟩,
           λ H, ⟨H.2, λ m hm, false.elim (not_le.2 hm bot_le), _⟩⟩,
   assume m hm,
-  have : (m : with_top ℕ) = ((0 : ℕ) : with_bot ℕ) := le_antisymm hm bot_le,
-  rw with_top.coe_eq_coe at this,
-  rw this,
+  obtain rfl : m = 0, by exact_mod_cast (hm.antisymm (zero_le _)),
   have : ∀ x ∈ s, p x 0 = (continuous_multilinear_curry_fin0 𝕜 E F).symm (f x),
     by { assume x hx, rw ← H.2 x hx, symmetry, exact continuous_multilinear_map.uncurry0_curry0 _ },
   rw [continuous_on_congr this, linear_isometry_equiv.comp_continuous_on_iff],
@@ -1649,20 +1647,14 @@ lemma has_ftaylor_series_up_to_on.continuous_linear_map_comp {n : with_top ℕ}
   (hf : has_ftaylor_series_up_to_on n f p s) :
   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,
   split,
-  { assume x hx, simp [(hf.zero_eq x hx).symm] },
-  { assume m hm x hx,
-    let A : (E [×m]→L[𝕜] F) → (E [×m]→L[𝕜] G) := λ f, g.comp_continuous_multilinear_map f,
-    have hA : is_bounded_linear_map 𝕜 A :=
-      is_bounded_bilinear_map_comp_multilinear.is_bounded_linear_map_right _,
-    have := hf.fderiv_within m hm x hx,
-    convert has_fderiv_at.comp_has_fderiv_within_at x (hA.has_fderiv_at) this },
-  { assume m hm,
-    let A : (E [×m]→L[𝕜] F) → (E [×m]→L[𝕜] G) :=
-      λ f, g.comp_continuous_multilinear_map f,
-    have hA : is_bounded_linear_map 𝕜 A :=
-      is_bounded_bilinear_map_comp_multilinear.is_bounded_linear_map_right _,
-    exact hA.continuous.comp_continuous_on (hf.cont m hm) }
+  { exact λ x hx, congr_arg g (hf.zero_eq x hx) },
+  { intros m hm x hx,
+    convert (L m).has_fderiv_at.comp_has_fderiv_within_at x (hf.fderiv_within m hm x hx) },
+  { intros m hm,
+    convert (L m).continuous.comp_continuous_on (hf.cont m hm) }
 end
 
 /-- Composition by continuous linear maps on the left preserves `C^n` functions in a domain
@@ -1815,17 +1807,14 @@ lemma has_ftaylor_series_up_to_on.prod {n : with_top ℕ} (hf : has_ftaylor_seri
   {g : E → G} {q : E → formal_multilinear_series 𝕜 E G} (hg : has_ftaylor_series_up_to_on n g q s) :
   has_ftaylor_series_up_to_on n (λ y, (f y, g y)) (λ y k, (p y k).prod (q y k)) s :=
 begin
+  set L := λ m, continuous_multilinear_map.prodL 𝕜 (λ i : fin m, E) F G,
   split,
   { assume x hx, rw [← hf.zero_eq x hx, ← hg.zero_eq x hx], refl },
   { assume m hm x hx,
-    let A : (E [×m]→L[𝕜] F) × (E [×m]→L[𝕜] G) → (E [×m]→L[𝕜] (F × G)) := λ p, p.1.prod p.2,
-    have hA : is_bounded_linear_map 𝕜 A := is_bounded_linear_map_prod_multilinear,
-    convert hA.has_fderiv_at.comp_has_fderiv_within_at x
+    convert (L m).has_fderiv_at.comp_has_fderiv_within_at x
       ((hf.fderiv_within m hm x hx).prod (hg.fderiv_within m hm x hx)) },
   { assume m hm,
-    let A : (E [×m]→L[𝕜] F) × (E [×m]→L[𝕜] G) → (E [×m]→L[𝕜] (F × G)) := λ p, p.1.prod p.2,
-    have hA : is_bounded_linear_map 𝕜 A := is_bounded_linear_map_prod_multilinear,
-    exact hA.continuous.comp_continuous_on ((hf.cont m hm).prod (hg.cont m hm)) }
+    exact (L m).continuous.comp_continuous_on ((hf.cont m hm).prod (hg.cont m hm)) }
 end
 
 /-- The cartesian product of `C^n` functions at a point in a domain is `C^n`. -/
@@ -1863,6 +1852,73 @@ lemma times_cont_diff.prod {n : with_top ℕ} {f : E → F} {g : E → G}
 times_cont_diff_on_univ.1 $ times_cont_diff_on.prod (times_cont_diff_on_univ.2 hf)
   (times_cont_diff_on_univ.2 hg)
 
+/-!
+### Smoothness of functions `f : E → Π i, F' i`
+-/
+
+section pi
+
+variables {ι : Type*} [fintype ι] {F' : ι → Type*} [Π i, normed_group (F' i)]
+  [Π i, normed_space 𝕜 (F' i)] {φ : Π i, E → F' i}
+  {p' : Π i, E → formal_multilinear_series 𝕜 E (F' i)}
+  {Φ : E → Π i, F' i} {P' : E → formal_multilinear_series 𝕜 E (Π i, F' i)}
+  {n : with_top ℕ}
+
+lemma has_ftaylor_series_up_to_on_pi :
+  has_ftaylor_series_up_to_on n (λ x i, φ i x)
+    (λ x m, continuous_multilinear_map.pi (λ i, p' i x m)) s ↔
+    ∀ i, has_ftaylor_series_up_to_on n (φ i) (p' i) s :=
+begin
+  set pr := @continuous_linear_map.proj 𝕜 _ ι F' _ _ _,
+  letI : Π (m : ℕ) (i : ι), normed_space 𝕜 (E [×m]→L[𝕜] (F' i)) := λ m i, infer_instance,
+  set L : Π m : ℕ, (Π i, E [×m]→L[𝕜] (F' i)) ≃ₗᵢ[𝕜] (E [×m]→L[𝕜] (Π i, F' i)) :=
+    λ m, continuous_multilinear_map.piₗᵢ _ _,
+  refine ⟨λ h i, _, λ h, ⟨λ x hx, _, _, _⟩⟩,
+  { convert h.continuous_linear_map_comp (pr i),
+    ext, refl },
+  { ext1 i,
+    exact (h i).zero_eq x hx },
+  { intros m hm x hx,
+    have := has_fderiv_within_at_pi.2 (λ i, (h i).fderiv_within m hm x hx),
+    convert (L m).has_fderiv_at.comp_has_fderiv_within_at x this },
+  { intros m hm,
+    have := continuous_on_pi.2 (λ i, (h i).cont m hm),
+    convert (L m).continuous.comp_continuous_on this }
+end
+
+@[simp] lemma has_ftaylor_series_up_to_on_pi' :
+  has_ftaylor_series_up_to_on n Φ P' s ↔
+    ∀ i, has_ftaylor_series_up_to_on n (λ x, Φ x i)
+      (λ x m, (@continuous_linear_map.proj 𝕜 _ ι F' _ _ _ i).comp_continuous_multilinear_map
+        (P' x m)) s :=
+by { convert has_ftaylor_series_up_to_on_pi, ext, refl }
+
+lemma times_cont_diff_within_at_pi :
+  times_cont_diff_within_at 𝕜 n Φ s x ↔
+    ∀ i, times_cont_diff_within_at 𝕜 n (λ x, Φ x i) s x :=
+begin
+  set pr := @continuous_linear_map.proj 𝕜 _ ι F' _ _ _,
+  refine ⟨λ h i, h.continuous_linear_map_comp (pr i), λ h m hm, _⟩,
+  choose u hux p hp using λ i, h i m hm,
+  exact ⟨⋂ i, u i, filter.Inter_mem_sets.2 hux, _,
+    has_ftaylor_series_up_to_on_pi.2 (λ i, (hp i).mono $ Inter_subset _ _)⟩,
+end
+
+lemma times_cont_diff_on_pi :
+  times_cont_diff_on 𝕜 n Φ s ↔ ∀ i, times_cont_diff_on 𝕜 n (λ x, Φ x i) s :=
+⟨λ h i x hx, times_cont_diff_within_at_pi.1 (h x hx) _,
+  λ h x hx, times_cont_diff_within_at_pi.2 (λ i, h i x hx)⟩
+
+lemma times_cont_diff_at_pi :
+  times_cont_diff_at 𝕜 n Φ x ↔ ∀ i, times_cont_diff_at 𝕜 n (λ x, Φ x i) x :=
+times_cont_diff_within_at_pi
+
+lemma times_cont_diff_pi :
+  times_cont_diff 𝕜 n Φ ↔ ∀ i, times_cont_diff 𝕜 n (λ x, Φ x i) :=
+by simp only [← times_cont_diff_on_univ, times_cont_diff_on_pi]
+
+end pi
+
 /-!
 ### Composition of `C^n` functions
 

src/analysis/normed_space/multilinear.lean

@@ -388,6 +388,26 @@ le_antisymm
     (f.op_norm_le_bound (norm_nonneg _) $ λ m, (le_max_left _ _).trans ((f.prod g).le_op_norm _))
     (g.op_norm_le_bound (norm_nonneg _) $ λ m, (le_max_right _ _).trans ((f.prod g).le_op_norm _))
 
+lemma norm_pi {ι' : Type v'} [fintype ι'] {E' : ι' → Type wE'} [Π i', normed_group (E' i')]
+  [Π i', normed_space 𝕜 (E' i')] (f : Π i', continuous_multilinear_map 𝕜 E (E' i')) :
+  ∥pi f∥ = ∥f∥ :=
+begin
+  apply le_antisymm,
+  { refine (op_norm_le_bound _ (norm_nonneg f) (λ m, _)),
+    dsimp,
+    rw pi_norm_le_iff,
+    exacts [λ i, (f i).le_of_op_norm_le m (norm_le_pi_norm f i),
+      mul_nonneg (norm_nonneg f) (prod_nonneg $ λ _ _, norm_nonneg _)] },
+  { refine (pi_norm_le_iff (norm_nonneg _)).2 (λ i, _),
+    refine (op_norm_le_bound _ (norm_nonneg _) (λ m, _)),
+    refine le_trans _ ((pi f).le_op_norm m),
+    convert norm_le_pi_norm (λ j, f j m) i }
+end
+
+section
+
+variables (𝕜 E E' G G')
+
 /-- `continuous_multilinear_map.prod` as a `linear_isometry_equiv`. -/
 def prodL :
   (continuous_multilinear_map 𝕜 E G) × (continuous_multilinear_map 𝕜 E G') ≃ₗᵢ[𝕜]
@@ -401,6 +421,23 @@ def prodL :
   right_inv := λ f, by ext; refl,
   norm_map' := λ f, op_norm_prod f.1 f.2 }
 
+/-- `continuous_multilinear_map.pi` as a `linear_isometry_equiv`. -/
+def piₗᵢ {ι' : Type v'} [fintype ι'] {E' : ι' → Type wE'} [Π i', normed_group (E' i')]
+  [Π i', normed_space 𝕜 (E' i')] :
+  @linear_isometry_equiv 𝕜 (Π i', continuous_multilinear_map 𝕜 E (E' i'))
+    (continuous_multilinear_map 𝕜 E (Π i, E' i)) _ _ _
+      (@pi.semimodule ι' _ 𝕜 _ _ (λ i', infer_instance)) _ :=
+{ to_fun := pi,
+  map_add' := λ f g, rfl,
+  map_smul' := λ c f, rfl,
+  inv_fun := λ f i,
+    (@continuous_linear_map.proj 𝕜 _ _ E' _ _ _ i).comp_continuous_multilinear_map f,
+  left_inv := λ f, by { ext, refl },
+  right_inv := λ f, by { ext, refl },
+  norm_map' := norm_pi }
+
+end
+
 section restrict_scalars
 
 variables [Π i, normed_space 𝕜' (E i)] [∀ i, is_scalar_tower 𝕜' 𝕜 (E i)]

src/geometry/manifold/times_cont_mdiff.lean

@@ -1712,17 +1712,66 @@ hf.prod_map hg
 
 end prod_map
 
+section pi_space
+
+/-!
+### Smoothness of functions with codomain `Π i, F i`
+
+We have no `model_with_corners.pi` yet, so we prove lemmas about functions `f : M → Π i, F i` and
+use `𝓘(𝕜, Π i, F i)` as the model space.
+-/
+
+variables {ι : Type*} [fintype ι] {Fi : ι → Type*} [Π i, normed_group (Fi i)]
+  [Π i, normed_space 𝕜 (Fi i)] {φ : M → Π i, Fi i}
+
+lemma times_cont_mdiff_within_at_pi_space :
+  times_cont_mdiff_within_at I (𝓘(𝕜, Π i, Fi i)) n φ s x ↔
+    ∀ i, times_cont_mdiff_within_at I (𝓘(𝕜, Fi i)) n (λ x, φ x i) s x :=
+by simp only [times_cont_mdiff_within_at_iff'', continuous_within_at_pi,
+  times_cont_diff_within_at_pi, forall_and_distrib, written_in_ext_chart_at,
+  ext_chart_model_space_eq_id, (∘), local_equiv.refl_coe, id]
+
+lemma times_cont_mdiff_on_pi_space :
+  times_cont_mdiff_on I (𝓘(𝕜, Π i, Fi i)) n φ s ↔
+    ∀ i, times_cont_mdiff_on I (𝓘(𝕜, Fi i)) n (λ x, φ x i) s :=
+⟨λ h i x hx, times_cont_mdiff_within_at_pi_space.1 (h x hx) i,
+  λ h x hx, times_cont_mdiff_within_at_pi_space.2 (λ i, h i x hx)⟩
+
+lemma times_cont_mdiff_at_pi_space :
+  times_cont_mdiff_at I (𝓘(𝕜, Π i, Fi i)) n φ x ↔
+    ∀ i, times_cont_mdiff_at I (𝓘(𝕜, Fi i)) n (λ x, φ x i) x :=
+times_cont_mdiff_within_at_pi_space
+
+lemma times_cont_mdiff_pi_space :
+  times_cont_mdiff I (𝓘(𝕜, Π i, Fi i)) n φ ↔
+    ∀ i, times_cont_mdiff I (𝓘(𝕜, Fi i)) n (λ x, φ x i) :=
+⟨λ h i x, times_cont_mdiff_at_pi_space.1 (h x) i,
+  λ h x, times_cont_mdiff_at_pi_space.2 (λ i, h i x)⟩
+
+lemma smooth_within_at_pi_space :
+  smooth_within_at I (𝓘(𝕜, Π i, Fi i)) φ s x ↔
+    ∀ i, smooth_within_at I (𝓘(𝕜, Fi i)) (λ x, φ x i) s x :=
+times_cont_mdiff_within_at_pi_space
+
+lemma smooth_on_pi_space :
+  smooth_on I (𝓘(𝕜, Π i, Fi i)) φ s ↔ ∀ i, smooth_on I (𝓘(𝕜, Fi i)) (λ x, φ x i) s :=
+times_cont_mdiff_on_pi_space
+
+lemma smooth_at_pi_space :
+  smooth_at I (𝓘(𝕜, Π i, Fi i)) φ x ↔ ∀ i, smooth_at I (𝓘(𝕜, Fi i)) (λ x, φ x i) x :=
+times_cont_mdiff_at_pi_space
+
+lemma smooth_pi_space :
+  smooth I (𝓘(𝕜, Π i, Fi i)) φ ↔ ∀ i, smooth I (𝓘(𝕜, Fi i)) (λ x, φ x i) :=
+times_cont_mdiff_pi_space
+
+end pi_space
+
 /-! ### Linear maps between normed spaces are smooth -/
 
 lemma continuous_linear_map.times_cont_mdiff (L : E →L[𝕜] F) :
   times_cont_mdiff 𝓘(𝕜, E) 𝓘(𝕜, F) n L :=
-begin
-  rw times_cont_mdiff_iff,
-  refine ⟨L.cont, λ x y, _⟩,
-  simp only with mfld_simps,
-  rw times_cont_diff_on_univ,
-  exact continuous_linear_map.times_cont_diff L,
-end
+L.times_cont_diff.times_cont_mdiff
 
 /-! ### Smoothness of standard operations -/
 

src/linear_algebra/multilinear.lean

@@ -165,6 +165,15 @@ def prod (f : multilinear_map R M₁ M₂) (g : multilinear_map R M₁ M₃) :
   map_add'  := λ m i x y, by simp,
   map_smul' := λ m i c x, by simp }
 
+/-- Combine a family of multilinear maps with the same domain and codomains `M' i` into a
+multilinear map taking values in the space of functions `Π i, M' i`. -/
+@[simps] def pi {ι' : Type*} {M' : ι' → Type*} [Π i, add_comm_monoid (M' i)]
+  [Π i, semimodule R (M' i)] (f : Π i, multilinear_map R M₁ (M' i)) :
+  multilinear_map R M₁ (Π i, M' i) :=
+{ to_fun := λ m i, f i m,
+  map_add' := λ m i x y, funext $ λ j, (f j).map_add _ _ _ _,
+  map_smul' := λ m i c x, funext $ λ j, (f j).map_smul _ _ _ _ }
+
 /-- Given a multilinear map `f` on `n` variables (parameterized by `fin n`) and a subset `s` of `k`
 of these variables, one gets a new multilinear map on `fin k` by varying these variables, and fixing
 the other ones equal to a given value `z`. It is denoted by `f.restr s hk z`, where `hk` is a

src/topology/algebra/multilinear.lean

@@ -140,6 +140,26 @@ def prod (f : continuous_multilinear_map R M₁ M₂) (g : continuous_multilinea
   (f : continuous_multilinear_map R M₁ M₂) (g : continuous_multilinear_map R M₁ M₃) (m : Πi, M₁ i) :
   (f.prod g) m = (f m, g m) := rfl
 
+/-- Combine a family of continuous multilinear maps with the same domain and codomains `M' i` into a
+continuous multilinear map taking values in the space of functions `Π i, M' i`. -/
+def pi {ι' : Type*} {M' : ι' → Type*} [Π i, add_comm_group (M' i)] [Π i, topological_space (M' i)]
+  [Π i, semimodule R (M' i)] (f : Π i, continuous_multilinear_map R M₁ (M' i)) :
+  continuous_multilinear_map R M₁ (Π i, M' i) :=
+{ cont := continuous_pi $ λ i, (f i).coe_continuous,
+  to_multilinear_map := multilinear_map.pi (λ i, (f i).to_multilinear_map) }
+
+@[simp] lemma coe_pi {ι' : Type*} {M' : ι' → Type*} [Π i, add_comm_group (M' i)]
+  [Π i, topological_space (M' i)] [Π i, semimodule R (M' i)]
+  (f : Π i, continuous_multilinear_map R M₁ (M' i)) :
+  ⇑(pi f) = λ m j, f j m :=
+rfl
+
+lemma pi_apply {ι' : Type*} {M' : ι' → Type*} [Π i, add_comm_group (M' i)]
+  [Π i, topological_space (M' i)] [Π i, semimodule R (M' i)]
+  (f : Π i, continuous_multilinear_map R M₁ (M' i)) (m : Π i, M₁ i) (j : ι') :
+  pi f m j = f j m :=
+rfl
+
 /-- If `g` is continuous multilinear and `f` is a collection of continuous linear maps,
 then `g (f₁ m₁, ..., fₙ mₙ)` is again a continuous multilinear map, that we call
 `g.comp_continuous_linear_map f`. -/