Normed groups are uniform groups #

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

source

instance NormedAddGroup.to_isometricVAdd_right {E : Type u_3} [SeminormedAddGroup E] :

IsometricVAdd Eᵃᵒᵖ E

Equations

⋯ = ⋯

source

instance NormedGroup.to_isometricSMul_right {E : Type u_3} [SeminormedGroup E] :

IsometricSMul Eᵐᵒᵖ E

Equations

⋯ = ⋯

source

theorem Isometry.norm_map_of_map_zero {E : Type u_3} {F : Type u_4} [SeminormedAddGroup E] [SeminormedAddGroup F] {f : E → F} (hi : Isometry f) (h₁ : f 0 = 0) (x : E) :

‖f x‖ = ‖x‖

source

theorem Isometry.norm_map_of_map_one {E : Type u_3} {F : Type u_4} [SeminormedGroup E] [SeminormedGroup F] {f : E → F} (hi : Isometry f) (h₁ : f 1 = 1) (x : E) :

‖f x‖ = ‖x‖

source

@[simp]

theorem dist_add_self_right {E : Type u_3} [SeminormedAddGroup E] (a : E) (b : E) :

dist b (a + b) = ‖a‖

source

@[simp]

theorem dist_mul_self_right {E : Type u_3} [SeminormedGroup E] (a : E) (b : E) :

dist b (a * b) = ‖a‖

source

@[simp]

theorem dist_add_self_left {E : Type u_3} [SeminormedAddGroup E] (a : E) (b : E) :

dist (a + b) b = ‖a‖

source

@[simp]

theorem dist_mul_self_left {E : Type u_3} [SeminormedGroup E] (a : E) (b : E) :

dist (a * b) b = ‖a‖

source

@[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)

source

@[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)

source

@[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

source

@[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

source

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.

source

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

source

theorem lipschitzOnWith_iff_norm_sub_le {E : Type u_3} {F : Type u_4} [SeminormedAddGroup E] [SeminormedAddGroup F] {s : Set E} {f : E → F} {C : NNReal} :

LipschitzOnWith C f s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ‖f x - f y‖ ≤ ↑C * ‖x - y‖

source

theorem lipschitzOnWith_iff_norm_div_le {E : Type u_3} {F : Type u_4} [SeminormedGroup E] [SeminormedGroup F] {s : Set E} {f : E → F} {C : NNReal} :

LipschitzOnWith C f s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ‖f x / f y‖ ≤ ↑C * ‖x / y‖

source

theorem LipschitzOnWith.norm_div_le {E : Type u_3} {F : Type u_4} [SeminormedGroup E] [SeminormedGroup F] {s : Set E} {f : E → F} {C : NNReal} :

LipschitzOnWith C f s → ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ‖f x / f y‖ ≤ ↑C * ‖x / y‖

Alias of the forward direction of lipschitzOnWith_iff_norm_div_le.

source

theorem LipschitzOnWith.norm_sub_le {E : Type u_3} {F : Type u_4} [SeminormedAddGroup E] [SeminormedAddGroup F] {s : Set E} {f : E → F} {C : NNReal} :

LipschitzOnWith C f s → ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ‖f x - f y‖ ≤ ↑C * ‖x - y‖

source

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 : E → F} {C : NNReal} (h : LipschitzOnWith C f s) (ha : a ∈ s) (hb : b ∈ s) (hr : ‖a - b‖ ≤ r) :

‖f a - f b‖ ≤ ↑C * r

source

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 : E → F} {C : NNReal} (h : LipschitzOnWith C f s) (ha : a ∈ s) (hb : b ∈ s) (hr : ‖a / b‖ ≤ r) :

‖f a / f b‖ ≤ ↑C * r

source

theorem lipschitzWith_iff_norm_sub_le {E : Type u_3} {F : Type u_4} [SeminormedAddGroup E] [SeminormedAddGroup F] {f : E → F} {C : NNReal} :

LipschitzWith C f ↔ ∀ (x y : E), ‖f x - f y‖ ≤ ↑C * ‖x - y‖

source

theorem lipschitzWith_iff_norm_div_le {E : Type u_3} {F : Type u_4} [SeminormedGroup E] [SeminormedGroup F] {f : E → F} {C : NNReal} :

LipschitzWith C f ↔ ∀ (x y : E), ‖f x / f y‖ ≤ ↑C * ‖x / y‖

source

theorem LipschitzWith.norm_div_le {E : Type u_3} {F : Type u_4} [SeminormedGroup E] [SeminormedGroup F] {f : E → F} {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.

source

theorem LipschitzWith.norm_sub_le {E : Type u_3} {F : Type u_4} [SeminormedAddGroup E] [SeminormedAddGroup F] {f : E → F} {C : NNReal} :

LipschitzWith C f → ∀ (x y : E), ‖f x - f y‖ ≤ ↑C * ‖x - y‖

source

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 : E → F} {C : NNReal} (h : LipschitzWith C f) (hr : ‖a - b‖ ≤ r) :

‖f a - f b‖ ≤ ↑C * r

source

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 : E → F} {C : NNReal} (h : LipschitzWith C f) (hr : ‖a / b‖ ≤ r) :

‖f a / f b‖ ≤ ↑C * r

source

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‖) :

Continuous ⇑f

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‖

source

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‖) :

Continuous ⇑f

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‖.

source

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‖) :

UniformContinuous ⇑f

source

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‖) :

UniformContinuous ⇑f

source

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‖

source

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‖

source

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.

source

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

source

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‖₊) :

LipschitzWith C ⇑f

source

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‖₊) :

LipschitzWith C ⇑f

source

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‖) :

AntilipschitzWith K ⇑f

source

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‖) :

AntilipschitzWith K ⇑f

source

theorem LipschitzWith.norm_le_mul {E : Type u_3} {F : Type u_4} [SeminormedAddGroup E] [SeminormedAddGroup F] {f : E → F} {K : NNReal} (h : LipschitzWith K f) (hf : f 0 = 0) (x : E) :

‖f x‖ ≤ ↑K * ‖x‖

source

theorem LipschitzWith.norm_le_mul' {E : Type u_3} {F : Type u_4} [SeminormedGroup E] [SeminormedGroup F] {f : E → F} {K : NNReal} (h : LipschitzWith K f) (hf : f 1 = 1) (x : E) :

‖f x‖ ≤ ↑K * ‖x‖

source

theorem LipschitzWith.nnorm_le_mul {E : Type u_3} {F : Type u_4} [SeminormedAddGroup E] [SeminormedAddGroup F] {f : E → F} {K : NNReal} (h : LipschitzWith K f) (hf : f 0 = 0) (x : E) :

‖f x‖₊ ≤ K * ‖x‖₊

source

theorem LipschitzWith.nnorm_le_mul' {E : Type u_3} {F : Type u_4} [SeminormedGroup E] [SeminormedGroup F] {f : E → F} {K : NNReal} (h : LipschitzWith K f) (hf : f 1 = 1) (x : E) :

‖f x‖₊ ≤ K * ‖x‖₊

source

theorem AntilipschitzWith.le_mul_norm {E : Type u_3} {F : Type u_4} [SeminormedAddGroup E] [SeminormedAddGroup F] {f : E → F} {K : NNReal} (h : AntilipschitzWith K f) (hf : f 0 = 0) (x : E) :

‖x‖ ≤ ↑K * ‖f x‖

source

theorem AntilipschitzWith.le_mul_norm' {E : Type u_3} {F : Type u_4} [SeminormedGroup E] [SeminormedGroup F] {f : E → F} {K : NNReal} (h : AntilipschitzWith K f) (hf : f 1 = 1) (x : E) :

‖x‖ ≤ ↑K * ‖f x‖

source

theorem AntilipschitzWith.le_mul_nnnorm {E : Type u_3} {F : Type u_4} [SeminormedAddGroup E] [SeminormedAddGroup F] {f : E → F} {K : NNReal} (h : AntilipschitzWith K f) (hf : f 0 = 0) (x : E) :

‖x‖₊ ≤ K * ‖f x‖₊

source

theorem AntilipschitzWith.le_mul_nnnorm' {E : Type u_3} {F : Type u_4} [SeminormedGroup E] [SeminormedGroup F] {f : E → F} {K : NNReal} (h : AntilipschitzWith K f) (hf : f 1 = 1) (x : E) :

‖x‖₊ ≤ K * ‖f x‖₊

source

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‖

source

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‖

source

theorem Isometry.nnnorm_map_of_map_zero {E : Type u_3} {F : Type u_4} [SeminormedAddGroup E] [SeminormedAddGroup F] {f : E → F} (hi : Isometry f) (h₁ : f 0 = 0) (x : E) :

‖f x‖₊ = ‖x‖₊

source

theorem Isometry.nnnorm_map_of_map_one {E : Type u_3} {F : Type u_4} [SeminormedGroup E] [SeminormedGroup F] {f : E → F} (hi : Isometry f) (h₁ : f 1 = 1) (x : E) :

‖f x‖₊ = ‖x‖₊

source

theorem lipschitzWith_one_norm {E : Type u_3} [SeminormedAddGroup E] :

LipschitzWith 1 norm

source

theorem lipschitzWith_one_norm' {E : Type u_3} [SeminormedGroup E] :

LipschitzWith 1 norm

source

theorem lipschitzWith_one_nnnorm {E : Type u_3} [SeminormedAddGroup E] :

LipschitzWith 1 nnnorm

source

theorem lipschitzWith_one_nnnorm' {E : Type u_3} [SeminormedGroup E] :

LipschitzWith 1 nnnorm

source

theorem uniformContinuous_norm {E : Type u_3} [SeminormedAddGroup E] :

UniformContinuous norm

source

theorem uniformContinuous_norm' {E : Type u_3} [SeminormedGroup E] :

UniformContinuous norm

source

theorem uniformContinuous_nnnorm {E : Type u_3} [SeminormedAddGroup E] :

UniformContinuous fun (a : E) => ‖a‖₊

source

theorem uniformContinuous_nnnorm' {E : Type u_3} [SeminormedGroup E] :

UniformContinuous fun (a : E) => ‖a‖₊

source

instance NormedAddGroup.to_isometricVAdd_left {E : Type u_3} [SeminormedAddCommGroup E] :

IsometricVAdd E E

Equations

⋯ = ⋯

source

instance NormedGroup.to_isometricSMul_left {E : Type u_3} [SeminormedCommGroup E] :

IsometricSMul E E

Equations

⋯ = ⋯

source

@[simp]

theorem dist_self_add_right {E : Type u_3} [SeminormedAddCommGroup E] (a : E) (b : E) :

dist a (a + b) = ‖b‖

source

@[simp]

theorem dist_self_mul_right {E : Type u_3} [SeminormedCommGroup E] (a : E) (b : E) :

dist a (a * b) = ‖b‖

source

@[simp]

theorem dist_self_add_left {E : Type u_3} [SeminormedAddCommGroup E] (a : E) (b : E) :

dist (a + b) a = ‖b‖

source

@[simp]

theorem dist_self_mul_left {E : Type u_3} [SeminormedCommGroup E] (a : E) (b : E) :

dist (a * b) a = ‖b‖

source

@[simp]

theorem dist_self_sub_right {E : Type u_3} [SeminormedAddCommGroup E] (a : E) (b : E) :

dist a (a - b) = ‖b‖

source

@[simp]

theorem dist_self_div_right {E : Type u_3} [SeminormedCommGroup E] (a : E) (b : E) :

dist a (a / b) = ‖b‖

source

@[simp]

theorem dist_self_sub_left {E : Type u_3} [SeminormedAddCommGroup E] (a : E) (b : E) :

dist (a - b) a = ‖b‖

source

@[simp]

theorem dist_self_div_left {E : Type u_3} [SeminormedCommGroup E] (a : E) (b : E) :

dist (a / b) a = ‖b‖

source

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₂

source

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₂

source

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₂

source

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₂

source

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₂

source

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₂

source

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₂

source

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₂

source

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₂)

source

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₂)

source

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₂

source

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₂

source

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₂

source

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₂

source

@[simp]

theorem lipschitzWith_neg_iff {α : Type u_5} {E : Type u_6} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {K : NNReal} {f : α → E} :

LipschitzWith K (-f) ↔ LipschitzWith K f

source

@[simp]

theorem lipschitzWith_inv_iff {α : Type u_5} {E : Type u_6} [SeminormedCommGroup E] [PseudoEMetricSpace α] {K : NNReal} {f : α → E} :

LipschitzWith K f⁻¹ ↔ LipschitzWith K f

source

@[simp]

theorem antilipschitzWith_neg_iff {α : Type u_5} {E : Type u_6} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {K : NNReal} {f : α → E} :

AntilipschitzWith K (-f) ↔ AntilipschitzWith K f

source

@[simp]

theorem antilipschitzWith_inv_iff {α : Type u_5} {E : Type u_6} [SeminormedCommGroup E] [PseudoEMetricSpace α] {K : NNReal} {f : α → E} :

AntilipschitzWith K f⁻¹ ↔ AntilipschitzWith K f

source

@[simp]

theorem lipschitzOnWith_neg_iff {α : Type u_5} {E : Type u_6} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {K : NNReal} {f : α → E} {s : Set α} :

LipschitzOnWith K (-f) s ↔ LipschitzOnWith K f s

source

@[simp]

theorem lipschitzOnWith_inv_iff {α : Type u_5} {E : Type u_6} [SeminormedCommGroup E] [PseudoEMetricSpace α] {K : NNReal} {f : α → E} {s : Set α} :

LipschitzOnWith K f⁻¹ s ↔ LipschitzOnWith K f s

source

@[simp]

theorem locallyLipschitz_neg_iff {α : Type u_5} {E : Type u_6} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {f : α → E} :

LocallyLipschitz (-f) ↔ LocallyLipschitz f

source

@[simp]

theorem locallyLipschitz_inv_iff {α : Type u_5} {E : Type u_6} [SeminormedCommGroup E] [PseudoEMetricSpace α] {f : α → E} :

LocallyLipschitz f⁻¹ ↔ LocallyLipschitz f

source

@[simp]

theorem locallyLipschitzOn_neg_iff {α : Type u_5} {E : Type u_6} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {f : α → E} {s : Set α} :

LocallyLipschitzOn s (-f) ↔ LocallyLipschitzOn s f

source

@[simp]

theorem locallyLipschitzOn_inv_iff {α : Type u_5} {E : Type u_6} [SeminormedCommGroup E] [PseudoEMetricSpace α] {f : α → E} {s : Set α} :

LocallyLipschitzOn s f⁻¹ ↔ LocallyLipschitzOn s f

source

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

LipschitzWith K f → LipschitzWith K f⁻¹

Alias of the reverse direction of lipschitzWith_inv_iff.

source

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

LipschitzWith K f⁻¹ → LipschitzWith K f

Alias of the forward direction of lipschitzWith_inv_iff.

source

theorem LipschitzWith.of_neg {α : Type u_5} {E : Type u_6} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {K : NNReal} {f : α → E} :

LipschitzWith K (-f) → LipschitzWith K f

source

theorem LipschitzWith.neg {α : Type u_5} {E : Type u_6} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {K : NNReal} {f : α → E} :

LipschitzWith K f → LipschitzWith K (-f)

source

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

AntilipschitzWith K f → AntilipschitzWith K f⁻¹

Alias of the reverse direction of antilipschitzWith_inv_iff.

source

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

AntilipschitzWith K f⁻¹ → AntilipschitzWith K f

Alias of the forward direction of antilipschitzWith_inv_iff.

source

theorem AntilipschitzWith.neg {α : Type u_5} {E : Type u_6} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {K : NNReal} {f : α → E} :

AntilipschitzWith K f → AntilipschitzWith K (-f)

source

theorem AntilipschitzWith.of_neg {α : Type u_5} {E : Type u_6} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {K : NNReal} {f : α → E} :

AntilipschitzWith K (-f) → AntilipschitzWith K f

source

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

LipschitzOnWith K f⁻¹ s → LipschitzOnWith K f s

Alias of the forward direction of lipschitzOnWith_inv_iff.

source

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

LipschitzOnWith K f s → LipschitzOnWith K f⁻¹ s

Alias of the reverse direction of lipschitzOnWith_inv_iff.

source

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

LipschitzOnWith K (-f) s → LipschitzOnWith K f s

source

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

LipschitzOnWith K f s → LipschitzOnWith K (-f) s

source

theorem LocallyLipschitz.of_inv {α : Type u_5} {E : Type u_6} [SeminormedCommGroup E] [PseudoEMetricSpace α] {f : α → E} :

LocallyLipschitz f⁻¹ → LocallyLipschitz f

Alias of the forward direction of locallyLipschitz_inv_iff.

source

theorem LocallyLipschitz.inv {α : Type u_5} {E : Type u_6} [SeminormedCommGroup E] [PseudoEMetricSpace α] {f : α → E} :

LocallyLipschitz f → LocallyLipschitz f⁻¹

Alias of the reverse direction of locallyLipschitz_inv_iff.

source

theorem LocallyLipschitz.of_neg {α : Type u_5} {E : Type u_6} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {f : α → E} :

LocallyLipschitz (-f) → LocallyLipschitz f

source

theorem LocallyLipschitz.neg {α : Type u_5} {E : Type u_6} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {f : α → E} :

LocallyLipschitz f → LocallyLipschitz (-f)

source

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

LocallyLipschitzOn s f → LocallyLipschitzOn s f⁻¹

Alias of the reverse direction of locallyLipschitzOn_inv_iff.

source

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

LocallyLipschitzOn s f⁻¹ → LocallyLipschitzOn s f

Alias of the forward direction of locallyLipschitzOn_inv_iff.

source

theorem LocallyLipschitzOn.of_neg {α : Type u_5} {E : Type u_6} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {f : α → E} {s : Set α} :

LocallyLipschitzOn s (-f) → LocallyLipschitzOn s f

source

theorem LocallyLipschitzOn.neg {α : Type u_5} {E : Type u_6} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {f : α → E} {s : Set α} :

LocallyLipschitzOn s f → LocallyLipschitzOn s (-f)

source

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

source

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

source

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

source

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

source

@[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.

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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⁻¹) :

AntilipschitzWith (Kf⁻¹ - Kg)⁻¹ g

source

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⁻¹) :

AntilipschitzWith (Kf⁻¹ - Kg)⁻¹ g

source

theorem AntilipschitzWith.le_mul_norm_sub {F : Type u_4} [SeminormedAddCommGroup F] {E : Type u_6} [SeminormedAddCommGroup E] {K : NNReal} {f : E → F} (hf : AntilipschitzWith K f) (x : E) (y : E) :

‖x - y‖ ≤ ↑K * ‖f x - f y‖

source

theorem AntilipschitzWith.le_mul_norm_div {F : Type u_4} [SeminormedCommGroup F] {E : Type u_6} [SeminormedCommGroup E] {K : NNReal} {f : E → F} (hf : AntilipschitzWith K f) (x : E) (y : E) :

‖x / y‖ ≤ ↑K * ‖f x / f y‖

source

@[instance 100]

instance SeminormedAddCommGroup.to_lipschitzAdd {E : Type u_3} [SeminormedAddCommGroup E] :

LipschitzAdd E

Equations

⋯ = ⋯

source

@[instance 100]

instance SeminormedCommGroup.to_lipschitzMul {E : Type u_3} [SeminormedCommGroup E] :

LipschitzMul E

Equations

⋯ = ⋯

source

@[instance 100]

instance SeminormedAddCommGroup.to_uniformAddGroup {E : Type u_3} [SeminormedAddCommGroup E] :

UniformAddGroup E

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

Equations

⋯ = ⋯

source

@[instance 100]

instance SeminormedCommGroup.to_uniformGroup {E : Type u_3} [SeminormedCommGroup E] :

UniformGroup E

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

Equations

⋯ = ⋯

source

@[instance 100]

instance SeminormedAddCommGroup.toTopologicalAddGroup {E : Type u_3} [SeminormedAddCommGroup E] :

TopologicalAddGroup E

Equations

⋯ = ⋯

source

@[instance 100]

instance SeminormedCommGroup.toTopologicalGroup {E : Type u_3} [SeminormedCommGroup E] :

TopologicalGroup E

Equations

⋯ = ⋯

SeparationQuotient #

source

instance SeparationQuotient.instNorm {E : Type u_3} [SeminormedAddCommGroup E] :

Norm (SeparationQuotient E)

Equations

SeparationQuotient.instNorm = { norm := SeparationQuotient.lift norm ⋯ }

source

theorem SeparationQuotient.instNorm.proof_1 {E : Type u_1} [SeminormedAddCommGroup E] :

∀ (x x_1 : E), Inseparable x x_1 → ‖x‖ = ‖x_1‖

source

instance SeparationQuotient.instMulNorm {E : Type u_3} [SeminormedCommGroup E] :

Norm (SeparationQuotient E)

Equations

SeparationQuotient.instMulNorm = { norm := SeparationQuotient.lift norm ⋯ }

source

@[simp]

theorem SeparationQuotient.norm_mk {E : Type u_3} [SeminormedAddCommGroup E] (p : E) :

‖SeparationQuotient.mk p‖ = ‖p‖

source

@[simp]

theorem SeparationQuotient.norm_mk' {E : Type u_3} [SeminormedCommGroup E] (p : E) :

‖SeparationQuotient.mk p‖ = ‖p‖

source

instance SeparationQuotient.instNormedAddCommGroup {E : Type u_3} [SeminormedAddCommGroup E] :

NormedAddCommGroup (SeparationQuotient E)

Equations

SeparationQuotient.instNormedAddCommGroup = NormedAddCommGroup.mk ⋯

source

theorem SeparationQuotient.instNormedAddCommGroup.proof_1 {E : Type u_1} [SeminormedAddCommGroup E] (q₁ : Quotient (inseparableSetoid E)) (q₂ : Quotient (inseparableSetoid E)) :

dist q₁ q₂ = ‖q₁ - q₂‖

source

instance SeparationQuotient.instNormedCommGroup {E : Type u_3} [SeminormedCommGroup E] :

NormedCommGroup (SeparationQuotient E)

Equations

SeparationQuotient.instNormedCommGroup = NormedCommGroup.mk ⋯

source

@[simp]

theorem SeparationQuotient.nnnorm_mk {E : Type u_3} [SeminormedAddCommGroup E] (p : E) :

‖SeparationQuotient.mk p‖₊ = ‖p‖₊

source

@[simp]

theorem SeparationQuotient.nnnorm_mk' {E : Type u_3} [SeminormedCommGroup E] (p : E) :

‖SeparationQuotient.mk p‖₊ = ‖p‖₊

source

theorem cauchySeq_sum_of_eventually_eq {E : Type u_3} [SeminormedAddCommGroup E] {u : ℕ → E} {v : ℕ → E} {N : ℕ} (huv : ∀ n ≥ N, u n = v n) (hv : CauchySeq fun (n : ℕ) => ∑ k ∈ Finset.range (n + 1), v k) :

CauchySeq fun (n : ℕ) => ∑ k ∈ Finset.range (n + 1), u k

source

theorem cauchySeq_prod_of_eventually_eq {E : Type u_3} [SeminormedCommGroup E] {u : ℕ → E} {v : ℕ → E} {N : ℕ} (huv : ∀ n ≥ N, u n = v n) (hv : CauchySeq fun (n : ℕ) => ∏ k ∈ Finset.range (n + 1), v k) :

CauchySeq fun (n : ℕ) => ∏ k ∈ Finset.range (n + 1), u k

source

theorem CauchySeq.norm_bddAbove {G : Type u_5} [SeminormedAddGroup G] {u : ℕ → G} (hu : CauchySeq u) :

BddAbove (Set.range fun (n : ℕ) => ‖u n‖)

source

theorem CauchySeq.mul_norm_bddAbove {G : Type u_5} [SeminormedGroup G] {u : ℕ → G} (hu : CauchySeq u) :

BddAbove (Set.range fun (n : ℕ) => ‖u n‖)

HepLean Documentation

Mathlib.Analysis.Normed.Group.Uniform

Normed groups are uniform groups #

SeparationQuotient #