Exact source: Mathlib/Topology/MetricSpace/Lipschitz.lean
Pinned GitHub source · Raw UTF-8 source
Back to One boundary extension with all five analytic properties
1/-2Copyright (c) 2018 Rohan Mitta. All rights reserved.3Released under Apache 2.0 license as described in the file LICENSE.4Authors: Rohan Mitta, Kevin Buzzard, Alistair Tucker, Johannes Hölzl, Yury Kudryashov5-/6module78public import Mathlib.Order.Interval.Set.ProjIcc9public import Mathlib.Topology.Bornology.Hom10public import Mathlib.Topology.EMetricSpace.Lipschitz11public import Mathlib.Topology.Maps.Proper.Basic12public import Mathlib.Topology.MetricSpace.Basic13public import Mathlib.Topology.MetricSpace.Bounded1415/-!16# Lipschitz continuous functions1718A map `f : α → β` between two (extended) metric spaces is called *Lipschitz continuous*19with constant `K ≥ 0` if for all `x, y` we have `edist (f x) (f y) ≤ K * edist x y`.20For a metric space, the latter inequality is equivalent to `dist (f x) (f y) ≤ K * dist x y`.21There is also a version asserting this inequality only for `x` and `y` in some set `s`.22Finally, `f : α → β` is called *locally Lipschitz continuous* if each `x : α` has a neighbourhood23on which `f` is Lipschitz continuous (with some constant).2425In this file we specialize various facts about Lipschitz continuous maps26to the case of (pseudo) metric spaces.2728## Implementation notes2930The parameter `K` has type `ℝ≥0`. This way we avoid conjunction in the definition and have31coercions both to `ℝ` and `ℝ≥0∞`. Constructors whose names end with `'` take `K : ℝ` as an32argument, and return `LipschitzWith (Real.toNNReal K) f`.33-/3435@[expose] public section3637assert_not_exists Module.Basis Ideal ContinuousMul3839universe u v w x4041open Filter Function Set Topology NNReal ENNReal Bornology4243variable {α : Type u} {β : Type v} {γ : Type w} {ι : Type x}4445theorem lipschitzWith_iff_dist_le_mul [PseudoMetricSpace α] [PseudoMetricSpace β] {K : ℝ≥0}46 {f : α → β} : LipschitzWith K f ↔ ∀ x y, dist (f x) (f y) ≤ K * dist x y := by47 simp only [LipschitzWith, edist_nndist, dist_nndist]48 norm_cast4950alias ⟨LipschitzWith.dist_le_mul, LipschitzWith.of_dist_le_mul⟩ := lipschitzWith_iff_dist_le_mul5152theorem lipschitzOnWith_iff_dist_le_mul [PseudoMetricSpace α] [PseudoMetricSpace β] {K : ℝ≥0}53 {s : Set α} {f : α → β} :54 LipschitzOnWith K f s ↔ ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ K * dist x y := by55 simp only [LipschitzOnWith, edist_nndist, dist_nndist]56 norm_cast5758alias ⟨LipschitzOnWith.dist_le_mul, LipschitzOnWith.of_dist_le_mul⟩ :=59 lipschitzOnWith_iff_dist_le_mul6061namespace LipschitzWith6263section Metric6465variable [PseudoMetricSpace α] [PseudoMetricSpace β] [PseudoMetricSpace γ] {K : ℝ≥0} {f : α → β}66 {x y : α} {r : ℝ}6768protected theorem of_dist_le' {K : ℝ} (h : ∀ x y, dist (f x) (f y) ≤ K * dist x y) :69 LipschitzWith (Real.toNNReal K) f :=70 of_dist_le_mul fun x y =>71 le_trans (h x y) <| by gcongr; apply Real.le_coe_toNNReal7273protected theorem mk_one (h : ∀ x y, dist (f x) (f y) ≤ dist x y) : LipschitzWith 1 f :=74 of_dist_le_mul <| by simpa only [NNReal.coe_one, one_mul] using h7576/-- For functions to `ℝ`, it suffices to prove `f x ≤ f y + K * dist x y`; this version77doesn't assume `0≤K`. -/78protected theorem of_le_add_mul' {f : α → ℝ} (K : ℝ) (h : ∀ x y, f x ≤ f y + K * dist x y) :79 LipschitzWith (Real.toNNReal K) f :=80 have I : ∀ x y, f x - f y ≤ K * dist x y := fun x y => sub_le_iff_le_add'.2 (h x y)81 LipschitzWith.of_dist_le' fun x y => abs_sub_le_iff.2 ⟨I x y, dist_comm y x ▸ I y x⟩8283/-- For functions to `ℝ`, it suffices to prove `f x ≤ f y + K * dist x y`; this version84assumes `0≤K`. -/85protected theorem of_le_add_mul {f : α → ℝ} (K : ℝ≥0) (h : ∀ x y, f x ≤ f y + K * dist x y) :86 LipschitzWith K f := by simpa only [Real.toNNReal_coe] using LipschitzWith.of_le_add_mul' K h8788protected theorem of_le_add {f : α → ℝ} (h : ∀ x y, f x ≤ f y + dist x y) : LipschitzWith 1 f :=89 LipschitzWith.of_le_add_mul 1 <| by simpa only [NNReal.coe_one, one_mul]9091protected theorem le_add_mul {f : α → ℝ} {K : ℝ≥0} (h : LipschitzWith K f) (x y) :92 f x ≤ f y + K * dist x y :=93 sub_le_iff_le_add'.1 <| le_trans (le_abs_self _) <| h.dist_le_mul x y9495protected theorem iff_le_add_mul {f : α → ℝ} {K : ℝ≥0} :96 LipschitzWith K f ↔ ∀ x y, f x ≤ f y + K * dist x y :=97 ⟨LipschitzWith.le_add_mul, LipschitzWith.of_le_add_mul K⟩9899theorem nndist_le (hf : LipschitzWith K f) (x y : α) : nndist (f x) (f y) ≤ K * nndist x y :=100 hf.dist_le_mul x y101102theorem dist_le_mul_of_le (hf : LipschitzWith K f) (hr : dist x y ≤ r) : dist (f x) (f y) ≤ K * r :=103 (hf.dist_le_mul x y).trans <| by gcongr104105theorem mapsTo_closedBall (hf : LipschitzWith K f) (x : α) (r : ℝ) :106 MapsTo f (Metric.closedBall x r) (Metric.closedBall (f x) (K * r)) := fun _y hy =>107 hf.dist_le_mul_of_le hy108109theorem dist_lt_mul_of_lt (hf : LipschitzWith K f) (hK : K ≠ 0) (hr : dist x y < r) :110 dist (f x) (f y) < K * r :=111 (hf.dist_le_mul x y).trans_lt <| by gcongr112113theorem mapsTo_ball (hf : LipschitzWith K f) (hK : K ≠ 0) (x : α) (r : ℝ) :114 MapsTo f (Metric.ball x r) (Metric.ball (f x) (K * r)) := fun _y hy =>115 hf.dist_lt_mul_of_lt hK hy116117/-- A Lipschitz continuous map is a locally bounded map. -/118def toLocallyBoundedMap (f : α → β) (hf : LipschitzWith K f) : LocallyBoundedMap α β :=119 LocallyBoundedMap.ofMapBounded f fun _s hs =>120 let ⟨C, hC⟩ := Metric.isBounded_iff.1 hs121 Metric.isBounded_iff.2 ⟨K * C, forall_mem_image.2 fun _x hx => forall_mem_image.2 fun _y hy =>122 hf.dist_le_mul_of_le (hC hx hy)⟩123124@[simp]125theorem coe_toLocallyBoundedMap (hf : LipschitzWith K f) : ⇑(hf.toLocallyBoundedMap f) = f :=126 rfl127128theorem comap_cobounded_le (hf : LipschitzWith K f) :129 comap f (Bornology.cobounded β) ≤ Bornology.cobounded α :=130 (hf.toLocallyBoundedMap f).2131132/-- The image of a bounded set under a Lipschitz map is bounded. -/133theorem isBounded_image (hf : LipschitzWith K f) {s : Set α} (hs : IsBounded s) :134 IsBounded (f '' s) :=135 hs.image (toLocallyBoundedMap f hf)136137theorem diam_image_le (hf : LipschitzWith K f) (s : Set α) (hs : IsBounded s) :138 Metric.diam (f '' s) ≤ K * Metric.diam s :=139 Metric.diam_le_of_forall_dist_le (mul_nonneg K.coe_nonneg Metric.diam_nonneg) <|140 forall_mem_image.2 fun _x hx =>141 forall_mem_image.2 fun _y hy => hf.dist_le_mul_of_le <| Metric.dist_le_diam_of_mem hs hx hy142143protected theorem dist_left (y : α) : LipschitzWith 1 (dist · y) :=144 LipschitzWith.mk_one fun _ _ => dist_dist_dist_le_left _ _ _145146protected theorem dist_right (x : α) : LipschitzWith 1 (dist x) :=147 LipschitzWith.of_le_add fun _ _ => dist_triangle_right _ _ _148149protected theorem dist : LipschitzWith 2 (Function.uncurry <| @dist α _) := by150 rw [← one_add_one_eq_two]151 exact LipschitzWith.uncurry LipschitzWith.dist_left LipschitzWith.dist_right152153theorem dist_iterate_succ_le_geometric {f : α → α} (hf : LipschitzWith K f) (x n) :154 dist (f^[n] x) (f^[n + 1] x) ≤ dist x (f x) * (K : ℝ) ^ n := by155 rw [iterate_succ, mul_comm]156 simpa only [NNReal.coe_pow] using! (hf.iterate n).dist_le_mul x (f x)157158theorem _root_.lipschitzWith_max : LipschitzWith 1 fun p : ℝ × ℝ => max p.1 p.2 :=159 LipschitzWith.of_le_add fun _ _ => sub_le_iff_le_add'.1 <|160 (le_abs_self _).trans (abs_max_sub_max_le_max _ _ _ _)161162theorem _root_.lipschitzWith_min : LipschitzWith 1 fun p : ℝ × ℝ => min p.1 p.2 :=163 LipschitzWith.of_le_add fun _ _ => sub_le_iff_le_add'.1 <|164 (le_abs_self _).trans (abs_min_sub_min_le_max _ _ _ _)165166lemma _root_.Real.lipschitzWith_toNNReal : LipschitzWith 1 Real.toNNReal := by167 refine lipschitzWith_iff_dist_le_mul.mpr (fun x y ↦ ?_)168 simpa only [NNReal.coe_one, dist_prod_same_right, one_mul, Real.dist_eq] using!169 lipschitzWith_iff_dist_le_mul.mp lipschitzWith_max (x, 0) (y, 0)170171end Metric172173section EMetric174175variable [PseudoEMetricSpace α] {f g : α → ℝ} {Kf Kg : ℝ≥0}176177protected theorem max (hf : LipschitzWith Kf f) (hg : LipschitzWith Kg g) :178 LipschitzWith (max Kf Kg) fun x => max (f x) (g x) := by179 simpa only [(· ∘ ·), one_mul] using! lipschitzWith_max.comp (hf.prodMk hg)180181protected theorem min (hf : LipschitzWith Kf f) (hg : LipschitzWith Kg g) :182 LipschitzWith (max Kf Kg) fun x => min (f x) (g x) := by183 simpa only [(· ∘ ·), one_mul] using! lipschitzWith_min.comp (hf.prodMk hg)184185theorem max_const (hf : LipschitzWith Kf f) (a : ℝ) : LipschitzWith Kf fun x => max (f x) a := by186 simpa using hf.max (LipschitzWith.const a)187188theorem const_max (hf : LipschitzWith Kf f) (a : ℝ) : LipschitzWith Kf fun x => max a (f x) := by189 simpa only [max_comm] using hf.max_const a190191theorem min_const (hf : LipschitzWith Kf f) (a : ℝ) : LipschitzWith Kf fun x => min (f x) a := by192 simpa using hf.min (LipschitzWith.const a)193194theorem const_min (hf : LipschitzWith Kf f) (a : ℝ) : LipschitzWith Kf fun x => min a (f x) := by195 simpa only [min_comm] using hf.min_const a196197end EMetric198199protected theorem projIcc {a b : ℝ} (h : a ≤ b) : LipschitzWith 1 (projIcc a b h) :=200 ((LipschitzWith.id.const_min _).const_max _).subtype_mk _201202end LipschitzWith203204/-- The preimage of a proper space under a Lipschitz proper map is proper. -/205lemma LipschitzWith.properSpace {X Y : Type*} [PseudoMetricSpace X]206 [PseudoMetricSpace Y] [ProperSpace Y] {f : X → Y} (hf : IsProperMap f)207 {K : ℝ≥0} (hf' : LipschitzWith K f) : ProperSpace X :=208 ⟨fun x r ↦ (hf.isCompact_preimage (isCompact_closedBall (f x) (K * r))).of_isClosed_subset209 Metric.isClosed_closedBall (hf'.mapsTo_closedBall x r).subset_preimage⟩210211namespace LipschitzOnWith212213section Metric214215variable [PseudoMetricSpace α] [PseudoMetricSpace β] [PseudoMetricSpace γ]216variable {K : ℝ≥0} {s : Set α} {f : α → β}217218protected theorem of_dist_le' {K : ℝ} (h : ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ K * dist x y) :219 LipschitzOnWith (Real.toNNReal K) f s :=220 of_dist_le_mul fun x hx y hy =>221 le_trans (h x hx y hy) <| by gcongr; apply Real.le_coe_toNNReal222223protected theorem mk_one (h : ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ dist x y) :224 LipschitzOnWith 1 f s :=225 of_dist_le_mul <| by simpa only [NNReal.coe_one, one_mul] using h226227/-- For functions to `ℝ`, it suffices to prove `f x ≤ f y + K * dist x y`; this version228doesn't assume `0≤K`. -/229protected theorem of_le_add_mul' {f : α → ℝ} (K : ℝ)230 (h : ∀ x ∈ s, ∀ y ∈ s, f x ≤ f y + K * dist x y) : LipschitzOnWith (Real.toNNReal K) f s :=231 have I : ∀ x ∈ s, ∀ y ∈ s, f x - f y ≤ K * dist x y := fun x hx y hy =>232 sub_le_iff_le_add'.2 (h x hx y hy)233 LipschitzOnWith.of_dist_le' fun x hx y hy =>234 abs_sub_le_iff.2 ⟨I x hx y hy, dist_comm y x ▸ I y hy x hx⟩235236/-- For functions to `ℝ`, it suffices to prove `f x ≤ f y + K * dist x y`; this version237assumes `0≤K`. -/238protected theorem of_le_add_mul {f : α → ℝ} (K : ℝ≥0)239 (h : ∀ x ∈ s, ∀ y ∈ s, f x ≤ f y + K * dist x y) : LipschitzOnWith K f s := by240 simpa only [Real.toNNReal_coe] using LipschitzOnWith.of_le_add_mul' K h241242protected theorem of_le_add {f : α → ℝ} (h : ∀ x ∈ s, ∀ y ∈ s, f x ≤ f y + dist x y) :243 LipschitzOnWith 1 f s :=244 LipschitzOnWith.of_le_add_mul 1 <| by simpa only [NNReal.coe_one, one_mul]245246protected theorem le_add_mul {f : α → ℝ} {K : ℝ≥0} (h : LipschitzOnWith K f s) {x : α} (hx : x ∈ s)247 {y : α} (hy : y ∈ s) : f x ≤ f y + K * dist x y :=248 sub_le_iff_le_add'.1 <| le_trans (le_abs_self _) <| h.dist_le_mul x hx y hy249250protected theorem iff_le_add_mul {f : α → ℝ} {K : ℝ≥0} :251 LipschitzOnWith K f s ↔ ∀ x ∈ s, ∀ y ∈ s, f x ≤ f y + K * dist x y :=252 ⟨LipschitzOnWith.le_add_mul, LipschitzOnWith.of_le_add_mul K⟩253254theorem isBounded_image2 (f : α → β → γ) {K₁ K₂ : ℝ≥0} {s : Set α} {t : Set β}255 (hs : Bornology.IsBounded s) (ht : Bornology.IsBounded t)256 (hf₁ : ∀ b ∈ t, LipschitzOnWith K₁ (fun a => f a b) s)257 (hf₂ : ∀ a ∈ s, LipschitzOnWith K₂ (f a) t) : Bornology.IsBounded (Set.image2 f s t) :=258 Metric.isBounded_iff_ediam_ne_top.2 <|259 ne_top_of_le_ne_top260 (ENNReal.add_ne_top.mpr261 ⟨ENNReal.mul_ne_top ENNReal.coe_ne_top hs.ediam_ne_top,262 ENNReal.mul_ne_top ENNReal.coe_ne_top ht.ediam_ne_top⟩)263 (ediam_image2_le _ _ _ hf₁ hf₂)264265end Metric266267end LipschitzOnWith268269namespace LocallyLipschitz270271section Real272273variable [PseudoEMetricSpace α] {f g : α → ℝ}274275/-- The minimum of locally Lipschitz functions is locally Lipschitz. -/276protected lemma min (hf : LocallyLipschitz f) (hg : LocallyLipschitz g) :277 LocallyLipschitz (fun x => min (f x) (g x)) :=278 lipschitzWith_min.locallyLipschitz.comp (hf.prodMk hg)279280/-- The maximum of locally Lipschitz functions is locally Lipschitz. -/281protected lemma max (hf : LocallyLipschitz f) (hg : LocallyLipschitz g) :282 LocallyLipschitz (fun x => max (f x) (g x)) :=283 lipschitzWith_max.locallyLipschitz.comp (hf.prodMk hg)284285theorem max_const (hf : LocallyLipschitz f) (a : ℝ) : LocallyLipschitz fun x => max (f x) a :=286 hf.max (LocallyLipschitz.const a)287288theorem const_max (hf : LocallyLipschitz f) (a : ℝ) : LocallyLipschitz fun x => max a (f x) := by289 simpa [max_comm] using (hf.max_const a)290291theorem min_const (hf : LocallyLipschitz f) (a : ℝ) : LocallyLipschitz fun x => min (f x) a :=292 hf.min (LocallyLipschitz.const a)293294theorem const_min (hf : LocallyLipschitz f) (a : ℝ) : LocallyLipschitz fun x => min a (f x) := by295 simpa [min_comm] using (hf.min_const a)296297end Real298end LocallyLipschitz299300open Metric301302variable [PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β}303304/-- A function `f : α → ℝ` which is `K`-Lipschitz on a subset `s` admits a `K`-Lipschitz extension305to the whole space. -/306theorem LipschitzOnWith.extend_real {f : α → ℝ} {s : Set α} {K : ℝ≥0} (hf : LipschitzOnWith K f s) :307 ∃ g : α → ℝ, LipschitzWith K g ∧ EqOn f g s := by308 /- An extension is given by `g y = Inf {f x + K * dist y x | x ∈ s}`. Taking `x = y`, one has309 `g y ≤ f y` for `y ∈ s`, and the other inequality holds because `f` is `K`-Lipschitz, so that it310 cannot counterbalance the growth of `K * dist y x`. One readily checks from the formula that311 the extended function is also `K`-Lipschitz. -/312 rcases eq_empty_or_nonempty s with (rfl | hs)313 · exact ⟨fun _ => 0, (LipschitzWith.const _).weaken zero_le, eqOn_empty _ _⟩314 have : Nonempty s := by simp only [hs, nonempty_coe_sort]315 let g := fun y : α => iInf fun x : s => f x + K * dist y x316 have B : ∀ y : α, BddBelow (range fun x : s => f x + K * dist y x) := fun y => by317 rcases hs with ⟨z, hz⟩318 refine ⟨f z - K * dist y z, ?_⟩319 rintro w ⟨t, rfl⟩320 dsimp321 rw [sub_le_iff_le_add, add_assoc, ← mul_add, add_comm (dist y t)]322 calc323 f z ≤ f t + K * dist z t := hf.le_add_mul hz t.2324 _ ≤ f t + K * (dist y z + dist y t) := by gcongr; apply dist_triangle_left325 have E : EqOn f g s := fun x hx => by326 refine le_antisymm (le_ciInf fun y => hf.le_add_mul hx y.2) ?_327 simpa only [add_zero, Subtype.coe_mk, mul_zero, dist_self] using ciInf_le (B x) ⟨x, hx⟩328 refine ⟨g, LipschitzWith.of_le_add_mul K fun x y => ?_, E⟩329 rw [← sub_le_iff_le_add]330 refine le_ciInf fun z => ?_331 rw [sub_le_iff_le_add]332 calc333 g x ≤ f z + K * dist x z := ciInf_le (B x) _334 _ ≤ f z + K * dist y z + K * dist x y := by335 rw [add_assoc, ← mul_add, add_comm (dist y z)]336 gcongr337 apply dist_triangle338339/-- A function `f : α → (ι → ℝ)` which is `K`-Lipschitz on a subset `s` admits a `K`-Lipschitz340extension to the whole space. The same result for the space `ℓ^∞ (ι, ℝ)` over a possibly infinite341type `ι` is implemented in `LipschitzOnWith.extend_lp_infty`. -/342theorem LipschitzOnWith.extend_pi [Fintype ι] {f : α → ι → ℝ} {s : Set α}343 {K : ℝ≥0} (hf : LipschitzOnWith K f s) : ∃ g : α → ι → ℝ, LipschitzWith K g ∧ EqOn f g s := by344 have : ∀ i, ∃ g : α → ℝ, LipschitzWith K g ∧ EqOn (fun x => f x i) g s := fun i => by345 have : LipschitzOnWith K (fun x : α => f x i) s :=346 LipschitzOnWith.of_dist_le_mul fun x hx y hy =>347 (dist_le_pi_dist _ _ i).trans (hf.dist_le_mul x hx y hy)348 exact this.extend_real349 choose g hg using this350 refine ⟨fun x i => g i x, LipschitzWith.of_dist_le_mul fun x y => ?_, fun x hx ↦ ?_⟩351 · exact (dist_pi_le_iff (mul_nonneg K.2 dist_nonneg)).2 fun i => (hg i).1.dist_le_mul x y352 · ext1 i353 exact (hg i).2 hx