topology.metric_space.lipschitz

source

def lipschitz_with {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] (K : nnreal) (f : α → β) :

Prop

A function f is Lipschitz continuous with constant K ≥ 0 if for all x, y we have dist (f x) (f y) ≤ K * dist x y

Equations

lipschitz_with K f = ∀ (x y : α), has_edist.edist (f x) (f y) ≤ ↑K * has_edist.edist x y

source

theorem lipschitz_with_iff_dist_le_mul {α : Type u} {β : Type v} [pseudo_metric_space α] [pseudo_metric_space β] {K : nnreal} {f : α → β} :

lipschitz_with K f ↔ ∀ (x y : α), has_dist.dist (f x) (f y) ≤ ↑K * has_dist.dist x y

source

theorem lipschitz_with.of_dist_le_mul {α : Type u} {β : Type v} [pseudo_metric_space α] [pseudo_metric_space β] {K : nnreal} {f : α → β} :

(∀ (x y : α), has_dist.dist (f x) (f y) ≤ ↑K * has_dist.dist x y) → lipschitz_with K f

Alias of the reverse direction of lipschitz_with_iff_dist_le_mul.

source

theorem lipschitz_with.dist_le_mul {α : Type u} {β : Type v} [pseudo_metric_space α] [pseudo_metric_space β] {K : nnreal} {f : α → β} :

lipschitz_with K f → ∀ (x y : α), has_dist.dist (f x) (f y) ≤ ↑K * has_dist.dist x y

Alias of the forward direction of lipschitz_with_iff_dist_le_mul.

source

def lipschitz_on_with {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] (K : nnreal) (f : α → β) (s : set α) :

Prop

A function f is Lipschitz continuous with constant K ≥ 0 on s if for all x, y in s we have dist (f x) (f y) ≤ K * dist x y

Equations

lipschitz_on_with K f s = ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → has_edist.edist (f x) (f y) ≤ ↑K * has_edist.edist x y

source

@[simp]

theorem lipschitz_on_with_empty {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] (K : nnreal) (f : α → β) :

lipschitz_on_with K f ∅

source

theorem lipschitz_on_with.mono {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] {K : nnreal} {s t : set α} {f : α → β} (hf : lipschitz_on_with K f t) (h : s ⊆ t) :

lipschitz_on_with K f s

source

theorem lipschitz_on_with_iff_dist_le_mul {α : Type u} {β : Type v} [pseudo_metric_space α] [pseudo_metric_space β] {K : nnreal} {s : set α} {f : α → β} :

lipschitz_on_with K f s ↔ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → has_dist.dist (f x) (f y) ≤ ↑K * has_dist.dist x y

source

theorem lipschitz_on_with.dist_le_mul {α : Type u} {β : Type v} [pseudo_metric_space α] [pseudo_metric_space β] {K : nnreal} {s : set α} {f : α → β} :

lipschitz_on_with K f s → ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → has_dist.dist (f x) (f y) ≤ ↑K * has_dist.dist x y

Alias of the forward direction of lipschitz_on_with_iff_dist_le_mul.

source

theorem lipschitz_on_with.of_dist_le_mul {α : Type u} {β : Type v} [pseudo_metric_space α] [pseudo_metric_space β] {K : nnreal} {s : set α} {f : α → β} :

(∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → has_dist.dist (f x) (f y) ≤ ↑K * has_dist.dist x y) → lipschitz_on_with K f s

Alias of the reverse direction of lipschitz_on_with_iff_dist_le_mul.

source

@[simp]

theorem lipschitz_on_univ {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] {K : nnreal} {f : α → β} :

lipschitz_on_with K f set.univ ↔ lipschitz_with K f

source

theorem lipschitz_on_with_iff_restrict {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] {K : nnreal} {f : α → β} {s : set α} :

lipschitz_on_with K f s ↔ lipschitz_with K (s.restrict f)

source

theorem lipschitz_on_with.to_restrict {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] {K : nnreal} {f : α → β} {s : set α} :

lipschitz_on_with K f s → lipschitz_with K (s.restrict f)

Alias of the forward direction of lipschitz_on_with_iff_restrict.

source

theorem maps_to.lipschitz_on_with_iff_restrict {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] {K : nnreal} {f : α → β} {s : set α} {t : set β} (h : set.maps_to f s t) :

lipschitz_on_with K f s ↔ lipschitz_with K (set.maps_to.restrict f s t h)

source

theorem lipschitz_on_with.to_restrict_maps_to {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] {K : nnreal} {f : α → β} {s : set α} {t : set β} (h : set.maps_to f s t) :

lipschitz_on_with K f s → lipschitz_with K (set.maps_to.restrict f s t h)

Alias of the forward direction of maps_to.lipschitz_on_with_iff_restrict.

source

@[protected]

theorem lipschitz_with.lipschitz_on_with {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] {K : nnreal} {f : α → β} (h : lipschitz_with K f) (s : set α) :

lipschitz_on_with K f s

source

theorem lipschitz_with.edist_le_mul {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] {K : nnreal} {f : α → β} (h : lipschitz_with K f) (x y : α) :

has_edist.edist (f x) (f y) ≤ ↑K * has_edist.edist x y

source

theorem lipschitz_with.edist_le_mul_of_le {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] {K : nnreal} {f : α → β} {x y : α} {r : ennreal} (h : lipschitz_with K f) (hr : has_edist.edist x y ≤ r) :

has_edist.edist (f x) (f y) ≤ ↑K * r

source

theorem lipschitz_with.edist_lt_mul_of_lt {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] {K : nnreal} {f : α → β} {x y : α} {r : ennreal} (h : lipschitz_with K f) (hK : K ≠ 0) (hr : has_edist.edist x y < r) :

has_edist.edist (f x) (f y) < ↑K * r

source

theorem lipschitz_with.maps_to_emetric_closed_ball {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] {K : nnreal} {f : α → β} (h : lipschitz_with K f) (x : α) (r : ennreal) :

set.maps_to f (emetric.closed_ball x r) (emetric.closed_ball (f x) (↑K * r))

source

theorem lipschitz_with.maps_to_emetric_ball {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] {K : nnreal} {f : α → β} (h : lipschitz_with K f) (hK : K ≠ 0) (x : α) (r : ennreal) :

set.maps_to f (emetric.ball x r) (emetric.ball (f x) (↑K * r))

source

theorem lipschitz_with.edist_lt_top {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] {K : nnreal} {f : α → β} (hf : lipschitz_with K f) {x y : α} (h : has_edist.edist x y ≠ ⊤) :

has_edist.edist (f x) (f y) < ⊤

source

theorem lipschitz_with.mul_edist_le {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] {K : nnreal} {f : α → β} (h : lipschitz_with K f) (x y : α) :

(↑K)⁻¹ * has_edist.edist (f x) (f y) ≤ has_edist.edist x y

source

@[protected]

theorem lipschitz_with.of_edist_le {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] {f : α → β} (h : ∀ (x y : α), has_edist.edist (f x) (f y) ≤ has_edist.edist x y) :

lipschitz_with 1 f

source

@[protected]

theorem lipschitz_with.weaken {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] {K : nnreal} {f : α → β} (hf : lipschitz_with K f) {K' : nnreal} (h : K ≤ K') :

lipschitz_with K' f

source

theorem lipschitz_with.ediam_image_le {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] {K : nnreal} {f : α → β} (hf : lipschitz_with K f) (s : set α) :

emetric.diam (f '' s) ≤ ↑K * emetric.diam s

source

theorem lipschitz_with.edist_lt_of_edist_lt_div {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] {K : nnreal} {f : α → β} (hf : lipschitz_with K f) {x y : α} {d : ennreal} (h : has_edist.edist x y < d / ↑K) :

has_edist.edist (f x) (f y) < d

source

@[protected]

theorem lipschitz_with.uniform_continuous {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] {K : nnreal} {f : α → β} (hf : lipschitz_with K f) :

uniform_continuous f

A Lipschitz function is uniformly continuous

source

@[protected]

theorem lipschitz_with.continuous {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] {K : nnreal} {f : α → β} (hf : lipschitz_with K f) :

continuous f

A Lipschitz function is continuous

source

@[protected]

theorem lipschitz_with.const {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] (b : β) :

lipschitz_with 0 (λ (a : α), b)

source

@[protected]

theorem lipschitz_with.id {α : Type u} [pseudo_emetric_space α] :

lipschitz_with 1 id

source

@[protected]

theorem lipschitz_with.subtype_val {α : Type u} [pseudo_emetric_space α] (s : set α) :

lipschitz_with 1 subtype.val

source

@[protected]

theorem lipschitz_with.subtype_coe {α : Type u} [pseudo_emetric_space α] (s : set α) :

lipschitz_with 1 coe

source

theorem lipschitz_with.subtype_mk {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] {K : nnreal} {f : α → β} (hf : lipschitz_with K f) {p : β → Prop} (hp : ∀ (x : α), p (f x)) :

lipschitz_with K (λ (x : α), ⟨f x, _⟩)

source

@[protected]

theorem lipschitz_with.eval {ι : Type x} {α : ι → Type u} [Π (i : ι), pseudo_emetric_space (α i)] [fintype ι] (i : ι) :

lipschitz_with 1 (function.eval i)

source

@[protected]

theorem lipschitz_with.restrict {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] {K : nnreal} {f : α → β} (hf : lipschitz_with K f) (s : set α) :

lipschitz_with K (s.restrict f)

source

@[protected]

theorem lipschitz_with.comp {α : Type u} {β : Type v} {γ : Type w} [pseudo_emetric_space α] [pseudo_emetric_space β] [pseudo_emetric_space γ] {Kf Kg : nnreal} {f : β → γ} {g : α → β} (hf : lipschitz_with Kf f) (hg : lipschitz_with Kg g) :

lipschitz_with (Kf * Kg) (f ∘ g)

source

theorem lipschitz_with.comp_lipschitz_on_with {α : Type u} {β : Type v} {γ : Type w} [pseudo_emetric_space α] [pseudo_emetric_space β] [pseudo_emetric_space γ] {Kf Kg : nnreal} {f : β → γ} {g : α → β} {s : set α} (hf : lipschitz_with Kf f) (hg : lipschitz_on_with Kg g s) :

lipschitz_on_with (Kf * Kg) (f ∘ g) s

source

@[protected]

theorem lipschitz_with.prod_fst {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] :

lipschitz_with 1 prod.fst

source

@[protected]

theorem lipschitz_with.prod_snd {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] :

lipschitz_with 1 prod.snd

source

@[protected]

theorem lipschitz_with.prod {α : Type u} {β : Type v} {γ : Type w} [pseudo_emetric_space α] [pseudo_emetric_space β] [pseudo_emetric_space γ] {f : α → β} {Kf : nnreal} (hf : lipschitz_with Kf f) {g : α → γ} {Kg : nnreal} (hg : lipschitz_with Kg g) :

lipschitz_with (linear_order.max Kf Kg) (λ (x : α), (f x, g x))

source

@[protected]

theorem lipschitz_with.prod_mk_left {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] (a : α) :

lipschitz_with 1 (prod.mk a)

source

@[protected]

theorem lipschitz_with.prod_mk_right {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] (b : β) :

lipschitz_with 1 (λ (a : α), (a, b))

source

@[protected]

theorem lipschitz_with.uncurry {α : Type u} {β : Type v} {γ : Type w} [pseudo_emetric_space α] [pseudo_emetric_space β] [pseudo_emetric_space γ] {f : α → β → γ} {Kα Kβ : nnreal} (hα : ∀ (b : β), lipschitz_with Kα (λ (a : α), f a b)) (hβ : ∀ (a : α), lipschitz_with Kβ (f a)) :

lipschitz_with (Kα + Kβ) (function.uncurry f)

source

@[protected]

theorem lipschitz_with.iterate {α : Type u} [pseudo_emetric_space α] {K : nnreal} {f : α → α} (hf : lipschitz_with K f) (n : ℕ) :

lipschitz_with (K ^ n) f^[n]

source

theorem lipschitz_with.edist_iterate_succ_le_geometric {α : Type u} [pseudo_emetric_space α] {K : nnreal} {f : α → α} (hf : lipschitz_with K f) (x : α) (n : ℕ) :

has_edist.edist (f^[n] x) (f^[n + 1] x) ≤ has_edist.edist x (f x) * ↑K ^ n

source

@[protected]

theorem lipschitz_with.mul {α : Type u} [pseudo_emetric_space α] {f g : function.End α} {Kf Kg : nnreal} (hf : lipschitz_with Kf f) (hg : lipschitz_with Kg g) :

lipschitz_with (Kf * Kg) (f * g)

source

@[protected]

theorem lipschitz_with.list_prod {α : Type u} {ι : Type x} [pseudo_emetric_space α] (f : ι → function.End α) (K : ι → nnreal) (h : ∀ (i : ι), lipschitz_with (K i) (f i)) (l : list ι) :

lipschitz_with (list.map K l).prod (list.map f l).prod

The product of a list of Lipschitz continuous endomorphisms is a Lipschitz continuous endomorphism.

source

@[protected]

theorem lipschitz_with.pow {α : Type u} [pseudo_emetric_space α] {f : function.End α} {K : nnreal} (h : lipschitz_with K f) (n : ℕ) :

lipschitz_with (K ^ n) (f ^ n)

source

@[protected]

theorem lipschitz_with.of_dist_le' {α : Type u} {β : Type v} [pseudo_metric_space α] [pseudo_metric_space β] {f : α → β} {K : ℝ} (h : ∀ (x y : α), has_dist.dist (f x) (f y) ≤ K * has_dist.dist x y) :

lipschitz_with K.to_nnreal f

source

@[protected]

theorem lipschitz_with.mk_one {α : Type u} {β : Type v} [pseudo_metric_space α] [pseudo_metric_space β] {f : α → β} (h : ∀ (x y : α), has_dist.dist (f x) (f y) ≤ has_dist.dist x y) :

lipschitz_with 1 f

source

@[protected]

theorem lipschitz_with.of_le_add_mul' {α : Type u} [pseudo_metric_space α] {f : α → ℝ} (K : ℝ) (h : ∀ (x y : α), f x ≤ f y + K * has_dist.dist x y) :

lipschitz_with K.to_nnreal f

For functions to ℝ, it suffices to prove f x ≤ f y + K * dist x y; this version doesn't assume 0≤K.

source

@[protected]

theorem lipschitz_with.of_le_add_mul {α : Type u} [pseudo_metric_space α] {f : α → ℝ} (K : nnreal) (h : ∀ (x y : α), f x ≤ f y + ↑K * has_dist.dist x y) :

lipschitz_with K f

For functions to ℝ, it suffices to prove f x ≤ f y + K * dist x y; this version assumes 0≤K.

source

@[protected]

theorem lipschitz_with.of_le_add {α : Type u} [pseudo_metric_space α] {f : α → ℝ} (h : ∀ (x y : α), f x ≤ f y + has_dist.dist x y) :

lipschitz_with 1 f

source

@[protected]

theorem lipschitz_with.le_add_mul {α : Type u} [pseudo_metric_space α] {f : α → ℝ} {K : nnreal} (h : lipschitz_with K f) (x y : α) :

f x ≤ f y + ↑K * has_dist.dist x y

source

@[protected]

theorem lipschitz_with.iff_le_add_mul {α : Type u} [pseudo_metric_space α] {f : α → ℝ} {K : nnreal} :

lipschitz_with K f ↔ ∀ (x y : α), f x ≤ f y + ↑K * has_dist.dist x y

source

theorem lipschitz_with.nndist_le {α : Type u} {β : Type v} [pseudo_metric_space α] [pseudo_metric_space β] {K : nnreal} {f : α → β} (hf : lipschitz_with K f) (x y : α) :

has_nndist.nndist (f x) (f y) ≤ K * has_nndist.nndist x y

source

theorem lipschitz_with.dist_le_mul_of_le {α : Type u} {β : Type v} [pseudo_metric_space α] [pseudo_metric_space β] {K : nnreal} {f : α → β} {x y : α} {r : ℝ} (hf : lipschitz_with K f) (hr : has_dist.dist x y ≤ r) :

has_dist.dist (f x) (f y) ≤ ↑K * r

source

theorem lipschitz_with.maps_to_closed_ball {α : Type u} {β : Type v} [pseudo_metric_space α] [pseudo_metric_space β] {K : nnreal} {f : α → β} (hf : lipschitz_with K f) (x : α) (r : ℝ) :

set.maps_to f (metric.closed_ball x r) (metric.closed_ball (f x) (↑K * r))

source

theorem lipschitz_with.dist_lt_mul_of_lt {α : Type u} {β : Type v} [pseudo_metric_space α] [pseudo_metric_space β] {K : nnreal} {f : α → β} {x y : α} {r : ℝ} (hf : lipschitz_with K f) (hK : K ≠ 0) (hr : has_dist.dist x y < r) :

has_dist.dist (f x) (f y) < ↑K * r

source

theorem lipschitz_with.maps_to_ball {α : Type u} {β : Type v} [pseudo_metric_space α] [pseudo_metric_space β] {K : nnreal} {f : α → β} (hf : lipschitz_with K f) (hK : K ≠ 0) (x : α) (r : ℝ) :

set.maps_to f (metric.ball x r) (metric.ball (f x) (↑K * r))

source

def lipschitz_with.to_locally_bounded_map {α : Type u} {β : Type v} [pseudo_metric_space α] [pseudo_metric_space β] {K : nnreal} (f : α → β) (hf : lipschitz_with K f) :

locally_bounded_map α β

A Lipschitz continuous map is a locally bounded map.

Equations

lipschitz_with.to_locally_bounded_map f hf = locally_bounded_map.of_map_bounded f _

source

@[simp]

theorem lipschitz_with.coe_to_locally_bounded_map {α : Type u} {β : Type v} [pseudo_metric_space α] [pseudo_metric_space β] {K : nnreal} {f : α → β} (hf : lipschitz_with K f) :

⇑(lipschitz_with.to_locally_bounded_map f hf) = f

source

theorem lipschitz_with.comap_cobounded_le {α : Type u} {β : Type v} [pseudo_metric_space α] [pseudo_metric_space β] {K : nnreal} {f : α → β} (hf : lipschitz_with K f) :

filter.comap f (bornology.cobounded β) ≤ bornology.cobounded α

source

theorem lipschitz_with.bounded_image {α : Type u} {β : Type v} [pseudo_metric_space α] [pseudo_metric_space β] {K : nnreal} {f : α → β} (hf : lipschitz_with K f) {s : set α} (hs : metric.bounded s) :

metric.bounded (f '' s)

source

theorem lipschitz_with.diam_image_le {α : Type u} {β : Type v} [pseudo_metric_space α] [pseudo_metric_space β] {K : nnreal} {f : α → β} (hf : lipschitz_with K f) (s : set α) (hs : metric.bounded s) :

metric.diam (f '' s) ≤ ↑K * metric.diam s

source

@[protected]

theorem lipschitz_with.dist_left {α : Type u} [pseudo_metric_space α] (y : α) :

lipschitz_with 1 (λ (x : α), has_dist.dist x y)

source

@[protected]

theorem lipschitz_with.dist_right {α : Type u} [pseudo_metric_space α] (x : α) :

lipschitz_with 1 (has_dist.dist x)

source

@[protected]

theorem lipschitz_with.dist {α : Type u} [pseudo_metric_space α] :

lipschitz_with 2 (function.uncurry has_dist.dist)

source

theorem lipschitz_with.dist_iterate_succ_le_geometric {α : Type u} [pseudo_metric_space α] {K : nnreal} {f : α → α} (hf : lipschitz_with K f) (x : α) (n : ℕ) :

has_dist.dist (f^[n] x) (f^[n + 1] x) ≤ has_dist.dist x (f x) * ↑K ^ n

source

theorem lipschitz_with_max :

lipschitz_with 1 (λ (p : ℝ × ℝ), linear_order.max p.fst p.snd)

source

theorem lipschitz_with_min :

lipschitz_with 1 (λ (p : ℝ × ℝ), linear_order.min p.fst p.snd)

source

@[protected]

theorem lipschitz_with.max {α : Type u} [pseudo_emetric_space α] {f g : α → ℝ} {Kf Kg : nnreal} (hf : lipschitz_with Kf f) (hg : lipschitz_with Kg g) :

lipschitz_with (linear_order.max Kf Kg) (λ (x : α), linear_order.max (f x) (g x))

source

@[protected]

theorem lipschitz_with.min {α : Type u} [pseudo_emetric_space α] {f g : α → ℝ} {Kf Kg : nnreal} (hf : lipschitz_with Kf f) (hg : lipschitz_with Kg g) :

lipschitz_with (linear_order.max Kf Kg) (λ (x : α), linear_order.min (f x) (g x))

source

theorem lipschitz_with.max_const {α : Type u} [pseudo_emetric_space α] {f : α → ℝ} {Kf : nnreal} (hf : lipschitz_with Kf f) (a : ℝ) :

lipschitz_with Kf (λ (x : α), linear_order.max (f x) a)

source

theorem lipschitz_with.const_max {α : Type u} [pseudo_emetric_space α] {f : α → ℝ} {Kf : nnreal} (hf : lipschitz_with Kf f) (a : ℝ) :

lipschitz_with Kf (λ (x : α), linear_order.max a (f x))

source

theorem lipschitz_with.min_const {α : Type u} [pseudo_emetric_space α] {f : α → ℝ} {Kf : nnreal} (hf : lipschitz_with Kf f) (a : ℝ) :

lipschitz_with Kf (λ (x : α), linear_order.min (f x) a)

source

theorem lipschitz_with.const_min {α : Type u} [pseudo_emetric_space α] {f : α → ℝ} {Kf : nnreal} (hf : lipschitz_with Kf f) (a : ℝ) :

lipschitz_with Kf (λ (x : α), linear_order.min a (f x))

source

@[protected]

theorem lipschitz_with.proj_Icc {a b : ℝ} (h : a ≤ b) :

lipschitz_with 1 (set.proj_Icc a b h)

source

theorem metric.bounded.left_of_prod {α : Type u} {β : Type v} [pseudo_metric_space α] [pseudo_metric_space β] {s : set α} {t : set β} (h : metric.bounded (s ×ˢ t)) (ht : t.nonempty) :

metric.bounded s

source

theorem metric.bounded.right_of_prod {α : Type u} {β : Type v} [pseudo_metric_space α] [pseudo_metric_space β] {s : set α} {t : set β} (h : metric.bounded (s ×ˢ t)) (hs : s.nonempty) :

metric.bounded t

source

theorem metric.bounded_prod_of_nonempty {α : Type u} {β : Type v} [pseudo_metric_space α] [pseudo_metric_space β] {s : set α} {t : set β} (hs : s.nonempty) (ht : t.nonempty) :

metric.bounded (s ×ˢ t) ↔ metric.bounded s ∧ metric.bounded t

source

theorem metric.bounded_prod {α : Type u} {β : Type v} [pseudo_metric_space α] [pseudo_metric_space β] {s : set α} {t : set β} :

metric.bounded (s ×ˢ t) ↔ s = ∅ ∨ t = ∅ ∨ metric.bounded s ∧ metric.bounded t

source

@[protected]

theorem lipschitz_on_with.uniform_continuous_on {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] {K : nnreal} {s : set α} {f : α → β} (hf : lipschitz_on_with K f s) :

uniform_continuous_on f s

source

@[protected]

theorem lipschitz_on_with.continuous_on {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] {K : nnreal} {s : set α} {f : α → β} (hf : lipschitz_on_with K f s) :

continuous_on f s

source

theorem lipschitz_on_with.edist_lt_of_edist_lt_div {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] {K : nnreal} {s : set α} {f : α → β} (hf : lipschitz_on_with K f s) {x y : α} (hx : x ∈ s) (hy : y ∈ s) {d : ennreal} (hd : has_edist.edist x y < d / ↑K) :

has_edist.edist (f x) (f y) < d

source

@[protected]

theorem lipschitz_on_with.comp {α : Type u} {β : Type v} {γ : Type w} [pseudo_emetric_space α] [pseudo_emetric_space β] [pseudo_emetric_space γ] {K : nnreal} {s : set α} {f : α → β} {g : β → γ} {t : set β} {Kg : nnreal} (hg : lipschitz_on_with Kg g t) (hf : lipschitz_on_with K f s) (hmaps : set.maps_to f s t) :

lipschitz_on_with (Kg * K) (g ∘ f) s

source

@[protected]

theorem lipschitz_on_with.of_dist_le' {α : Type u} {β : Type v} [pseudo_metric_space α] [pseudo_metric_space β] {s : set α} {f : α → β} {K : ℝ} (h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → has_dist.dist (f x) (f y) ≤ K * has_dist.dist x y) :

lipschitz_on_with K.to_nnreal f s

source

@[protected]

theorem lipschitz_on_with.mk_one {α : Type u} {β : Type v} [pseudo_metric_space α] [pseudo_metric_space β] {s : set α} {f : α → β} (h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → has_dist.dist (f x) (f y) ≤ has_dist.dist x y) :

lipschitz_on_with 1 f s

source

@[protected]

theorem lipschitz_on_with.of_le_add_mul' {α : Type u} [pseudo_metric_space α] {s : set α} {f : α → ℝ} (K : ℝ) (h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f x ≤ f y + K * has_dist.dist x y) :

lipschitz_on_with K.to_nnreal f s

For functions to ℝ, it suffices to prove f x ≤ f y + K * dist x y; this version doesn't assume 0≤K.

source

@[protected]

theorem lipschitz_on_with.of_le_add_mul {α : Type u} [pseudo_metric_space α] {s : set α} {f : α → ℝ} (K : nnreal) (h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f x ≤ f y + ↑K * has_dist.dist x y) :

lipschitz_on_with K f s

For functions to ℝ, it suffices to prove f x ≤ f y + K * dist x y; this version assumes 0≤K.

source

@[protected]

theorem lipschitz_on_with.of_le_add {α : Type u} [pseudo_metric_space α] {s : set α} {f : α → ℝ} (h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f x ≤ f y + has_dist.dist x y) :

lipschitz_on_with 1 f s

source

@[protected]

theorem lipschitz_on_with.le_add_mul {α : Type u} [pseudo_metric_space α] {s : set α} {f : α → ℝ} {K : nnreal} (h : lipschitz_on_with K f s) {x : α} (hx : x ∈ s) {y : α} (hy : y ∈ s) :

f x ≤ f y + ↑K * has_dist.dist x y

source

@[protected]

theorem lipschitz_on_with.iff_le_add_mul {α : Type u} [pseudo_metric_space α] {s : set α} {f : α → ℝ} {K : nnreal} :

lipschitz_on_with K f s ↔ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f x ≤ f y + ↑K * has_dist.dist x y

source

theorem continuous_on_prod_of_continuous_on_lipschitz_on {α : Type u} {β : Type v} {γ : Type w} [pseudo_emetric_space α] [topological_space β] [pseudo_emetric_space γ] (f : α × β → γ) {s : set α} {t : set β} (K : nnreal) (ha : ∀ (a : α), a ∈ s → continuous_on (λ (y : β), f (a, y)) t) (hb : ∀ (b : β), b ∈ t → lipschitz_on_with K (λ (x : α), f (x, b)) s) :

continuous_on f (s ×ˢ t)

Consider a function f : α × β → γ. Suppose that it is continuous on each “vertical fiber” {a} × t, a ∈ s, and is Lipschitz continuous on each “horizontal fiber” s × {b}, b ∈ t with the same Lipschitz constant K. Then it is continuous on s × t.

The actual statement uses (Lipschitz) continuity of λ y, f (a, y) and λ x, f (x, b) instead of continuity of f on subsets of the product space.

source

theorem continuous_prod_of_continuous_lipschitz {α : Type u} {β : Type v} {γ : Type w} [pseudo_emetric_space α] [topological_space β] [pseudo_emetric_space γ] (f : α × β → γ) (K : nnreal) (ha : ∀ (a : α), continuous (λ (y : β), f (a, y))) (hb : ∀ (b : β), lipschitz_with K (λ (x : α), f (x, b))) :

continuous f

Consider a function f : α × β → γ. Suppose that it is continuous on each “vertical section” {a} × univ, a : α, and is Lipschitz continuous on each “horizontal section” univ × {b}, b : β with the same Lipschitz constant K. Then it is continuous.

The actual statement uses (Lipschitz) continuity of λ y, f (a, y) and λ x, f (x, b) instead of continuity of f on subsets of the product space.

source

theorem continuous_at_of_locally_lipschitz {α : Type u} {β : Type v} [pseudo_metric_space α] [pseudo_metric_space β] {f : α → β} {x : α} {r : ℝ} (hr : 0 < r) (K : ℝ) (h : ∀ (y : α), has_dist.dist y x < r → has_dist.dist (f y) (f x) ≤ K * has_dist.dist y x) :

continuous_at f x

If a function is locally Lipschitz around a point, then it is continuous at this point.

source

theorem lipschitz_on_with.extend_real {α : Type u} [pseudo_metric_space α] {f : α → ℝ} {s : set α} {K : nnreal} (hf : lipschitz_on_with K f s) :

∃ (g : α → ℝ), lipschitz_with K g ∧ set.eq_on f g s

A function f : α → ℝ which is K-Lipschitz on a subset s admits a K-Lipschitz extension to the whole space.

source

theorem lipschitz_on_with.extend_pi {α : Type u} {ι : Type x} [pseudo_metric_space α] [fintype ι] {f : α → ι → ℝ} {s : set α} {K : nnreal} (hf : lipschitz_on_with K f s) :

∃ (g : α → ι → ℝ), lipschitz_with K g ∧ set.eq_on f g s

A function f : α → (ι → ℝ) which is K-Lipschitz on a subset s admits a K-Lipschitz extension to the whole space. TODO: state the same result (with the same proof) for the space ℓ^∞ (ι, ℝ) over a possibly infinite type ι.

mathlib3 documentation

Lipschitz continuous functions #

Main definitions and lemmas #

Implementation notes #