feat: change definition for p = 0 in piLp (#8290)

The current definition of the distance in `piLp` uses the distance for `p > 0`, but avoids it for `p = 0`. We change the definition for `p = 0` to also have it in terms of the distance, to make sure it is reasonable even when one uses non-Hausdorff spaces.This matches what has been done for `prodLp` in #6136.

Author: sgouezel

Mathlib/Analysis/NormedSpace/LpEquiv.lean

@@ -74,7 +74,7 @@ theorem coe_equiv_lpPiLp_symm (f : PiLp p E) : (Equiv.lpPiLp.symm f : ∀ i, E i
 
 theorem equiv_lpPiLp_norm (f : lp E p) : ‖Equiv.lpPiLp f‖ = ‖f‖ := by
   rcases p.trichotomy with (rfl | rfl | h)
-  · rw [PiLp.norm_eq_card, lp.norm_eq_card_dsupport]
+  · simp [Equiv.lpPiLp, PiLp.norm_eq_card, lp.norm_eq_card_dsupport]
   · rw [PiLp.norm_eq_ciSup, lp.norm_eq_ciSup]; rfl
   · rw [PiLp.norm_eq_sum h, lp.norm_eq_tsum_rpow h, tsum_fintype]; rfl
 #align equiv_lp_pi_Lp_norm equiv_lpPiLp_norm

Mathlib/Analysis/NormedSpace/PiLp.lean

@@ -19,8 +19,8 @@ is given by
 $$
 d(x, y) = \left(\sum d(x_i, y_i)^p\right)^{1/p}.
 $$,
-whereas for `p = 0` it is the cardinality of the set ${ i | x_i ≠ y_i}$. For `p = ∞` the distance
-is the supremum of the distances.
+whereas for `p = 0` it is the cardinality of the set ${i | d (x_i, y_i) ≠ 0}$. For `p = ∞` the
+distance is the supremum of the distances.
 
 We give instances of this construction for emetric spaces, metric spaces, normed groups and normed
 spaces.
@@ -129,13 +129,14 @@ satisfying a relaxed triangle inequality. The terminology for this varies throug
 literature, but it is sometimes called a *quasi-metric* or *semi-metric*. -/
 instance : EDist (PiLp p β) where
   edist f g :=
-    if p = 0 then { i | f i ≠ g i }.toFinite.toFinset.card
+    if p = 0 then {i | edist (f i) (g i) ≠ 0}.toFinite.toFinset.card
     else
       if p = ∞ then ⨆ i, edist (f i) (g i) else (∑ i, edist (f i) (g i) ^ p.toReal) ^ (1 / p.toReal)
 
 variable {β}
 
-theorem edist_eq_card (f g : PiLp 0 β) : edist f g = { i | f i ≠ g i }.toFinite.toFinset.card :=
+theorem edist_eq_card (f g : PiLp 0 β) :
+    edist f g = {i | edist (f i) (g i) ≠ 0}.toFinite.toFinset.card :=
   if_pos rfl
 #align pi_Lp.edist_eq_card PiLp.edist_eq_card
 
@@ -170,7 +171,7 @@ protected theorem edist_self (f : PiLp p β) : edist f f = 0 := by
 from `pi_Lp.pseudo_emetric_space` so it can be used also for `p < 1`. -/
 protected theorem edist_comm (f g : PiLp p β) : edist f g = edist g f := by
   rcases p.trichotomy with (rfl | rfl | h)
-  · simp only [edist_eq_card, eq_comm, Ne.def]
+  · simp only [edist_eq_card, edist_comm]
   · simp only [edist_eq_iSup, edist_comm]
   · simp only [edist_eq_sum h, edist_comm]
 #align pi_Lp.edist_comm PiLp.edist_comm
@@ -190,13 +191,14 @@ satisfying a relaxed triangle inequality. The terminology for this varies throug
 literature, but it is sometimes called a *quasi-metric* or *semi-metric*. -/
 instance : Dist (PiLp p α) where
   dist f g :=
-    if _hp : p = 0 then { i | f i ≠ g i }.toFinite.toFinset.card
+    if p = 0 then {i | dist (f i) (g i) ≠ 0}.toFinite.toFinset.card
     else
       if p = ∞ then ⨆ i, dist (f i) (g i) else (∑ i, dist (f i) (g i) ^ p.toReal) ^ (1 / p.toReal)
 
 variable {α}
 
-theorem dist_eq_card (f g : PiLp 0 α) : dist f g = { i | f i ≠ g i }.toFinite.toFinset.card :=
+theorem dist_eq_card (f g : PiLp 0 α) :
+    dist f g = {i | dist (f i) (g i) ≠ 0}.toFinite.toFinset.card :=
   if_pos rfl
 #align pi_Lp.dist_eq_card PiLp.dist_eq_card
 
@@ -215,7 +217,7 @@ end Dist
 
 section Norm
 
-variable [∀ i, Norm (β i)] [∀ i, Zero (β i)]
+variable [∀ i, Norm (β i)]
 
 /-- Endowing the space `PiLp p β` with the `L^p` norm. We register this instance
 separate from `PiLp.seminormedAddCommGroup` since the latter requires the type class hypothesis
@@ -225,13 +227,13 @@ Registering this separately allows for a future norm-like structure on `PiLp p 
 satisfying a relaxed triangle inequality. These are called *quasi-norms*. -/
 instance hasNorm : Norm (PiLp p β) where
   norm f :=
-    if _hp : p = 0 then { i | f i ≠ 0 }.toFinite.toFinset.card
+    if p = 0 then {i | ‖f i‖ ≠ 0}.toFinite.toFinset.card
     else if p = ∞ then ⨆ i, ‖f i‖ else (∑ i, ‖f i‖ ^ p.toReal) ^ (1 / p.toReal)
 #align pi_Lp.has_norm PiLp.hasNorm
 
 variable {p β}
 
-theorem norm_eq_card (f : PiLp 0 β) : ‖f‖ = { i | f i ≠ 0 }.toFinite.toFinset.card :=
+theorem norm_eq_card (f : PiLp 0 β) : ‖f‖ = {i | ‖f i‖ ≠ 0}.toFinite.toFinset.card :=
   if_pos rfl
 #align pi_Lp.norm_eq_card PiLp.norm_eq_card