feat(analysis/inner_product_space/pi_L2): norms of basis vectors (#19020

)

This adds `‖euclidean_space.single i (a : 𝕜)‖ = ‖a‖` and other similar results.
They hold more generally for `pi_Lp`, so they are proven there first.

The statement of `linear_isometry_equiv.pi_Lp_congr_left_single` has also been corrected to include the missing typecast.

src/analysis/inner_product_space/pi_L2.lean

@@ -226,18 +226,45 @@ 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

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