refactor(Analysis/Lp): EuclideanSpace.single -> PiLp.single (leanprover-community#36685)

Resolving a TODO in the code. This also makes `PiLp.single` the simp-normal form, as opposite to `toLp _ (Pi.single _ _)` that was in the code.

Author: wwylele

Mathlib/Analysis/CStarAlgebra/Matrix.lean

@@ -129,7 +129,7 @@ lemma inner_toEuclideanCLM (A : Matrix n n ℝ) (x y : EuclideanSpace ℝ n) :
     toLin_apply, mulVec_eq_sum, OrthonormalBasis.coe_toBasis_repr_apply,
     EuclideanSpace.basisFun_repr, op_smul_eq_smul, Finset.sum_apply, Pi.smul_apply, transpose_apply,
     smul_eq_mul, OrthonormalBasis.coe_toBasis, EuclideanSpace.basisFun_apply, PiLp.inner_apply,
-    ofLp_sum, ofLp_smul, EuclideanSpace.ofLp_single, RCLike.inner_apply, conj_trivial, dotProduct]
+    ofLp_sum, ofLp_smul, PiLp.ofLp_single, RCLike.inner_apply, conj_trivial, dotProduct]
   congr with i
   rw [mul_comm (x.ofLp i)]
   simp [Pi.single_apply]

Mathlib/Analysis/InnerProductSpace/PiL2.lean

@@ -288,25 +288,26 @@ section DecEq
 
 variable [DecidableEq ι]
 
--- TODO : This should be generalized to `PiLp`.
 /-- The vector given in Euclidean space by being `a : 𝕜` at coordinate `i : ι` and `0 : 𝕜` at
 all other coordinates. -/
-def EuclideanSpace.single (i : ι) (a : 𝕜) : EuclideanSpace 𝕜 ι :=
-  toLp _ (Pi.single i a)
+abbrev EuclideanSpace.single (i : ι) (a : 𝕜) : EuclideanSpace 𝕜 ι := PiLp.single 2 i a
 
-@[simp] lemma EuclideanSpace.ofLp_single (i : ι) (a : 𝕜) : ofLp (single i a) = Pi.single i a := rfl
+@[deprecated PiLp.ofLp_single (since := "2026-03-15")]
+lemma EuclideanSpace.ofLp_single (i : ι) (a : 𝕜) : ofLp (single i a) = Pi.single i a := by
+  simp
 
-@[simp]
-lemma EuclideanSpace.toLp_single (i : ι) (a : 𝕜) : toLp _ (Pi.single i a) = single i a := rfl
+@[deprecated PiLp.toLp_single (since := "2026-03-15")]
+lemma EuclideanSpace.toLp_single (i : ι) (a : 𝕜) : toLp _ (Pi.single i a) = single i a := by
+  simp
 
-@[simp]
+@[deprecated PiLp.single_apply (since := "2026-03-15")]
 theorem EuclideanSpace.single_apply (i : ι) (a : 𝕜) (j : ι) :
     (EuclideanSpace.single i a) j = ite (j = i) a 0 := by
-  rw [EuclideanSpace.single, PiLp.toLp_apply, ← Pi.single_apply i a j]
+  simp
 
-@[simp]
+@[deprecated PiLp.single_eq_zero_iff (since := "2026-03-15")]
 theorem EuclideanSpace.single_eq_zero_iff {i : ι} {a : 𝕜} :
-    EuclideanSpace.single i a = 0 ↔ a = 0 := (toLp_eq_zero 2).trans Pi.single_eq_zero_iff
+    EuclideanSpace.single i a = 0 ↔ a = 0 := by simp
 
 variable [Fintype ι]
 
@@ -317,36 +318,34 @@ theorem EuclideanSpace.inner_single_left (i : ι) (a : 𝕜) (v : EuclideanSpace
 theorem EuclideanSpace.inner_single_right (i : ι) (a : 𝕜) (v : EuclideanSpace 𝕜 ι) :
     ⟪v, EuclideanSpace.single i (a : 𝕜)⟫ = a * conj (v i) := by simp [PiLp.inner_apply]
 
-@[simp]
+@[deprecated PiLp.norm_single (since := "2026-03-15")]
 theorem EuclideanSpace.norm_single (i : ι) (a : 𝕜) :
-    ‖EuclideanSpace.single i (a : 𝕜)‖ = ‖a‖ :=
-  PiLp.norm_toLp_single 2 (fun _ => 𝕜) i a
+    ‖EuclideanSpace.single i (a : 𝕜)‖ = ‖a‖ := by simp
 
-@[simp]
+@[deprecated PiLp.nnnorm_single (since := "2026-03-15")]
 theorem EuclideanSpace.nnnorm_single (i : ι) (a : 𝕜) :
-    ‖EuclideanSpace.single i (a : 𝕜)‖₊ = ‖a‖₊ :=
-  PiLp.nnnorm_toLp_single 2 (fun _ => 𝕜) i a
+    ‖EuclideanSpace.single i (a : 𝕜)‖₊ = ‖a‖₊ := by simp
 
-@[simp]
+@[deprecated PiLp.dist_single_same (since := "2026-03-15")]
 theorem EuclideanSpace.dist_single_same (i : ι) (a b : 𝕜) :
-    dist (EuclideanSpace.single i (a : 𝕜)) (EuclideanSpace.single i (b : 𝕜)) = dist a b :=
-  PiLp.dist_toLp_single_same 2 (fun _ => 𝕜) i a b
+    dist (EuclideanSpace.single i (a : 𝕜)) (EuclideanSpace.single i (b : 𝕜)) = dist a b := by
+  simp
 
-@[simp]
+@[deprecated PiLp.nndist_single_same (since := "2026-03-15")]
 theorem EuclideanSpace.nndist_single_same (i : ι) (a b : 𝕜) :
-    nndist (EuclideanSpace.single i (a : 𝕜)) (EuclideanSpace.single i (b : 𝕜)) = nndist a b :=
-  PiLp.nndist_toLp_single_same 2 (fun _ => 𝕜) i a b
+    nndist (EuclideanSpace.single i (a : 𝕜)) (EuclideanSpace.single i (b : 𝕜)) = nndist a b := by
+  simp
 
-@[simp]
+@[deprecated PiLp.edist_single_same (since := "2026-03-15")]
 theorem EuclideanSpace.edist_single_same (i : ι) (a b : 𝕜) :
-    edist (EuclideanSpace.single i (a : 𝕜)) (EuclideanSpace.single i (b : 𝕜)) = edist a b :=
-  PiLp.edist_toLp_single_same 2 (fun _ => 𝕜) i a b
+    edist (EuclideanSpace.single i (a : 𝕜)) (EuclideanSpace.single i (b : 𝕜)) = edist a b := by
+  simp
 
 /-- `EuclideanSpace.single` forms an orthonormal family. -/
 theorem EuclideanSpace.orthonormal_single :
     Orthonormal 𝕜 fun i : ι => EuclideanSpace.single i (1 : 𝕜) := by
   simp_rw [orthonormal_iff_ite, EuclideanSpace.inner_single_left, map_one, one_mul,
-    EuclideanSpace.single_apply]
+    PiLp.single_apply]
   intros
   trivial
 
@@ -411,7 +410,7 @@ instance instFunLike : FunLike (OrthonormalBasis ι 𝕜 E) ι E where
         rw [this, Pi.single_smul]
         replace h := congr_fun h i
         simp only [LinearEquiv.comp_coe, map_smul, LinearEquiv.coe_coe, LinearEquiv.trans_apply,
-          coe_symm_linearEquiv, EuclideanSpace.toLp_single,
+          coe_symm_linearEquiv, PiLp.toLp_single,
           LinearIsometryEquiv.coe_symm_toLinearEquiv] at h ⊢
         rw [h]
 
@@ -445,7 +444,7 @@ protected theorem orthonormal (b : OrthonormalBasis ι 𝕜 E) : Orthonormal 
     rw [orthonormal_iff_ite]
     intro i j
     rw [← b.repr.inner_map_map (b i) (b j), b.repr_self i, b.repr_self j,
-      EuclideanSpace.inner_single_left, EuclideanSpace.single_apply, map_one, one_mul]
+      EuclideanSpace.inner_single_left, PiLp.single_apply, map_one, one_mul]
 
 @[simp]
 lemma norm_eq_one (b : OrthonormalBasis ι 𝕜 E) (i : ι) :
@@ -678,18 +677,18 @@ theorem _root_.Pi.orthonormalBasis_apply {η : Type*} [Fintype η] [DecidableEq
     [∀ i, Fintype (ι i)] {𝕜 : Type*} [RCLike 𝕜] {E : η → Type*} [∀ i, NormedAddCommGroup (E i)]
     [∀ i, InnerProductSpace 𝕜 (E i)] (B : ∀ i, OrthonormalBasis (ι i) 𝕜 (E i))
     (j : (i : η) × (ι i)) :
-    Pi.orthonormalBasis B j = toLp _ (Pi.single _ (B j.fst j.snd)) := by
+    Pi.orthonormalBasis B j = PiLp.single 2 j.fst (B j.fst j.snd) := by
   classical
   ext k
   obtain ⟨i, j⟩ := j
   simp only [Pi.orthonormalBasis, coe_ofRepr, LinearIsometryEquiv.symm_trans,
     LinearIsometryEquiv.symm_symm, LinearIsometryEquiv.piLpCongrRight_symm,
     LinearIsometryEquiv.trans_apply, LinearIsometryEquiv.piLpCongrRight_apply,
-    LinearIsometryEquiv.piLpCurry_apply, EuclideanSpace.ofLp_single, PiLp.toLp_apply,
+    LinearIsometryEquiv.piLpCurry_apply, PiLp.ofLp_single, PiLp.toLp_apply,
     Sigma.curry_single (γ := fun _ _ => 𝕜)]
   obtain rfl | hi := Decidable.eq_or_ne i k
-  · simp only [Pi.single_eq_same, EuclideanSpace.toLp_single, OrthonormalBasis.repr_symm_single]
-  · simp only [Pi.single_eq_of_ne' hi, toLp_zero, map_zero]
+  · simp
+  · simp [hi]
 
 @[simp]
 theorem _root_.Pi.orthonormalBasis_repr {η : Type*} [Fintype η] {ι : η → Type*}
@@ -841,7 +840,7 @@ lemma equiv_apply_basis (i : ι) : b.equiv b' e (b i) = b' (e i) := by
   simp only [OrthonormalBasis.equiv, LinearIsometryEquiv.trans_apply, OrthonormalBasis.repr_self]
   refine DFunLike.congr rfl ?_
   ext j
-  simp [Pi.single_apply, Equiv.symm_apply_eq]
+  simp
 
 @[simp]
 lemma equiv_self_rfl : b.equiv b (.refl ι) = .refl 𝕜 E := by

Mathlib/Analysis/Matrix/Spectrum.lean

@@ -127,13 +127,13 @@ theorem conjStarAlgAut_star_eigenvectorUnitary :
       diagonal (RCLike.ofReal ∘ hA.eigenvalues) := by
   apply Matrix.toEuclideanLin.injective <| (EuclideanSpace.basisFun n 𝕜).toBasis.ext fun i ↦ ?_
   simp only [conjStarAlgAut_star_apply, toLpLin_apply, OrthonormalBasis.coe_toBasis,
-    EuclideanSpace.basisFun_apply, EuclideanSpace.ofLp_single, ← mulVec_mulVec,
+    EuclideanSpace.basisFun_apply, PiLp.ofLp_single, ← mulVec_mulVec,
     eigenvectorUnitary_mulVec, ← mulVec_mulVec, mulVec_eigenvectorBasis,
     Matrix.diagonal_mulVec_single, mulVec_smul, star_eigenvectorUnitary_mulVec,
-    RCLike.real_smul_eq_coe_smul (K := 𝕜), WithLp.toLp_smul, EuclideanSpace.toLp_single,
+    RCLike.real_smul_eq_coe_smul (K := 𝕜), WithLp.toLp_smul, PiLp.toLp_single,
     Function.comp_apply, mul_one]
   apply PiLp.ext fun j ↦ ?_
-  simp only [PiLp.smul_apply, EuclideanSpace.single_apply, smul_eq_mul, mul_ite, mul_one, mul_zero]
+  simp only [PiLp.smul_apply, PiLp.single_apply, smul_eq_mul, mul_ite, mul_one, mul_zero]
 
 @[deprecated (since := "2025-11-06")] alias star_mul_self_mul_eq_diagonal :=
   conjStarAlgAut_star_eigenvectorUnitary

Mathlib/Analysis/Normed/Lp/PiLp.lean

@@ -137,6 +137,67 @@ end
 
 lemma toLp_apply (x : ∀ i, α i) (i : ι) : toLp p x i = x i := rfl
 
+section Single
+variable [DecidableEq ι]
+variable {β}
+
+section Zero
+variable [∀ i, Zero (β i)]
+
+/-- The vector given in `PiLp` by being `a : β i` at coordinate `i : ι` and `0 : β j` at
+all other coordinates `j`. -/
+def single (i : ι) (a : β i) : PiLp p β := toLp p (Pi.single i a)
+
+@[simp]
+lemma ofLp_single (i : ι) (a : β i) : ofLp (single p i a) = Pi.single i a := rfl
+
+@[simp]
+lemma toLp_single (i : ι) (a : β i) : toLp p (Pi.single i a) = single p i a := rfl
+
+@[simp]
+lemma single_eq_same (i : ι) (a : β i) : single p i a i = a := by
+  rw [ofLp_single, Pi.single_eq_same]
+
+@[simp]
+lemma single_eq_of_ne {i i' : ι} (h : i' ≠ i) (a : β i) : single p i a i' = 0 := by
+  rw [ofLp_single, Pi.single_eq_of_ne h]
+
+/-- Changing the hypothesis direction in `PiLp.single_eq_of_ne` for for ease of use by simp. -/
+@[simp]
+lemma single_eq_of_ne' {i i' : ι} (h : i ≠ i') (a : β i) : single p i a i' = 0 := by
+  rw [ofLp_single, Pi.single_eq_of_ne' h]
+
+end Zero
+
+@[simp]
+lemma single_apply [Zero 𝕜] (i : ι) (a : 𝕜) (j : ι) :
+    (single p i a : PiLp p (fun _ ↦ 𝕜)) j = ite (j = i) a 0 := by
+  rw [← toLp_single, PiLp.toLp_apply, ← Pi.single_apply i a j]
+
+section AddCommGroup
+variable [∀ i, AddCommGroup (β i)]
+
+@[simp]
+theorem single_eq_zero_iff (p : ℝ≥0∞) (i : ι) {a : β i} :
+    single p i a = 0 ↔ a = 0 :=
+  (toLp_eq_zero p).trans Pi.single_eq_zero_iff
+
+lemma single_add (p : ℝ≥0∞) (i : ι) {a b : β i} :
+    single p i (a + b) = single p i a + single p i b := by
+  simp_rw [← toLp_single, Pi.single_add, toLp_add]
+
+lemma single_sub (p : ℝ≥0∞) (i : ι) {a b : β i} :
+    single p i (a - b) = single p i a - single p i b := by
+  simp_rw [← toLp_single, Pi.single_sub, toLp_sub]
+
+lemma single_neg (p : ℝ≥0∞) (i : ι) {a : β i} :
+    single p i (-a) = -single p i a := by
+  simp_rw [← toLp_single, Pi.single_neg, toLp_neg]
+
+end AddCommGroup
+
+end Single
+
 section DistNorm
 
 variable [Fintype ι]
@@ -798,8 +859,7 @@ theorem _root_.LinearIsometryEquiv.piLpCongrLeft_symm (e : ι ≃ ι') :
 @[simp high]
 theorem _root_.LinearIsometryEquiv.piLpCongrLeft_single [DecidableEq ι] [DecidableEq ι']
     (e : ι ≃ ι') (i : ι) (v : E) :
-    LinearIsometryEquiv.piLpCongrLeft p 𝕜 E e (toLp p <| Pi.single i v) =
-      toLp p (Pi.single (e i) v) := by
+    LinearIsometryEquiv.piLpCongrLeft p 𝕜 E e (single p i v) = single p (e i) v := by
   ext x
   simp [LinearIsometryEquiv.piLpCongrLeft_apply, Equiv.piCongrLeft',
     Pi.single, Function.update, Equiv.symm_apply_eq]
@@ -847,8 +907,7 @@ theorem _root_.LinearIsometryEquiv.piLpCongrRight_symm (e : ∀ i, α i ≃ₗ
 @[simp high]
 theorem _root_.LinearIsometryEquiv.piLpCongrRight_single (e : ∀ i, α i ≃ₗᵢ[𝕜] β i) [DecidableEq ι]
     (i : ι) (v : α i) :
-    LinearIsometryEquiv.piLpCongrRight p e (toLp p <| Pi.single i v) =
-      toLp p (Pi.single i (e _ v)) :=
+    LinearIsometryEquiv.piLpCongrRight p e (single p i v) = single p i (e _ v) :=
   PiLp.ext <| Pi.apply_single (e ·) (fun _ => map_zero _) _ _
 
 end piLpCongrRight
@@ -927,46 +986,68 @@ variable [DecidableEq ι]
 
 set_option backward.isDefEq.respectTransparency false in
 @[simp]
-theorem nnnorm_toLp_single (i : ι) (b : β i) :
-    ‖toLp p (Pi.single i b)‖₊ = ‖b‖₊ := by
+theorem nnnorm_single (i : ι) (b : β i) : ‖single p i b‖₊ = ‖b‖₊ := by
   haveI : Nonempty ι := ⟨i⟩
   induction p generalizing hp with
   | top =>
     simp_rw [nnnorm_eq_ciSup]
     refine
       ciSup_eq_of_forall_le_of_forall_lt_exists_gt (fun j => ?_) fun 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]
+      · rw [single_eq_same]
+      · rw [single_eq_of_ne' _ hij, nnnorm_zero]
         exact zero_le _
-    · rw [Pi.single_eq_same]
+    · rw [single_eq_same]
   | coe p =>
     have hp0 : (p : ℝ) ≠ 0 :=
       mod_cast (zero_lt_one.trans_le <| Fact.out (p := 1 ≤ (p : ℝ≥0∞))).ne'
     rw [nnnorm_eq_sum ENNReal.coe_ne_top, ENNReal.coe_toReal, Fintype.sum_eq_single i,
-      toLp_apply, Pi.single_eq_same, ← NNReal.rpow_mul, one_div,
+      toLp_apply, single_eq_same, ← NNReal.rpow_mul, one_div,
       mul_inv_cancel₀ hp0, NNReal.rpow_one]
     intro j hij
-    rw [toLp_apply, Pi.single_eq_of_ne hij, nnnorm_zero, NNReal.zero_rpow hp0]
+    rw [toLp_apply, single_eq_of_ne _ hij, nnnorm_zero, NNReal.zero_rpow hp0]
+
+@[deprecated nnnorm_single (since := "2026-03-15")]
+theorem nnnorm_toLp_single (i : ι) (b : β i) : ‖toLp p (Pi.single i b)‖₊ = ‖b‖₊ :=
+  nnnorm_single p β i b
 
 @[simp]
+lemma norm_single (i : ι) (b : β i) : ‖single p i b‖ = ‖b‖ :=
+  congr_arg ((↑) : ℝ≥0 → ℝ) <| nnnorm_single p β i b
+
+@[deprecated norm_single (since := "2026-03-15")]
 lemma norm_toLp_single (i : ι) (b : β i) : ‖toLp p (Pi.single i b)‖ = ‖b‖ :=
-  congr_arg ((↑) : ℝ≥0 → ℝ) <| nnnorm_toLp_single p β i b
+  norm_single p β i b
 
 @[simp]
+lemma nndist_single_same (i : ι) (b₁ b₂ : β i) :
+    nndist (single p i b₁) (single p i b₂) = nndist b₁ b₂ := by
+  rw [nndist_eq_nnnorm, nndist_eq_nnnorm, ← single_sub, nnnorm_single]
+
+@[deprecated nndist_single_same (since := "2026-03-15")]
 lemma nndist_toLp_single_same (i : ι) (b₁ b₂ : β i) :
-    nndist (toLp p (Pi.single i b₁)) (toLp p (Pi.single i b₂)) = nndist b₁ b₂ := by
-  rw [nndist_eq_nnnorm, nndist_eq_nnnorm, ← toLp_sub, ← Pi.single_sub, nnnorm_toLp_single]
+    nndist (toLp p (Pi.single i b₁)) (toLp p (Pi.single i b₂)) = nndist b₁ b₂ :=
+  nndist_single_same p β i b₁ b₂
 
 @[simp]
+lemma dist_single_same (i : ι) (b₁ b₂ : β i) :
+    dist (single p i b₁) (single p i b₂) = dist b₁ b₂ :=
+  congr_arg ((↑) : ℝ≥0 → ℝ) <| nndist_single_same p β i b₁ b₂
+
+@[deprecated dist_single_same (since := "2026-03-15")]
 lemma dist_toLp_single_same (i : ι) (b₁ b₂ : β i) :
     dist (toLp p (Pi.single i b₁)) (toLp p (Pi.single i b₂)) = dist b₁ b₂ :=
-  congr_arg ((↑) : ℝ≥0 → ℝ) <| nndist_toLp_single_same p β i b₁ b₂
+  dist_single_same p β i b₁ b₂
 
 @[simp]
+lemma edist_single_same (i : ι) (b₁ b₂ : β i) :
+    edist (single p i b₁) (single p i b₂) = edist b₁ b₂ := by
+  simp only [edist_nndist, nndist_single_same p β i b₁ b₂]
+
+@[deprecated edist_single_same (since := "2026-03-15")]
 lemma edist_toLp_single_same (i : ι) (b₁ b₂ : β i) :
-    edist (toLp p (Pi.single i b₁)) (toLp p (Pi.single i b₂)) = edist b₁ b₂ := by
-  simp only [edist_nndist, nndist_toLp_single_same p β i b₁ b₂]
+    edist (toLp p (Pi.single i b₁)) (toLp p (Pi.single i b₂)) = edist b₁ b₂ :=
+  edist_single_same p β i b₁ b₂
 
 end Single
 
@@ -1061,8 +1142,8 @@ def basisFun : Basis ι 𝕜 (PiLp p fun _ : ι => 𝕜) :=
 
 @[simp]
 theorem basisFun_apply [DecidableEq ι] (i) :
-    basisFun p 𝕜 ι i = toLp p (Pi.single i 1) := by
-  simp_rw [basisFun, Basis.coe_ofEquivFun, WithLp.coe_symm_linearEquiv]
+    basisFun p 𝕜 ι i = single p i 1 := by
+  simp_rw [basisFun, Basis.coe_ofEquivFun, WithLp.coe_symm_linearEquiv, toLp_single]
 
 @[simp]
 theorem basisFun_repr (x : PiLp p fun _ : ι => 𝕜) (i : ι) : (basisFun p 𝕜 ι).repr x i = x i :=