From e7667987b25702ab840103f3d41b0f6739e30e21 Mon Sep 17 00:00:00 2001 From: Yakov Pechersky Date: Thu, 18 Mar 2021 19:27:36 +0000 Subject: [PATCH] feat(normed_space/inner_product): euclidean_space.norm_eq (#6744) Co-authored-by: Yakov Pechersky --- src/analysis/normed_space/inner_product.lean | 9 +++++++++ src/topology/metric_space/pi_Lp.lean | 5 +++++ 2 files changed, 14 insertions(+) diff --git a/src/analysis/normed_space/inner_product.lean b/src/analysis/normed_space/inner_product.lean index d583b0e539f38..f0f47dd5eb358 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), @@ -1430,6 +1435,10 @@ 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) := +pi_Lp.norm_eq_of_L2 x + /-! ### Inner product space structure on subspaces -/ /-- Induced inner product on a submodule. -/ 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. -/