Documentation

Mathlib.Analysis.Normed.Group.Uniform

Normed groups are uniform groups #

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

theorem Isometry.norm_map_of_map_zero {E : Type u_3} {F : Type u_4} [SeminormedAddGroup E] [SeminormedAddGroup F] {f : EF} (hi : Isometry f) (h₁ : f 0 = 0) (x : E) :
theorem Isometry.norm_map_of_map_one {E : Type u_3} {F : Type u_4} [SeminormedGroup E] [SeminormedGroup F] {f : EF} (hi : Isometry f) (h₁ : f 1 = 1) (x : E) :
@[simp]
theorem dist_add_self_right {E : Type u_3} [SeminormedAddGroup E] (a : E) (b : E) :
dist b (a + b) = a
@[simp]
theorem dist_mul_self_right {E : Type u_3} [SeminormedGroup E] (a : E) (b : E) :
dist b (a * b) = a
@[simp]
theorem dist_add_self_left {E : Type u_3} [SeminormedAddGroup E] (a : E) (b : E) :
dist (a + b) b = a
@[simp]
theorem dist_mul_self_left {E : Type u_3} [SeminormedGroup E] (a : E) (b : E) :
dist (a * b) b = a
@[simp]
theorem dist_sub_eq_dist_add_left {E : Type u_3} [SeminormedAddGroup E] (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} [SeminormedGroup E] (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} [SeminormedAddGroup E] (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} [SeminormedGroup E] (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} [SeminormedAddGroup E] [SeminormedAddGroup F] [FunLike 𝓕 E F] [AddMonoidHomClass 𝓕 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} [SeminormedGroup E] [SeminormedGroup F] [FunLike 𝓕 E F] [MonoidHomClass 𝓕 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} [SeminormedAddGroup E] [SeminormedAddGroup F] {s : Set E} {f : EF} {C : NNReal} :
LipschitzOnWith C f s ∀ ⦃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} [SeminormedGroup E] [SeminormedGroup F] {s : Set E} {f : EF} {C : NNReal} :
LipschitzOnWith C f s ∀ ⦃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} [SeminormedGroup E] [SeminormedGroup F] {s : Set E} {f : EF} {C : NNReal} :
LipschitzOnWith C f s∀ ⦃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} [SeminormedAddGroup E] [SeminormedAddGroup F] {s : Set E} {f : EF} {C : NNReal} :
LipschitzOnWith C f s∀ ⦃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} [SeminormedAddGroup E] [SeminormedAddGroup F] {s : Set E} {a : E} {b : E} {r : } {f : EF} {C : NNReal} (h : LipschitzOnWith C f s) (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} [SeminormedGroup E] [SeminormedGroup F] {s : Set E} {a : E} {b : E} {r : } {f : EF} {C : NNReal} (h : LipschitzOnWith C f s) (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} [SeminormedAddGroup E] [SeminormedAddGroup F] {f : EF} {C : NNReal} :
LipschitzWith C f ∀ (x y : E), f x - f y C * x - y
theorem lipschitzWith_iff_norm_div_le {E : Type u_3} {F : Type u_4} [SeminormedGroup E] [SeminormedGroup F] {f : EF} {C : NNReal} :
LipschitzWith C f ∀ (x y : E), f x / f y C * x / y
theorem LipschitzWith.norm_div_le {E : Type u_3} {F : Type u_4} [SeminormedGroup E] [SeminormedGroup F] {f : EF} {C : NNReal} :
LipschitzWith C f∀ (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} [SeminormedAddGroup E] [SeminormedAddGroup F] {f : EF} {C : NNReal} :
LipschitzWith C f∀ (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} [SeminormedAddGroup E] [SeminormedAddGroup F] {a : E} {b : E} {r : } {f : EF} {C : NNReal} (h : LipschitzWith C f) (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} [SeminormedGroup E] [SeminormedGroup F] {a : E} {b : E} {r : } {f : EF} {C : NNReal} (h : LipschitzWith C f) (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} [SeminormedAddGroup E] [SeminormedAddGroup F] [FunLike 𝓕 E F] [AddMonoidHomClass 𝓕 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} [SeminormedGroup E] [SeminormedGroup F] [FunLike 𝓕 E F] [MonoidHomClass 𝓕 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} [SeminormedAddGroup E] [SeminormedAddGroup F] [FunLike 𝓕 E F] [AddMonoidHomClass 𝓕 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} [SeminormedGroup E] [SeminormedGroup F] [FunLike 𝓕 E F] [MonoidHomClass 𝓕 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} [SeminormedAddGroup E] [SeminormedAddGroup F] [FunLike 𝓕 E F] [AddMonoidHomClass 𝓕 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} [SeminormedGroup E] [SeminormedGroup F] [FunLike 𝓕 E F] [MonoidHomClass 𝓕 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} [SeminormedGroup E] [SeminormedGroup F] [FunLike 𝓕 E F] [MonoidHomClass 𝓕 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} [SeminormedAddGroup E] [SeminormedAddGroup F] [FunLike 𝓕 E F] [AddMonoidHomClass 𝓕 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} [SeminormedAddGroup E] [SeminormedAddGroup F] [FunLike 𝓕 E F] [AddMonoidHomClass 𝓕 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} [SeminormedGroup E] [SeminormedGroup F] [FunLike 𝓕 E F] [MonoidHomClass 𝓕 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} [SeminormedAddGroup E] [SeminormedAddGroup F] [FunLike 𝓕 E F] [AddMonoidHomClass 𝓕 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} [SeminormedGroup E] [SeminormedGroup F] [FunLike 𝓕 E F] [MonoidHomClass 𝓕 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} [SeminormedAddGroup E] [SeminormedAddGroup F] {f : EF} {K : NNReal} (h : LipschitzWith K f) (hf : f 0 = 0) (x : E) :
f x K * x
theorem LipschitzWith.norm_le_mul' {E : Type u_3} {F : Type u_4} [SeminormedGroup E] [SeminormedGroup F] {f : EF} {K : NNReal} (h : LipschitzWith K f) (hf : f 1 = 1) (x : E) :
f x K * x
theorem LipschitzWith.nnorm_le_mul {E : Type u_3} {F : Type u_4} [SeminormedAddGroup E] [SeminormedAddGroup F] {f : EF} {K : NNReal} (h : LipschitzWith K f) (hf : f 0 = 0) (x : E) :
theorem LipschitzWith.nnorm_le_mul' {E : Type u_3} {F : Type u_4} [SeminormedGroup E] [SeminormedGroup F] {f : EF} {K : NNReal} (h : LipschitzWith K f) (hf : f 1 = 1) (x : E) :
theorem AntilipschitzWith.le_mul_norm {E : Type u_3} {F : Type u_4} [SeminormedAddGroup E] [SeminormedAddGroup F] {f : EF} {K : NNReal} (h : AntilipschitzWith K f) (hf : f 0 = 0) (x : E) :
x K * f x
theorem AntilipschitzWith.le_mul_norm' {E : Type u_3} {F : Type u_4} [SeminormedGroup E] [SeminormedGroup F] {f : EF} {K : NNReal} (h : AntilipschitzWith K f) (hf : f 1 = 1) (x : E) :
x K * f x
theorem AntilipschitzWith.le_mul_nnnorm {E : Type u_3} {F : Type u_4} [SeminormedAddGroup E] [SeminormedAddGroup F] {f : EF} {K : NNReal} (h : AntilipschitzWith K f) (hf : f 0 = 0) (x : E) :
theorem AntilipschitzWith.le_mul_nnnorm' {E : Type u_3} {F : Type u_4} [SeminormedGroup E] [SeminormedGroup F] {f : EF} {K : NNReal} (h : AntilipschitzWith K f) (hf : f 1 = 1) (x : E) :
theorem ZeroHomClass.bound_of_antilipschitz {𝓕 : Type u_1} {E : Type u_3} {F : Type u_4} [SeminormedAddGroup E] [SeminormedAddGroup F] [FunLike 𝓕 E F] [ZeroHomClass 𝓕 E F] (f : 𝓕) {K : NNReal} (h : AntilipschitzWith K f) (x : E) :
x K * f x
theorem OneHomClass.bound_of_antilipschitz {𝓕 : Type u_1} {E : Type u_3} {F : Type u_4} [SeminormedGroup E] [SeminormedGroup F] [FunLike 𝓕 E F] [OneHomClass 𝓕 E F] (f : 𝓕) {K : NNReal} (h : AntilipschitzWith K f) (x : E) :
x K * f x
theorem Isometry.nnnorm_map_of_map_zero {E : Type u_3} {F : Type u_4} [SeminormedAddGroup E] [SeminormedAddGroup F] {f : EF} (hi : Isometry f) (h₁ : f 0 = 0) (x : E) :
theorem Isometry.nnnorm_map_of_map_one {E : Type u_3} {F : Type u_4} [SeminormedGroup E] [SeminormedGroup F] {f : EF} (hi : Isometry f) (h₁ : f 1 = 1) (x : E) :
@[simp]
theorem dist_self_add_right {E : Type u_3} [SeminormedAddCommGroup E] (a : E) (b : E) :
dist a (a + b) = b
@[simp]
theorem dist_self_mul_right {E : Type u_3} [SeminormedCommGroup E] (a : E) (b : E) :
dist a (a * b) = b
@[simp]
theorem dist_self_add_left {E : Type u_3} [SeminormedAddCommGroup E] (a : E) (b : E) :
dist (a + b) a = b
@[simp]
theorem dist_self_mul_left {E : Type u_3} [SeminormedCommGroup E] (a : E) (b : E) :
dist (a * b) a = b
@[simp]
theorem dist_self_sub_right {E : Type u_3} [SeminormedAddCommGroup E] (a : E) (b : E) :
dist a (a - b) = b
@[simp]
theorem dist_self_div_right {E : Type u_3} [SeminormedCommGroup E] (a : E) (b : E) :
dist a (a / b) = b
@[simp]
theorem dist_self_sub_left {E : Type u_3} [SeminormedAddCommGroup E] (a : E) (b : E) :
dist (a - b) a = b
@[simp]
theorem dist_self_div_left {E : Type u_3} [SeminormedCommGroup E] (a : E) (b : E) :
dist (a / b) a = b
theorem dist_add_add_le {E : Type u_3} [SeminormedAddCommGroup E] (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} [SeminormedCommGroup E] (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} [SeminormedAddCommGroup E] {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} [SeminormedCommGroup E] {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} [SeminormedAddCommGroup E] (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} [SeminormedCommGroup E] (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} [SeminormedAddCommGroup E] {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} [SeminormedCommGroup E] {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} [SeminormedAddCommGroup E] (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} [SeminormedCommGroup E] (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} [SeminormedAddCommGroup E] (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} [SeminormedCommGroup E] (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} [SeminormedAddCommGroup E] (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} [SeminormedCommGroup E] (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} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {K : NNReal} {f : αE} :
@[simp]
theorem lipschitzWith_inv_iff {α : Type u_5} {E : Type u_6} [SeminormedCommGroup E] [PseudoEMetricSpace α] {K : NNReal} {f : αE} :
@[simp]
theorem antilipschitzWith_neg_iff {α : Type u_5} {E : Type u_6} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {K : NNReal} {f : αE} :
@[simp]
@[simp]
theorem lipschitzOnWith_neg_iff {α : Type u_5} {E : Type u_6} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {K : NNReal} {f : αE} {s : Set α} :
@[simp]
theorem lipschitzOnWith_inv_iff {α : Type u_5} {E : Type u_6} [SeminormedCommGroup E] [PseudoEMetricSpace α] {K : NNReal} {f : αE} {s : Set α} :
@[simp]
theorem locallyLipschitzOn_neg_iff {α : Type u_5} {E : Type u_6} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {f : αE} {s : Set α} :
@[simp]
theorem locallyLipschitzOn_inv_iff {α : Type u_5} {E : Type u_6} [SeminormedCommGroup E] [PseudoEMetricSpace α] {f : αE} {s : Set α} :
theorem LipschitzWith.of_inv {α : Type u_5} {E : Type u_6} [SeminormedCommGroup E] [PseudoEMetricSpace α] {K : NNReal} {f : αE} :

Alias of the forward direction of lipschitzWith_inv_iff.

theorem LipschitzWith.inv {α : Type u_5} {E : Type u_6} [SeminormedCommGroup E] [PseudoEMetricSpace α] {K : NNReal} {f : αE} :

Alias of the reverse direction of lipschitzWith_inv_iff.

theorem LipschitzWith.neg {α : Type u_5} {E : Type u_6} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {K : NNReal} {f : αE} :
theorem LipschitzWith.of_neg {α : Type u_5} {E : Type u_6} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {K : NNReal} {f : αE} :
theorem AntilipschitzWith.inv {α : Type u_5} {E : Type u_6} [SeminormedCommGroup E] [PseudoEMetricSpace α] {K : NNReal} {f : αE} :

Alias of the reverse direction of antilipschitzWith_inv_iff.

theorem AntilipschitzWith.of_inv {α : Type u_5} {E : Type u_6} [SeminormedCommGroup E] [PseudoEMetricSpace α] {K : NNReal} {f : αE} :

Alias of the forward direction of antilipschitzWith_inv_iff.

theorem AntilipschitzWith.neg {α : Type u_5} {E : Type u_6} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {K : NNReal} {f : αE} :
theorem AntilipschitzWith.of_neg {α : Type u_5} {E : Type u_6} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {K : NNReal} {f : αE} :
theorem LipschitzOnWith.of_inv {α : Type u_5} {E : Type u_6} [SeminormedCommGroup E] [PseudoEMetricSpace α] {K : NNReal} {f : αE} {s : Set α} :

Alias of the forward direction of lipschitzOnWith_inv_iff.

theorem LipschitzOnWith.inv {α : Type u_5} {E : Type u_6} [SeminormedCommGroup E] [PseudoEMetricSpace α] {K : NNReal} {f : αE} {s : Set α} :

Alias of the reverse direction of lipschitzOnWith_inv_iff.

theorem LipschitzOnWith.neg {α : Type u_5} {E : Type u_6} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {K : NNReal} {f : αE} {s : Set α} :
theorem LipschitzOnWith.of_neg {α : Type u_5} {E : Type u_6} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {K : NNReal} {f : αE} {s : Set α} :
theorem LocallyLipschitz.inv {α : Type u_5} {E : Type u_6} [SeminormedCommGroup E] [PseudoEMetricSpace α] {f : αE} :

Alias of the reverse direction of locallyLipschitz_inv_iff.

Alias of the forward direction of locallyLipschitz_inv_iff.

theorem LocallyLipschitzOn.of_inv {α : Type u_5} {E : Type u_6} [SeminormedCommGroup E] [PseudoEMetricSpace α] {f : αE} {s : Set α} :

Alias of the forward direction of locallyLipschitzOn_inv_iff.

theorem LocallyLipschitzOn.inv {α : Type u_5} {E : Type u_6} [SeminormedCommGroup E] [PseudoEMetricSpace α] {f : αE} {s : Set α} :

Alias of the reverse direction of locallyLipschitzOn_inv_iff.

theorem LocallyLipschitzOn.neg {α : Type u_5} {E : Type u_6} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {f : αE} {s : Set α} :
theorem LocallyLipschitzOn.of_neg {α : Type u_5} {E : Type u_6} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {f : αE} {s : Set α} :
theorem LipschitzOnWith.add {α : Type u_5} {E : Type u_6} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {Kf : NNReal} {Kg : NNReal} {f : αE} {g : αE} {s : Set α} (hf : LipschitzOnWith Kf f s) (hg : LipschitzOnWith Kg g s) :
LipschitzOnWith (Kf + Kg) (fun (x : α) => f x + g x) s
theorem LipschitzOnWith.mul {α : Type u_5} {E : Type u_6} [SeminormedCommGroup E] [PseudoEMetricSpace α] {Kf : NNReal} {Kg : NNReal} {f : αE} {g : αE} {s : Set α} (hf : LipschitzOnWith Kf f s) (hg : LipschitzOnWith Kg g s) :
LipschitzOnWith (Kf + Kg) (fun (x : α) => f x * g x) s
theorem LipschitzWith.add {α : Type u_5} {E : Type u_6} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {Kf : NNReal} {Kg : NNReal} {f : αE} {g : αE} (hf : LipschitzWith Kf f) (hg : LipschitzWith Kg g) :
LipschitzWith (Kf + Kg) fun (x : α) => f x + g x
theorem LipschitzWith.mul {α : Type u_5} {E : Type u_6} [SeminormedCommGroup E] [PseudoEMetricSpace α] {Kf : NNReal} {Kg : NNReal} {f : αE} {g : αE} (hf : LipschitzWith Kf f) (hg : LipschitzWith Kg g) :
LipschitzWith (Kf + Kg) fun (x : α) => f x * g x
@[deprecated LipschitzWith.mul]
theorem LipschitzWith.mul' {α : Type u_5} {E : Type u_6} [SeminormedCommGroup E] [PseudoEMetricSpace α] {Kf : NNReal} {Kg : NNReal} {f : αE} {g : αE} (hf : LipschitzWith Kf f) (hg : LipschitzWith Kg g) :
LipschitzWith (Kf + Kg) fun (x : α) => f x * g x

Alias of LipschitzWith.mul.

theorem LocallyLipschitzOn.add {α : Type u_5} {E : Type u_6} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {f : αE} {g : αE} {s : Set α} (hf : LocallyLipschitzOn s f) (hg : LocallyLipschitzOn s g) :
LocallyLipschitzOn s fun (x : α) => f x + g x
theorem LocallyLipschitzOn.mul {α : Type u_5} {E : Type u_6} [SeminormedCommGroup E] [PseudoEMetricSpace α] {f : αE} {g : αE} {s : Set α} (hf : LocallyLipschitzOn s f) (hg : LocallyLipschitzOn s g) :
LocallyLipschitzOn s fun (x : α) => f x * g x
theorem LocallyLipschitz.add {α : Type u_5} {E : Type u_6} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {f : αE} {g : αE} (hf : LocallyLipschitz f) (hg : LocallyLipschitz g) :
LocallyLipschitz fun (x : α) => f x + g x
theorem LocallyLipschitz.mul {α : Type u_5} {E : Type u_6} [SeminormedCommGroup E] [PseudoEMetricSpace α] {f : αE} {g : αE} (hf : LocallyLipschitz f) (hg : LocallyLipschitz g) :
LocallyLipschitz fun (x : α) => f x * g x
theorem LipschitzOnWith.sub {α : Type u_5} {E : Type u_6} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {Kf : NNReal} {Kg : NNReal} {f : αE} {g : αE} {s : Set α} (hf : LipschitzOnWith Kf f s) (hg : LipschitzOnWith Kg g s) :
LipschitzOnWith (Kf + Kg) (fun (x : α) => f x - g x) s
theorem LipschitzOnWith.div {α : Type u_5} {E : Type u_6} [SeminormedCommGroup E] [PseudoEMetricSpace α] {Kf : NNReal} {Kg : NNReal} {f : αE} {g : αE} {s : Set α} (hf : LipschitzOnWith Kf f s) (hg : LipschitzOnWith Kg g s) :
LipschitzOnWith (Kf + Kg) (fun (x : α) => f x / g x) s
theorem LipschitzWith.sub {α : Type u_5} {E : Type u_6} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {Kf : NNReal} {Kg : NNReal} {f : αE} {g : αE} (hf : LipschitzWith Kf f) (hg : LipschitzWith Kg g) :
LipschitzWith (Kf + Kg) fun (x : α) => f x - g x
theorem LipschitzWith.div {α : Type u_5} {E : Type u_6} [SeminormedCommGroup E] [PseudoEMetricSpace α] {Kf : NNReal} {Kg : NNReal} {f : αE} {g : αE} (hf : LipschitzWith Kf f) (hg : LipschitzWith Kg g) :
LipschitzWith (Kf + Kg) fun (x : α) => f x / g x
theorem LocallyLipschitzOn.sub {α : Type u_5} {E : Type u_6} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {f : αE} {g : αE} {s : Set α} (hf : LocallyLipschitzOn s f) (hg : LocallyLipschitzOn s g) :
LocallyLipschitzOn s fun (x : α) => f x - g x
theorem LocallyLipschitzOn.div {α : Type u_5} {E : Type u_6} [SeminormedCommGroup E] [PseudoEMetricSpace α] {f : αE} {g : αE} {s : Set α} (hf : LocallyLipschitzOn s f) (hg : LocallyLipschitzOn s g) :
LocallyLipschitzOn s fun (x : α) => f x / g x
theorem LocallyLipschitz.sub {α : Type u_5} {E : Type u_6} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {f : αE} {g : αE} (hf : LocallyLipschitz f) (hg : LocallyLipschitz g) :
LocallyLipschitz fun (x : α) => f x - g x
theorem LocallyLipschitz.div {α : Type u_5} {E : Type u_6} [SeminormedCommGroup E] [PseudoEMetricSpace α] {f : αE} {g : αE} (hf : LocallyLipschitz f) (hg : LocallyLipschitz g) :
LocallyLipschitz fun (x : α) => f x / g x
theorem AntilipschitzWith.add_lipschitzWith {α : Type u_5} {E : Type u_6} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {Kf : NNReal} {Kg : NNReal} {f : αE} {g : αE} (hf : AntilipschitzWith Kf f) (hg : LipschitzWith Kg g) (hK : Kg < Kf⁻¹) :
AntilipschitzWith (Kf⁻¹ - Kg)⁻¹ fun (x : α) => f x + g x
theorem AntilipschitzWith.mul_lipschitzWith {α : Type u_5} {E : Type u_6} [SeminormedCommGroup E] [PseudoEMetricSpace α] {Kf : NNReal} {Kg : NNReal} {f : αE} {g : αE} (hf : AntilipschitzWith Kf f) (hg : LipschitzWith Kg g) (hK : Kg < Kf⁻¹) :
AntilipschitzWith (Kf⁻¹ - Kg)⁻¹ fun (x : α) => f x * g x
theorem AntilipschitzWith.add_sub_lipschitzWith {α : Type u_5} {E : Type u_6} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {Kf : NNReal} {Kg : NNReal} {f : αE} {g : αE} (hf : AntilipschitzWith Kf f) (hg : LipschitzWith Kg (g - f)) (hK : Kg < Kf⁻¹) :
theorem AntilipschitzWith.mul_div_lipschitzWith {α : Type u_5} {E : Type u_6} [SeminormedCommGroup E] [PseudoEMetricSpace α] {Kf : NNReal} {Kg : NNReal} {f : αE} {g : αE} (hf : AntilipschitzWith Kf f) (hg : LipschitzWith Kg (g / f)) (hK : Kg < Kf⁻¹) :
theorem AntilipschitzWith.le_mul_norm_sub {F : Type u_4} [SeminormedAddCommGroup F] {E : Type u_6} [SeminormedAddCommGroup E] {K : NNReal} {f : EF} (hf : AntilipschitzWith K f) (x : E) (y : E) :
x - y K * f x - f y
theorem AntilipschitzWith.le_mul_norm_div {F : Type u_4} [SeminormedCommGroup F] {E : Type u_6} [SeminormedCommGroup E] {K : NNReal} {f : EF} (hf : AntilipschitzWith K f) (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
  • =

SeparationQuotient #

Equations
Equations
Equations
Equations
theorem cauchySeq_sum_of_eventually_eq {E : Type u_3} [SeminormedAddCommGroup E] {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} [SeminormedCommGroup E] {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.norm_bddAbove {G : Type u_5} [SeminormedAddGroup G] {u : G} (hu : CauchySeq u) :
BddAbove (Set.range fun (n : ) => u n)
theorem CauchySeq.mul_norm_bddAbove {G : Type u_5} [SeminormedGroup G] {u : G} (hu : CauchySeq u) :
BddAbove (Set.range fun (n : ) => u n)