feat(topology/metric_space/holder): add holder_on_with (#8454)

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

src/analysis/special_functions/pow.lean

@@ -1692,4 +1692,12 @@ begin
     exact ennreal.continuous_inv.continuous_at.comp (continuous_at_rpow_const_of_pos z_pos) }
 end
 
+lemma tendsto_const_mul_rpow_nhds_zero_of_pos {c : ℝ≥0∞} (hc : c ≠ ∞) {y : ℝ} (hy : 0 < y) :
+  tendsto (λ x : ℝ≥0∞, c * x ^ y) (𝓝 0) (𝓝 0) :=
+begin
+  convert ennreal.tendsto.const_mul (ennreal.continuous_rpow_const.tendsto 0) _,
+  { simp [hy] },
+  { exact or.inr hc }
+end
+
 end ennreal

src/topology/metric_space/holder.lean

@@ -9,9 +9,15 @@ import analysis.special_functions.pow
 /-!
 # Hölder continuous functions
 
-In this file we define `f : X → Y` to be *Hölder continuous* with constant `C : ℝ≥0` and exponent
-`r : ℝ≥0`, if `edist (f x) (f y) ≤ C * edist x y ^ r` for all `x y : X`. We also prove some basic
-facts about this definition.
+In this file we define Hölder continuity on a set and on the whole space. We also prove some basic
+properties of Hölder continuous functions.
+
+## Main definitions
+
+* `holder_on_with`: `f : X → Y` is said to be *Hölder continuous* with constant `C : ℝ≥0` and
+  exponent `r : ℝ≥0` on a set `s`, if `edist (f x) (f y) ≤ C * edist x y ^ r` for all `x y ∈ s`;
+* `holder_with`: `f : X → Y` is said to be *Hölder continuous* with constant `C : ℝ≥0` and exponent
+  `r : ℝ≥0`, if `edist (f x) (f y) ≤ C * edist x y ^ r` for all `x y : X`.
 
 ## Implementation notes
 
@@ -28,7 +34,7 @@ Hölder continuity, Lipschitz continuity
 
 variables {X Y Z : Type*}
 
-open filter
+open filter set
 open_locale nnreal ennreal topological_space
 
 section emetric
@@ -40,12 +46,120 @@ variables [pseudo_emetric_space X] [pseudo_emetric_space Y] [pseudo_emetric_spac
 def holder_with (C r : ℝ≥0) (f : X → Y) : Prop :=
 ∀ x y, edist (f x) (f y) ≤ C * edist x y ^ (r : ℝ)
 
+/-- A function `f : X → Y` between two `pseudo_emeteric_space`s is Hölder continuous with constant
+`C : ℝ≥0` and exponent `r : ℝ≥0` on a set `s : set X`, if `edist (f x) (f y) ≤ C * edist x y ^ r`
+for all `x y ∈ s`. -/
+def holder_on_with (C r : ℝ≥0) (f : X → Y) (s : set X) : Prop :=
+∀ (x ∈ s) (y ∈ s), edist (f x) (f y) ≤ C * edist x y ^ (r : ℝ)
+
+@[simp] lemma holder_on_with_empty (C r : ℝ≥0) (f : X → Y) : holder_on_with C r f ∅ :=
+λ x hx, hx.elim
+
+@[simp] lemma holder_on_with_singleton (C r : ℝ≥0) (f : X → Y) (x : X) : holder_on_with C r f {x} :=
+by { rintro a (rfl : a = x) b (rfl : b = a), rw edist_self, exact zero_le _  }
+
+lemma set.subsingleton.holder_on_with {s : set X} (hs : s.subsingleton) (C r : ℝ≥0) (f : X → Y) :
+  holder_on_with C r f s :=
+hs.induction_on (holder_on_with_empty C r f) (holder_on_with_singleton C r f)
+
+lemma holder_on_with_univ {C r : ℝ≥0} {f : X → Y} :
+  holder_on_with C r f univ ↔ holder_with C r f :=
+by simp only [holder_on_with, holder_with, mem_univ, true_implies_iff]
+
+@[simp] lemma holder_on_with_one {C : ℝ≥0} {f : X → Y} {s : set X} :
+  holder_on_with C 1 f s ↔ lipschitz_on_with C f s :=
+by simp only [holder_on_with, lipschitz_on_with, nnreal.coe_one, ennreal.rpow_one]
+
+alias holder_on_with_one ↔ _ lipschitz_on_with.holder_on_with
+
 @[simp] lemma holder_with_one {C : ℝ≥0} {f : X → Y} :
   holder_with C 1 f ↔ lipschitz_with C f :=
-by simp only [holder_with, lipschitz_with, nnreal.coe_one, ennreal.rpow_one]
+holder_on_with_univ.symm.trans $ holder_on_with_one.trans lipschitz_on_univ
+
+alias holder_with_one ↔ _ lipschitz_with.holder_with
 
 lemma holder_with_id : holder_with 1 1 (id : X → X) :=
-holder_with_one.mpr lipschitz_with.id
+lipschitz_with.id.holder_with
+
+protected lemma holder_with.holder_on_with {C r : ℝ≥0} {f : X → Y} (h : holder_with C r f)
+  (s : set X) :
+  holder_on_with C r f s :=
+λ x _ y _, h x y
+
+namespace holder_on_with
+
+variables {C r : ℝ≥0} {f : X → Y} {s t : set X}
+
+lemma edist_le (h : holder_on_with C r f s) {x y : X} (hx : x ∈ s) (hy : y ∈ s) :
+  edist (f x) (f y) ≤ C * edist x y ^ (r : ℝ) :=
+h x hx y hy
+
+lemma edist_le_of_le (h : holder_on_with C r f s) {x y : X} (hx : x ∈ s) (hy : y ∈ s)
+  {d : ℝ≥0∞} (hd : edist x y ≤ d) :
+  edist (f x) (f y) ≤ C * d ^ (r : ℝ) :=
+(h.edist_le hx hy).trans (mul_le_mul_left' (ennreal.rpow_le_rpow hd r.coe_nonneg) _)
+
+lemma comp {Cg rg : ℝ≥0} {g : Y → Z} {t : set Y} (hg : holder_on_with Cg rg g t)
+  {Cf rf : ℝ≥0} {f : X → Y} (hf : holder_on_with Cf rf f s) (hst : maps_to f s t) :
+  holder_on_with (Cg * Cf ^ (rg : ℝ)) (rg * rf) (g ∘ f) s :=
+begin
+  intros x hx y hy,
+  rw [ennreal.coe_mul, mul_comm rg, nnreal.coe_mul, ennreal.rpow_mul, mul_assoc,
+    ← ennreal.coe_rpow_of_nonneg _ rg.coe_nonneg, ← ennreal.mul_rpow_of_nonneg _ _ rg.coe_nonneg],
+  exact hg.edist_le_of_le (hst hx) (hst hy) (hf.edist_le hx hy)
+end
+
+lemma comp_holder_with {Cg rg : ℝ≥0} {g : Y → Z} {t : set Y} (hg : holder_on_with Cg rg g t)
+  {Cf rf : ℝ≥0} {f : X → Y} (hf : holder_with Cf rf f) (ht : ∀ x, f x ∈ t) :
+  holder_with (Cg * Cf ^ (rg : ℝ)) (rg * rf) (g ∘ f) :=
+holder_on_with_univ.mp $ hg.comp (hf.holder_on_with univ) (λ x _, ht x)
+
+/-- A Hölder continuouf sunction is uniformly continuous -/
+protected lemma uniform_continuous_on (hf : holder_on_with C r f s) (h0 : 0 < r) :
+  uniform_continuous_on f s :=
+begin
+  refine emetric.uniform_continuous_on_iff.2 (λε εpos, _),
+  have : tendsto (λ d : ℝ≥0∞, (C : ℝ≥0∞) * d ^ (r : ℝ)) (𝓝 0) (𝓝 0),
+    from ennreal.tendsto_const_mul_rpow_nhds_zero_of_pos ennreal.coe_ne_top h0,
+  rcases ennreal.nhds_zero_basis.mem_iff.1 (this (gt_mem_nhds εpos)) with ⟨δ, δ0, H⟩,
+  exact ⟨δ, δ0, λ x y hx hy h, (hf.edist_le hx hy).trans_lt (H h)⟩,
+end
+
+protected lemma continuous_on (hf : holder_on_with C r f s) (h0 : 0 < r) : continuous_on f s :=
+(hf.uniform_continuous_on h0).continuous_on
+
+protected lemma mono (hf : holder_on_with C r f s) (ht : t ⊆ s) : holder_on_with C r f t :=
+λ x hx y hy, hf.edist_le (ht hx) (ht hy)
+
+lemma ediam_image_le_of_le (hf : holder_on_with C r f s) {d : ℝ≥0∞} (hd : emetric.diam s ≤ d) :
+  emetric.diam (f '' s) ≤ C * d ^ (r : ℝ) :=
+emetric.diam_image_le_iff.2 $ λ x hx y hy, hf.edist_le_of_le hx hy $
+  (emetric.edist_le_diam_of_mem hx hy).trans hd
+
+lemma ediam_image_le (hf : holder_on_with C r f s) :
+  emetric.diam (f '' s) ≤ C * emetric.diam s ^ (r : ℝ) :=
+hf.ediam_image_le_of_le le_rfl
+
+lemma ediam_image_le_of_subset (hf : holder_on_with C r f s) (ht : t ⊆ s) :
+  emetric.diam (f '' t) ≤ C * emetric.diam t ^ (r : ℝ) :=
+(hf.mono ht).ediam_image_le
+
+lemma ediam_image_le_of_subset_of_le (hf : holder_on_with C r f s) (ht : t ⊆ s) {d : ℝ≥0∞}
+  (hd : emetric.diam t ≤ d) :
+  emetric.diam (f '' t) ≤ C * d ^ (r : ℝ) :=
+(hf.mono ht).ediam_image_le_of_le hd
+
+lemma ediam_image_inter_le_of_le (hf : holder_on_with C r f s) {d : ℝ≥0∞}
+  (hd : emetric.diam t ≤ d) :
+  emetric.diam (f '' (t ∩ s)) ≤ C * d ^ (r : ℝ) :=
+hf.ediam_image_le_of_subset_of_le (inter_subset_right _ _) $
+  (emetric.diam_mono $ inter_subset_left _ _).trans hd
+
+lemma ediam_image_inter_le (hf : holder_on_with C r f s) (t : set X) :
+  emetric.diam (f '' (t ∩ s)) ≤ C * emetric.diam t ^ (r : ℝ) :=
+hf.ediam_image_inter_le_of_le le_rfl
+
+end holder_on_with
 
 namespace holder_with
 
@@ -57,29 +171,21 @@ h x y
 
 lemma edist_le_of_le (h : holder_with C r f) {x y : X} {d : ℝ≥0∞} (hd : edist x y ≤ d) :
   edist (f x) (f y) ≤ C * d ^ (r : ℝ) :=
-(h _ _).trans (mul_le_mul_left' (ennreal.rpow_le_rpow hd r.coe_nonneg) _)
+(h.holder_on_with univ).edist_le_of_le trivial trivial hd
 
 lemma comp {Cg rg : ℝ≥0} {g : Y → Z} (hg : holder_with Cg rg g)
   {Cf rf : ℝ≥0} {f : X → Y} (hf : holder_with Cf rf f) :
   holder_with (Cg * Cf ^ (rg : ℝ)) (rg * rf) (g ∘ f) :=
-begin
-  intros x y,
-  rw [ennreal.coe_mul, mul_comm rg, nnreal.coe_mul, ennreal.rpow_mul, mul_assoc,
-    ← ennreal.coe_rpow_of_nonneg _ rg.coe_nonneg, ← ennreal.mul_rpow_of_nonneg _ _ rg.coe_nonneg],
-  exact hg.edist_le_of_le (hf _ _)
-end
+(hg.holder_on_with univ).comp_holder_with hf (λ _, trivial)
+
+lemma comp_holder_on_with {Cg rg : ℝ≥0} {g : Y → Z} (hg : holder_with Cg rg g)
+  {Cf rf : ℝ≥0} {f : X → Y} {s : set X} (hf : holder_on_with Cf rf f s) :
+  holder_on_with (Cg * Cf ^ (rg : ℝ)) (rg * rf) (g ∘ f) s :=
+(hg.holder_on_with univ).comp hf (λ _ _, trivial)
 
 /-- A Hölder continuous function is uniformly continuous -/
 protected lemma uniform_continuous (hf : holder_with C r f) (h0 : 0 < r) : uniform_continuous f :=
-begin
-  refine emetric.uniform_continuous_iff.2 (λε εpos, _),
-  have : tendsto (λ d : ℝ≥0∞, (C : ℝ≥0∞) * d ^ (r : ℝ)) (𝓝 0) (𝓝 0),
-  { convert ennreal.tendsto.const_mul (ennreal.continuous_rpow_const.tendsto 0) _,
-    { simp [h0] },
-    { exact or.inr ennreal.coe_ne_top } },
-  rcases ennreal.nhds_zero_basis.mem_iff.1 (this (gt_mem_nhds εpos)) with ⟨δ, δ0, H⟩,
-  exact ⟨δ, δ0, λ x y h, (hf x y).trans_lt (H h)⟩,
-end
+uniform_continuous_on_univ.mp $ (hf.holder_on_with univ).uniform_continuous_on h0
 
 protected lemma continuous (hf : holder_with C r f) (h0 : 0 < r) : continuous f :=
 (hf.uniform_continuous h0).continuous

src/topology/metric_space/lipschitz.lean

@@ -91,6 +91,9 @@ section emetric
 variables [pseudo_emetric_space α] [pseudo_emetric_space β] [pseudo_emetric_space γ]
 variables {K : ℝ≥0} {f : α → β}
 
+protected lemma lipschitz_on_with (h : lipschitz_with K f) (s : set α) : lipschitz_on_with K f s :=
+λ x _ y _, h x y
+
 lemma edist_le_mul (h : lipschitz_with K f) (x y : α) : edist (f x) (f y) ≤ K * edist x y := h x y
 
 lemma edist_lt_top (hf : lipschitz_with K f) {x y : α} (h : edist x y < ⊤) :
@@ -100,10 +103,8 @@ lt_of_le_of_lt (hf x y) $ ennreal.mul_lt_top ennreal.coe_lt_top h
 lemma mul_edist_le (h : lipschitz_with K f) (x y : α) :
   (K⁻¹ : ℝ≥0∞) * edist (f x) (f y) ≤ edist x y :=
 begin
-  have := h x y,
-  rw [mul_comm] at this,
-  replace := ennreal.div_le_of_le_mul this,
-  rwa [div_eq_mul_inv, mul_comm] at this
+  rw [mul_comm, ← div_eq_mul_inv],
+  exact ennreal.div_le_of_le_mul' (h x y)
 end
 
 protected lemma of_edist_le (h : ∀ x y, edist (f x) (f y) ≤ edist x y) :

src/topology/uniform_space/basic.lean

@@ -872,6 +872,10 @@ theorem uniform_continuous_iff_eventually [uniform_space β] {f : α → β} :
   uniform_continuous f ↔ ∀ r ∈ 𝓤 β, ∀ᶠ (x : α × α) in 𝓤 α, (f x.1, f x.2) ∈ r :=
 iff.rfl
 
+theorem uniform_continuous_on_univ [uniform_space β] {f : α → β} :
+  uniform_continuous_on f univ ↔ uniform_continuous f :=
+by rw [uniform_continuous_on, uniform_continuous, univ_prod_univ, principal_univ, inf_top_eq]
+
 lemma uniform_continuous_of_const [uniform_space β] {c : α → β} (h : ∀a b, c a = c b) :
   uniform_continuous c :=
 have (λ (x : α × α), (c (x.fst), c (x.snd))) ⁻¹' id_rel = univ, from