mathlib documentation

analysis.normed.group.basic

Normed (semi)groups #

In this file we define four classes:

We also prove basic properties of (semi)normed groups and provide some instances.

Tags #

normed group

source
@[class]
structure has_norm (E : Type u_6) :
Type u_6
  • norm : E → ℝ

Auxiliary class, endowing a type E with a function norm : E → ℝ with notation ∥x∥. This class is designed to be extended in more interesting classes specifying the properties of the norm.

Instances of this typeclass
Instances of other typeclasses for has_norm
  • has_norm.has_sizeof_inst
source
@[class]
structure semi_normed_group (E : Type u_6) :
Type u_6

A seminormed group is an additive group endowed with a norm for which dist x y = ∥x - y∥ defines a pseudometric space structure.

Instances of this typeclass
Instances of other typeclasses for semi_normed_group
  • semi_normed_group.has_sizeof_inst
source
@[class]
structure normed_group (E : Type u_6) :
Type u_6

A normed group is an additive group endowed with a norm for which dist x y = ∥x - y∥ defines a metric space structure.

Instances of this typeclass
Instances of other typeclasses for normed_group
  • normed_group.has_sizeof_inst
source
@[protected, instance]
def normed_group.to_semi_normed_group {E : Type u_3} [h : normed_group E] :
semi_normed_group E

A normed group is a seminormed group.

Equations
source
def semi_normed_group.of_add_dist {E : Type u_3} [has_norm E] [add_comm_group E] [pseudo_metric_space E] (H1 : ∀ (x : E), ∥x∥ = has_dist.dist x 0) (H2 : ∀ (x y z : E), has_dist.dist x y ≤ has_dist.dist (x + z) (y + z)) :
semi_normed_group E

Construct a seminormed group from a translation invariant pseudodistance.

Equations
source
def semi_normed_group.of_add_dist' {E : Type u_3} [has_norm E] [add_comm_group E] [pseudo_metric_space E] (H1 : ∀ (x : E), ∥x∥ = has_dist.dist x 0) (H2 : ∀ (x y z : E), has_dist.dist (x + z) (y + z) ≤ has_dist.dist x y) :
semi_normed_group E

Construct a seminormed group from a translation invariant pseudodistance

Equations
source
structure semi_normed_group.core (E : Type u_6) [add_comm_group E] [has_norm E] :
Prop

A seminormed group can be built from a seminorm that satisfies algebraic properties. This is formalised in this structure.

source
def semi_normed_group.of_core (E : Type u_1) [add_comm_group E] [has_norm E] (C : semi_normed_group.core E) :
semi_normed_group E

Constructing a seminormed group from core properties of a seminorm, i.e., registering the pseudodistance and the pseudometric space structure from the seminorm properties. Note that in most cases this instance creates bad definitional equalities (e.g., it does not take into account a possibly existing uniform_space instance on E).

Equations
source
@[protected, instance]
def punit.normed_group  :
normed_group punit
Equations
source
@[simp]
theorem punit.norm_eq_zero (r : punit) :
∥r∥ = 0
source
@[protected, instance]
noncomputable def real.normed_group  :
normed_group ℝ
Equations
source
theorem real.norm_eq_abs (r : ℝ) :
∥r∥ = |r|
source
theorem dist_eq_norm {E : Type u_3} [semi_normed_group E] (g h : E) :
has_dist.dist g h = ∥g - h∥
source
theorem dist_eq_norm' {E : Type u_3} [semi_normed_group E] (g h : E) :
has_dist.dist g h = ∥h - g∥
source
@[simp]
theorem dist_zero_right {E : Type u_3} [semi_normed_group E] (g : E) :
has_dist.dist g 0 = ∥g∥
source
@[simp]
theorem dist_zero_left {E : Type u_3} [semi_normed_group E] :
has_dist.dist 0 = has_norm.norm
source
theorem tendsto_norm_cocompact_at_top {E : Type u_3} [semi_normed_group E] [proper_space E] :
filter.tendsto has_norm.norm (filter.cocompact E) filter.at_top
source
theorem norm_sub_rev {E : Type u_3} [semi_normed_group E] (g h : E) :
∥g - h∥ = ∥h - g∥
source
@[simp]
theorem norm_neg {E : Type u_3} [semi_normed_group E] (g : E) :
∥-g∥ = ∥g∥
source
@[simp]
theorem dist_add_left {E : Type u_3} [semi_normed_group E] (g h₁ h₂ : E) :
has_dist.dist (g + h₁) (g + h₂) = has_dist.dist h₁ h₂
source
@[simp]
theorem dist_add_right {E : Type u_3} [semi_normed_group E] (g₁ g₂ h : E) :
has_dist.dist (g₁ + h) (g₂ + h) = has_dist.dist g₁ g₂
source
theorem dist_neg {E : Type u_3} [semi_normed_group E] (x y : E) :
has_dist.dist (-x) y = has_dist.dist x (-y)
source
@[simp]
theorem dist_neg_neg {E : Type u_3} [semi_normed_group E] (g h : E) :
has_dist.dist (-g) (-h) = has_dist.dist g h
source
@[simp]
theorem dist_sub_left {E : Type u_3} [semi_normed_group E] (g h₁ h₂ : E) :
has_dist.dist (g - h₁) (g - h₂) = has_dist.dist h₁ h₂
source
@[simp]
theorem dist_sub_right {E : Type u_3} [semi_normed_group E] (g₁ g₂ h : E) :
has_dist.dist (g₁ - h) (g₂ - h) = has_dist.dist g₁ g₂
source
@[simp]
theorem dist_self_add_right {E : Type u_3} [semi_normed_group E] (g h : E) :
has_dist.dist g (g + h) = ∥h∥
source
@[simp]
theorem dist_self_add_left {E : Type u_3} [semi_normed_group E] (g h : E) :
has_dist.dist (g + h) g = ∥h∥
source
@[simp]
theorem dist_self_sub_right {E : Type u_3} [semi_normed_group E] (g h : E) :
has_dist.dist g (g - h) = ∥h∥
source
@[simp]
theorem dist_self_sub_left {E : Type u_3} [semi_normed_group E] (g h : E) :
has_dist.dist (g - h) g = ∥h∥
source
theorem filter.tendsto_neg_cobounded {E : Type u_3} [semi_normed_group E] :
filter.tendsto has_neg.neg (filter.comap has_norm.norm filter.at_top) (filter.comap has_norm.norm filter.at_top)

In a (semi)normed group, negation x ↦ -x tends to infinity at infinity. TODO: use bornology.cobounded instead of filter.comap has_norm.norm filter.at_top.

source
theorem norm_add_le {E : Type u_3} [semi_normed_group E] (g h : E) :
∥g + h∥ ≤ ∥g∥ + ∥h∥

Triangle inequality for the norm.

source
theorem norm_add_le_of_le {E : Type u_3} [semi_normed_group E] {g₁ g₂ : E} {n₁ n₂ : ℝ} (H₁ : ∥g₁∥ ≤ n₁) (H₂ : ∥g₂∥ ≤ n₂) :
∥g₁ + g₂∥ ≤ n₁ + n₂
source
theorem dist_add_add_le {E : Type u_3} [semi_normed_group E] (g₁ g₂ h₁ h₂ : E) :
has_dist.dist (g₁ + g₂) (h₁ + h₂) ≤ has_dist.dist g₁ h₁ + has_dist.dist g₂ h₂
source
theorem dist_add_add_le_of_le {E : Type u_3} [semi_normed_group E] {g₁ g₂ h₁ h₂ : E} {d₁ d₂ : ℝ} (H₁ : has_dist.dist g₁ h₁ ≤ d₁) (H₂ : has_dist.dist g₂ h₂ ≤ d₂) :
has_dist.dist (g₁ + g₂) (h₁ + h₂) ≤ d₁ + d₂
source
theorem dist_sub_sub_le {E : Type u_3} [semi_normed_group E] (g₁ g₂ h₁ h₂ : E) :
has_dist.dist (g₁ - g₂) (h₁ - h₂) ≤ has_dist.dist g₁ h₁ + has_dist.dist g₂ h₂
source
theorem dist_sub_sub_le_of_le {E : Type u_3} [semi_normed_group E] {g₁ g₂ h₁ h₂ : E} {d₁ d₂ : ℝ} (H₁ : has_dist.dist g₁ h₁ ≤ d₁) (H₂ : has_dist.dist g₂ h₂ ≤ d₂) :
has_dist.dist (g₁ - g₂) (h₁ - h₂) ≤ d₁ + d₂
source
theorem abs_dist_sub_le_dist_add_add {E : Type u_3} [semi_normed_group E] (g₁ g₂ h₁ h₂ : E) :
|has_dist.dist g₁ h₁ - has_dist.dist g₂ h₂| ≤ has_dist.dist (g₁ + g₂) (h₁ + h₂)
source
@[simp]
theorem norm_nonneg {E : Type u_3} [semi_normed_group E] (g : E) :
0 ≤ ∥g∥
source
@[simp]
theorem norm_zero {E : Type u_3} [semi_normed_group E] :
∥0∥ = 0
source
theorem ne_zero_of_norm_ne_zero {E : Type u_3} [semi_normed_group E] {g : E} :
∥g∥ ≠ 0 → g ≠ 0
source
theorem norm_of_subsingleton {E : Type u_3} [semi_normed_group E] [subsingleton E] (x : E) :
∥x∥ = 0
source
theorem norm_sum_le {ι : Type u_2} {E : Type u_3} [semi_normed_group E] (s : finset ι) (f : ι → E) :
∥s.sum (λ (i : ι), f i)∥ ≤ s.sum (λ (i : ι), ∥f i∥)
source
theorem norm_sum_le_of_le {ι : Type u_2} {E : Type u_3} [semi_normed_group E] (s : finset ι) {f : ι → E} {n : ι → ℝ} (h : ∀ (b : ι), b ∈ s → ∥f b∥ ≤ n b) :
∥s.sum (λ (b : ι), f b)∥ ≤ s.sum (λ (b : ι), n b)
source
theorem dist_sum_sum_le_of_le {ι : Type u_2} {E : Type u_3} [semi_normed_group E] (s : finset ι) {f g : ι → E} {d : ι → ℝ} (h : ∀ (b : ι), b ∈ s → has_dist.dist (f b) (g b) ≤ d b) :
has_dist.dist (s.sum (λ (b : ι), f b)) (s.sum (λ (b : ι), g b)) ≤ s.sum (λ (b : ι), d b)
source
theorem dist_sum_sum_le {ι : Type u_2} {E : Type u_3} [semi_normed_group E] (s : finset ι) (f g : ι → E) :
has_dist.dist (s.sum (λ (b : ι), f b)) (s.sum (λ (b : ι), g b)) ≤ s.sum (λ (b : ι), has_dist.dist (f b) (g b))
source
theorem norm_sub_le {E : Type u_3} [semi_normed_group E] (g h : E) :
∥g - h∥ ≤ ∥g∥ + ∥h∥
source
theorem norm_sub_le_of_le {E : Type u_3} [semi_normed_group E] {g₁ g₂ : E} {n₁ n₂ : ℝ} (H₁ : ∥g₁∥ ≤ n₁) (H₂ : ∥g₂∥ ≤ n₂) :
∥g₁ - g₂∥ ≤ n₁ + n₂
source
theorem dist_le_norm_add_norm {E : Type u_3} [semi_normed_group E] (g h : E) :
has_dist.dist g h ≤ ∥g∥ + ∥h∥
source
theorem abs_norm_sub_norm_le {E : Type u_3} [semi_normed_group E] (g h : E) :
|∥g∥ - ∥h∥| ≤ ∥g - h∥
source
theorem norm_sub_norm_le {E : Type u_3} [semi_normed_group E] (g h : E) :
∥g∥ - ∥h∥ ≤ ∥g - h∥
source
theorem dist_norm_norm_le {E : Type u_3} [semi_normed_group E] (g h : E) :
has_dist.dist ∥g∥ ∥h∥ ≤ ∥g - h∥
source
theorem norm_le_insert {E : Type u_3} [semi_normed_group E] (u v : E) :
∥v∥ ≤ ∥u∥ + ∥u - v∥

The direct path from 0 to v is shorter than the path with u inserted in between.

source
theorem norm_le_insert' {E : Type u_3} [semi_normed_group E] (u v : E) :
∥u∥ ≤ ∥v∥ + ∥u - v∥
source
theorem norm_le_add_norm_add {E : Type u_3} [semi_normed_group E] (u v : E) :
∥u∥ ≤ ∥u + v∥ + ∥v∥
source
theorem ball_eq {E : Type u_3} [semi_normed_group E] (y : E) (ε : ℝ) :
metric.ball y ε = {x : E | ∥x - y∥ < ε}
source
theorem ball_zero_eq {E : Type u_3} [semi_normed_group E] (ε : ℝ) :
metric.ball 0 ε = {x : E | ∥x∥ < ε}
source
theorem mem_ball_iff_norm {E : Type u_3} [semi_normed_group E] {g h : E} {r : ℝ} :
h ∈ metric.ball g r ↔ ∥h - g∥ < r
source
theorem add_mem_ball_iff_norm {E : Type u_3} [semi_normed_group E] {g h : E} {r : ℝ} :
g + h ∈ metric.ball g r ↔ ∥h∥ < r
source
theorem mem_ball_iff_norm' {E : Type u_3} [semi_normed_group E] {g h : E} {r : ℝ} :
h ∈ metric.ball g r ↔ ∥g - h∥ < r
source
@[simp]
theorem mem_ball_zero_iff {E : Type u_3} [semi_normed_group E] {ε : ℝ} {x : E} :
x ∈ metric.ball 0 ε ↔ ∥x∥ < ε
source
theorem mem_closed_ball_iff_norm {E : Type u_3} [semi_normed_group E] {g h : E} {r : ℝ} :
h ∈ metric.closed_ball g r ↔ ∥h - g∥ ≤ r
source
@[simp]
theorem mem_closed_ball_zero_iff {E : Type u_3} [semi_normed_group E] {ε : ℝ} {x : E} :
x ∈ metric.closed_ball 0 ε ↔ ∥x∥ ≤ ε
source
theorem add_mem_closed_ball_iff_norm {E : Type u_3} [semi_normed_group E] {g h : E} {r : ℝ} :
g + h ∈ metric.closed_ball g r ↔ ∥h∥ ≤ r
source
theorem mem_closed_ball_iff_norm' {E : Type u_3} [semi_normed_group E] {g h : E} {r : ℝ} :
h ∈ metric.closed_ball g r ↔ ∥g - h∥ ≤ r
source
theorem norm_le_of_mem_closed_ball {E : Type u_3} [semi_normed_group E] {g h : E} {r : ℝ} (H : h ∈ metric.closed_ball g r) :
∥h∥ ≤ ∥g∥ + r
source
theorem norm_le_norm_add_const_of_dist_le {E : Type u_3} [semi_normed_group E] {a b : E} {c : ℝ} (h : has_dist.dist a b ≤ c) :
∥a∥ ≤ ∥b∥ + c
source
theorem norm_lt_of_mem_ball {E : Type u_3} [semi_normed_group E] {g h : E} {r : ℝ} (H : h ∈ metric.ball g r) :
∥h∥ < ∥g∥ + r
source
theorem norm_lt_norm_add_const_of_dist_lt {E : Type u_3} [semi_normed_group E] {a b : E} {c : ℝ} (h : has_dist.dist a b < c) :
∥a∥ < ∥b∥ + c
source
theorem bounded_iff_forall_norm_le {E : Type u_3} [semi_normed_group E] {s : set E} :
metric.bounded s ↔ ∃ (C : ℝ), ∀ (x : E), x ∈ s → ∥x∥ ≤ C
source
@[simp]
theorem preimage_add_ball {E : Type u_3} [semi_normed_group E] (x y : E) (r : ℝ) :
has_add.add y ⁻¹' metric.ball x r = metric.ball (x - y) r
source
@[simp]
theorem preimage_add_closed_ball {E : Type u_3} [semi_normed_group E] (x y : E) (r : ℝ) :
has_add.add y ⁻¹' metric.closed_ball x r = metric.closed_ball (x - y) r
source
@[simp]
theorem mem_sphere_iff_norm {E : Type u_3} [semi_normed_group E] (v w : E) (r : ℝ) :
w ∈ metric.sphere v r ↔ ∥w - v∥ = r
source
@[simp]
theorem mem_sphere_zero_iff_norm {E : Type u_3} [semi_normed_group E] {w : E} {r : ℝ} :
w ∈ metric.sphere 0 r ↔ ∥w∥ = r
source
@[simp]
theorem norm_eq_of_mem_sphere {E : Type u_3} [semi_normed_group E] {r : ℝ} (x : ↥(metric.sphere 0 r)) :
∥↑x∥ = r
source
theorem preimage_add_sphere {E : Type u_3} [semi_normed_group E] (x y : E) (r : ℝ) :
has_add.add y ⁻¹' metric.sphere x r = metric.sphere (x - y) r
source
theorem ne_zero_of_mem_sphere {E : Type u_3} [semi_normed_group E] {r : ℝ} (hr : r ≠ 0) (x : ↥(metric.sphere 0 r)) :
↑x ≠ 0
source
theorem ne_zero_of_mem_unit_sphere {E : Type u_3} [semi_normed_group E] (x : ↥(metric.sphere 0 1)) :
↑x ≠ 0
source
@[protected, instance]
def metric.sphere.has_neg {E : Type u_3} [semi_normed_group E] {r : ℝ} :
has_neg ↥(metric.sphere 0 r)

We equip the sphere, in a seminormed group, with a formal operation of negation, namely the antipodal map.

Equations
source
@[simp]
theorem coe_neg_sphere {E : Type u_3} [semi_normed_group E] {r : ℝ} (v : ↥(metric.sphere 0 r)) :
↑-v = -↑v
source
@[protected]
def isometric.add_right {E : Type u_3} [semi_normed_group E] (x : E) :
E ≃ᵢ E

Addition y ↦ y + x as an isometry.

Equations
source
@[simp]
theorem isometric.add_right_to_equiv {E : Type u_3} [semi_normed_group E] (x : E) :
(isometric.add_right x).to_equiv = equiv.add_right x
source
@[simp]
theorem isometric.coe_add_right {E : Type u_3} [semi_normed_group E] (x : E) :
⇑(isometric.add_right x) = λ (y : E), y + x
source
theorem isometric.add_right_apply {E : Type u_3} [semi_normed_group E] (x y : E) :
⇑(isometric.add_right x) y = y + x
source
@[simp]
theorem isometric.add_right_symm {E : Type u_3} [semi_normed_group E] (x : E) :
(isometric.add_right x).symm = isometric.add_right (-x)
source
@[protected]
def isometric.add_left {E : Type u_3} [semi_normed_group E] (x : E) :
E ≃ᵢ E

Addition y ↦ x + y as an isometry.

Equations
source
@[simp]
theorem isometric.add_left_to_equiv {E : Type u_3} [semi_normed_group E] (x : E) :
(isometric.add_left x).to_equiv = equiv.add_left x
source
@[simp]
theorem isometric.coe_add_left {E : Type u_3} [semi_normed_group E] (x : E) :
⇑(isometric.add_left x) = has_add.add x
source
@[simp]
theorem isometric.add_left_symm {E : Type u_3} [semi_normed_group E] (x : E) :
(isometric.add_left x).symm = isometric.add_left (-x)
source
@[protected]
def isometric.neg (E : Type u_3) [semi_normed_group E] :
E ≃ᵢ E

Negation x ↦ -x as an isometry.

Equations
source
@[simp]
theorem isometric.neg_symm {E : Type u_3} [semi_normed_group E] :
(isometric.neg E).symm = isometric.neg E
source
@[simp]
theorem isometric.neg_to_equiv {E : Type u_3} [semi_normed_group E] :
(isometric.neg E).to_equiv = equiv.neg E
source
@[simp]
theorem isometric.coe_neg {E : Type u_3} [semi_normed_group E] :
⇑(isometric.neg E) = has_neg.neg
source
theorem normed_group.tendsto_nhds_zero {α : Type u_1} {E : Type u_3} [semi_normed_group E] {f : α → E} {l : filter α} :
filter.tendsto f l (nhds 0) ↔ ∀ (ε : ℝ), ε > 0 → (∀ᶠ (x : α) in l, ∥f x∥ < ε)
source
theorem normed_group.tendsto_nhds_nhds {E : Type u_3} {F : Type u_4} [semi_normed_group E] [semi_normed_group F] {f : E → F} {x : E} {y : F} :
filter.tendsto f (nhds x) (nhds y) ↔ ∀ (ε : ℝ), ε > 0 → (∃ (δ : ℝ) (H : δ > 0), ∀ (x' : E), ∥x' - x∥ < δ → ∥f x' - y∥ < ε)
source
theorem normed_group.cauchy_seq_iff {α : Type u_1} {E : Type u_3} [semi_normed_group E] [nonempty α] [semilattice_sup α] {u : α → E} :
cauchy_seq u ↔ ∀ (ε : ℝ), ε > 0 → (∃ (N : α), ∀ (m : α), N ≤ m → ∀ (n : α), N ≤ n → ∥u m - u n∥ < ε)
source
theorem normed_group.nhds_basis_norm_lt {E : Type u_3} [semi_normed_group E] (x : E) :
(nhds x).has_basis (λ (ε : ℝ), 0 < ε) (λ (ε : ℝ), {y : E | ∥y - x∥ < ε})
source
theorem normed_group.nhds_zero_basis_norm_lt {E : Type u_3} [semi_normed_group E] :
(nhds 0).has_basis (λ (ε : ℝ), 0 < ε) (λ (ε : ℝ), {y : E | ∥y∥ < ε})
source
theorem normed_group.uniformity_basis_dist {E : Type u_3} [semi_normed_group E] :
(uniformity E).has_basis (λ (ε : ℝ), 0 < ε) (λ (ε : ℝ), {p : E × E | ∥p.fst - p.snd∥ < ε})
source
theorem add_monoid_hom.lipschitz_of_bound {E : Type u_3} {F : Type u_4} [semi_normed_group E] [semi_normed_group F] (f : E →+ F) (C : ℝ) (h : ∀ (x : E), ∥⇑f x∥ ≤ C * ∥x∥) :
lipschitz_with C.to_nnreal ⇑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 normed_space.operator_norm.

source
theorem lipschitz_on_with_iff_norm_sub_le {E : Type u_3} {F : Type u_4} [semi_normed_group E] [semi_normed_group F] {f : E → F} {C : nnreal} {s : set E} :
lipschitz_on_with C f s ↔ ∀ (x : E), x ∈ s → ∀ (y : E), y ∈ s → ∥f x - f y∥ ≤ ↑C * ∥x - y∥
source
theorem lipschitz_on_with.norm_sub_le {E : Type u_3} {F : Type u_4} [semi_normed_group E] [semi_normed_group F] {f : E → F} {C : nnreal} {s : set E} (h : lipschitz_on_with C f s) {x y : E} (x_in : x ∈ s) (y_in : y ∈ s) :
∥f x - f y∥ ≤ ↑C * ∥x - y∥
source
theorem lipschitz_on_with.norm_sub_le_of_le {E : Type u_3} {F : Type u_4} [semi_normed_group E] [semi_normed_group F] {f : E → F} {C : nnreal} {s : set E} (h : lipschitz_on_with C f s) {x y : E} (x_in : x ∈ s) (y_in : y ∈ s) {d : ℝ} (hd : ∥x - y∥ ≤ d) :
∥f x - f y∥ ≤ ↑C * d
source
theorem lipschitz_with_iff_norm_sub_le {E : Type u_3} {F : Type u_4} [semi_normed_group E] [semi_normed_group F] {f : E → F} {C : nnreal} :
lipschitz_with C f ↔ ∀ (x y : E), ∥f x - f y∥ ≤ ↑C * ∥x - y∥
source
theorem lipschitz_with.norm_sub_le {E : Type u_3} {F : Type u_4} [semi_normed_group E] [semi_normed_group F] {f : E → F} {C : nnreal} :
lipschitz_with C f → ∀ (x y : E), ∥f x - f y∥ ≤ ↑C * ∥x - y∥

Alias of the forward direction of lipschitz_with_iff_norm_sub_le`.

source
theorem lipschitz_with.norm_sub_le_of_le {E : Type u_3} {F : Type u_4} [semi_normed_group E] [semi_normed_group F] {f : E → F} {C : nnreal} (h : lipschitz_with C f) {x y : E} {d : ℝ} (hd : ∥x - y∥ ≤ d) :
∥f x - f y∥ ≤ ↑C * d
source
theorem add_monoid_hom.continuous_of_bound {E : Type u_3} {F : Type u_4} [semi_normed_group E] [semi_normed_group F] (f : E →+ 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∥. The analogous condition for a linear map of normed spaces is in normed_space.operator_norm.

source
theorem is_compact.exists_bound_of_continuous_on {α : Type u_1} {E : Type u_3} [semi_normed_group E] [topological_space α] {s : set α} (hs : is_compact s) {f : α → E} (hf : continuous_on f s) :
∃ (C : ℝ), ∀ (x : α), x ∈ s → ∥f x∥ ≤ C
source
theorem add_monoid_hom.isometry_iff_norm {E : Type u_3} {F : Type u_4} [semi_normed_group E] [semi_normed_group F] (f : E →+ F) :
isometry ⇑f ↔ ∀ (x : E), ∥⇑f x∥ = ∥x∥
source
theorem add_monoid_hom.isometry_of_norm {E : Type u_3} {F : Type u_4} [semi_normed_group E] [semi_normed_group F] (f : E →+ F) (hf : ∀ (x : E), ∥⇑f x∥ = ∥x∥) :
isometry ⇑f
source
theorem controlled_sum_of_mem_closure {E : Type u_3} [semi_normed_group E] {s : add_subgroup E} {g : E} (hg : g ∈ closure ↑s) {b : ℕ → ℝ} (b_pos : ∀ (n : ℕ), 0 < b n) :
∃ (v : ℕ → E), filter.tendsto (λ (n : ℕ), (finset.range (n + 1)).sum (λ (i : ℕ), v i)) filter.at_top (nhds g) ∧ (∀ (n : ℕ), v n ∈ s) ∧ ∥v 0 - g∥ < b 0 ∧ ∀ (n : ℕ), n > 0 → ∥v n∥ < b n
source
theorem controlled_sum_of_mem_closure_range {E : Type u_3} {F : Type u_4} [semi_normed_group E] [semi_normed_group F] {j : E →+ F} {h : F} (Hh : h ∈ closure ↑(j.range)) {b : ℕ → ℝ} (b_pos : ∀ (n : ℕ), 0 < b n) :
∃ (g : ℕ → E), filter.tendsto (λ (n : ℕ), (finset.range (n + 1)).sum (λ (i : ℕ), ⇑j (g i))) filter.at_top (nhds h) ∧ ∥⇑j (g 0) - h∥ < b 0 ∧ ∀ (n : ℕ), n > 0 → ∥⇑j (g n)∥ < b n
source
@[class]
structure has_nnnorm (E : Type u_6) :
Type u_6

Auxiliary class, endowing a type α with a function nnnorm : α → ℝ≥0 with notation ∥x∥₊.

Instances of this typeclass
Instances of other typeclasses for has_nnnorm
  • has_nnnorm.has_sizeof_inst
source
@[protected, instance]
def semi_normed_group.to_has_nnnorm {E : Type u_3} [semi_normed_group E] :
has_nnnorm E
Equations
source
@[simp, norm_cast]
theorem coe_nnnorm {E : Type u_3} [semi_normed_group E] (a : E) :
↑∥a∥₊ = ∥a∥
source
@[simp]
theorem coe_comp_nnnorm {E : Type u_3} [semi_normed_group E] :
coe ∘ has_nnnorm.nnnorm = has_norm.norm
source
theorem norm_to_nnreal {E : Type u_3} [semi_normed_group E] {a : E} :
∥a∥.to_nnreal = ∥a∥₊
source
theorem nndist_eq_nnnorm {E : Type u_3} [semi_normed_group E] (a b : E) :
has_nndist.nndist a b = ∥a - b∥₊
source
@[simp]
theorem nnnorm_zero {E : Type u_3} [semi_normed_group E] :
∥0∥₊ = 0
source
theorem ne_zero_of_nnnorm_ne_zero {E : Type u_3} [semi_normed_group E] {g : E} :
∥g∥₊ ≠ 0 → g ≠ 0
source
theorem nnnorm_add_le {E : Type u_3} [semi_normed_group E] (g h : E) :
∥g + h∥₊ ≤ ∥g∥₊ + ∥h∥₊
source
@[simp]
theorem nnnorm_neg {E : Type u_3} [semi_normed_group E] (g : E) :
∥-g∥₊ = ∥g∥₊
source
theorem nndist_nnnorm_nnnorm_le {E : Type u_3} [semi_normed_group E] (g h : E) :
has_nndist.nndist ∥g∥₊ ∥h∥₊ ≤ ∥g - h∥₊
source
theorem nnnorm_le_insert {E : Type u_3} [semi_normed_group E] (u v : E) :
∥v∥₊ ≤ ∥u∥₊ + ∥u - v∥₊

The direct path from 0 to v is shorter than the path with u inserted in between.

source
theorem nnnorm_le_insert' {E : Type u_3} [semi_normed_group E] (u v : E) :
∥u∥₊ ≤ ∥v∥₊ + ∥u - v∥₊
source
theorem nnnorm_le_add_nnnorm_add {E : Type u_3} [semi_normed_group E] (u v : E) :
∥u∥₊ ≤ ∥u + v∥₊ + ∥v∥₊
source
theorem of_real_norm_eq_coe_nnnorm {E : Type u_3} [semi_normed_group E] (x : E) :
ennreal.of_real ∥x∥ = ↑∥x∥₊
source
theorem edist_eq_coe_nnnorm_sub {E : Type u_3} [semi_normed_group E] (x y : E) :
has_edist.edist x y = ↑∥x - y∥₊
source
theorem edist_eq_coe_nnnorm {E : Type u_3} [semi_normed_group E] (x : E) :
has_edist.edist x 0 = ↑∥x∥₊
source
theorem mem_emetric_ball_zero_iff {E : Type u_3} [semi_normed_group E] {x : E} {r : ennreal} :
x ∈ emetric.ball 0 r ↔ ↑∥x∥₊ < r
source
theorem nndist_add_add_le {E : Type u_3} [semi_normed_group E] (g₁ g₂ h₁ h₂ : E) :
has_nndist.nndist (g₁ + g₂) (h₁ + h₂) ≤ has_nndist.nndist g₁ h₁ + has_nndist.nndist g₂ h₂
source
theorem edist_add_add_le {E : Type u_3} [semi_normed_group E] (g₁ g₂ h₁ h₂ : E) :
has_edist.edist (g₁ + g₂) (h₁ + h₂) ≤ has_edist.edist g₁ h₁ + has_edist.edist g₂ h₂
source
@[simp]
theorem edist_add_left {E : Type u_3} [semi_normed_group E] (g h₁ h₂ : E) :
has_edist.edist (g + h₁) (g + h₂) = has_edist.edist h₁ h₂
source
@[simp]
theorem edist_add_right {E : Type u_3} [semi_normed_group E] (g₁ g₂ h : E) :
has_edist.edist (g₁ + h) (g₂ + h) = has_edist.edist g₁ g₂
source
theorem edist_neg {E : Type u_3} [semi_normed_group E] (x y : E) :
has_edist.edist (-x) y = has_edist.edist x (-y)
source
@[simp]
theorem edist_neg_neg {E : Type u_3} [semi_normed_group E] (x y : E) :
has_edist.edist (-x) (-y) = has_edist.edist x y
source
@[simp]
theorem edist_sub_left {E : Type u_3} [semi_normed_group E] (g h₁ h₂ : E) :
has_edist.edist (g - h₁) (g - h₂) = has_edist.edist h₁ h₂
source
@[simp]
theorem edist_sub_right {E : Type u_3} [semi_normed_group E] (g₁ g₂ h : E) :
has_edist.edist (g₁ - h) (g₂ - h) = has_edist.edist g₁ g₂
source
theorem nnnorm_sum_le {ι : Type u_2} {E : Type u_3} [semi_normed_group E] (s : finset ι) (f : ι → E) :
∥s.sum (λ (a : ι), f a)∥₊ ≤ s.sum (λ (a : ι), ∥f a∥₊)
source
theorem nnnorm_sum_le_of_le {ι : Type u_2} {E : Type u_3} [semi_normed_group E] (s : finset ι) {f : ι → E} {n : ι → nnreal} (h : ∀ (b : ι), b ∈ s → ∥f b∥₊ ≤ n b) :
∥s.sum (λ (b : ι), f b)∥₊ ≤ s.sum (λ (b : ι), n b)
source
theorem add_monoid_hom.lipschitz_of_bound_nnnorm {E : Type u_3} {F : Type u_4} [semi_normed_group E] [semi_normed_group F] (f : E →+ F) (C : nnreal) (h : ∀ (x : E), ∥⇑f x∥₊ ≤ C * ∥x∥₊) :
lipschitz_with C ⇑f
source
theorem lipschitz_with.neg {α : Type u_1} {E : Type u_3} [semi_normed_group E] [pseudo_emetric_space α] {K : nnreal} {f : α → E} (hf : lipschitz_with K f) :
lipschitz_with K (λ (x : α), -f x)
source
theorem lipschitz_with.add {α : Type u_1} {E : Type u_3} [semi_normed_group E] [pseudo_emetric_space α] {Kf Kg : nnreal} {f g : α → E} (hf : lipschitz_with Kf f) (hg : lipschitz_with Kg g) :
lipschitz_with (Kf + Kg) (λ (x : α), f x + g x)
source
theorem lipschitz_with.sub {α : Type u_1} {E : Type u_3} [semi_normed_group E] [pseudo_emetric_space α] {Kf Kg : nnreal} {f g : α → E} (hf : lipschitz_with Kf f) (hg : lipschitz_with Kg g) :
lipschitz_with (Kf + Kg) (λ (x : α), f x - g x)
source
theorem antilipschitz_with.add_lipschitz_with {α : Type u_1} {E : Type u_3} [semi_normed_group E] [pseudo_emetric_space α] {Kf Kg : nnreal} {f g : α → E} (hf : antilipschitz_with Kf f) (hg : lipschitz_with Kg g) (hK : Kg < Kf⁻¹) :
antilipschitz_with (Kf⁻¹ - Kg)⁻¹ (λ (x : α), f x + g x)
source
theorem antilipschitz_with.add_sub_lipschitz_with {α : Type u_1} {E : Type u_3} [semi_normed_group E] [pseudo_emetric_space α] {Kf Kg : nnreal} {f g : α → E} (hf : antilipschitz_with Kf f) (hg : lipschitz_with Kg (g - f)) (hK : Kg < Kf⁻¹) :
antilipschitz_with (Kf⁻¹ - Kg)⁻¹ g
source
theorem antilipschitz_with.le_mul_norm_sub {E : Type u_3} {F : Type u_4} [semi_normed_group E] [semi_normed_group F] {K : nnreal} {f : E → F} (hf : antilipschitz_with K f) (x y : E) :
∥x - y∥ ≤ ↑K * ∥f x - f y∥
source
def semi_normed_group.induced {F : Type u_4} [semi_normed_group F] {E : Type u_1} [add_comm_group E] (f : E →+ F) :
semi_normed_group E

A group homomorphism from an add_comm_group to a semi_normed_group induces a semi_normed_group structure on the domain.

See note [reducible non-instances]

Equations
source
@[protected, instance]
def add_subgroup.semi_normed_group {E : Type u_3} [semi_normed_group E] (s : add_subgroup E) :
semi_normed_group ↥s

A subgroup of a seminormed group is also a seminormed group, with the restriction of the norm.

Equations
source
@[simp]
theorem add_subgroup.coe_norm {E : Type u_1} [semi_normed_group E] {s : add_subgroup E} (x : ↥s) :
∥x∥ = ∥↑x∥

If x is an element of a subgroup s of a seminormed group E, its norm in s is equal to its norm in E.

source
@[norm_cast]
theorem add_subgroup.norm_coe {E : Type u_1} [semi_normed_group E] {s : add_subgroup E} (x : ↥s) :
∥↑x∥ = ∥x∥

If x is an element of a subgroup s of a seminormed group E, its norm in s is equal to its norm in E.

This is a reversed version of the simp lemma add_subgroup.coe_norm for use by norm_cast.

source
@[protected, instance]
def submodule.semi_normed_group {𝕜 : Type u_1} {_x : ring 𝕜} {E : Type u_2} [semi_normed_group E] {_x_1 : module 𝕜 E} (s : submodule 𝕜 E) :
semi_normed_group ↥s

A submodule of a seminormed group is also a seminormed group, with the restriction of the norm.

See note [implicit instance arguments].

Equations
source
@[simp]
theorem submodule.coe_norm {𝕜 : Type u_1} {_x : ring 𝕜} {E : Type u_2} [semi_normed_group E] {_x_1 : module 𝕜 E} {s : submodule 𝕜 E} (x : ↥s) :
∥x∥ = ∥↑x∥

If x is an element of a submodule s of a normed group E, its norm in s is equal to its norm in E.

See note [implicit instance arguments].

source
@[norm_cast]
theorem submodule.norm_coe {𝕜 : Type u_1} {_x : ring 𝕜} {E : Type u_2} [semi_normed_group E] {_x_1 : module 𝕜 E} {s : submodule 𝕜 E} (x : ↥s) :
∥↑x∥ = ∥x∥

If x is an element of a submodule s of a normed group E, its norm in E is equal to its norm in s.

This is a reversed version of the simp lemma submodule.coe_norm for use by norm_cast.

See note [implicit instance arguments].

source
@[protected, instance]
def ulift.semi_normed_group {E : Type u_3} [semi_normed_group E] :
semi_normed_group (ulift E)
Equations
source
theorem ulift.norm_def {E : Type u_3} [semi_normed_group E] (x : ulift E) :
∥x∥ = ∥x.down∥
source
theorem ulift.nnnorm_def {E : Type u_3} [semi_normed_group E] (x : ulift E) :
∥x∥₊ = ∥x.down∥₊
source
@[simp]
theorem ulift.norm_up {E : Type u_3} [semi_normed_group E] (x : E) :
∥{down := x}∥ = ∥x∥
source
@[simp]
theorem ulift.nnnorm_up {E : Type u_3} [semi_normed_group E] (x : E) :
∥{down := x}∥₊ = ∥x∥₊
source
@[protected, instance]
noncomputable def prod.semi_normed_group {E : Type u_3} {F : Type u_4} [semi_normed_group E] [semi_normed_group F] :
semi_normed_group (E × F)

seminormed group instance on the product of two seminormed groups, using the sup norm.

Equations
source
theorem prod.norm_def {E : Type u_3} {F : Type u_4} [semi_normed_group E] [semi_normed_group F] (x : E × F) :
∥x∥ = linear_order.max ∥x.fst∥ ∥x.snd∥
source
theorem prod.nnnorm_def {E : Type u_3} {F : Type u_4} [semi_normed_group E] [semi_normed_group F] (x : E × F) :
∥x∥₊ = linear_order.max ∥x.fst∥₊ ∥x.snd∥₊
source
theorem norm_fst_le {E : Type u_3} {F : Type u_4} [semi_normed_group E] [semi_normed_group F] (x : E × F) :
∥x.fst∥ ≤ ∥x∥
source
theorem norm_snd_le {E : Type u_3} {F : Type u_4} [semi_normed_group E] [semi_normed_group F] (x : E × F) :
∥x.snd∥ ≤ ∥x∥
source
theorem norm_prod_le_iff {E : Type u_3} {F : Type u_4} [semi_normed_group E] [semi_normed_group F] {x : E × F} {r : ℝ} :
∥x∥ ≤ r ↔ ∥x.fst∥ ≤ r ∧ ∥x.snd∥ ≤ r
source
@[protected, instance]
noncomputable def pi.semi_normed_group {ι : Type u_2} {π : ι → Type u_1} [fintype ι] [Π (i : ι), semi_normed_group (π i)] :
semi_normed_group (Π (i : ι), π i)

seminormed group instance on the product of finitely many seminormed groups, using the sup norm.

Equations
source
theorem pi.norm_def {ι : Type u_2} {π : ι → Type u_1} [fintype ι] [Π (i : ι), semi_normed_group (π i)] (f : Π (i : ι), π i) :
∥f∥ = ↑(finset.univ.sup (λ (b : ι), ∥f b∥₊))
source
theorem pi.nnnorm_def {ι : Type u_2} {π : ι → Type u_1} [fintype ι] [Π (i : ι), semi_normed_group (π i)] (f : Π (i : ι), π i) :
∥f∥₊ = finset.univ.sup (λ (b : ι), ∥f b∥₊)
source
theorem pi_norm_le_iff {ι : Type u_2} {π : ι → Type u_1} [fintype ι] [Π (i : ι), semi_normed_group (π i)] {r : ℝ} (hr : 0 ≤ r) {x : Π (i : ι), π i} :
∥x∥ ≤ r ↔ ∀ (i : ι), ∥x i∥ ≤ r

The seminorm of an element in a product space is ≤ r if and only if the norm of each component is.

source
theorem pi_nnnorm_le_iff {ι : Type u_2} {π : ι → Type u_1} [fintype ι] [Π (i : ι), semi_normed_group (π i)] {r : nnreal} {x : Π (i : ι), π i} :
∥x∥₊ ≤ r ↔ ∀ (i : ι), ∥x i∥₊ ≤ r
source
theorem pi_norm_lt_iff {ι : Type u_2} {π : ι → Type u_1} [fintype ι] [Π (i : ι), semi_normed_group (π i)] {r : ℝ} (hr : 0 < r) {x : Π (i : ι), π i} :
∥x∥ < r ↔ ∀ (i : ι), ∥x i∥ < r

The seminorm of an element in a product space is < r if and only if the norm of each component is.

source
theorem pi_nnnorm_lt_iff {ι : Type u_2} {π : ι → Type u_1} [fintype ι] [Π (i : ι), semi_normed_group (π i)] {r : nnreal} (hr : 0 < r) {x : Π (i : ι), π i} :
∥x∥₊ < r ↔ ∀ (i : ι), ∥x i∥₊ < r
source
theorem norm_le_pi_norm {ι : Type u_2} {π : ι → Type u_1} [fintype ι] [Π (i : ι), semi_normed_group (π i)] (x : Π (i : ι), π i) (i : ι) :
∥x i∥ ≤ ∥x∥
source
theorem nnnorm_le_pi_nnnorm {ι : Type u_2} {π : ι → Type u_1} [fintype ι] [Π (i : ι), semi_normed_group (π i)] (x : Π (i : ι), π i) (i : ι) :
∥x i∥₊ ≤ ∥x∥₊
source
@[simp]
theorem pi_norm_const {ι : Type u_2} {E : Type u_3} [semi_normed_group E] [nonempty ι] [fintype ι] (a : E) :
∥(λ (i : ι), a)∥ = ∥a∥
source
@[simp]
theorem pi_nnnorm_const {ι : Type u_2} {E : Type u_3} [semi_normed_group E] [nonempty ι] [fintype ι] (a : E) :
∥(λ (i : ι), a)∥₊ = ∥a∥₊
source
theorem pi.sum_norm_apply_le_norm {ι : Type u_2} {π : ι → Type u_1} [fintype ι] [Π (i : ι), semi_normed_group (π i)] (x : Π (i : ι), π i) :
finset.univ.sum (λ (i : ι), ∥x i∥) ≤ fintype.card ι • ∥x∥

The $L^1$ norm is less than the $L^\infty$ norm scaled by the cardinality.

source
theorem pi.sum_nnnorm_apply_le_nnnorm {ι : Type u_2} {π : ι → Type u_1} [fintype ι] [Π (i : ι), semi_normed_group (π i)] (x : Π (i : ι), π i) :
finset.univ.sum (λ (i : ι), ∥x i∥₊) ≤ fintype.card ι • ∥x∥₊

The $L^1$ norm is less than the $L^\infty$ norm scaled by the cardinality.

source
theorem tendsto_iff_norm_tendsto_zero {α : Type u_1} {E : Type u_3} [semi_normed_group E] {f : α → E} {a : filter α} {b : E} :
filter.tendsto f a (nhds b) ↔ filter.tendsto (λ (e : α), ∥f e - b∥) a (nhds 0)
source
theorem tendsto_zero_iff_norm_tendsto_zero {α : Type u_1} {E : Type u_3} [semi_normed_group E] {f : α → E} {a : filter α} :
filter.tendsto f a (nhds 0) ↔ filter.tendsto (λ (e : α), ∥f e∥) a (nhds 0)
source
theorem squeeze_zero_norm' {α : Type u_1} {E : Type u_3} [semi_normed_group E] {f : α → E} {g : α → ℝ} {t₀ : filter α} (h : ∀ᶠ (n : α) in t₀, ∥f n∥ ≤ g n) (h' : filter.tendsto g t₀ (nhds 0)) :
filter.tendsto f t₀ (nhds 0)

Special case of the sandwich theorem: if the norm of f is eventually bounded by a real function g which tends to 0, then f tends to 0. In this pair of lemmas (squeeze_zero_norm' and squeeze_zero_norm), following a convention of similar lemmas in topology.metric_space.basic and topology.algebra.order, the ' version is phrased using "eventually" and the non-' version is phrased absolutely.

source
theorem squeeze_zero_norm {α : Type u_1} {E : Type u_3} [semi_normed_group E] {f : α → E} {g : α → ℝ} {t₀ : filter α} (h : ∀ (n : α), ∥f n∥ ≤ g n) (h' : filter.tendsto g t₀ (nhds 0)) :
filter.tendsto f t₀ (nhds 0)

Special case of the sandwich theorem: if the norm of f is bounded by a real function g which tends to 0, then f tends to 0.

source
theorem tendsto_norm_sub_self {E : Type u_3} [semi_normed_group E] (x : E) :
filter.tendsto (λ (g : E), ∥g - x∥) (nhds x) (nhds 0)
source
theorem tendsto_norm {E : Type u_3} [semi_normed_group E] {x : E} :
filter.tendsto (λ (g : E), ∥g∥) (nhds x) (nhds ∥x∥)
source
theorem tendsto_norm_zero {E : Type u_3} [semi_normed_group E] :
filter.tendsto (λ (g : E), ∥g∥) (nhds 0) (nhds 0)
source
@[continuity]
theorem continuous_norm {E : Type u_3} [semi_normed_group E] :
continuous (λ (g : E), ∥g∥)
source
@[continuity]
theorem continuous_nnnorm {E : Type u_3} [semi_normed_group E] :
continuous (λ (a : E), ∥a∥₊)
source
theorem lipschitz_with_one_norm {E : Type u_3} [semi_normed_group E] :
lipschitz_with 1 has_norm.norm
source
theorem lipschitz_with_one_nnnorm {E : Type u_3} [semi_normed_group E] :
lipschitz_with 1 has_nnnorm.nnnorm
source
theorem uniform_continuous_norm {E : Type u_3} [semi_normed_group E] :
uniform_continuous has_norm.norm
source
theorem uniform_continuous_nnnorm {E : Type u_3} [semi_normed_group E] :
uniform_continuous (λ (a : E), ∥a∥₊)
source
theorem filter.tendsto.op_zero_is_bounded_under_le' {α : Type u_1} {E : Type u_3} {F : Type u_4} {G : Type u_5} [semi_normed_group E] [semi_normed_group F] [semi_normed_group G] {f : α → E} {g : α → F} {l : filter α} (hf : filter.tendsto f l (nhds 0)) (hg : filter.is_bounded_under has_le.le l (has_norm.norm ∘ g)) (op : E → F → G) (h_op : ∃ (A : ℝ), ∀ (x : E) (y : F), ∥op x y∥ ≤ A * ∥x∥ * ∥y∥) :
filter.tendsto (λ (x : α), op (f x) (g x)) l (nhds 0)

A helper lemma used to prove that the (scalar or usual) product of a function that tends to zero and a bounded function tends to zero. This lemma is formulated for any binary operation op : E → F → G with an estimate ∥op x y∥ ≤ A * ∥x∥ * ∥y∥ for some constant A instead of multiplication so that it can be applied to (*), flip (*), (•), and flip (•).

source
theorem filter.tendsto.op_zero_is_bounded_under_le {α : Type u_1} {E : Type u_3} {F : Type u_4} {G : Type u_5} [semi_normed_group E] [semi_normed_group F] [semi_normed_group G] {f : α → E} {g : α → F} {l : filter α} (hf : filter.tendsto f l (nhds 0)) (hg : filter.is_bounded_under has_le.le l (has_norm.norm ∘ g)) (op : E → F → G) (h_op : ∀ (x : E) (y : F), ∥op x y∥ ≤ ∥x∥ * ∥y∥) :
filter.tendsto (λ (x : α), op (f x) (g x)) l (nhds 0)

A helper lemma used to prove that the (scalar or usual) product of a function that tends to zero and a bounded function tends to zero. This lemma is formulated for any binary operation op : E → F → G with an estimate ∥op x y∥ ≤ ∥x∥ * ∥y∥ instead of multiplication so that it can be applied to (*), flip (*), (•), and flip (•).

source
theorem filter.tendsto.norm {α : Type u_1} {E : Type u_3} [semi_normed_group E] {l : filter α} {f : α → E} {a : E} (h : filter.tendsto f l (nhds a)) :
filter.tendsto (λ (x : α), ∥f x∥) l (nhds ∥a∥)
source
theorem filter.tendsto.nnnorm {α : Type u_1} {E : Type u_3} [semi_normed_group E] {l : filter α} {f : α → E} {a : E} (h : filter.tendsto f l (nhds a)) :
filter.tendsto (λ (x : α), ∥f x∥₊) l (nhds ∥a∥₊)
source
theorem continuous.norm {α : Type u_1} {E : Type u_3} [semi_normed_group E] [topological_space α] {f : α → E} (h : continuous f) :
continuous (λ (x : α), ∥f x∥)
source
theorem continuous.nnnorm {α : Type u_1} {E : Type u_3} [semi_normed_group E] [topological_space α] {f : α → E} (h : continuous f) :
continuous (λ (x : α), ∥f x∥₊)
source
theorem continuous_at.norm {α : Type u_1} {E : Type u_3} [semi_normed_group E] [topological_space α] {f : α → E} {a : α} (h : continuous_at f a) :
continuous_at (λ (x : α), ∥f x∥) a
source
theorem continuous_at.nnnorm {α : Type u_1} {E : Type u_3} [semi_normed_group E] [topological_space α] {f : α → E} {a : α} (h : continuous_at f a) :
continuous_at (λ (x : α), ∥f x∥₊) a
source
theorem continuous_within_at.norm {α : Type u_1} {E : Type u_3} [semi_normed_group E] [topological_space α] {f : α → E} {s : set α} {a : α} (h : continuous_within_at f s a) :
continuous_within_at (λ (x : α), ∥f x∥) s a
source
theorem continuous_within_at.nnnorm {α : Type u_1} {E : Type u_3} [semi_normed_group E] [topological_space α] {f : α → E} {s : set α} {a : α} (h : continuous_within_at f s a) :
continuous_within_at (λ (x : α), ∥f x∥₊) s a
source
theorem continuous_on.norm {α : Type u_1} {E : Type u_3} [semi_normed_group E] [topological_space α] {f : α → E} {s : set α} (h : continuous_on f s) :
continuous_on (λ (x : α), ∥f x∥) s
source
theorem continuous_on.nnnorm {α : Type u_1} {E : Type u_3} [semi_normed_group E] [topological_space α] {f : α → E} {s : set α} (h : continuous_on f s) :
continuous_on (λ (x : α), ∥f x∥₊) s
source
theorem eventually_ne_of_tendsto_norm_at_top {α : Type u_1} {E : Type u_3} [semi_normed_group E] {l : filter α} {f : α → E} (h : filter.tendsto (λ (y : α), ∥f y∥) l filter.at_top) (x : E) :
∀ᶠ (y : α) in l, f y ≠ x

If ∥y∥→∞, then we can assume y≠x for any fixed x.

source
@[protected, instance]
def semi_normed_group.has_lipschitz_add {E : Type u_3} [semi_normed_group E] :
has_lipschitz_add E
source
@[protected, instance]
def normed_uniform_group {E : Type u_3} [semi_normed_group E] :
uniform_add_group E

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

source
@[protected, instance]
def normed_top_group {E : Type u_3} [semi_normed_group E] :
topological_add_group E
source
theorem nat.norm_cast_le {E : Type u_3} [semi_normed_group E] [has_one E] (n : ℕ) :
∥↑n∥ ≤ ↑n * ∥1∥
source
theorem semi_normed_group.mem_closure_iff {E : Type u_3} [semi_normed_group E] {s : set E} {x : E} :
x ∈ closure s ↔ ∀ (ε : ℝ), ε > 0 → (∃ (y : E) (H : y ∈ s), ∥x - y∥ < ε)
source
theorem norm_le_zero_iff' {E : Type u_3} [semi_normed_group E] [separated_space E] {g : E} :
∥g∥ ≤ 0 ↔ g = 0
source
theorem norm_eq_zero_iff' {E : Type u_3} [semi_normed_group E] [separated_space E] {g : E} :
∥g∥ = 0 ↔ g = 0
source
theorem norm_pos_iff' {E : Type u_3} [semi_normed_group E] [separated_space E] {g : E} :
0 < ∥g∥ ↔ g ≠ 0
source
theorem cauchy_seq_sum_of_eventually_eq {E : Type u_3} [semi_normed_group E] {u v : ℕ → E} {N : ℕ} (huv : ∀ (n : ℕ), n ≥ N → u n = v n) (hv : cauchy_seq (λ (n : ℕ), (finset.range (n + 1)).sum (λ (k : ℕ), v k))) :
cauchy_seq (λ (n : ℕ), (finset.range (n + 1)).sum (λ (k : ℕ), u k))
source
def normed_group.of_add_dist {E : Type u_3} [has_norm E] [add_comm_group E] [metric_space E] (H1 : ∀ (x : E), ∥x∥ = has_dist.dist x 0) (H2 : ∀ (x y z : E), has_dist.dist x y ≤ has_dist.dist (x + z) (y + z)) :
normed_group E

Construct a normed group from a translation invariant distance

Equations
source
structure normed_group.core (E : Type u_6) [add_comm_group E] [has_norm E] :
Prop

A normed group can be built from a norm that satisfies algebraic properties. This is formalised in this structure.

source
theorem normed_group.core.to_semi_normed_group.core {E : Type u_1} [add_comm_group E] [has_norm E] (C : normed_group.core E) :
semi_normed_group.core E

The semi_normed_group.core induced by a normed_group.core.

source
def normed_group.of_core (E : Type u_1) [add_comm_group E] [has_norm E] (C : normed_group.core E) :
normed_group E

Constructing a normed group from core properties of a norm, i.e., registering the distance and the metric space structure from the norm properties.

Equations
source
@[simp]
theorem norm_eq_zero {E : Type u_3} [normed_group E] {g : E} :
∥g∥ = 0 ↔ g = 0
source
theorem norm_ne_zero_iff {E : Type u_3} [normed_group E] {g : E} :
∥g∥ ≠ 0 ↔ g ≠ 0
source
@[simp]
theorem norm_pos_iff {E : Type u_3} [normed_group E] {g : E} :
0 < ∥g∥ ↔ g ≠ 0
source
@[simp]
theorem norm_le_zero_iff {E : Type u_3} [normed_group E] {g : E} :
∥g∥ ≤ 0 ↔ g = 0
source
theorem norm_sub_eq_zero_iff {E : Type u_3} [normed_group E] {u v : E} :
∥u - v∥ = 0 ↔ u = v
source
theorem eq_of_norm_sub_le_zero {E : Type u_3} [normed_group E] {g h : E} (a : ∥g - h∥ ≤ 0) :
g = h
source
theorem eq_of_norm_sub_eq_zero {E : Type u_3} [normed_group E] {u v : E} (h : ∥u - v∥ = 0) :
u = v
source
@[simp]
theorem nnnorm_eq_zero {E : Type u_3} [normed_group E] {a : E} :
∥a∥₊ = 0 ↔ a = 0
source
theorem nnnorm_ne_zero_iff {E : Type u_3} [normed_group E] {g : E} :
∥g∥₊ ≠ 0 ↔ g ≠ 0
source
def normed_group.induced {F : Type u_4} [normed_group F] {E : Type u_1} [add_comm_group E] (f : E →+ F) (h : function.injective ⇑f) :
normed_group E

An injective group homomorphism from an add_comm_group to a normed_group induces a normed_group structure on the domain.

See note [reducible non-instances].

Equations
source
@[protected, instance]
def add_subgroup.normed_group {E : Type u_3} [normed_group E] (s : add_subgroup E) :
normed_group ↥s

A subgroup of a normed group is also a normed group, with the restriction of the norm.

Equations
source
@[protected, instance]
def submodule.normed_group {𝕜 : Type u_1} {_x : ring 𝕜} {E : Type u_2} [normed_group E] {_x_1 : module 𝕜 E} (s : submodule 𝕜 E) :
normed_group ↥s

A submodule of a normed group is also a normed group, with the restriction of the norm.

See note [implicit instance arguments].

Equations
source
@[protected, instance]
def ulift.normed_group {E : Type u_3} [normed_group E] :
normed_group (ulift E)
Equations
source
@[protected, instance]
noncomputable def prod.normed_group {E : Type u_3} {F : Type u_4} [normed_group E] [normed_group F] :
normed_group (E × F)

normed group instance on the product of two normed groups, using the sup norm.

Equations
source
@[protected, instance]
noncomputable def pi.normed_group {ι : Type u_2} {π : ι → Type u_1} [fintype ι] [Π (i : ι), normed_group (π i)] :
normed_group (Π (i : ι), π i)

normed group instance on the product of finitely many normed groups, using the sup norm.

Equations
source
theorem tendsto_norm_sub_self_punctured_nhds {E : Type u_3} [normed_group E] (a : E) :
filter.tendsto (λ (x : E), ∥x - a∥) (nhds_within a {a}ᶜ) (nhds_within 0 (set.Ioi 0))
source
theorem tendsto_norm_nhds_within_zero {E : Type u_3} [normed_group E] :
filter.tendsto has_norm.norm (nhds_within 0 {0}ᶜ) (nhds_within 0 (set.Ioi 0))

Some relations with has_compact_support

source
theorem has_compact_support_norm_iff {α : Type u_1} {E : Type u_3} [normed_group E] [topological_space α] {f : α → E} :
has_compact_support (λ (x : α), ∥f x∥) ↔ has_compact_support f
source
theorem has_compact_support.norm {α : Type u_1} {E : Type u_3} [normed_group E] [topological_space α] {f : α → E} :
has_compact_support f → has_compact_support (λ (x : α), ∥f x∥)

Alias of the reverse direction of has_compact_support_norm_iff`.

source
theorem continuous.bounded_above_of_compact_support {α : Type u_1} {E : Type u_3} [normed_group E] [topological_space α] {f : α → E} (hf : continuous f) (hsupp : has_compact_support f) :
∃ (C : ℝ), ∀ (x : α), ∥f x∥ ≤ C