feat(analysis/calculus/times_cont_diff): equiv.prod_assoc is smooth. (

#10165)

Formalized as part of the Sphere Eversion project.

src/analysis/calculus/times_cont_diff.lean

@@ -1626,6 +1626,24 @@ lemma times_cont_diff_within_at_snd {s : set (E × F)} {p : E × F} {n : with_to
   times_cont_diff_within_at 𝕜 n (prod.snd : E × F → F) s p :=
 times_cont_diff_snd.times_cont_diff_within_at
 
+/--
+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
+reformulating the lemma that you're applying next using the tips in
+Note [continuity lemma statement]
+-/
+lemma times_cont_diff_prod_assoc : times_cont_diff 𝕜 ⊤ $ equiv.prod_assoc E F G :=
+(linear_isometry_equiv.prod_assoc 𝕜 E F G).times_cont_diff
+
+/--
+The natural equivalence `E × (F × G) ≃ (E × F) × G` is smooth.
+
+Warning: see remarks attached to `times_cont_diff_prod_assoc`
+-/
+lemma times_cont_diff_prod_assoc_symm : times_cont_diff 𝕜 ⊤ $ (equiv.prod_assoc E F G).symm :=
+(linear_isometry_equiv.prod_assoc 𝕜 E F G).symm.times_cont_diff
+
 /--
 The identity is `C^∞`.
 -/

src/analysis/normed_space/linear_isometry.lean

@@ -415,4 +415,27 @@ variables {R}
 
 @[simp] lemma symm_neg : (neg R : E ≃ₗᵢ[R] E).symm = neg R := rfl
 
+variables (R E E₂ E₃)
+
+/-- The natural equivalence `(E × E₂) × E₃ ≃ E × (E₂ × E₃)` is a linear isometry. -/
+noncomputable def prod_assoc [module R E₂] [module R E₃] : (E × E₂) × E₃ ≃ₗᵢ[R] E × E₂ × E₃ :=
+{ to_fun    := equiv.prod_assoc E E₂ E₃,
+  inv_fun   := (equiv.prod_assoc E E₂ E₃).symm,
+  map_add'  := by simp,
+  map_smul' := by simp,
+  norm_map' :=
+    begin
+      rintros ⟨⟨e, f⟩, g⟩,
+      simp only [linear_equiv.coe_mk, equiv.prod_assoc_apply, prod.semi_norm_def, max_assoc],
+    end,
+  .. equiv.prod_assoc E E₂ E₃, }
+
+@[simp] lemma coe_prod_assoc [module R E₂] [module R E₃] :
+  (prod_assoc R E E₂ E₃ : (E × E₂) × E₃ → E × E₂ × E₃) = equiv.prod_assoc E E₂ E₃ :=
+rfl
+
+@[simp] lemma coe_prod_assoc_symm [module R E₂] [module R E₃] :
+  ((prod_assoc R E E₂ E₃).symm : E × E₂ × E₃ → (E × E₂) × E₃) = (equiv.prod_assoc E E₂ E₃).symm :=
+rfl
+
 end linear_isometry_equiv