def Metric.IsUniformContinuousWith {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace X] [PseudoMetricSpace Y] (δ : ℝ → ℝ) (f : X → Y) : Prop

A function between metric spaces is uniformly continuous with modulus of continuity δ : ℝ → ℝ if dist x y ≤ δ(ε) → dist (f x) (f y) ≤ ε for all x, y.

Equations

• Metric.IsUniformContinuousWith δ f = ∀ ⦃ε : ℝ⦄, 0 < ε → ∀ ⦃x y : X⦄, dist x y ≤ δ ε → dist (f x) (f y) ≤ ε

theorem Metric.IsUniformContinuousWith.uniformContinuous {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace X] [PseudoMetricSpace Y] {δ : ℝ → ℝ} {f : X → Y} (hδ : ∀ ε > 0, 0 < δ ε) (hf : IsUniformContinuousWith δ f) : UniformContinuous f

theorem Metric.uniformContinuous_iff_exists_isUniformContinuousWith {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace X] [PseudoMetricSpace Y] {f : X → Y} : UniformContinuous f ↔ ∃ (δ : ℝ → ℝ), (∀ ε > 0, 0 < δ ε) ∧ IsUniformContinuousWith δ f

theorem LipschitzWith.isUniformContinuousWith {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace X] [PseudoMetricSpace Y] {f : X → Y} {K : NNReal} (hf : LipschitzWith K f) : Metric.IsUniformContinuousWith (fun (ε : ℝ) => ε / ↑K) f

A K-Lipschitz function is uniformly continuous with modulus of continuity ε ↦ ε / K.

def Metric.IsUniformContinuousOnWith {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace X] [PseudoMetricSpace Y] (δ : ℝ → ℝ) (f : X → Y) (S : Set X) : Prop

A function is uniformly continuous on a set S with modulus of continuity δ : ℝ → ℝ if dist x y ≤ δ(ε) → dist (f x) (f y) ≤ ε for all x, y in S.

This is the "on a set" version of IsUniformContinuousWith, and a quantitative version of UniformContinuousOn. It is implied by LipschitzOnWith.

Equations

• Metric.IsUniformContinuousOnWith δ f S = ∀ ⦃ε : ℝ⦄, 0 < ε → ∀ ⦃x : X⦄, x ∈ S → ∀ ⦃y : X⦄, y ∈ S → dist x y ≤ δ ε → dist (f x) (f y) ≤ ε

@[simp]

theorem Metric.isUniformContinuousOnWith_univ {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace X] [PseudoMetricSpace Y] {δ : ℝ → ℝ} {f : X → Y} : IsUniformContinuousOnWith δ f Set.univ ↔ IsUniformContinuousWith δ f

theorem Metric.IsUniformContinuousWith.isUniformContinuousOnWith {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace X] [PseudoMetricSpace Y] {δ : ℝ → ℝ} {f : X → Y} (hf : IsUniformContinuousWith δ f) (S : Set X) : IsUniformContinuousOnWith δ f S

A uniformly continuous function is uniformly continuous on every set.

theorem Metric.IsUniformContinuousOnWith.uniformContinuousOn {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace X] [PseudoMetricSpace Y] {δ : ℝ → ℝ} {f : X → Y} {S : Set X} (hδ : ∀ ε > 0, 0 < δ ε) (hf : IsUniformContinuousOnWith δ f S) : UniformContinuousOn f S

theorem Metric.uniformContinuousOn_iff_exists_isUniformContinuousOnWith {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace X] [PseudoMetricSpace Y] {f : X → Y} {S : Set X} : UniformContinuousOn f S ↔ ∃ (δ : ℝ → ℝ), (∀ ε > 0, 0 < δ ε) ∧ IsUniformContinuousOnWith δ f S

theorem LipschitzOnWith.isUniformContinuousOnWith {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace X] [PseudoMetricSpace Y] {f : X → Y} {K : NNReal} {S : Set X} (hf : LipschitzOnWith K f S) : Metric.IsUniformContinuousOnWith (fun (ε : ℝ) => ε / ↑K) f S

A function that is K-Lipschitz on a set S is uniformly continuous on S with modulus of continuity ε ↦ ε / K.

theorem Metric.IsUniformContinuousOnWith.lipschitzOnWith {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace X] [PseudoMetricSpace Y] {f : X → Y} {K : NNReal} {S : Set X} (hK : 0 < K) (hf : IsUniformContinuousOnWith (fun (ε : ℝ) => ε / ↑K) f S) : LipschitzOnWith K f S

If f is uniformly continuous on S with modulus ε ↦ ε / K for some 0 < K, then f is K-Lipschitz on S.

theorem Metric.lipschitzOnWith_iff_isUniformContinuousOnWith {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace X] [PseudoMetricSpace Y] {f : X → Y} {K : NNReal} {S : Set X} (hK : 0 < K) : LipschitzOnWith K f S ↔ IsUniformContinuousOnWith (fun (ε : ℝ) => ε / ↑K) f S

A function is K-Lipschitz on S iff it is uniformly continuous on S with modulus ε ↦ ε / K, provided 0 < K.

theorem Metric.IsUniformContinuousWith.lipschitzWith {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace X] [PseudoMetricSpace Y] {f : X → Y} {K : NNReal} (hK : 0 < K) (hf : IsUniformContinuousWith (fun (ε : ℝ) => ε / ↑K) f) : LipschitzWith K f

Conversely, if f is uniformly continuous with modulus ε ↦ ε / K for some 0 < K, then f is K-Lipschitz.

theorem Metric.lipschitzWith_iff_isUniformContinuousWith {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace X] [PseudoMetricSpace Y] {f : X → Y} {K : NNReal} (hK : 0 < K) : LipschitzWith K f ↔ IsUniformContinuousWith (fun (ε : ℝ) => ε / ↑K) f

A function is K-Lipschitz iff it is uniformly continuous with modulus ε ↦ ε / K, provided 0 < K.