feat(analysis/inner_product_space/pi_L2): Distance formula in the euclidean space (#14642)

A few missing results about `pi_Lp 2` and `euclidean_space`.

Author: YaelDillies

src/analysis/inner_product_space/pi_L2.lean

@@ -98,6 +98,18 @@ lemma euclidean_space.nnnorm_eq {𝕜 : Type*} [is_R_or_C 𝕜] {n : Type*} [fin
   (x : euclidean_space 𝕜 n) : ∥x∥₊ = nnreal.sqrt (∑ i, ∥x i∥₊ ^ 2) :=
 pi_Lp.nnnorm_eq_of_L2 x
 
+lemma euclidean_space.dist_eq {𝕜 : Type*} [is_R_or_C 𝕜] {n : Type*} [fintype n]
+  (x y : euclidean_space 𝕜 n) : dist x y = (∑ i, dist (x i) (y i) ^ 2).sqrt :=
+(pi_Lp.dist_eq_of_L2 x y : _)
+
+lemma euclidean_space.nndist_eq {𝕜 : Type*} [is_R_or_C 𝕜] {n : Type*} [fintype n]
+  (x y : euclidean_space 𝕜 n) : nndist x y = (∑ i, nndist (x i) (y i) ^ 2).sqrt :=
+(pi_Lp.nndist_eq_of_L2 x y : _)
+
+lemma euclidean_space.edist_eq {𝕜 : Type*} [is_R_or_C 𝕜] {n : Type*} [fintype n]
+  (x y : euclidean_space 𝕜 n) : edist x y = (∑ i, edist (x i) (y i) ^ 2) ^ (1 / 2 : ℝ) :=
+(pi_Lp.edist_eq_of_L2 x y : _)
+
 variables [fintype ι]
 
 section

src/analysis/normed_space/pi_Lp.lean

@@ -312,6 +312,18 @@ lemma nnnorm_eq_of_L2 {β : ι → Type*} [Π i, semi_normed_group (β i)] (x :
   ∥x∥₊ = nnreal.sqrt (∑ (i : ι), ∥x i∥₊ ^ 2) :=
 subtype.ext $ by { push_cast, exact norm_eq_of_L2 x }
 
+lemma dist_eq_of_L2 {β : ι → Type*} [Π i, semi_normed_group (β i)] (x y : pi_Lp 2 β) :
+  dist x y = (∑ i, dist (x i) (y i) ^ 2).sqrt :=
+by simp_rw [dist_eq_norm, norm_eq_of_L2, pi.sub_apply]
+
+lemma nndist_eq_of_L2 {β : ι → Type*} [Π i, semi_normed_group (β i)] (x y : pi_Lp 2 β) :
+  nndist x y = (∑ i, nndist (x i) (y i) ^ 2).sqrt :=
+subtype.ext $ by { push_cast, exact dist_eq_of_L2 _ _ }
+
+lemma edist_eq_of_L2 {β : ι → Type*} [Π i, semi_normed_group (β i)] (x y : pi_Lp 2 β) :
+  edist x y = (∑ i, edist (x i) (y i) ^ 2) ^ (1 / 2 : ℝ) :=
+by simp_rw [pi_Lp.edist_eq, ennreal.rpow_two]
+
 include fact_one_le_p
 
 variables [normed_field 𝕜]