From 64ad02aba150b6b180d1debf125fdb242db684dc Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Mon, 15 May 2023 16:31:33 +0000 Subject: [PATCH 1/2] feat(analysis/inner_product_space/pi_L2): norms of basis vectors --- src/analysis/inner_product_space/pi_L2.lean | 42 ++++++++++++--- src/analysis/normed_space/pi_Lp.lean | 57 ++++++++++++++++++++- 2 files changed, 91 insertions(+), 8 deletions(-) diff --git a/src/analysis/inner_product_space/pi_L2.lean b/src/analysis/inner_product_space/pi_L2.lean index 4c865e310c985..72a1f08221eea 100644 --- a/src/analysis/inner_product_space/pi_L2.lean +++ b/src/analysis/inner_product_space/pi_L2.lean @@ -226,18 +226,46 @@ by simp [apply_ite conj] lemma euclidean_space.inner_single_right [decidable_eq ι] (i : ι) (a : 𝕜) (v : euclidean_space 𝕜 ι) : - ⟪v, euclidean_space.single i (a : 𝕜)⟫ = a * conj (v i) := + ⟪v, euclidean_space.single i (a : 𝕜)⟫ = a * conj (v i) := by simp [apply_ite conj, mul_comm] -lemma euclidean_space.pi_Lp_congr_left_single [decidable_eq ι] {ι' : Type*} [fintype ι'] - [decidable_eq ι'] (e : ι' ≃ ι) (i' : ι') : - linear_isometry_equiv.pi_Lp_congr_left 2 𝕜 𝕜 e (euclidean_space.single i' (1:𝕜)) = - euclidean_space.single (e i') (1:𝕜) := +@[simp] lemma euclidean_space.norm_single [decidable_eq ι] (i : ι) (a : 𝕜) : + ‖euclidean_space.single i (a : 𝕜)‖ = ‖a‖ := +(pi_Lp.norm_equiv_symm_single 2 (λ i, 𝕜) i a : _) + +@[simp] lemma euclidean_space.nnnorm_single [decidable_eq ι] (i : ι) (a : 𝕜) : + ‖euclidean_space.single i (a : 𝕜)‖₊ = ‖a‖₊ := +(pi_Lp.nnnorm_equiv_symm_single 2 (λ i, 𝕜) i a : _) + +@[simp] lemma euclidean_space.dist_single_same [decidable_eq ι] (i : ι) (a b : 𝕜) : + dist (euclidean_space.single i (a : 𝕜)) (euclidean_space.single i (b : 𝕜)) = dist a b := +(pi_Lp.dist_equiv_symm_single_same 2 (λ i, 𝕜) i a b : _) + +@[simp] lemma euclidean_space.nndist_single_same [decidable_eq ι] (i : ι) (a b : 𝕜) : + nndist (euclidean_space.single i (a : 𝕜)) (euclidean_space.single i (b : 𝕜)) = nndist a b := +(pi_Lp.nndist_equiv_symm_single_same 2 (λ i, 𝕜) i a b : _) + +@[simp] lemma euclidean_space.edist_single_same [decidable_eq ι] (i : ι) (a b : 𝕜) : + edist (euclidean_space.single i (a : 𝕜)) (euclidean_space.single i (b : 𝕜)) = edist a b := +(pi_Lp.edist_equiv_symm_single_same 2 (λ i, 𝕜) i a b : _) + +/-- `euclidean_space.single` forms an orthonormal family. -/ +lemma euclidean_space.orthonormal_single [decidable_eq ι] : + orthonormal 𝕜 (λ i : ι, euclidean_space.single i (1 : 𝕜)) := + begin - ext i, - simpa using if_congr e.symm_apply_eq rfl rfl + simp_rw [orthonormal_iff_ite, euclidean_space.inner_single_left, map_one, one_mul, + euclidean_space.single_apply], + intros i j, + refl, end +lemma euclidean_space.pi_Lp_congr_left_single [decidable_eq ι] {ι' : Type*} [fintype ι'] + [decidable_eq ι'] (e : ι' ≃ ι) (i' : ι') (v : 𝕜): + linear_isometry_equiv.pi_Lp_congr_left 2 𝕜 𝕜 e (euclidean_space.single i' v) = + euclidean_space.single (e i') v := +linear_isometry_equiv.pi_Lp_congr_left_single e i' _ + variables (ι 𝕜 E) /-- An orthonormal basis on E is an identification of `E` with its dimensional-matching diff --git a/src/analysis/normed_space/pi_Lp.lean b/src/analysis/normed_space/pi_Lp.lean index d6ead6efaefb7..ec85d614f1aa0 100644 --- a/src/analysis/normed_space/pi_Lp.lean +++ b/src/analysis/normed_space/pi_Lp.lean @@ -623,7 +623,9 @@ linear_isometry_equiv.ext $ λ x, rfl @[simp] lemma _root_.linear_isometry_equiv.pi_Lp_congr_left_single [decidable_eq ι] [decidable_eq ι'] (e : ι ≃ ι') (i : ι) (v : E) : - linear_isometry_equiv.pi_Lp_congr_left p 𝕜 E e (pi.single i v) = pi.single (e i) v := + linear_isometry_equiv.pi_Lp_congr_left p 𝕜 E e ( + (pi_Lp.equiv p (λ _, E)).symm $ pi.single i v) = + (pi_Lp.equiv p (λ _, E)).symm (pi.single (e i) v) := begin funext x, simp [linear_isometry_equiv.pi_Lp_congr_left, linear_equiv.Pi_congr_left', equiv.Pi_congr_left', @@ -649,6 +651,59 @@ end @[simp] lemma equiv_symm_smul : (pi_Lp.equiv p β).symm (c • x') = c • (pi_Lp.equiv p β).symm x' := rfl +section single + +variables (p) +variables [decidable_eq ι] + +@[simp] +lemma nnnorm_equiv_symm_single (i : ι) (b : β i) : + ‖(pi_Lp.equiv p β).symm (pi.single i b)‖₊ = ‖b‖₊ := +begin + haveI : nonempty ι := ⟨i⟩, + unfreezingI { induction p using with_top.rec_top_coe }, + { simp_rw [nnnorm_eq_csupr, equiv_symm_apply], + refine csupr_eq_of_forall_le_of_forall_lt_exists_gt (λ j, _) (λ n hn, ⟨i, hn.trans_eq _⟩), + { obtain rfl | hij := decidable.eq_or_ne i j, + { rw pi.single_eq_same }, + { rw [pi.single_eq_of_ne' hij, nnnorm_zero], + exact zero_le _ } }, + { rw pi.single_eq_same } }, + { have hp0 : (p : ℝ) ≠ 0, + { exact_mod_cast (zero_lt_one.trans_le $ fact.out (1 ≤ (p : ℝ≥0∞))).ne' }, + rw [nnnorm_eq_sum ennreal.coe_ne_top, ennreal.coe_to_real, fintype.sum_eq_single i, + equiv_symm_apply, pi.single_eq_same, ←nnreal.rpow_mul, one_div, mul_inv_cancel hp0, + nnreal.rpow_one], + intros j hij, + rw [equiv_symm_apply, pi.single_eq_of_ne hij, nnnorm_zero, nnreal.zero_rpow hp0] }, +end + +@[simp] +lemma norm_equiv_symm_single (i : ι) (b : β i) : + ‖(pi_Lp.equiv p β).symm (pi.single i b)‖ = ‖b‖ := +congr_arg coe $ nnnorm_equiv_symm_single p β i b + +@[simp] +lemma nndist_equiv_symm_single_same (i : ι) (b₁ b₂ : β i) : + nndist ((pi_Lp.equiv p β).symm (pi.single i b₁)) ((pi_Lp.equiv p β).symm (pi.single i b₂)) = + nndist b₁ b₂ := +by rw [nndist_eq_nnnorm, nndist_eq_nnnorm, ←equiv_symm_sub, ←pi.single_sub, + nnnorm_equiv_symm_single] + +@[simp] +lemma dist_equiv_symm_single_same (i : ι) (b₁ b₂ : β i) : + dist ((pi_Lp.equiv p β).symm (pi.single i b₁)) ((pi_Lp.equiv p β).symm (pi.single i b₂)) = + dist b₁ b₂ := +congr_arg coe $ nndist_equiv_symm_single_same p β i b₁ b₂ + +@[simp] +lemma edist_equiv_symm_single_same (i : ι) (b₁ b₂ : β i) : + edist ((pi_Lp.equiv p β).symm (pi.single i b₁)) ((pi_Lp.equiv p β).symm (pi.single i b₂)) = + edist b₁ b₂ := +by simpa only [edist_nndist] using congr_arg coe (nndist_equiv_symm_single_same p β i b₁ b₂) + +end single + /-- When `p = ∞`, this lemma does not hold without the additional assumption `nonempty ι` because the left-hand side simplifies to `0`, while the right-hand side simplifies to `‖b‖₊`. See `pi_Lp.nnnorm_equiv_symm_const'` for a version which exchanges the hypothesis `p ≠ ∞` for From b955a57d3db7cd6f2fdf1d168dff0d4116243254 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 17 May 2023 12:39:42 +0100 Subject: [PATCH 2/2] Update src/analysis/inner_product_space/pi_L2.lean Co-authored-by: sgouezel --- src/analysis/inner_product_space/pi_L2.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/src/analysis/inner_product_space/pi_L2.lean b/src/analysis/inner_product_space/pi_L2.lean index 72a1f08221eea..011794e4a6975 100644 --- a/src/analysis/inner_product_space/pi_L2.lean +++ b/src/analysis/inner_product_space/pi_L2.lean @@ -252,7 +252,6 @@ by simp [apply_ite conj, mul_comm] /-- `euclidean_space.single` forms an orthonormal family. -/ lemma euclidean_space.orthonormal_single [decidable_eq ι] : orthonormal 𝕜 (λ i : ι, euclidean_space.single i (1 : 𝕜)) := - begin simp_rw [orthonormal_iff_ite, euclidean_space.inner_single_left, map_one, one_mul, euclidean_space.single_apply],