feat(Holder): basic lemmas for HolderWith (#16411)

Co-authored-by: Kexing Ying <kexing.ying@epfl.ch>

Mathlib/Topology/MetricSpace/Holder.lean

@@ -190,11 +190,23 @@ theorem ediam_image_le (hf : HolderWith C r f) (s : Set X) :
   EMetric.diam_image_le_iff.2 fun _ hx _ hy =>
     hf.edist_le_of_le <| EMetric.edist_le_diam_of_mem hx hy
 
+lemma const {y : Y} :
+    HolderWith C r (Function.const X y) := fun x₁ x₂ => by
+  simp only [Function.const_apply, edist_self, zero_le]
+
+lemma zero [Zero Y] : HolderWith C r (0 : X → Y) := .const
+
+lemma of_isEmpty [IsEmpty X] : HolderWith C r f := isEmptyElim
+
+lemma mono {C' : ℝ≥0} (hf : HolderWith C r f) (h : C ≤ C') :
+    HolderWith C' r f :=
+  fun x₁ x₂ ↦ (hf x₁ x₂).trans (mul_right_mono (coe_le_coe.2 h))
+
 end HolderWith
 
 end Emetric
 
-section Metric
+section PseudoMetric
 
 variable [PseudoMetricSpace X] [PseudoMetricSpace Y] {C r : ℝ≥0} {f : X → Y}
 
@@ -223,4 +235,40 @@ theorem dist_le (hf : HolderWith C r f) (x y : X) : dist (f x) (f y) ≤ C * dis
 
 end HolderWith
 
+end PseudoMetric
+
+section Metric
+
+variable [PseudoMetricSpace X] [MetricSpace Y] {C r : ℝ≥0} {f : X → Y}
+
+@[simp]
+lemma holderWith_zero_iff : HolderWith 0 r f ↔ ∀ x₁ x₂, f x₁ = f x₂ := by
+  refine ⟨fun h x₁ x₂ => ?_, fun h x₁ x₂ => h x₁ x₂ ▸ ?_⟩
+  · specialize h x₁ x₂
+    simp [ENNReal.coe_zero, zero_mul, nonpos_iff_eq_zero, edist_eq_zero] at h
+    assumption
+  · simp only [edist_self, ENNReal.coe_zero, zero_mul, le_refl]
+
 end Metric
+
+section SeminormedAddCommGroup
+
+variable [PseudoMetricSpace X] [SeminormedAddCommGroup Y] {C C' r : ℝ≥0} {f g : X → Y}
+
+namespace HolderWith
+
+lemma add (hf : HolderWith C r f) (hg : HolderWith C' r g) :
+    HolderWith (C + C') r (f + g) := fun x₁ x₂ => by
+  refine le_trans (edist_add_add_le _ _ _ _) <| le_trans (add_le_add (hf x₁ x₂) (hg x₁ x₂)) ?_
+  rw [coe_add, add_mul]
+
+lemma smul {α} [NormedDivisionRing α] [Module α Y] [BoundedSMul α Y] (a : α)
+    (hf : HolderWith C r f) : HolderWith (C * ‖a‖₊) r (a • f) := fun x₁ x₂ => by
+  rw [Pi.smul_apply, coe_mul, Pi.smul_apply, edist_smul₀, mul_comm (C : ℝ≥0∞),
+    ENNReal.smul_def, smul_eq_mul, mul_assoc]
+  gcongr
+  exact hf x₁ x₂
+
+end HolderWith
+
+end SeminormedAddCommGroup