Skip to content

Commit

Permalink
feat(normed_space/inner_product): euclidean_space.norm_eq (#6744)
Browse files Browse the repository at this point in the history
Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>
  • Loading branch information
2 people authored and b-mehta committed Apr 2, 2021
1 parent 40ac0a3 commit e766798
Show file tree
Hide file tree
Showing 2 changed files with 14 additions and 0 deletions.
9 changes: 9 additions & 0 deletions src/analysis/normed_space/inner_product.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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),
Expand All @@ -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. -/
Expand Down
5 changes: 5 additions & 0 deletions src/topology/metric_space/pi_Lp.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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. -/
Expand Down

0 comments on commit e766798

Please sign in to comment.