feat(topology/metric_space/basic): Distance between constant functions (

#16958)

The distance between `λ _, a` and `λ _, b` is at most the distance between `a` and `b`.

Also rename `pi_norm_le_iff` to `pi_norm_le_iff_of_nonneg`.

src/analysis/asymptotics/asymptotics.lean

@@ -1640,7 +1640,7 @@ theorem is_O_with_pi {ι : Type*} [fintype ι] {E' : ι → Type*} [Π i, normed
   {f : α → Π i, E' i} {C : ℝ} (hC : 0 ≤ C) :
   is_O_with C l f g' ↔ ∀ i, is_O_with C l (λ x, f x i) g' :=
 have ∀ x, 0 ≤ C * ∥g' x∥, from λ x, mul_nonneg hC (norm_nonneg _),
-by simp only [is_O_with_iff, pi_norm_le_iff (this _), eventually_all]
+by simp only [is_O_with_iff, pi_norm_le_iff_of_nonneg (this _), eventually_all]
 
 @[simp] theorem is_O_pi {ι : Type*} [fintype ι] {E' : ι → Type*} [Π i, normed_add_comm_group (E' i)]
   {f : α → Π i, E' i} :

src/analysis/matrix.lean

@@ -66,7 +66,7 @@ local attribute [instance] matrix.seminormed_add_comm_group
 
 lemma norm_le_iff {r : ℝ} (hr : 0 ≤ r) {A : matrix m n α} :
   ∥A∥ ≤ r ↔ ∀ i j, ∥A i j∥ ≤ r :=
-by simp [pi_norm_le_iff hr]
+by simp [pi_norm_le_iff_of_nonneg hr]
 
 lemma nnnorm_le_iff {r : ℝ≥0} {A : matrix m n α} :
   ∥A∥₊ ≤ r ↔ ∀ i j, ∥A i j∥₊ ≤ r :=

src/analysis/normed/group/basic.lean

@@ -1512,13 +1512,23 @@ subtype.eta _ _
 
 /-- The seminorm of an element in a product space is `≤ r` if and only if the norm of each
 component is. -/
-@[to_additive pi_norm_le_iff "The seminorm of an element in a product space is `≤ r` if and only if
-the norm of each component is."]
-lemma pi_norm_le_iff' (hr : 0 ≤ r) : ∥x∥ ≤ r ↔ ∀ i, ∥x i∥ ≤ r :=
+@[to_additive pi_norm_le_iff_of_nonneg "The seminorm of an element in a product space is `≤ r` if
+and only if the norm of each component is."]
+lemma pi_norm_le_iff_of_nonneg' (hr : 0 ≤ r) : ∥x∥ ≤ r ↔ ∀ i, ∥x i∥ ≤ r :=
 by simp only [←dist_one_right, dist_pi_le_iff hr, pi.one_apply]
 
 @[to_additive pi_nnnorm_le_iff]
-lemma pi_nnnorm_le_iff' {r : ℝ≥0} : ∥x∥₊ ≤ r ↔ ∀ i, ∥x i∥₊ ≤ r := pi_norm_le_iff' r.coe_nonneg
+lemma pi_nnnorm_le_iff' {r : ℝ≥0} : ∥x∥₊ ≤ r ↔ ∀ i, ∥x i∥₊ ≤ r :=
+pi_norm_le_iff_of_nonneg' r.coe_nonneg
+
+@[to_additive pi_norm_le_iff_of_nonempty]
+lemma pi_norm_le_iff_of_nonempty' [nonempty ι] : ∥f∥ ≤ r ↔ ∀ b, ∥f b∥ ≤ r :=
+begin
+  by_cases hr : 0 ≤ r,
+  { exact pi_norm_le_iff_of_nonneg' hr },
+  { exact iff_of_false (λ h, hr $ (norm_nonneg' _).trans h)
+      (λ h, hr $ (norm_nonneg' _).trans $ h $ classical.arbitrary _) }
+end
 
 /-- The seminorm of an element in a product space is `< r` if and only if the norm of each
 component is. -/
@@ -1531,11 +1541,19 @@ by simp only [←dist_one_right, dist_pi_lt_iff hr, pi.one_apply]
 lemma pi_nnnorm_lt_iff' {r : ℝ≥0} (hr : 0 < r) : ∥x∥₊ < r ↔ ∀ i, ∥x i∥₊ < r := pi_norm_lt_iff' hr
 
 @[to_additive norm_le_pi_norm]
-lemma norm_le_pi_norm' (i : ι) : ∥f i∥ ≤ ∥f∥ := (pi_norm_le_iff' $ norm_nonneg' _).1 le_rfl i
+lemma norm_le_pi_norm' (i : ι) : ∥f i∥ ≤ ∥f∥ :=
+(pi_norm_le_iff_of_nonneg' $ norm_nonneg' _).1 le_rfl i
 
 @[to_additive nnnorm_le_pi_nnnorm]
 lemma nnnorm_le_pi_nnnorm' (i : ι) : ∥f i∥₊ ≤ ∥f∥₊ := norm_le_pi_norm' _ i
 
+@[to_additive pi_norm_const_le]
+lemma pi_norm_const_le' (a : E) : ∥(λ _ : ι, a)∥ ≤ ∥a∥ :=
+(pi_norm_le_iff_of_nonneg' $ norm_nonneg' _).2 $ λ _, le_rfl
+
+@[to_additive pi_nnnorm_const_le]
+lemma pi_nnnorm_const_le' (a : E) : ∥(λ _ : ι, a)∥₊ ≤ ∥a∥₊ := pi_norm_const_le' _
+
 @[simp, to_additive pi_norm_const]
 lemma pi_norm_const' [nonempty ι] (a : E) : ∥(λ i : ι, a)∥ = ∥a∥ :=
 by simpa only [←dist_one_right] using dist_pi_const a 1

src/analysis/normed_space/finite_dimension.lean

@@ -671,7 +671,7 @@ begin
   intros N g hg,
   have : ∀ i, summable (λ x, ∥g x i∥) := λ i, (pi.summable.1 hg i).abs,
   refine summable_of_norm_bounded _ (summable_sum (λ i (hi : i ∈ finset.univ), this i)) (λ x, _),
-  rw [norm_norm, pi_norm_le_iff],
+  rw [norm_norm, pi_norm_le_iff_of_nonneg],
   { refine λ i, finset.single_le_sum (λ i hi, _) (finset.mem_univ i),
     exact norm_nonneg (g x i) },
   { exact finset.sum_nonneg (λ _ _, norm_nonneg _) }

src/analysis/normed_space/multilinear.lean

@@ -430,10 +430,10 @@ begin
   apply le_antisymm,
   { refine (op_norm_le_bound _ (norm_nonneg f) (λ m, _)),
     dsimp,
-    rw pi_norm_le_iff,
+    rw pi_norm_le_iff_of_nonneg,
     exacts [λ i, (f i).le_of_op_norm_le m (norm_le_pi_norm f i),
       mul_nonneg (norm_nonneg f) (prod_nonneg $ λ _ _, norm_nonneg _)] },
-  { refine (pi_norm_le_iff (norm_nonneg _)).2 (λ i, _),
+  { refine (pi_norm_le_iff_of_nonneg (norm_nonneg _)).2 (λ i, _),
     refine (op_norm_le_bound _ (norm_nonneg _) (λ m, _)),
     refine le_trans _ ((pi f).le_op_norm m),
     convert norm_le_pi_norm (λ j, f j m) i }

src/analysis/normed_space/star/matrix.lean

@@ -59,7 +59,7 @@ local attribute [instance] matrix.normed_add_comm_group
 lemma entrywise_sup_norm_bound_of_unitary {U : matrix n n 𝕜} (hU : U ∈ matrix.unitary_group n 𝕜) :
   ∥ U ∥ ≤ 1 :=
 begin
-  simp_rw pi_norm_le_iff zero_le_one,
+  simp_rw pi_norm_le_iff_of_nonneg zero_le_one,
   intros i j,
   exact entry_norm_bound_of_unitary hU _ _
 end

src/measure_theory/covering/besicovitch_vector_space.lean

@@ -234,13 +234,13 @@ begin
         exists_seq_strict_anti_tendsto (0 : ℝ),
     have A : ∀ n, F (u n) ∈ closed_ball (0 : fin N → E) 2,
     { assume n,
-      simp only [pi_norm_le_iff zero_le_two, mem_closed_ball, dist_zero_right,
+      simp only [pi_norm_le_iff_of_nonneg zero_le_two, mem_closed_ball, dist_zero_right,
                  (hF (u n) (zero_lt_u n)).left, forall_const], },
     obtain ⟨f, fmem, φ, φ_mono, hf⟩ : ∃ (f ∈ closed_ball (0 : fin N → E) 2) (φ : ℕ → ℕ),
       strict_mono φ ∧ tendsto ((F ∘ u) ∘ φ) at_top (𝓝 f) :=
         is_compact.tendsto_subseq (is_compact_closed_ball _ _) A,
     refine ⟨f, λ i, _, λ i j hij, _⟩,
-    { simp only [pi_norm_le_iff zero_le_two, mem_closed_ball, dist_zero_right] at fmem,
+    { simp only [pi_norm_le_iff_of_nonneg zero_le_two, mem_closed_ball, dist_zero_right] at fmem,
       exact fmem i },
     { have A : tendsto (λ n, ∥F (u (φ n)) i - F (u (φ n)) j∥) at_top (𝓝 (∥f i - f j∥)) :=
         ((hf.apply i).sub (hf.apply j)).norm,

src/topology/metric_space/basic.lean

@@ -1824,12 +1824,6 @@ nnreal.eq rfl
 lemma dist_pi_def (f g : Πb, π b) :
   dist f g = (sup univ (λb, nndist (f b) (g b)) : ℝ≥0) := rfl
 
-@[simp] lemma dist_pi_const [nonempty β] (a b : α) : dist (λ x : β, a) (λ _, b) = dist a b :=
-by simpa only [dist_edist] using congr_arg ennreal.to_real (edist_pi_const a b)
-
-@[simp] lemma nndist_pi_const [nonempty β] (a b : α) :
-  nndist (λ x : β, a) (λ _, b) = nndist a b := nnreal.eq $ dist_pi_const a b
-
 lemma nndist_pi_le_iff {f g : Πb, π b} {r : ℝ≥0} :
   nndist f g ≤ r ↔ ∀b, nndist (f b) (g b) ≤ r :=
 by simp [nndist_pi_def]
@@ -1848,6 +1842,27 @@ begin
   exact nndist_pi_le_iff
 end
 
+lemma dist_pi_le_iff' [nonempty β] {f g : Π b, π b} {r : ℝ} :
+  dist f g ≤ r ↔ ∀ b, dist (f b) (g b) ≤ r :=
+begin
+  by_cases hr : 0 ≤ r,
+  { exact dist_pi_le_iff hr },
+  { exact iff_of_false (λ h, hr $ dist_nonneg.trans h)
+      (λ h, hr $ dist_nonneg.trans $ h $ classical.arbitrary _) }
+end
+
+lemma dist_pi_const_le (a b : α) : dist (λ _ : β, a) (λ _, b) ≤ dist a b :=
+(dist_pi_le_iff dist_nonneg).2 $ λ _, le_rfl
+
+lemma nndist_pi_const_le (a b : α) : nndist (λ _ : β, a) (λ _, b) ≤ nndist a b :=
+nndist_pi_le_iff.2 $ λ _, le_rfl
+
+@[simp] lemma dist_pi_const [nonempty β] (a b : α) : dist (λ x : β, a) (λ _, b) = dist a b :=
+by simpa only [dist_edist] using congr_arg ennreal.to_real (edist_pi_const a b)
+
+@[simp] lemma nndist_pi_const [nonempty β] (a b : α) :
+  nndist (λ x : β, a) (λ _, b) = nndist a b := nnreal.eq $ dist_pi_const a b
+
 lemma nndist_le_pi_nndist (f g : Πb, π b) (b : β) : nndist (f b) (g b) ≤ nndist f g :=
 by { rw [nndist_pi_def], exact finset.le_sup (finset.mem_univ b) }
 

src/topology/metric_space/emetric_space.lean

@@ -478,10 +478,6 @@ instance pseudo_emetric_space_pi [∀b, pseudo_emetric_space (π b)] :
 lemma edist_pi_def [Π b, pseudo_emetric_space (π b)] (f g : Π b, π b) :
   edist f g = finset.sup univ (λb, edist (f b) (g b)) := rfl
 
-@[simp]
-lemma edist_pi_const [nonempty β] (a b : α) :
-  edist (λ x : β, a) (λ _, b) = edist a b := finset.sup_const univ_nonempty (edist a b)
-
 lemma edist_le_pi_edist [Π b, pseudo_emetric_space (π b)] (f g : Π b, π b) (b : β) :
   edist (f b) (g b) ≤ edist f g :=
 finset.le_sup (finset.mem_univ b)
@@ -490,6 +486,12 @@ lemma edist_pi_le_iff [Π b, pseudo_emetric_space (π b)] {f g : Π b, π b} {d
   edist f g ≤ d ↔ ∀ b, edist (f b) (g b) ≤ d :=
 finset.sup_le_iff.trans $ by simp only [finset.mem_univ, forall_const]
 
+lemma edist_pi_const_le (a b : α) : edist (λ _ : β, a) (λ _, b) ≤ edist a b :=
+edist_pi_le_iff.2 $ λ _, le_rfl
+
+@[simp] lemma edist_pi_const [nonempty β] (a b : α) : edist (λ x : β, a) (λ _, b) = edist a b :=
+finset.sup_const univ_nonempty (edist a b)
+
 end pi
 
 namespace emetric