From 0827f3a6297727b5942e4c3e920a4f2e479b64fb Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Sat, 31 Jul 2021 20:17:15 +0000 Subject: [PATCH] feat(topology/metric_space/holder): add `holder_on_with` (#8454) Co-authored-by: sgouezel --- src/analysis/special_functions/pow.lean | 8 ++ src/topology/metric_space/holder.lean | 150 +++++++++++++++++++---- src/topology/metric_space/lipschitz.lean | 9 +- src/topology/uniform_space/basic.lean | 4 + 4 files changed, 145 insertions(+), 26 deletions(-) diff --git a/src/analysis/special_functions/pow.lean b/src/analysis/special_functions/pow.lean index 99b43511414ea..84707b442a974 100644 --- a/src/analysis/special_functions/pow.lean +++ b/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 diff --git a/src/topology/metric_space/holder.lean b/src/topology/metric_space/holder.lean index 724702a921e6d..81fa9f35c98cb 100644 --- a/src/topology/metric_space/holder.lean +++ b/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 diff --git a/src/topology/metric_space/lipschitz.lean b/src/topology/metric_space/lipschitz.lean index b291a2c47f960..f9f9f13f432ad 100644 --- a/src/topology/metric_space/lipschitz.lean +++ b/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) : diff --git a/src/topology/uniform_space/basic.lean b/src/topology/uniform_space/basic.lean index 733ea8c3e668a..1477f9b7b8e96 100644 --- a/src/topology/uniform_space/basic.lean +++ b/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