# Normed groups are uniform groups #

This file proves lipschitzness of normed group operations and shows that normed groups are uniform groups.

Equations
• =
Equations
• =
theorem Isometry.norm_map_of_map_zero {E : Type u_3} {F : Type u_4} {f : EF} (hi : ) (h₁ : f 0 = 0) (x : E) :
theorem Isometry.norm_map_of_map_one {E : Type u_3} {F : Type u_4} [] [] {f : EF} (hi : ) (h₁ : f 1 = 1) (x : E) :
@[simp]
theorem dist_add_self_right {E : Type u_3} (a : E) (b : E) :
dist b (a + b) = a
@[simp]
theorem dist_mul_self_right {E : Type u_3} [] (a : E) (b : E) :
dist b (a * b) = a
@[simp]
theorem dist_add_self_left {E : Type u_3} (a : E) (b : E) :
dist (a + b) b = a
@[simp]
theorem dist_mul_self_left {E : Type u_3} [] (a : E) (b : E) :
dist (a * b) b = a
@[simp]
theorem dist_sub_eq_dist_add_left {E : Type u_3} (a : E) (b : E) (c : E) :
dist (a - b) c = dist a (c + b)
@[simp]
theorem dist_div_eq_dist_mul_left {E : Type u_3} [] (a : E) (b : E) (c : E) :
dist (a / b) c = dist a (c * b)
@[simp]
theorem dist_sub_eq_dist_add_right {E : Type u_3} (a : E) (b : E) (c : E) :
dist a (b - c) = dist (a + c) b
@[simp]
theorem dist_div_eq_dist_mul_right {E : Type u_3} [] (a : E) (b : E) (c : E) :
dist a (b / c) = dist (a * c) b
theorem AddMonoidHomClass.lipschitz_of_bound {𝓕 : Type u_1} {E : Type u_3} {F : Type u_4} [FunLike 𝓕 E F] [] (f : 𝓕) (C : ) (h : ∀ (x : E), f x C * x) :
LipschitzWith C.toNNReal f

A homomorphism f of seminormed groups is Lipschitz, if there exists a constant C such that for all x, one has ‖f x‖ ≤ C * ‖x‖. The analogous condition for a linear map of (semi)normed spaces is in Mathlib/Analysis/NormedSpace/OperatorNorm.lean.

theorem MonoidHomClass.lipschitz_of_bound {𝓕 : Type u_1} {E : Type u_3} {F : Type u_4} [] [] [FunLike 𝓕 E F] [] (f : 𝓕) (C : ) (h : ∀ (x : E), f x C * x) :
LipschitzWith C.toNNReal f

A homomorphism f of seminormed groups is Lipschitz, if there exists a constant C such that for all x, one has ‖f x‖ ≤ C * ‖x‖. The analogous condition for a linear map of (semi)normed spaces is in Mathlib/Analysis/NormedSpace/OperatorNorm.lean.

theorem lipschitzOnWith_iff_norm_sub_le {E : Type u_3} {F : Type u_4} {s : Set E} {f : EF} {C : NNReal} :
∀ ⦃x : E⦄, x s∀ ⦃y : E⦄, y sf x - f y C * x - y
theorem lipschitzOnWith_iff_norm_div_le {E : Type u_3} {F : Type u_4} [] [] {s : Set E} {f : EF} {C : NNReal} :
∀ ⦃x : E⦄, x s∀ ⦃y : E⦄, y sf x / f y C * x / y
theorem LipschitzOnWith.norm_div_le {E : Type u_3} {F : Type u_4} [] [] {s : Set E} {f : EF} {C : NNReal} :
∀ ⦃x : E⦄, x s∀ ⦃y : E⦄, y sf x / f y C * x / y

Alias of the forward direction of lipschitzOnWith_iff_norm_div_le.

theorem LipschitzOnWith.norm_sub_le {E : Type u_3} {F : Type u_4} {s : Set E} {f : EF} {C : NNReal} :
∀ ⦃x : E⦄, x s∀ ⦃y : E⦄, y sf x - f y C * x - y
theorem LipschitzOnWith.norm_sub_le_of_le {E : Type u_3} {F : Type u_4} {s : Set E} {a : E} {b : E} {r : } {f : EF} {C : NNReal} (h : ) (ha : a s) (hb : b s) (hr : a - b r) :
f a - f b C * r
theorem LipschitzOnWith.norm_div_le_of_le {E : Type u_3} {F : Type u_4} [] [] {s : Set E} {a : E} {b : E} {r : } {f : EF} {C : NNReal} (h : ) (ha : a s) (hb : b s) (hr : a / b r) :
f a / f b C * r
theorem lipschitzWith_iff_norm_sub_le {E : Type u_3} {F : Type u_4} {f : EF} {C : NNReal} :
∀ (x y : E), f x - f y C * x - y
theorem lipschitzWith_iff_norm_div_le {E : Type u_3} {F : Type u_4} [] [] {f : EF} {C : NNReal} :
∀ (x y : E), f x / f y C * x / y
theorem LipschitzWith.norm_div_le {E : Type u_3} {F : Type u_4} [] [] {f : EF} {C : NNReal} :
∀ (x y : E), f x / f y C * x / y

Alias of the forward direction of lipschitzWith_iff_norm_div_le.

theorem LipschitzWith.norm_sub_le {E : Type u_3} {F : Type u_4} {f : EF} {C : NNReal} :
∀ (x y : E), f x - f y C * x - y
theorem LipschitzWith.norm_sub_le_of_le {E : Type u_3} {F : Type u_4} {a : E} {b : E} {r : } {f : EF} {C : NNReal} (h : ) (hr : a - b r) :
f a - f b C * r
theorem LipschitzWith.norm_div_le_of_le {E : Type u_3} {F : Type u_4} [] [] {a : E} {b : E} {r : } {f : EF} {C : NNReal} (h : ) (hr : a / b r) :
f a / f b C * r
theorem AddMonoidHomClass.continuous_of_bound {𝓕 : Type u_1} {E : Type u_3} {F : Type u_4} [FunLike 𝓕 E F] [] (f : 𝓕) (C : ) (h : ∀ (x : E), f x C * x) :

A homomorphism f of seminormed groups is continuous, if there exists a constant C such that for all x, one has ‖f x‖ ≤ C * ‖x‖

theorem MonoidHomClass.continuous_of_bound {𝓕 : Type u_1} {E : Type u_3} {F : Type u_4} [] [] [FunLike 𝓕 E F] [] (f : 𝓕) (C : ) (h : ∀ (x : E), f x C * x) :

A homomorphism f of seminormed groups is continuous, if there exists a constant C such that for all x, one has ‖f x‖ ≤ C * ‖x‖.

theorem AddMonoidHomClass.uniformContinuous_of_bound {𝓕 : Type u_1} {E : Type u_3} {F : Type u_4} [FunLike 𝓕 E F] [] (f : 𝓕) (C : ) (h : ∀ (x : E), f x C * x) :
theorem MonoidHomClass.uniformContinuous_of_bound {𝓕 : Type u_1} {E : Type u_3} {F : Type u_4} [] [] [FunLike 𝓕 E F] [] (f : 𝓕) (C : ) (h : ∀ (x : E), f x C * x) :
theorem AddMonoidHomClass.isometry_iff_norm {𝓕 : Type u_1} {E : Type u_3} {F : Type u_4} [FunLike 𝓕 E F] [] (f : 𝓕) :
Isometry f ∀ (x : E), f x = x
theorem MonoidHomClass.isometry_iff_norm {𝓕 : Type u_1} {E : Type u_3} {F : Type u_4} [] [] [FunLike 𝓕 E F] [] (f : 𝓕) :
Isometry f ∀ (x : E), f x = x
theorem MonoidHomClass.isometry_of_norm {𝓕 : Type u_1} {E : Type u_3} {F : Type u_4} [] [] [FunLike 𝓕 E F] [] (f : 𝓕) :
(∀ (x : E), f x = x)Isometry f

Alias of the reverse direction of MonoidHomClass.isometry_iff_norm.

theorem AddMonoidHomClass.isometry_of_norm {𝓕 : Type u_1} {E : Type u_3} {F : Type u_4} [FunLike 𝓕 E F] [] (f : 𝓕) :
(∀ (x : E), f x = x)Isometry f
theorem AddMonoidHomClass.lipschitz_of_bound_nnnorm {𝓕 : Type u_1} {E : Type u_3} {F : Type u_4} [FunLike 𝓕 E F] [] (f : 𝓕) (C : NNReal) (h : ∀ (x : E), f x‖₊ C * x‖₊) :
theorem MonoidHomClass.lipschitz_of_bound_nnnorm {𝓕 : Type u_1} {E : Type u_3} {F : Type u_4} [] [] [FunLike 𝓕 E F] [] (f : 𝓕) (C : NNReal) (h : ∀ (x : E), f x‖₊ C * x‖₊) :
theorem AddMonoidHomClass.antilipschitz_of_bound {𝓕 : Type u_1} {E : Type u_3} {F : Type u_4} [FunLike 𝓕 E F] [] (f : 𝓕) {K : NNReal} (h : ∀ (x : E), x K * f x) :
theorem MonoidHomClass.antilipschitz_of_bound {𝓕 : Type u_1} {E : Type u_3} {F : Type u_4} [] [] [FunLike 𝓕 E F] [] (f : 𝓕) {K : NNReal} (h : ∀ (x : E), x K * f x) :
theorem LipschitzWith.norm_le_mul {E : Type u_3} {F : Type u_4} {f : EF} {K : NNReal} (h : ) (hf : f 0 = 0) (x : E) :
f x K * x
theorem LipschitzWith.norm_le_mul' {E : Type u_3} {F : Type u_4} [] [] {f : EF} {K : NNReal} (h : ) (hf : f 1 = 1) (x : E) :
f x K * x
theorem LipschitzWith.nnorm_le_mul {E : Type u_3} {F : Type u_4} {f : EF} {K : NNReal} (h : ) (hf : f 0 = 0) (x : E) :
theorem LipschitzWith.nnorm_le_mul' {E : Type u_3} {F : Type u_4} [] [] {f : EF} {K : NNReal} (h : ) (hf : f 1 = 1) (x : E) :
theorem AntilipschitzWith.le_mul_norm {E : Type u_3} {F : Type u_4} {f : EF} {K : NNReal} (h : ) (hf : f 0 = 0) (x : E) :
x K * f x
theorem AntilipschitzWith.le_mul_norm' {E : Type u_3} {F : Type u_4} [] [] {f : EF} {K : NNReal} (h : ) (hf : f 1 = 1) (x : E) :
x K * f x
theorem AntilipschitzWith.le_mul_nnnorm {E : Type u_3} {F : Type u_4} {f : EF} {K : NNReal} (h : ) (hf : f 0 = 0) (x : E) :
theorem AntilipschitzWith.le_mul_nnnorm' {E : Type u_3} {F : Type u_4} [] [] {f : EF} {K : NNReal} (h : ) (hf : f 1 = 1) (x : E) :
theorem ZeroHomClass.bound_of_antilipschitz {𝓕 : Type u_1} {E : Type u_3} {F : Type u_4} [FunLike 𝓕 E F] [ZeroHomClass 𝓕 E F] (f : 𝓕) {K : NNReal} (h : ) (x : E) :
x K * f x
theorem OneHomClass.bound_of_antilipschitz {𝓕 : Type u_1} {E : Type u_3} {F : Type u_4} [] [] [FunLike 𝓕 E F] [OneHomClass 𝓕 E F] (f : 𝓕) {K : NNReal} (h : ) (x : E) :
x K * f x
theorem Isometry.nnnorm_map_of_map_zero {E : Type u_3} {F : Type u_4} {f : EF} (hi : ) (h₁ : f 0 = 0) (x : E) :
theorem Isometry.nnnorm_map_of_map_one {E : Type u_3} {F : Type u_4} [] [] {f : EF} (hi : ) (h₁ : f 1 = 1) (x : E) :
theorem lipschitzWith_one_norm' {E : Type u_3} [] :
theorem lipschitzWith_one_nnnorm' {E : Type u_3} [] :
LipschitzWith 1 nnnorm
theorem uniformContinuous_norm' {E : Type u_3} [] :
theorem uniformContinuous_nnnorm' {E : Type u_3} [] :
Equations
• =
Equations
• =
@[simp]
theorem dist_self_add_right {E : Type u_3} (a : E) (b : E) :
dist a (a + b) = b
@[simp]
theorem dist_self_mul_right {E : Type u_3} (a : E) (b : E) :
dist a (a * b) = b
@[simp]
theorem dist_self_add_left {E : Type u_3} (a : E) (b : E) :
dist (a + b) a = b
@[simp]
theorem dist_self_mul_left {E : Type u_3} (a : E) (b : E) :
dist (a * b) a = b
@[simp]
theorem dist_self_sub_right {E : Type u_3} (a : E) (b : E) :
dist a (a - b) = b
@[simp]
theorem dist_self_div_right {E : Type u_3} (a : E) (b : E) :
dist a (a / b) = b
@[simp]
theorem dist_self_sub_left {E : Type u_3} (a : E) (b : E) :
dist (a - b) a = b
@[simp]
theorem dist_self_div_left {E : Type u_3} (a : E) (b : E) :
dist (a / b) a = b
theorem dist_add_add_le {E : Type u_3} (a₁ : E) (a₂ : E) (b₁ : E) (b₂ : E) :
dist (a₁ + a₂) (b₁ + b₂) dist a₁ b₁ + dist a₂ b₂
theorem dist_mul_mul_le {E : Type u_3} (a₁ : E) (a₂ : E) (b₁ : E) (b₂ : E) :
dist (a₁ * a₂) (b₁ * b₂) dist a₁ b₁ + dist a₂ b₂
theorem dist_add_add_le_of_le {E : Type u_3} {a₁ : E} {a₂ : E} {b₁ : E} {b₂ : E} {r₁ : } {r₂ : } (h₁ : dist a₁ b₁ r₁) (h₂ : dist a₂ b₂ r₂) :
dist (a₁ + a₂) (b₁ + b₂) r₁ + r₂
theorem dist_mul_mul_le_of_le {E : Type u_3} {a₁ : E} {a₂ : E} {b₁ : E} {b₂ : E} {r₁ : } {r₂ : } (h₁ : dist a₁ b₁ r₁) (h₂ : dist a₂ b₂ r₂) :
dist (a₁ * a₂) (b₁ * b₂) r₁ + r₂
theorem dist_sub_sub_le {E : Type u_3} (a₁ : E) (a₂ : E) (b₁ : E) (b₂ : E) :
dist (a₁ - a₂) (b₁ - b₂) dist a₁ b₁ + dist a₂ b₂
theorem dist_div_div_le {E : Type u_3} (a₁ : E) (a₂ : E) (b₁ : E) (b₂ : E) :
dist (a₁ / a₂) (b₁ / b₂) dist a₁ b₁ + dist a₂ b₂
theorem dist_sub_sub_le_of_le {E : Type u_3} {a₁ : E} {a₂ : E} {b₁ : E} {b₂ : E} {r₁ : } {r₂ : } (h₁ : dist a₁ b₁ r₁) (h₂ : dist a₂ b₂ r₂) :
dist (a₁ - a₂) (b₁ - b₂) r₁ + r₂
theorem dist_div_div_le_of_le {E : Type u_3} {a₁ : E} {a₂ : E} {b₁ : E} {b₂ : E} {r₁ : } {r₂ : } (h₁ : dist a₁ b₁ r₁) (h₂ : dist a₂ b₂ r₂) :
dist (a₁ / a₂) (b₁ / b₂) r₁ + r₂
theorem abs_dist_sub_le_dist_add_add {E : Type u_3} (a₁ : E) (a₂ : E) (b₁ : E) (b₂ : E) :
|dist a₁ b₁ - dist a₂ b₂| dist (a₁ + a₂) (b₁ + b₂)
theorem abs_dist_sub_le_dist_mul_mul {E : Type u_3} (a₁ : E) (a₂ : E) (b₁ : E) (b₂ : E) :
|dist a₁ b₁ - dist a₂ b₂| dist (a₁ * a₂) (b₁ * b₂)
theorem nndist_add_add_le {E : Type u_3} (a₁ : E) (a₂ : E) (b₁ : E) (b₂ : E) :
nndist (a₁ + a₂) (b₁ + b₂) nndist a₁ b₁ + nndist a₂ b₂
theorem nndist_mul_mul_le {E : Type u_3} (a₁ : E) (a₂ : E) (b₁ : E) (b₂ : E) :
nndist (a₁ * a₂) (b₁ * b₂) nndist a₁ b₁ + nndist a₂ b₂
theorem edist_add_add_le {E : Type u_3} (a₁ : E) (a₂ : E) (b₁ : E) (b₂ : E) :
edist (a₁ + a₂) (b₁ + b₂) edist a₁ b₁ + edist a₂ b₂
theorem edist_mul_mul_le {E : Type u_3} (a₁ : E) (a₂ : E) (b₁ : E) (b₂ : E) :
edist (a₁ * a₂) (b₁ * b₂) edist a₁ b₁ + edist a₂ b₂
@[simp]
theorem lipschitzWith_neg_iff {α : Type u_5} {E : Type u_6} {K : NNReal} {f : αE} :
@[simp]
theorem lipschitzWith_inv_iff {α : Type u_5} {E : Type u_6} {K : NNReal} {f : αE} :
@[simp]
theorem antilipschitzWith_neg_iff {α : Type u_5} {E : Type u_6} {K : NNReal} {f : αE} :
@[simp]
theorem antilipschitzWith_inv_iff {α : Type u_5} {E : Type u_6} {K : NNReal} {f : αE} :
@[simp]
theorem lipschitzOnWith_neg_iff {α : Type u_5} {E : Type u_6} {K : NNReal} {f : αE} {s : Set α} :
@[simp]
theorem lipschitzOnWith_inv_iff {α : Type u_5} {E : Type u_6} {K : NNReal} {f : αE} {s : Set α} :
@[simp]
theorem locallyLipschitz_neg_iff {α : Type u_5} {E : Type u_6} {f : αE} :
@[simp]
theorem locallyLipschitz_inv_iff {α : Type u_5} {E : Type u_6} {f : αE} :
theorem LipschitzWith.inv {α : Type u_5} {E : Type u_6} {K : NNReal} {f : αE} :

Alias of the reverse direction of lipschitzWith_inv_iff.

theorem LipschitzWith.of_inv {α : Type u_5} {E : Type u_6} {K : NNReal} {f : αE} :

Alias of the forward direction of lipschitzWith_inv_iff.

theorem LipschitzWith.of_neg {α : Type u_5} {E : Type u_6} {K : NNReal} {f : αE} :
LipschitzWith K (-f)
theorem LipschitzWith.neg {α : Type u_5} {E : Type u_6} {K : NNReal} {f : αE} :
LipschitzWith K (-f)
theorem AntilipschitzWith.of_inv {α : Type u_5} {E : Type u_6} {K : NNReal} {f : αE} :

Alias of the forward direction of antilipschitzWith_inv_iff.

theorem AntilipschitzWith.inv {α : Type u_5} {E : Type u_6} {K : NNReal} {f : αE} :

Alias of the reverse direction of antilipschitzWith_inv_iff.

theorem AntilipschitzWith.of_neg {α : Type u_5} {E : Type u_6} {K : NNReal} {f : αE} :
theorem AntilipschitzWith.neg {α : Type u_5} {E : Type u_6} {K : NNReal} {f : αE} :
theorem LipschitzOnWith.inv {α : Type u_5} {E : Type u_6} {K : NNReal} {f : αE} {s : Set α} :

Alias of the reverse direction of lipschitzOnWith_inv_iff.

theorem LipschitzOnWith.of_inv {α : Type u_5} {E : Type u_6} {K : NNReal} {f : αE} {s : Set α} :

Alias of the forward direction of lipschitzOnWith_inv_iff.

theorem LipschitzOnWith.of_neg {α : Type u_5} {E : Type u_6} {K : NNReal} {f : αE} {s : Set α} :
LipschitzOnWith K (-f) s
theorem LipschitzOnWith.neg {α : Type u_5} {E : Type u_6} {K : NNReal} {f : αE} {s : Set α} :
LipschitzOnWith K (-f) s
theorem LocallyLipschitz.of_inv {α : Type u_5} {E : Type u_6} {f : αE} :

Alias of the forward direction of locallyLipschitz_inv_iff.

theorem LocallyLipschitz.inv {α : Type u_5} {E : Type u_6} {f : αE} :

Alias of the reverse direction of locallyLipschitz_inv_iff.

theorem LocallyLipschitz.of_neg {α : Type u_5} {E : Type u_6} {f : αE} :
theorem LocallyLipschitz.neg {α : Type u_5} {E : Type u_6} {f : αE} :
theorem LipschitzWith.add {α : Type u_5} {E : Type u_6} {Kf : NNReal} {Kg : NNReal} {f : αE} {g : αE} (hf : ) (hg : ) :
LipschitzWith (Kf + Kg) fun (x : α) => f x + g x
theorem LipschitzWith.mul' {α : Type u_5} {E : Type u_6} {Kf : NNReal} {Kg : NNReal} {f : αE} {g : αE} (hf : ) (hg : ) :
LipschitzWith (Kf + Kg) fun (x : α) => f x * g x
theorem LipschitzWith.sub {α : Type u_5} {E : Type u_6} {Kf : NNReal} {Kg : NNReal} {f : αE} {g : αE} (hf : ) (hg : ) :
LipschitzWith (Kf + Kg) fun (x : α) => f x - g x
theorem LipschitzWith.div {α : Type u_5} {E : Type u_6} {Kf : NNReal} {Kg : NNReal} {f : αE} {g : αE} (hf : ) (hg : ) :
LipschitzWith (Kf + Kg) fun (x : α) => f x / g x
theorem AntilipschitzWith.add_lipschitzWith {α : Type u_5} {E : Type u_6} {Kf : NNReal} {Kg : NNReal} {f : αE} {g : αE} (hf : ) (hg : ) (hK : Kg < Kf⁻¹) :
AntilipschitzWith (Kf⁻¹ - Kg)⁻¹ fun (x : α) => f x + g x
theorem AntilipschitzWith.mul_lipschitzWith {α : Type u_5} {E : Type u_6} {Kf : NNReal} {Kg : NNReal} {f : αE} {g : αE} (hf : ) (hg : ) (hK : Kg < Kf⁻¹) :
AntilipschitzWith (Kf⁻¹ - Kg)⁻¹ fun (x : α) => f x * g x
theorem AntilipschitzWith.add_sub_lipschitzWith {α : Type u_5} {E : Type u_6} {Kf : NNReal} {Kg : NNReal} {f : αE} {g : αE} (hf : ) (hg : LipschitzWith Kg (g - f)) (hK : Kg < Kf⁻¹) :
theorem AntilipschitzWith.mul_div_lipschitzWith {α : Type u_5} {E : Type u_6} {Kf : NNReal} {Kg : NNReal} {f : αE} {g : αE} (hf : ) (hg : LipschitzWith Kg (g / f)) (hK : Kg < Kf⁻¹) :
theorem AntilipschitzWith.le_mul_norm_sub {F : Type u_4} {E : Type u_6} {K : NNReal} {f : EF} (hf : ) (x : E) (y : E) :
x - y K * f x - f y
theorem AntilipschitzWith.le_mul_norm_div {F : Type u_4} {E : Type u_6} {K : NNReal} {f : EF} (hf : ) (x : E) (y : E) :
x / y K * f x / f y
@[instance 100]
Equations
• =
@[instance 100]
Equations
• =
@[instance 100]

A seminormed group is a uniform additive group, i.e., addition and subtraction are uniformly continuous.

Equations
• =
@[instance 100]

A seminormed group is a uniform group, i.e., multiplication and division are uniformly continuous.

Equations
• =
@[instance 100]
Equations
• =
@[instance 100]
Equations
• =
theorem cauchySeq_sum_of_eventually_eq {E : Type u_3} {u : E} {v : E} {N : } (huv : nN, u n = v n) (hv : CauchySeq fun (n : ) => kFinset.range (n + 1), v k) :
CauchySeq fun (n : ) => kFinset.range (n + 1), u k
theorem cauchySeq_prod_of_eventually_eq {E : Type u_3} {u : E} {v : E} {N : } (huv : nN, u n = v n) (hv : CauchySeq fun (n : ) => kFinset.range (n + 1), v k) :
CauchySeq fun (n : ) => kFinset.range (n + 1), u k