feat: shorthand lemmas for the L1 norm (#20383)

These are consistent with the existing lemmas about the L2 norm.

Mathlib/Analysis/Matrix.lean

@@ -246,7 +246,7 @@ theorem linfty_opNorm_def (A : Matrix m n α) :
     ‖A‖ = ((Finset.univ : Finset m).sup fun i : m => ∑ j : n, ‖A i j‖₊ : ℝ≥0) := by
   -- Porting note: added
   change ‖fun i => (WithLp.equiv 1 _).symm (A i)‖ = _
-  simp [Pi.norm_def, PiLp.nnnorm_eq_sum ENNReal.one_ne_top]
+  simp [Pi.norm_def, PiLp.nnnorm_eq_of_L1]
 
 @[deprecated (since := "2024-02-02")] alias linfty_op_norm_def := linfty_opNorm_def
 

Mathlib/Analysis/Normed/Lp/PiLp.lean

@@ -575,15 +575,37 @@ theorem norm_eq_of_nat {p : ℝ≥0∞} [Fact (1 ≤ p)] {β : ι → Type*}
   simp only [one_div, h, Real.rpow_natCast, ENNReal.toReal_nat, eq_self_iff_true, Finset.sum_congr,
     norm_eq_sum this]
 
-theorem norm_eq_of_L2 {β : ι → Type*} [∀ i, SeminormedAddCommGroup (β i)] (x : PiLp 2 β) :
+section L1
+variable {β} [∀ i, SeminormedAddCommGroup (β i)]
+
+theorem norm_eq_of_L1 (x : PiLp 1 β) : ‖x‖ = ∑ i : ι, ‖x i‖ := by
+  simp [norm_eq_sum]
+
+theorem nnnorm_eq_of_L1 (x : PiLp 1 β) : ‖x‖₊ = ∑ i : ι, ‖x i‖₊ :=
+  NNReal.eq <| by push_cast; exact norm_eq_of_L1 x
+
+theorem dist_eq_of_L1 (x y : PiLp 1 β) : dist x y = ∑ i, dist (x i) (y i) := by
+  simp_rw [dist_eq_norm, norm_eq_of_L1, sub_apply]
+
+theorem nndist_eq_of_L1 (x y : PiLp 1 β) : nndist x y = ∑ i, nndist (x i) (y i) :=
+  NNReal.eq <| by push_cast; exact dist_eq_of_L1 _ _
+
+theorem edist_eq_of_L1 (x y : PiLp 1 β) : edist x y = ∑ i, edist (x i) (y i) := by
+  simp [PiLp.edist_eq_sum]
+
+end L1
+
+section L2
+variable {β} [∀ i, SeminormedAddCommGroup (β i)]
+
+theorem norm_eq_of_L2 (x : PiLp 2 β) :
     ‖x‖ = √(∑ i : ι, ‖x i‖ ^ 2) := by
-  rw [norm_eq_of_nat 2 (by norm_cast) _] -- Porting note: was `convert`
+  rw [norm_eq_of_nat 2 (by norm_cast) _]
   rw [Real.sqrt_eq_rpow]
   norm_cast
 
-theorem nnnorm_eq_of_L2 {β : ι → Type*} [∀ i, SeminormedAddCommGroup (β i)] (x : PiLp 2 β) :
+theorem nnnorm_eq_of_L2 (x : PiLp 2 β) :
     ‖x‖₊ = NNReal.sqrt (∑ i : ι, ‖x i‖₊ ^ 2) :=
-  -- Porting note: was `Subtype.ext`
   NNReal.eq <| by
     push_cast
     exact norm_eq_of_L2 x
@@ -594,20 +616,21 @@ theorem norm_sq_eq_of_L2 (β : ι → Type*) [∀ i, SeminormedAddCommGroup (β
     simpa only [NNReal.coe_sum] using congr_arg ((↑) : ℝ≥0 → ℝ) this
   rw [nnnorm_eq_of_L2, NNReal.sq_sqrt]
 
-theorem dist_eq_of_L2 {β : ι → Type*} [∀ i, SeminormedAddCommGroup (β i)] (x y : PiLp 2 β) :
+theorem dist_eq_of_L2 (x y : PiLp 2 β) :
     dist x y = √(∑ i, dist (x i) (y i) ^ 2) := by
   simp_rw [dist_eq_norm, norm_eq_of_L2, sub_apply]
 
-theorem nndist_eq_of_L2 {β : ι → Type*} [∀ i, SeminormedAddCommGroup (β i)] (x y : PiLp 2 β) :
+theorem nndist_eq_of_L2 (x y : PiLp 2 β) :
     nndist x y = NNReal.sqrt (∑ i, nndist (x i) (y i) ^ 2) :=
-  -- Porting note: was `Subtype.ext`
   NNReal.eq <| by
     push_cast
     exact dist_eq_of_L2 _ _
 
-theorem edist_eq_of_L2 {β : ι → Type*} [∀ i, SeminormedAddCommGroup (β i)] (x y : PiLp 2 β) :
+theorem edist_eq_of_L2 (x y : PiLp 2 β) :
     edist x y = (∑ i, edist (x i) (y i) ^ 2) ^ (1 / 2 : ℝ) := by simp [PiLp.edist_eq_sum]
 
+end L2
+
 instance instBoundedSMul [SeminormedRing 𝕜] [∀ i, SeminormedAddCommGroup (β i)]
     [∀ i, Module 𝕜 (β i)] [∀ i, BoundedSMul 𝕜 (β i)] :
     BoundedSMul 𝕜 (PiLp p β) :=

Mathlib/Analysis/Normed/Lp/ProdLp.lean

@@ -627,6 +627,36 @@ theorem prod_nnnorm_eq_sup (f : WithLp ∞ (α × β)) : ‖f‖₊ = ‖f.fst
 @[simp] theorem prod_norm_equiv_symm (f : α × β) : ‖(WithLp.equiv ⊤ _).symm f‖ = ‖f‖ :=
   (prod_norm_equiv _).symm
 
+section L1
+
+theorem prod_norm_eq_of_L1 (x : WithLp 1 (α × β)) :
+    ‖x‖ = ‖x.fst‖ + ‖x.snd‖ := by
+  simp [prod_norm_eq_add]
+
+theorem prod_nnnorm_eq_of_L1 (x : WithLp 1 (α × β)) :
+    ‖x‖₊ = ‖x.fst‖₊ + ‖x.snd‖₊ :=
+  NNReal.eq <| by
+    push_cast
+    exact prod_norm_eq_of_L1 x
+
+theorem prod_dist_eq_of_L1 (x y : WithLp 1 (α × β)) :
+    dist x y = dist x.fst y.fst + dist x.snd y.snd := by
+  simp_rw [dist_eq_norm, prod_norm_eq_of_L1, sub_fst, sub_snd]
+
+theorem prod_nndist_eq_of_L1 (x y : WithLp 1 (α × β)) :
+    nndist x y = nndist x.fst y.fst + nndist x.snd y.snd :=
+  NNReal.eq <| by
+    push_cast
+    exact prod_dist_eq_of_L1 _ _
+
+theorem prod_edist_eq_of_L1 (x y : WithLp 1 (α × β)) :
+    edist x y = edist x.fst y.fst + edist x.snd y.snd := by
+  simp [prod_edist_eq_add]
+
+end L1
+
+section L2
+
 theorem prod_norm_eq_of_L2 (x : WithLp 2 (α × β)) :
     ‖x‖ = √(‖x.fst‖ ^ 2 + ‖x.snd‖ ^ 2) := by
   rw [prod_norm_eq_of_nat 2 (by norm_cast) _, Real.sqrt_eq_rpow]
@@ -645,8 +675,7 @@ theorem prod_norm_sq_eq_of_L2 (x : WithLp 2 (α × β)) : ‖x‖ ^ 2 = ‖x.fst
 
 theorem prod_dist_eq_of_L2 (x y : WithLp 2 (α × β)) :
     dist x y = √(dist x.fst y.fst ^ 2 + dist x.snd y.snd ^ 2) := by
-  simp_rw [dist_eq_norm, prod_norm_eq_of_L2]
-  rfl
+  simp_rw [dist_eq_norm, prod_norm_eq_of_L2, sub_fst, sub_snd]
 
 theorem prod_nndist_eq_of_L2 (x y : WithLp 2 (α × β)) :
     nndist x y = NNReal.sqrt (nndist x.fst y.fst ^ 2 + nndist x.snd y.snd ^ 2) :=
@@ -658,6 +687,8 @@ theorem prod_edist_eq_of_L2 (x y : WithLp 2 (α × β)) :
     edist x y = (edist x.fst y.fst ^ 2 + edist x.snd y.snd ^ 2) ^ (1 / 2 : ℝ) := by
   simp [prod_edist_eq_add]
 
+end L2
+
 end norm_of
 
 variable [SeminormedAddCommGroup α] [SeminormedAddCommGroup β]