From 53756f0e34b003a412e060294f500f0cd76939be Mon Sep 17 00:00:00 2001
From: Yakov Pechersky <ffxen158@gmail.com>
Date: Mon, 15 Mar 2021 21:56:52 -0400
Subject: [PATCH 1/3] feat(normed_space/inner_product): euclidean_space.norm_eq

---
 src/analysis/normed_space/inner_product.lean | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/src/analysis/normed_space/inner_product.lean b/src/analysis/normed_space/inner_product.lean
index 86bb5e233c09e..ec163a06dcfeb 100644
--- a/src/analysis/normed_space/inner_product.lean
+++ b/src/analysis/normed_space/inner_product.lean
@@ -1430,6 +1430,15 @@ space use `euclidean_space 𝕜 (fin n)`. -/
 def euclidean_space (𝕜 : Type*) [is_R_or_C 𝕜]
   (n : Type*) [fintype n] : Type* := pi_Lp 2 one_le_two (λ (i : n), 𝕜)
 
+lemma euclidean_space.norm_eq {𝕜 : Type*} [is_R_or_C 𝕜] {n : Type*} [fintype n]
+  (x : euclidean_space 𝕜 n) : ∥ x ∥ = real.sqrt (∑ (i : n), ∥x i∥ ^ 2) :=
+begin
+  have : (2 : ℝ) = (2 : ℕ) := by norm_num,
+  have h : ∀ (x : ℝ) (n : ℕ), real.rpow x n = monoid.pow x n := by simp,
+  simp_rw [pi_Lp.norm_eq, real.sqrt_eq_rpow, this, ←real.rpow_eq_pow, h],
+  simp
+end
+
 /-! ### Inner product space structure on subspaces -/
 
 /-- Induced inner product on a submodule. -/

From f0c564c90387f80f8c916d3de23cef309e1d7ecb Mon Sep 17 00:00:00 2001
From: Yakov Pechersky <ffxen158@gmail.com>
Date: Tue, 16 Mar 2021 00:37:29 -0400
Subject: [PATCH 2/3] add pi_Lp norm of nat and L2 norm lemmas

---
 src/analysis/normed_space/inner_product.lean | 12 ++++++------
 src/topology/metric_space/pi_Lp.lean         |  5 +++++
 2 files changed, 11 insertions(+), 6 deletions(-)

diff --git a/src/analysis/normed_space/inner_product.lean b/src/analysis/normed_space/inner_product.lean
index ec163a06dcfeb..410e3ce8bc211 100644
--- a/src/analysis/normed_space/inner_product.lean
+++ b/src/analysis/normed_space/inner_product.lean
@@ -1413,6 +1413,11 @@ instance pi_Lp.inner_product_space {ι : Type*} [fintype ι] (f : ι → Type*)
   ⟪x, y⟫ = ∑ i, ⟪x i, y i⟫ :=
 rfl
 
+lemma pi_Lp.norm_eq_of_L2 {ι : Type*} [fintype ι] {f : ι → Type*}
+  [Π i, inner_product_space 𝕜 (f i)] (x : pi_Lp 2 one_le_two f) :
+  ∥ x ∥ = sqrt (∑ (i : ι), ∥x i∥ ^ 2) :=
+by { rw [pi_Lp.norm_eq_of_nat 2]; simp [sqrt_eq_rpow] }
+
 /-- A field `𝕜` satisfying `is_R_or_C` is itself a `𝕜`-inner product space. -/
 instance is_R_or_C.inner_product_space : inner_product_space 𝕜 𝕜 :=
 { inner := (λ x y, (conj x) * y),
@@ -1432,12 +1437,7 @@ def euclidean_space (𝕜 : Type*) [is_R_or_C 𝕜]
 
 lemma euclidean_space.norm_eq {𝕜 : Type*} [is_R_or_C 𝕜] {n : Type*} [fintype n]
   (x : euclidean_space 𝕜 n) : ∥ x ∥ = real.sqrt (∑ (i : n), ∥x i∥ ^ 2) :=
-begin
-  have : (2 : ℝ) = (2 : ℕ) := by norm_num,
-  have h : ∀ (x : ℝ) (n : ℕ), real.rpow x n = monoid.pow x n := by simp,
-  simp_rw [pi_Lp.norm_eq, real.sqrt_eq_rpow, this, ←real.rpow_eq_pow, h],
-  simp
-end
+pi_Lp.norm_eq_of_L2 x
 
 /-! ### Inner product space structure on subspaces -/
 
diff --git a/src/topology/metric_space/pi_Lp.lean b/src/topology/metric_space/pi_Lp.lean
index cb20e8185a424..91d2f9bc46b74 100644
--- a/src/topology/metric_space/pi_Lp.lean
+++ b/src/topology/metric_space/pi_Lp.lean
@@ -229,6 +229,11 @@ lemma norm_eq {p : ℝ} {hp : 1 ≤ p} {α : ι → Type*}
   [∀i, normed_group (α i)] (f : pi_Lp p hp α) :
   ∥f∥ = (∑ (i : ι), ∥f i∥ ^ p) ^ (1/p) := rfl
 
+lemma norm_eq_of_nat {p : ℝ} {hp : 1 ≤ p} {α : ι → Type*}
+  [∀i, normed_group (α i)] (n : ℕ) (h : p = n) (f : pi_Lp p hp α) :
+  ∥f∥ = (∑ (i : ι), ∥f i∥ ^ n) ^ (1/(n : ℝ)) :=
+by simp [norm_eq, h, real.sqrt_eq_rpow, ←real.rpow_nat_cast]
+
 variables (𝕜 : Type*) [normed_field 𝕜]
 
 /-- The product of finitely many normed spaces is a normed space, with the `L^p` norm. -/

From 05ba1e0d47196d1ce06ba3ce6d80842eaf21c9fa Mon Sep 17 00:00:00 2001
From: Yakov Pechersky <pechersky@users.noreply.github.com>
Date: Wed, 17 Mar 2021 23:29:08 -0400
Subject: [PATCH 3/3] Apply suggestions from code review

Co-authored-by: hrmacbeth <25316162+hrmacbeth@users.noreply.github.com>
---
 src/analysis/normed_space/inner_product.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/analysis/normed_space/inner_product.lean b/src/analysis/normed_space/inner_product.lean
index 410e3ce8bc211..dab2715f8b04b 100644
--- a/src/analysis/normed_space/inner_product.lean
+++ b/src/analysis/normed_space/inner_product.lean
@@ -1415,7 +1415,7 @@ rfl
 
 lemma pi_Lp.norm_eq_of_L2 {ι : Type*} [fintype ι] {f : ι → Type*}
   [Π i, inner_product_space 𝕜 (f i)] (x : pi_Lp 2 one_le_two f) :
-  ∥ x ∥ = sqrt (∑ (i : ι), ∥x i∥ ^ 2) :=
+  ∥x∥ = sqrt (∑ (i : ι), ∥x i∥ ^ 2) :=
 by { rw [pi_Lp.norm_eq_of_nat 2]; simp [sqrt_eq_rpow] }
 
 /-- A field `𝕜` satisfying `is_R_or_C` is itself a `𝕜`-inner product space. -/
@@ -1436,7 +1436,7 @@ def euclidean_space (𝕜 : Type*) [is_R_or_C 𝕜]
   (n : Type*) [fintype n] : Type* := pi_Lp 2 one_le_two (λ (i : n), 𝕜)
 
 lemma euclidean_space.norm_eq {𝕜 : Type*} [is_R_or_C 𝕜] {n : Type*} [fintype n]
-  (x : euclidean_space 𝕜 n) : ∥ x ∥ = real.sqrt (∑ (i : n), ∥x i∥ ^ 2) :=
+  (x : euclidean_space 𝕜 n) : ∥x∥ = real.sqrt (∑ (i : n), ∥x i∥ ^ 2) :=
 pi_Lp.norm_eq_of_L2 x
 
 /-! ### Inner product space structure on subspaces -/