feat(analysis/normed_space/multilinear): define mk_pi_algebra (#4316)

I'm going to use this definition for converting `(mv_)power_series` to `formal_multilinear_series`.

src/analysis/normed_space/multilinear.lean

@@ -539,6 +539,112 @@ begin
   exact mul_nonneg (norm_nonneg _) (pow_nonneg (norm_nonneg _) _)
 end
 
+section
+
+variables (𝕜 ι) (A : Type*) [normed_comm_ring A] [normed_algebra 𝕜 A]
+
+/-- The continuous multilinear map on `A^ι`, where `A` is a normed commutative algebra
+over `𝕜`, associating to `m` the product of all the `m i`.
+
+See also `continuous_multilinear_map.mk_pi_algebra_fin`. -/
+protected def mk_pi_algebra : continuous_multilinear_map 𝕜 (λ i : ι, A) A :=
+@multilinear_map.mk_continuous 𝕜 ι (λ i : ι, A) A _ _ _ _ _ _ _
+  (multilinear_map.mk_pi_algebra 𝕜 ι A) (if nonempty ι then 1 else ∥(1 : A)∥) $
+  begin
+    intro m,
+    by_cases hι : nonempty ι,
+    { resetI, simp [hι, norm_prod_le' univ univ_nonempty] },
+    { simp [eq_empty_of_not_nonempty hι univ, hι] }
+  end
+
+variables {A 𝕜 ι}
+
+@[simp] lemma mk_pi_algebra_apply (m : ι → A) :
+  continuous_multilinear_map.mk_pi_algebra 𝕜 ι A m = ∏ i, m i :=
+rfl
+
+lemma norm_mk_pi_algebra_le [nonempty ι] :
+  ∥continuous_multilinear_map.mk_pi_algebra 𝕜 ι A∥ ≤ 1 :=
+calc ∥continuous_multilinear_map.mk_pi_algebra 𝕜 ι A∥ ≤ if nonempty ι then 1 else ∥(1 : A)∥ :
+  multilinear_map.mk_continuous_norm_le _ (by split_ifs; simp [zero_le_one]) _
+... = _ : if_pos ‹_›
+
+lemma norm_mk_pi_algebra_of_empty (h : ¬nonempty ι) :
+  ∥continuous_multilinear_map.mk_pi_algebra 𝕜 ι A∥ = ∥(1 : A)∥ :=
+begin
+  apply le_antisymm,
+  calc ∥continuous_multilinear_map.mk_pi_algebra 𝕜 ι A∥ ≤ if nonempty ι then 1 else ∥(1 : A)∥ :
+    multilinear_map.mk_continuous_norm_le _ (by split_ifs; simp [zero_le_one]) _
+  ... = ∥(1 : A)∥ : if_neg ‹_›,
+  convert ratio_le_op_norm _ (λ _, 1); [skip, apply_instance],
+  simp [eq_empty_of_not_nonempty h univ]
+end
+
+@[simp] lemma norm_mk_pi_algebra [norm_one_class A] :
+  ∥continuous_multilinear_map.mk_pi_algebra 𝕜 ι A∥ = 1 :=
+begin
+  by_cases hι : nonempty ι,
+  { resetI,
+    refine le_antisymm norm_mk_pi_algebra_le _,
+    convert ratio_le_op_norm _ (λ _, 1); [skip, apply_instance],
+    simp },
+  { simp [norm_mk_pi_algebra_of_empty hι] }
+end
+
+end
+
+section
+
+variables (𝕜 n) (A : Type*) [normed_ring A] [normed_algebra 𝕜 A]
+
+/-- The continuous multilinear map on `A^n`, where `A` is a normed algebra over `𝕜`, associating to
+`m` the product of all the `m i`.
+
+See also: `multilinear_map.mk_pi_algebra`. -/
+protected def mk_pi_algebra_fin : continuous_multilinear_map 𝕜 (λ i : fin n, A) A :=
+@multilinear_map.mk_continuous 𝕜 (fin n) (λ i : fin n, A) A _ _ _ _ _ _ _
+  (multilinear_map.mk_pi_algebra_fin 𝕜 n A) (nat.cases_on n ∥(1 : A)∥ (λ _, 1)) $
+  begin
+    intro m,
+    cases n,
+    { simp },
+    { have : @list.of_fn A n.succ m ≠ [] := by simp,
+      simpa [← fin.prod_of_fn] using list.norm_prod_le' this }
+  end
+
+variables {A 𝕜 n}
+
+@[simp] lemma mk_pi_algebra_fin_apply (m : fin n → A) :
+  continuous_multilinear_map.mk_pi_algebra_fin 𝕜 n A m = (list.of_fn m).prod :=
+rfl
+
+lemma norm_mk_pi_algebra_fin_succ_le :
+  ∥continuous_multilinear_map.mk_pi_algebra_fin 𝕜 n.succ A∥ ≤ 1 :=
+multilinear_map.mk_continuous_norm_le _ zero_le_one _
+
+lemma norm_mk_pi_algebra_fin_le_of_pos (hn : 0 < n) :
+  ∥continuous_multilinear_map.mk_pi_algebra_fin 𝕜 n A∥ ≤ 1 :=
+by cases n; [exact hn.false.elim, exact norm_mk_pi_algebra_fin_succ_le]
+
+lemma norm_mk_pi_algebra_fin_zero :
+  ∥continuous_multilinear_map.mk_pi_algebra_fin 𝕜 0 A∥ = ∥(1 : A)∥ :=
+begin
+  refine le_antisymm (multilinear_map.mk_continuous_norm_le _ (norm_nonneg _) _) _,
+  convert ratio_le_op_norm _ (λ _, 1); [simp, apply_instance]
+end
+
+lemma norm_mk_pi_algebra_fin [norm_one_class A] :
+  ∥continuous_multilinear_map.mk_pi_algebra_fin 𝕜 n A∥ = 1 :=
+begin
+  cases n,
+  { simp [norm_mk_pi_algebra_fin_zero] },
+  { refine le_antisymm norm_mk_pi_algebra_fin_succ_le _,
+    convert ratio_le_op_norm _ (λ _, 1); [skip, apply_instance],
+    simp }
+end
+
+end
+
 variables (𝕜 ι)
 
 /-- The canonical continuous multilinear map on `𝕜^ι`, associating to `m` the product of all the
@@ -553,14 +659,9 @@ variables {𝕜 ι}
 @[simp] lemma mk_pi_field_apply (z : E₂) (m : ι → 𝕜) :
   (continuous_multilinear_map.mk_pi_field 𝕜 ι z : (ι → 𝕜) → E₂) m = (∏ i, m i) • z := rfl
 
-lemma mk_pi_ring_apply_one_eq_self (f : continuous_multilinear_map 𝕜 (λ(i : ι), 𝕜) E₂) :
+lemma mk_pi_field_apply_one_eq_self (f : continuous_multilinear_map 𝕜 (λ(i : ι), 𝕜) E₂) :
   continuous_multilinear_map.mk_pi_field 𝕜 ι (f (λi, 1)) = f :=
-begin
-  ext m,
-  have : m = (λi, m i • 1), by { ext j, simp },
-  conv_rhs { rw [this, f.map_smul_univ] },
-  refl
-end
+to_multilinear_map_inj f.to_multilinear_map.mk_pi_ring_apply_one_eq_self
 
 variables (𝕜 ι E₂)
 
@@ -575,7 +676,7 @@ protected def pi_field_equiv_aux : E₂ ≃ₗ[𝕜] (continuous_multilinear_map
   map_add'  := λ z z', by { ext m, simp [smul_add] },
   map_smul' := λ c z, by { ext m, simp [smul_smul, mul_comm] },
   left_inv  := λ z, by simp,
-  right_inv := λ f, f.mk_pi_ring_apply_one_eq_self }
+  right_inv := λ f, f.mk_pi_field_apply_one_eq_self }
 
 /-- Continuous multilinear maps on `𝕜^n` with values in `E₂` are in bijection with `E₂`, as such a
 continuous multilinear map is completely determined by its value on the constant vector made of

src/linear_algebra/multilinear.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
 import linear_algebra.basic
+import algebra.algebra.basic
 import tactic.omega
 import data.fintype.sort
 
@@ -414,6 +415,29 @@ end apply_sum
 
 end semiring
 
+end multilinear_map
+
+namespace linear_map
+variables [semiring R] [Πi, add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [add_comm_monoid M₃]
+[∀i, semimodule R (M₁ i)] [semimodule R M₂] [semimodule R M₃]
+
+/-- Composing a multilinear map with a linear map gives again a multilinear map. -/
+def comp_multilinear_map (g : M₂ →ₗ[R] M₃) (f : multilinear_map R M₁ M₂) :
+  multilinear_map R M₁ M₃ :=
+{ to_fun    := g ∘ f,
+  map_add'  := λ m i x y, by simp,
+  map_smul' := λ m i c x, by simp }
+
+@[simp] lemma coe_comp_multilinear_map (g : M₂ →ₗ[R] M₃) (f : multilinear_map R M₁ M₂) :
+  ⇑(g.comp_multilinear_map f) = g ∘ f := rfl
+
+lemma comp_multilinear_map_apply (g : M₂ →ₗ[R] M₃) (f : multilinear_map R M₁ M₂) (m : Π i, M₁ i) :
+  g.comp_multilinear_map f m = g (f m) := rfl
+
+end linear_map
+
+namespace multilinear_map
+
 section comm_semiring
 
 variables [comm_semiring R] [∀i, add_comm_monoid (M₁ i)] [∀i, add_comm_monoid (M i)] [add_comm_monoid M₂]
@@ -450,15 +474,83 @@ instance : has_scalar R (multilinear_map R M₁ M₂) := ⟨λ c f,
 
 @[simp] lemma smul_apply (c : R) (m : Πi, M₁ i) : (c • f) m = c • f m := rfl
 
+section
+
+variables (R ι) (A : Type*) [comm_semiring A] [algebra R A] [fintype ι]
+
+/-- Given an `R`-algebra `A`, `mk_pi_algebra` is the multilinear map on `A^ι` associating
+to `m` the product of all the `m i`.
+
+See also `multilinear_map.mk_pi_algebra_fin` for a version that works with a non-commutative
+algebra `A` but requires `ι = fin n`. -/
+protected def mk_pi_algebra : multilinear_map R (λ i : ι, A) A :=
+{ to_fun := λ m, ∏ i, m i,
+  map_add' := λ m i x y, by simp [finset.prod_update_of_mem, add_mul],
+  map_smul' := λ m i c x, by simp [finset.prod_update_of_mem] }
+
+variables {R A ι}
+
+@[simp] lemma mk_pi_algebra_apply (m : ι → A) :
+  multilinear_map.mk_pi_algebra R ι A m = ∏ i, m i :=
+rfl
+
+end
+
+section
+
+variables (R n) (A : Type*) [semiring A] [algebra R A]
+
+/-- Given an `R`-algebra `A`, `mk_pi_algebra_fin` is the multilinear map on `A^n` associating
+to `m` the product of all the `m i`.
+
+See also `multilinear_map.mk_pi_algebra` for a version that assumes `[comm_semiring A]` but works
+for `A^ι` with any finite type `ι`. -/
+protected def mk_pi_algebra_fin : multilinear_map R (λ i : fin n, A) A :=
+{ to_fun := λ m, (list.of_fn m).prod,
+  map_add' :=
+    begin
+      intros m i x y,
+      have : (list.fin_range n).index_of i < n,
+        by simpa using list.index_of_lt_length.2 (list.mem_fin_range i),
+      simp [list.of_fn_eq_map, (list.nodup_fin_range n).map_update, list.prod_update_nth, add_mul,
+        this, mul_add, add_mul]
+    end,
+  map_smul' :=
+    begin
+      intros m i c x,
+      have : (list.fin_range n).index_of i < n,
+        by simpa using list.index_of_lt_length.2 (list.mem_fin_range i),
+      simp [list.of_fn_eq_map, (list.nodup_fin_range n).map_update, list.prod_update_nth, this]
+    end }
+
+variables {R A n}
+
+@[simp] lemma mk_pi_algebra_fin_apply (m : fin n → A) :
+  multilinear_map.mk_pi_algebra_fin R n A m = (list.of_fn m).prod :=
+rfl
+
+lemma mk_pi_algebra_fin_apply_const (a : A) :
+  multilinear_map.mk_pi_algebra_fin R n A (λ _, a) = a ^ n :=
+by simp
+
+end
+
+/-- Given an `R`-multilinear map `f` taking values in `R`, `f.smul_right z` is the map
+sending `m` to `f m • z`. -/
+def smul_right (f : multilinear_map R M₁ R) (z : M₂) : multilinear_map R M₁ M₂ :=
+(linear_map.smul_right linear_map.id z).comp_multilinear_map f
+
+@[simp] lemma smul_right_apply (f : multilinear_map R M₁ R) (z : M₂) (m : Π i, M₁ i) :
+  f.smul_right z m = f m • z :=
+rfl
+
 variables (R ι)
 
 /-- The canonical multilinear map on `R^ι` when `ι` is finite, associating to `m` the product of
-all the `m i` (multiplied by a fixed reference element `z` in the target module) -/
+all the `m i` (multiplied by a fixed reference element `z` in the target module). See also
+`mk_pi_algebra` for a more general version. -/
 protected def mk_pi_ring [fintype ι] (z : M₂) : multilinear_map R (λ(i : ι), R) M₂ :=
-{ to_fun := λm, (∏ i, m i) • z,
-  map_add'  := λ m i x y, by simp [finset.prod_update_of_mem, add_mul, add_smul],
-  map_smul' := λ m i c x, by { rw [smul_eq_mul],
-    simp [finset.prod_update_of_mem, smul_smul, mul_assoc] } }
+(multilinear_map.mk_pi_algebra R ι R).smul_right z
 
 variables {R ι}
 
@@ -529,18 +621,6 @@ end comm_ring
 
 end multilinear_map
 
-namespace linear_map
-variables [ring R] [∀i, add_comm_group (M₁ i)] [add_comm_group M₂] [add_comm_group M₃]
-[∀i, module R (M₁ i)] [module R M₂] [module R M₃]
-
-/-- Composing a multilinear map with a linear map gives again a multilinear map. -/
-def comp_multilinear_map (g : M₂ →ₗ[R] M₃) (f : multilinear_map R M₁ M₂) : multilinear_map R M₁ M₃ :=
-{ to_fun    := λ m, g (f m),
-  map_add'  := λ m i x y, by simp,
-  map_smul' := λ m i c x, by simp }
-
-end linear_map
-
 section currying
 /-!
 ### Currying

src/topology/algebra/multilinear.lean

@@ -70,8 +70,13 @@ instance : has_coe_to_fun (continuous_multilinear_map R M₁ M₂) :=
 
 @[simp] lemma coe_coe : (f.to_multilinear_map : (Π i, M₁ i) → M₂) = f := rfl
 
+theorem to_multilinear_map_inj :
+  function.injective (continuous_multilinear_map.to_multilinear_map :
+    continuous_multilinear_map R M₁ M₂ → multilinear_map R M₁ M₂)
+| ⟨f, hf⟩ ⟨g, hg⟩ rfl := rfl
+
 @[ext] theorem ext {f f' : continuous_multilinear_map R M₁ M₂} (H : ∀ x, f x = f' x) : f = f' :=
-by { cases f, cases f', congr' with x, exact H x }
+to_multilinear_map_inj $ multilinear_map.ext H
 
 @[simp] lemma map_add (m : Πi, M₁ i) (i : ι) (x y : M₁ i) :
   f (update m i (x + y)) = f (update m i x) + f (update m i y) :=