analysis.normed.group.basic

@[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 seminormed_add_comm_group (E : Type u_6) :

Type u_6

to_has_norm : has_norm E
to_add_comm_group : add_comm_group E
to_pseudo_metric_space : pseudo_metric_space E
dist_eq : ∀ (x y : E), has_dist.dist x y = ∥x - y∥

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 seminormed_add_comm_group

seminormed_add_comm_group.has_sizeof_inst

source

@[class]

structure normed_add_comm_group (E : Type u_6) :

Type u_6

to_has_norm : has_norm E
to_add_comm_group : add_comm_group E
to_metric_space : metric_space E
dist_eq : ∀ (x y : E), has_dist.dist x y = ∥x - y∥

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_add_comm_group

normed_add_comm_group.has_sizeof_inst

source

@[protected, instance]

def normed_add_comm_group.to_seminormed_add_comm_group {E : Type u_3} [h : normed_add_comm_group E] :

seminormed_add_comm_group E

A normed group is a seminormed group.

Equations

normed_add_comm_group.to_seminormed_add_comm_group = {to_has_norm := normed_add_comm_group.to_has_norm h, to_add_comm_group := normed_add_comm_group.to_add_comm_group h, to_pseudo_metric_space := metric_space.to_pseudo_metric_space normed_add_comm_group.to_metric_space, dist_eq := _}

source

def seminormed_add_comm_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)) :

seminormed_add_comm_group E

Construct a seminormed group from a translation invariant pseudodistance.

Equations

seminormed_add_comm_group.of_add_dist H1 H2 = {to_has_norm := _inst_1, to_add_comm_group := _inst_2, to_pseudo_metric_space := _inst_3, dist_eq := _}

source

def seminormed_add_comm_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) :

seminormed_add_comm_group E

Construct a seminormed group from a translation invariant pseudodistance

Equations

seminormed_add_comm_group.of_add_dist' H1 H2 = {to_has_norm := _inst_1, to_add_comm_group := _inst_2, to_pseudo_metric_space := _inst_3, dist_eq := _}

source

structure seminormed_add_comm_group.core (E : Type u_6) [add_comm_group E] [has_norm E] :

Prop

norm_zero : ∥0∥ = 0
triangle : ∀ (x y : E), ∥x + y∥ ≤ ∥x∥ + ∥y∥
norm_neg : ∀ (x : E), ∥-x∥ = ∥x∥

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

source

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

seminormed_add_comm_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

seminormed_add_comm_group.of_core E C = {to_has_norm := _inst_2, to_add_comm_group := _inst_1, to_pseudo_metric_space := {to_has_dist := {dist := λ (x y : E), ∥x - y∥}, dist_self := _, dist_comm := _, dist_triangle := _, edist := λ (x y : E), ↑⟨(λ (x y : E), ∥x - y∥) x y, _⟩, edist_dist := _, to_uniform_space := uniform_space_of_dist (λ (x y : E), ∥x - y∥) _ _ _, uniformity_dist := _, to_bornology := bornology.of_dist (λ (x y : E), ∥x - y∥) _ _ _, cobounded_sets := _}, dist_eq := _}

source

@[protected, instance]

def punit.normed_add_comm_group :

normed_add_comm_group punit

Equations

punit.normed_add_comm_group = {to_has_norm := {norm := function.const punit 0}, to_add_comm_group := punit.add_comm_group, to_metric_space := punit.metric_space, dist_eq := punit.normed_add_comm_group._proof_1}

source

@[simp]

theorem punit.norm_eq_zero (r : punit) :

∥r∥ = 0

source

@[protected, instance]

def real.has_norm :

has_norm ℝ

Equations

real.has_norm = {norm := λ (x : ℝ), |x|}

source

@[simp]

theorem real.norm_eq_abs (r : ℝ) :

∥r∥ = |r|

source

@[protected, instance]

def real.normed_add_comm_group :

normed_add_comm_group ℝ

Equations

real.normed_add_comm_group = {to_has_norm := real.has_norm, to_add_comm_group := real.add_comm_group, to_metric_space := real.metric_space, dist_eq := real.normed_add_comm_group._proof_1}

source

theorem dist_eq_norm {E : Type u_3} [seminormed_add_comm_group E] (g h : E) :

has_dist.dist g h = ∥g - h∥

source

theorem dist_eq_norm' {E : Type u_3} [seminormed_add_comm_group E] (g h : E) :

has_dist.dist g h = ∥h - g∥

source

@[simp]

theorem dist_zero_right {E : Type u_3} [seminormed_add_comm_group E] (g : E) :

has_dist.dist g 0 = ∥g∥

source

@[simp]

theorem dist_zero_left {E : Type u_3} [seminormed_add_comm_group E] :

has_dist.dist 0 = has_norm.norm

source

theorem isometry.norm_map_of_map_zero {E : Type u_3} {F : Type u_4} [seminormed_add_comm_group E] [seminormed_add_comm_group F] {f : E → F} (hi : isometry f) (h0 : f 0 = 0) (x : E) :

∥f x∥ = ∥x∥

source

theorem tendsto_norm_cocompact_at_top {E : Type u_3} [seminormed_add_comm_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} [seminormed_add_comm_group E] (g h : E) :

∥g - h∥ = ∥h - g∥

source

@[simp]

theorem norm_neg {E : Type u_3} [seminormed_add_comm_group E] (g : E) :

∥-g∥ = ∥g∥

source

@[simp]

theorem dist_add_left {E : Type u_3} [seminormed_add_comm_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} [seminormed_add_comm_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} [seminormed_add_comm_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} [seminormed_add_comm_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} [seminormed_add_comm_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} [seminormed_add_comm_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} [seminormed_add_comm_group E] (g h : E) :

has_dist.dist g (g + h) = ∥h∥

source

@[simp]

theorem dist_self_add_left {E : Type u_3} [seminormed_add_comm_group E] (g h : E) :

has_dist.dist (g + h) g = ∥h∥

source

@[simp]

theorem dist_self_sub_right {E : Type u_3} [seminormed_add_comm_group E] (g h : E) :

has_dist.dist g (g - h) = ∥h∥

source

@[simp]

theorem dist_self_sub_left {E : Type u_3} [seminormed_add_comm_group E] (g h : E) :

has_dist.dist (g - h) g = ∥h∥

source

theorem filter.tendsto_neg_cobounded {E : Type u_3} [seminormed_add_comm_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} [seminormed_add_comm_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} [seminormed_add_comm_group E] {g₁ g₂ : E} {n₁ n₂ : ℝ} (H₁ : ∥g₁∥ ≤ n₁) (H₂ : ∥g₂∥ ≤ n₂) :

∥g₁ + g₂∥ ≤ n₁ + n₂

source

theorem norm_add₃_le {E : Type u_3} [seminormed_add_comm_group E] (x y z : E) :

∥x + y + z∥ ≤ ∥x∥ + ∥y∥ + ∥z∥

source

theorem dist_add_add_le {E : Type u_3} [seminormed_add_comm_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} [seminormed_add_comm_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} [seminormed_add_comm_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} [seminormed_add_comm_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} [seminormed_add_comm_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} [seminormed_add_comm_group E] (g : E) :

0 ≤ ∥g∥

source

meta def tactic.positivity_norm :

expr → tactic tactic.positivity.strictness

Extension for the positivity tactic: norms are nonnegative.

source

@[simp]

theorem norm_zero {E : Type u_3} [seminormed_add_comm_group E] :

∥0∥ = 0

source

theorem ne_zero_of_norm_ne_zero {E : Type u_3} [seminormed_add_comm_group E] {g : E} :

∥g∥ ≠ 0 → g ≠ 0

source

theorem norm_of_subsingleton {E : Type u_3} [seminormed_add_comm_group E] [subsingleton E] (x : E) :

∥x∥ = 0

source

theorem norm_multiset_sum_le {E : Type u_3} [seminormed_add_comm_group E] (m : multiset E) :

∥m.sum ∥ ≤ (multiset.map (λ (x : E), ∥x∥) m).sum

source

theorem norm_sum_le {ι : Type u_2} {E : Type u_3} [seminormed_add_comm_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} [seminormed_add_comm_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} [seminormed_add_comm_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} [seminormed_add_comm_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} [seminormed_add_comm_group E] (g h : E) :

∥g - h∥ ≤ ∥g∥ + ∥h∥

source

theorem norm_sub_le_of_le {E : Type u_3} [seminormed_add_comm_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} [seminormed_add_comm_group E] (g h : E) :

has_dist.dist g h ≤ ∥g∥ + ∥h∥

source

theorem abs_norm_sub_norm_le {E : Type u_3} [seminormed_add_comm_group E] (g h : E) :

|∥g∥ - ∥h∥| ≤ ∥g - h∥

source

theorem norm_sub_norm_le {E : Type u_3} [seminormed_add_comm_group E] (g h : E) :

∥g∥ - ∥h∥ ≤ ∥g - h∥

source

theorem dist_norm_norm_le {E : Type u_3} [seminormed_add_comm_group E] (g h : E) :

has_dist.dist ∥g∥ ∥h∥ ≤ ∥g - h∥

source

theorem norm_le_insert {E : Type u_3} [seminormed_add_comm_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} [seminormed_add_comm_group E] (u v : E) :

∥u∥ ≤ ∥v∥ + ∥u - v∥

source

theorem norm_le_add_norm_add {E : Type u_3} [seminormed_add_comm_group E] (u v : E) :

∥u∥ ≤ ∥u + v∥ + ∥v∥

source

theorem ball_eq {E : Type u_3} [seminormed_add_comm_group E] (y : E) (ε : ℝ) :

metric.ball y ε = {x : E | ∥x - y∥ < ε}

source

theorem ball_zero_eq {E : Type u_3} [seminormed_add_comm_group E] (ε : ℝ) :

metric.ball 0 ε = {x : E | ∥x∥ < ε}

source

theorem mem_ball_iff_norm {E : Type u_3} [seminormed_add_comm_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} [seminormed_add_comm_group E] {g h : E} {r : ℝ} :

g + h ∈ metric.ball g r ↔ ∥h∥ < r

source

theorem mem_ball_iff_norm' {E : Type u_3} [seminormed_add_comm_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} [seminormed_add_comm_group E] {ε : ℝ} {x : E} :

x ∈ metric.ball 0 ε ↔ ∥x∥ < ε

source

theorem mem_closed_ball_iff_norm {E : Type u_3} [seminormed_add_comm_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} [seminormed_add_comm_group E] {ε : ℝ} {x : E} :

x ∈ metric.closed_ball 0 ε ↔ ∥x∥ ≤ ε

source

theorem add_mem_closed_ball_iff_norm {E : Type u_3} [seminormed_add_comm_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} [seminormed_add_comm_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} [seminormed_add_comm_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} [seminormed_add_comm_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} [seminormed_add_comm_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} [seminormed_add_comm_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} [seminormed_add_comm_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} [seminormed_add_comm_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} [seminormed_add_comm_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} [seminormed_add_comm_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} [seminormed_add_comm_group E] {w : E} {r : ℝ} :

w ∈ metric.sphere 0 r ↔ ∥w∥ = r

source

@[simp]

theorem norm_eq_of_mem_sphere {E : Type u_3} [seminormed_add_comm_group E] {r : ℝ} (x : ↥(metric.sphere 0 r)) :

∥↑x∥ = r

source

theorem preimage_add_sphere {E : Type u_3} [seminormed_add_comm_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} [seminormed_add_comm_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} [seminormed_add_comm_group E] (x : ↥(metric.sphere 0 1)) :

↑x ≠ 0

source

def norm_add_group_seminorm (E : Type u_3) [seminormed_add_comm_group E] :

add_group_seminorm E

The norm of a seminormed group as an additive group seminorm.

Equations

norm_add_group_seminorm E = {to_fun := has_norm.norm seminormed_add_comm_group.to_has_norm, map_zero' := _, add_le' := _, neg' := _}

source

@[simp]

theorem coe_norm_add_group_seminorm (E : Type u_3) [seminormed_add_comm_group E] :

⇑(norm_add_group_seminorm E) = has_norm.norm

source

@[protected]

def isometric.add_right {E : Type u_3} [seminormed_add_comm_group E] (x : E) :

E ≃ᵢ E

Addition y ↦ y + x as an isometry.

Equations

isometric.add_right x = {to_equiv := {to_fun := (equiv.add_right x).to_fun, inv_fun := (equiv.add_right x).inv_fun, left_inv := _, right_inv := _}, isometry_to_fun := _}

source

@[simp]

theorem isometric.add_right_to_equiv {E : Type u_3} [seminormed_add_comm_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} [seminormed_add_comm_group E] (x : E) :

⇑(isometric.add_right x) = λ (y : E), y + x

source

theorem isometric.add_right_apply {E : Type u_3} [seminormed_add_comm_group E] (x y : E) :

⇑(isometric.add_right x) y = y + x

source

@[simp]

theorem isometric.add_right_symm {E : Type u_3} [seminormed_add_comm_group E] (x : E) :

(isometric.add_right x).symm = isometric.add_right (-x)

source

@[protected]

def isometric.add_left {E : Type u_3} [seminormed_add_comm_group E] (x : E) :

E ≃ᵢ E

Addition y ↦ x + y as an isometry.

Equations

isometric.add_left x = {to_equiv := equiv.add_left x, isometry_to_fun := _}

source

@[simp]

theorem isometric.add_left_to_equiv {E : Type u_3} [seminormed_add_comm_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} [seminormed_add_comm_group E] (x : E) :

⇑(isometric.add_left x) = has_add.add x

source

@[simp]

theorem isometric.add_left_symm {E : Type u_3} [seminormed_add_comm_group E] (x : E) :

(isometric.add_left x).symm = isometric.add_left (-x)

source

@[protected]

def isometric.neg (E : Type u_3) [seminormed_add_comm_group E] :

E ≃ᵢ E

Negation x ↦ -x as an isometry.

Equations

isometric.neg E = {to_equiv := equiv.neg E (subtraction_monoid.to_has_involutive_neg E), isometry_to_fun := _}

source

@[simp]

theorem isometric.neg_symm {E : Type u_3} [seminormed_add_comm_group E] :

(isometric.neg E).symm = isometric.neg E

source

@[simp]

theorem isometric.neg_to_equiv {E : Type u_3} [seminormed_add_comm_group E] :

(isometric.neg E).to_equiv = equiv.neg E

source

@[simp]

theorem isometric.coe_neg {E : Type u_3} [seminormed_add_comm_group E] :

⇑(isometric.neg E) = has_neg.neg

source

theorem normed_add_comm_group.tendsto_nhds_zero {α : Type u_1} {E : Type u_3} [seminormed_add_comm_group E] {f : α → E} {l : filter α} :

filter.tendsto f l (nhds 0) ↔ ∀ (ε : ℝ), ε > 0 → (∀ᶠ (x : α) in l, ∥f x∥ < ε)

source

theorem normed_add_comm_group.tendsto_nhds_nhds {E : Type u_3} {F : Type u_4} [seminormed_add_comm_group E] [seminormed_add_comm_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_add_comm_group.cauchy_seq_iff {α : Type u_1} {E : Type u_3} [seminormed_add_comm_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_add_comm_group.nhds_basis_norm_lt {E : Type u_3} [seminormed_add_comm_group E] (x : E) :

(nhds x).has_basis (λ (ε : ℝ), 0 < ε) (λ (ε : ℝ), {y : E | ∥y - x∥ < ε})

source

theorem normed_add_comm_group.nhds_zero_basis_norm_lt {E : Type u_3} [seminormed_add_comm_group E] :

(nhds 0).has_basis (λ (ε : ℝ), 0 < ε) (λ (ε : ℝ), {y : E | ∥y∥ < ε})

source

theorem normed_add_comm_group.uniformity_basis_dist {E : Type u_3} [seminormed_add_comm_group E] :

(uniformity E).has_basis (λ (ε : ℝ), 0 < ε) (λ (ε : ℝ), {p : E × E | ∥p.fst - p.snd∥ < ε})

source

theorem normed_add_comm_group.tendsto_uniformly_on_zero {ι : Type u_2} {G : Type u_5} [seminormed_add_comm_group G] {E' : Type u_6} {f : ι → E' → G} {s : set E'} {l : filter ι} :

tendsto_uniformly_on f 0 l s ↔ ∀ (ε : ℝ), ε > 0 → (∀ᶠ (N : ι) in l, ∀ (x : E'), x ∈ s → ∥f N x∥ < ε)

source

theorem normed_add_comm_group.uniform_cauchy_seq_on_filter_iff_tendsto_uniformly_on_filter_zero {ι : Type u_2} {G : Type u_5} [seminormed_add_comm_group G] {E' : Type u_6} {f : ι → E' → G} {l : filter ι} {l' : filter E'} :

uniform_cauchy_seq_on_filter f l l' ↔ tendsto_uniformly_on_filter (λ (n : ι × ι) (z : E'), f n.fst z - f n.snd z) 0 (l.prod l) l'

source

theorem normed_add_comm_group.uniform_cauchy_seq_on_iff_tendsto_uniformly_on_zero {ι : Type u_2} {G : Type u_5} [seminormed_add_comm_group G] {E' : Type u_6} {f : ι → E' → G} {s : set E'} {l : filter ι} :

uniform_cauchy_seq_on f l s ↔ tendsto_uniformly_on (λ (n : ι × ι) (z : E'), f n.fst z - f n.snd z) 0 (l.prod l) s

source

theorem add_monoid_hom_class.lipschitz_of_bound {E : Type u_3} {F : Type u_4} [seminormed_add_comm_group E] [seminormed_add_comm_group F] {𝓕 : Type u_1} [add_monoid_hom_class 𝓕 E F] (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} [seminormed_add_comm_group E] [seminormed_add_comm_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} [seminormed_add_comm_group E] [seminormed_add_comm_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} [seminormed_add_comm_group E] [seminormed_add_comm_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} [seminormed_add_comm_group E] [seminormed_add_comm_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} [seminormed_add_comm_group E] [seminormed_add_comm_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} [seminormed_add_comm_group E] [seminormed_add_comm_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_class.continuous_of_bound {E : Type u_3} {F : Type u_4} [seminormed_add_comm_group E] [seminormed_add_comm_group F] {𝓕 : Type u_1} [add_monoid_hom_class 𝓕 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 add_monoid_hom_class.uniform_continuous_of_bound {E : Type u_3} {F : Type u_4} [seminormed_add_comm_group E] [seminormed_add_comm_group F] {𝓕 : Type u_1} [add_monoid_hom_class 𝓕 E F] (f : 𝓕) (C : ℝ) (h : ∀ (x : E), ∥⇑f x∥ ≤ C * ∥x∥) :

uniform_continuous ⇑f

source

theorem is_compact.exists_bound_of_continuous_on {α : Type u_1} {E : Type u_3} [seminormed_add_comm_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_class.isometry_iff_norm {E : Type u_3} {F : Type u_4} [seminormed_add_comm_group E] [seminormed_add_comm_group F] {𝓕 : Type u_1} [add_monoid_hom_class 𝓕 E F] (f : 𝓕) :

isometry ⇑f ↔ ∀ (x : E), ∥⇑f x∥ = ∥x∥

source

theorem add_monoid_hom_class.isometry_of_norm {E : Type u_3} {F : Type u_4} [seminormed_add_comm_group E] [seminormed_add_comm_group F] {𝓕 : Type u_1} [add_monoid_hom_class 𝓕 E F] (f : 𝓕) (hf : ∀ (x : E), ∥⇑f x∥ = ∥x∥) :

isometry ⇑f

source

theorem controlled_sum_of_mem_closure {E : Type u_3} [seminormed_add_comm_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} [seminormed_add_comm_group E] [seminormed_add_comm_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

nnnorm : E → nnreal

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

Instances of this typeclass

seminormed_add_comm_group.to_has_nnnorm

Instances of other typeclasses for has_nnnorm

has_nnnorm.has_sizeof_inst

source

@[protected, instance]

def seminormed_add_comm_group.to_has_nnnorm {E : Type u_3} [seminormed_add_comm_group E] :

has_nnnorm E

Equations

seminormed_add_comm_group.to_has_nnnorm = {nnnorm := λ (a : E), ⟨∥a∥, _⟩}

source

@[simp, norm_cast]

theorem coe_nnnorm {E : Type u_3} [seminormed_add_comm_group E] (a : E) :

↑∥a∥₊ = ∥a∥

source

@[simp]

theorem coe_comp_nnnorm {E : Type u_3} [seminormed_add_comm_group E] :

coe ∘ has_nnnorm.nnnorm = has_norm.norm

source

theorem norm_to_nnreal {E : Type u_3} [seminormed_add_comm_group E] {a : E} :

∥a∥.to_nnreal = ∥a∥₊

source

theorem nndist_eq_nnnorm {E : Type u_3} [seminormed_add_comm_group E] (a b : E) :

has_nndist.nndist a b = ∥a - b∥₊

source

@[simp]

theorem nnnorm_zero {E : Type u_3} [seminormed_add_comm_group E] :

∥0∥₊ = 0

source

theorem ne_zero_of_nnnorm_ne_zero {E : Type u_3} [seminormed_add_comm_group E] {g : E} :

∥g∥₊ ≠ 0 → g ≠ 0

source

theorem nnnorm_add_le {E : Type u_3} [seminormed_add_comm_group E] (g h : E) :

∥g + h∥₊ ≤ ∥g∥₊ + ∥h∥₊

source

@[simp]

theorem nnnorm_neg {E : Type u_3} [seminormed_add_comm_group E] (g : E) :

∥-g∥₊ = ∥g∥₊

source

theorem nndist_nnnorm_nnnorm_le {E : Type u_3} [seminormed_add_comm_group E] (g h : E) :

has_nndist.nndist ∥g∥₊ ∥h∥₊ ≤ ∥g - h∥₊

source

theorem nnnorm_le_insert {E : Type u_3} [seminormed_add_comm_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} [seminormed_add_comm_group E] (u v : E) :

∥u∥₊ ≤ ∥v∥₊ + ∥u - v∥₊

source

theorem nnnorm_le_add_nnnorm_add {E : Type u_3} [seminormed_add_comm_group E] (u v : E) :

∥u∥₊ ≤ ∥u + v∥₊ + ∥v∥₊

source

theorem of_real_norm_eq_coe_nnnorm {E : Type u_3} [seminormed_add_comm_group E] (x : E) :

ennreal.of_real ∥x∥ = ↑∥x∥₊

source

theorem edist_eq_coe_nnnorm_sub {E : Type u_3} [seminormed_add_comm_group E] (x y : E) :

has_edist.edist x y = ↑∥x - y∥₊

source

theorem edist_eq_coe_nnnorm {E : Type u_3} [seminormed_add_comm_group E] (x : E) :

has_edist.edist x 0 = ↑∥x∥₊

source

theorem mem_emetric_ball_zero_iff {E : Type u_3} [seminormed_add_comm_group E] {x : E} {r : ennreal} :

x ∈ emetric.ball 0 r ↔ ↑∥x∥₊ < r

source

theorem nndist_add_add_le {E : Type u_3} [seminormed_add_comm_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} [seminormed_add_comm_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} [seminormed_add_comm_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} [seminormed_add_comm_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} [seminormed_add_comm_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} [seminormed_add_comm_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} [seminormed_add_comm_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} [seminormed_add_comm_group E] (g₁ g₂ h : E) :

has_edist.edist (g₁ - h) (g₂ - h) = has_edist.edist g₁ g₂

source

theorem nnnorm_multiset_sum_le {E : Type u_3} [seminormed_add_comm_group E] (m : multiset E) :

∥m.sum ∥₊ ≤ (multiset.map (λ (x : E), ∥x∥₊) m).sum

source

theorem nnnorm_sum_le {ι : Type u_2} {E : Type u_3} [seminormed_add_comm_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} [seminormed_add_comm_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_class.lipschitz_of_bound_nnnorm {E : Type u_3} {F : Type u_4} [seminormed_add_comm_group E] [seminormed_add_comm_group F] {𝓕 : Type u_1} [add_monoid_hom_class 𝓕 E F] (f : 𝓕) (C : nnreal) (h : ∀ (x : E), ∥⇑f x∥₊ ≤ C * ∥x∥₊) :

lipschitz_with C ⇑f

source

theorem add_monoid_hom_class.antilipschitz_of_bound {E : Type u_3} {F : Type u_4} [seminormed_add_comm_group E] [seminormed_add_comm_group F] {𝓕 : Type u_1} [add_monoid_hom_class 𝓕 E F] (f : 𝓕) {K : nnreal} (h : ∀ (x : E), ∥x∥ ≤ ↑K * ∥⇑f x∥) :

antilipschitz_with K ⇑f

source

theorem add_monoid_hom_class.bound_of_antilipschitz {E : Type u_3} {F : Type u_4} [seminormed_add_comm_group E] [seminormed_add_comm_group F] {𝓕 : Type u_1} [add_monoid_hom_class 𝓕 E F] (f : 𝓕) {K : nnreal} (h : antilipschitz_with K ⇑f) (x : E) :

∥x∥ ≤ ↑K * ∥⇑f x∥

source

theorem lipschitz_with.neg {α : Type u_1} {E : Type u_3} [seminormed_add_comm_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} [seminormed_add_comm_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} [seminormed_add_comm_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} [seminormed_add_comm_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} [seminormed_add_comm_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} [seminormed_add_comm_group E] [seminormed_add_comm_group F] {K : nnreal} {f : E → F} (hf : antilipschitz_with K f) (x y : E) :

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

source

@[reducible]

def seminormed_add_comm_group.induced {F : Type u_4} [seminormed_add_comm_group F] {E : Type u_1} [add_comm_group E] (f : E →+ F) :

seminormed_add_comm_group E

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

See note [reducible non-instances]

Equations

seminormed_add_comm_group.induced f = {to_has_norm := {norm := λ (x : E), ∥⇑f x∥}, to_add_comm_group := _inst_4, to_pseudo_metric_space := {to_has_dist := pseudo_metric_space.to_has_dist (pseudo_metric_space.induced ⇑f seminormed_add_comm_group.to_pseudo_metric_space), dist_self := _, dist_comm := _, dist_triangle := _, edist := pseudo_metric_space.edist (pseudo_metric_space.induced ⇑f seminormed_add_comm_group.to_pseudo_metric_space), edist_dist := _, to_uniform_space := pseudo_metric_space.to_uniform_space (pseudo_metric_space.induced ⇑f seminormed_add_comm_group.to_pseudo_metric_space), uniformity_dist := _, to_bornology := pseudo_metric_space.to_bornology (pseudo_metric_space.induced ⇑f seminormed_add_comm_group.to_pseudo_metric_space), cobounded_sets := _}, dist_eq := _}

source

@[protected, instance]

def add_subgroup.seminormed_add_comm_group {E : Type u_3} [seminormed_add_comm_group E] (s : add_subgroup E) :

seminormed_add_comm_group ↥s

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

Equations

s.seminormed_add_comm_group = seminormed_add_comm_group.induced s.subtype

source

@[simp]

theorem add_subgroup.coe_norm {E : Type u_1} [seminormed_add_comm_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} [seminormed_add_comm_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.seminormed_add_comm_group {𝕜 : Type u_1} {E : Type u_2} {_x : ring 𝕜} [seminormed_add_comm_group E] {_x_1 : module 𝕜 E} (s : submodule 𝕜 E) :

seminormed_add_comm_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

s.seminormed_add_comm_group = {to_has_norm := {norm := λ (x : ↥s), ∥↑x∥}, to_add_comm_group := s.add_comm_group, to_pseudo_metric_space := subtype.pseudo_metric_space (λ (x : E), x ∈ s), dist_eq := _}

source

@[simp]

theorem submodule.coe_norm {𝕜 : Type u_1} {_x : ring 𝕜} {E : Type u_2} [seminormed_add_comm_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} [seminormed_add_comm_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.seminormed_add_comm_group {E : Type u_3} [seminormed_add_comm_group E] :

seminormed_add_comm_group (ulift E)

Equations

ulift.seminormed_add_comm_group = seminormed_add_comm_group.induced {to_fun := ulift.down E, map_zero' := _, map_add' := _}

source

theorem ulift.norm_def {E : Type u_3} [seminormed_add_comm_group E] (x : ulift E) :

∥x∥ = ∥x.down ∥

source

theorem ulift.nnnorm_def {E : Type u_3} [seminormed_add_comm_group E] (x : ulift E) :

∥x∥₊ = ∥x.down ∥₊

source

@[simp]

theorem ulift.norm_up {E : Type u_3} [seminormed_add_comm_group E] (x : E) :

∥{down := x}∥ = ∥x∥

source

@[simp]

theorem ulift.nnnorm_up {E : Type u_3} [seminormed_add_comm_group E] (x : E) :

∥{down := x}∥₊ = ∥x∥₊

source

@[protected, instance]

noncomputable def prod.seminormed_add_comm_group {E : Type u_3} {F : Type u_4} [seminormed_add_comm_group E] [seminormed_add_comm_group F] :

seminormed_add_comm_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} [seminormed_add_comm_group E] [seminormed_add_comm_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} [seminormed_add_comm_group E] [seminormed_add_comm_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} [seminormed_add_comm_group E] [seminormed_add_comm_group F] (x : E × F) :

∥x.fst ∥ ≤ ∥x∥

source

theorem norm_snd_le {E : Type u_3} {F : Type u_4} [seminormed_add_comm_group E] [seminormed_add_comm_group F] (x : E × F) :

∥x.snd ∥ ≤ ∥x∥

source

theorem norm_prod_le_iff {E : Type u_3} {F : Type u_4} [seminormed_add_comm_group E] [seminormed_add_comm_group F] {x : E × F} {r : ℝ} :

∥x∥ ≤ r ↔ ∥x.fst ∥ ≤ r ∧ ∥x.snd ∥ ≤ r

source

@[protected, instance]

noncomputable def pi.seminormed_add_comm_group {ι : Type u_2} {π : ι → Type u_6} [fintype ι] [Π (i : ι), seminormed_add_comm_group (π i)] :

seminormed_add_comm_group (Π (i : ι), π i)

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

Equations

pi.seminormed_add_comm_group = {to_has_norm := {norm := λ (f : Π (i : ι), π i), ↑(finset.univ.sup (λ (b : ι), ∥f b∥₊))}, to_add_comm_group := pi.add_comm_group (λ (i : ι), seminormed_add_comm_group.to_add_comm_group), to_pseudo_metric_space := pseudo_metric_space_pi (λ (b : ι), seminormed_add_comm_group.to_pseudo_metric_space), dist_eq := _}

source

theorem pi.norm_def {ι : Type u_2} {π : ι → Type u_6} [fintype ι] [Π (i : ι), seminormed_add_comm_group (π i)] (f : Π (i : ι), π i) :

∥f∥ = ↑(finset.univ.sup (λ (b : ι), ∥f b∥₊))

source

theorem pi.nnnorm_def {ι : Type u_2} {π : ι → Type u_6} [fintype ι] [Π (i : ι), seminormed_add_comm_group (π i)] (f : Π (i : ι), π i) :

∥f∥₊ = finset.univ.sup (λ (b : ι), ∥f b∥₊)

source

theorem pi_norm_le_iff {ι : Type u_2} {π : ι → Type u_6} [fintype ι] [Π (i : ι), seminormed_add_comm_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_6} [fintype ι] [Π (i : ι), seminormed_add_comm_group (π i)] {r : nnreal} {x : Π (i : ι), π i} :

∥x∥₊ ≤ r ↔ ∀ (i : ι), ∥x i∥₊ ≤ r

source

theorem pi_norm_lt_iff {ι : Type u_2} {π : ι → Type u_6} [fintype ι] [Π (i : ι), seminormed_add_comm_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_6} [fintype ι] [Π (i : ι), seminormed_add_comm_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_6} [fintype ι] [Π (i : ι), seminormed_add_comm_group (π i)] (f : Π (i : ι), π i) (i : ι) :

∥f i∥ ≤ ∥f∥

source

theorem nnnorm_le_pi_nnnorm {ι : Type u_2} {π : ι → Type u_6} [fintype ι] [Π (i : ι), seminormed_add_comm_group (π i)] (f : Π (i : ι), π i) (i : ι) :

∥f i∥₊ ≤ ∥f∥₊

source

@[simp]

theorem pi_norm_const {ι : Type u_2} {E : Type u_3} [seminormed_add_comm_group E] [fintype ι] [nonempty ι] (a : E) :

∥(λ (i : ι), a)∥ = ∥a∥

source

@[simp]

theorem pi_nnnorm_const {ι : Type u_2} {E : Type u_3} [seminormed_add_comm_group E] [fintype ι] [nonempty ι] (a : E) :

∥(λ (i : ι), a)∥₊ = ∥a∥₊

source

theorem pi.sum_norm_apply_le_norm {ι : Type u_2} {π : ι → Type u_6} [fintype ι] [Π (i : ι), seminormed_add_comm_group (π i)] (f : Π (i : ι), π i) :

finset.univ.sum (λ (i : ι), ∥f i∥) ≤ fintype.card ι • ∥f∥

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_6} [fintype ι] [Π (i : ι), seminormed_add_comm_group (π i)] (f : Π (i : ι), π i) :

finset.univ.sum (λ (i : ι), ∥f i∥₊) ≤ fintype.card ι • ∥f∥₊

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} [seminormed_add_comm_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} [seminormed_add_comm_group E] {f : α → E} {a : filter α} :

filter.tendsto f a (nhds 0) ↔ filter.tendsto (λ (e : α), ∥f e∥) a (nhds 0)

source

theorem comap_norm_nhds_zero {E : Type u_3} [seminormed_add_comm_group E] :

filter.comap has_norm.norm (nhds 0) = nhds 0

source

theorem squeeze_zero_norm' {α : Type u_1} {E : Type u_3} [seminormed_add_comm_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} [seminormed_add_comm_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} [seminormed_add_comm_group E] (x : E) :

filter.tendsto (λ (g : E), ∥g - x∥) (nhds x) (nhds 0)

source

theorem lipschitz_with_one_norm {E : Type u_3} [seminormed_add_comm_group E] :

lipschitz_with 1 has_norm.norm

source

theorem lipschitz_with_one_nnnorm {E : Type u_3} [seminormed_add_comm_group E] :

lipschitz_with 1 has_nnnorm.nnnorm

source

theorem uniform_continuous_norm {E : Type u_3} [seminormed_add_comm_group E] :

uniform_continuous has_norm.norm

source

theorem uniform_continuous_nnnorm {E : Type u_3} [seminormed_add_comm_group E] :

uniform_continuous (λ (a : E), ∥a∥₊)

source

@[continuity]

theorem continuous_norm {E : Type u_3} [seminormed_add_comm_group E] :

continuous (λ (g : E), ∥g∥)

source

@[continuity]

theorem continuous_nnnorm {E : Type u_3} [seminormed_add_comm_group E] :

continuous (λ (a : E), ∥a∥₊)

source

theorem tendsto_norm {E : Type u_3} [seminormed_add_comm_group E] {x : E} :

filter.tendsto (λ (g : E), ∥g∥) (nhds x) (nhds ∥x∥)

source

theorem tendsto_norm_zero {E : Type u_3} [seminormed_add_comm_group E] :

filter.tendsto (λ (g : E), ∥g∥) (nhds 0) (nhds 0)

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} [seminormed_add_comm_group E] [seminormed_add_comm_group F] [seminormed_add_comm_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} [seminormed_add_comm_group E] [seminormed_add_comm_group F] [seminormed_add_comm_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} [seminormed_add_comm_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} [seminormed_add_comm_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} [seminormed_add_comm_group E] [topological_space α] {f : α → E} (h : continuous f) :

continuous (λ (x : α), ∥f x∥)

source

theorem continuous.nnnorm {α : Type u_1} {E : Type u_3} [seminormed_add_comm_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} [seminormed_add_comm_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} [seminormed_add_comm_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} [seminormed_add_comm_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} [seminormed_add_comm_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} [seminormed_add_comm_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} [seminormed_add_comm_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} [seminormed_add_comm_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 seminormed_add_comm_group.has_lipschitz_add {E : Type u_3} [seminormed_add_comm_group E] :

has_lipschitz_add E

source

@[protected, instance]

def normed_uniform_group {E : Type u_3} [seminormed_add_comm_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} [seminormed_add_comm_group E] :

topological_add_group E

source

theorem seminormed_add_comm_group.mem_closure_iff {E : Type u_3} [seminormed_add_comm_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} [seminormed_add_comm_group E] [t0_space E] {g : E} :

∥g∥ ≤ 0 ↔ g = 0

source

theorem norm_eq_zero_iff' {E : Type u_3} [seminormed_add_comm_group E] [t0_space E] {g : E} :

∥g∥ = 0 ↔ g = 0

source

theorem norm_pos_iff' {E : Type u_3} [seminormed_add_comm_group E] [t0_space E] {g : E} :

0 < ∥g∥ ↔ g ≠ 0

source

theorem cauchy_seq_sum_of_eventually_eq {E : Type u_3} [seminormed_add_comm_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_add_comm_group.of_separation {E : Type u_3} [h₁ : seminormed_add_comm_group E] (h₂ : ∀ (x : E), ∥x∥ = 0 → x = 0) :

normed_add_comm_group E

Construct a normed_add_comm_group from a seminormed_add_comm_group satisfying ∀ x, ∥x∥ = 0 → x = 0. This avoids having to go back to the (pseudo_)metric_space level when declaring a normed_add_comm_group instance as a special case of a more general seminormed_add_comm_group instance.

Equations

normed_add_comm_group.of_separation h₂ = {to_has_norm := seminormed_add_comm_group.to_has_norm h₁, to_add_comm_group := seminormed_add_comm_group.to_add_comm_group h₁, to_metric_space := {to_pseudo_metric_space := seminormed_add_comm_group.to_pseudo_metric_space h₁, eq_of_dist_eq_zero := _}, dist_eq := _}

source

def normed_add_comm_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_add_comm_group E

Construct a normed group from a translation invariant distance

Equations

normed_add_comm_group.of_add_dist H1 H2 = {to_has_norm := _inst_1, to_add_comm_group := _inst_2, to_metric_space := _inst_3, dist_eq := _}

source

structure normed_add_comm_group.core (E : Type u_6) [add_comm_group E] [has_norm E] :

Prop

norm_eq_zero_iff : ∀ (x : E), ∥x∥ = 0 ↔ x = 0
triangle : ∀ (x y : E), ∥x + y∥ ≤ ∥x∥ + ∥y∥
norm_neg : ∀ (x : E), ∥-x∥ = ∥x∥

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

source

theorem normed_add_comm_group.core.to_seminormed_add_comm_group.core {E : Type u_1} [add_comm_group E] [has_norm E] (C : normed_add_comm_group.core E) :

seminormed_add_comm_group.core E

The seminormed_add_comm_group.core induced by a normed_add_comm_group.core.

source

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

normed_add_comm_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

normed_add_comm_group.of_core E C = {to_has_norm := seminormed_add_comm_group.to_has_norm (seminormed_add_comm_group.of_core E _), to_add_comm_group := seminormed_add_comm_group.to_add_comm_group (seminormed_add_comm_group.of_core E _), to_metric_space := {to_pseudo_metric_space := seminormed_add_comm_group.to_pseudo_metric_space (seminormed_add_comm_group.of_core E _), eq_of_dist_eq_zero := _}, dist_eq := _}

source

@[simp]

theorem norm_eq_zero {E : Type u_3} [normed_add_comm_group E] {g : E} :

∥g∥ = 0 ↔ g = 0

source

theorem norm_ne_zero_iff {E : Type u_3} [normed_add_comm_group E] {g : E} :

∥g∥ ≠ 0 ↔ g ≠ 0

source

@[simp]

theorem norm_pos_iff {E : Type u_3} [normed_add_comm_group E] {g : E} :

0 < ∥g∥ ↔ g ≠ 0

source

@[simp]

theorem norm_le_zero_iff {E : Type u_3} [normed_add_comm_group E] {g : E} :

∥g∥ ≤ 0 ↔ g = 0

source

theorem norm_sub_eq_zero_iff {E : Type u_3} [normed_add_comm_group E] {u v : E} :

∥u - v∥ = 0 ↔ u = v

source

theorem norm_sub_pos_iff {E : Type u_3} [normed_add_comm_group E] {x y : E} :

0 < ∥x - y∥ ↔ x ≠ y

source

theorem eq_of_norm_sub_le_zero {E : Type u_3} [normed_add_comm_group E] {g h : E} (a : ∥g - h∥ ≤ 0) :

g = h

source

theorem eq_of_norm_sub_eq_zero {E : Type u_3} [normed_add_comm_group E] {u v : E} (h : ∥u - v∥ = 0) :

u = v

source

@[simp]

theorem nnnorm_eq_zero {E : Type u_3} [normed_add_comm_group E] {a : E} :

∥a∥₊ = 0 ↔ a = 0

source

theorem nnnorm_ne_zero_iff {E : Type u_3} [normed_add_comm_group E] {g : E} :

∥g∥₊ ≠ 0 ↔ g ≠ 0

source

def norm_add_group_norm (E : Type u_3) [normed_add_comm_group E] :

add_group_norm E

The norm of a normed group as an additive group norm.

Equations

norm_add_group_norm E = {to_fun := has_norm.norm normed_add_comm_group.to_has_norm, map_zero' := _, add_le' := _, neg' := _, eq_zero_of_map_eq_zero' := _}

source

@[simp]

theorem coe_norm_add_group_norm (E : Type u_3) [normed_add_comm_group E] :

⇑(norm_add_group_norm E) = has_norm.norm

source

@[reducible]

def normed_add_comm_group.induced {F : Type u_4} [normed_add_comm_group F] {E : Type u_1} [add_comm_group E] (f : E →+ F) (h : function.injective ⇑f) :

normed_add_comm_group E

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

See note [reducible non-instances].

Equations

normed_add_comm_group.induced f h = {to_has_norm := seminormed_add_comm_group.to_has_norm (seminormed_add_comm_group.induced f), to_add_comm_group := seminormed_add_comm_group.to_add_comm_group (seminormed_add_comm_group.induced f), to_metric_space := {to_pseudo_metric_space := seminormed_add_comm_group.to_pseudo_metric_space (seminormed_add_comm_group.induced f), eq_of_dist_eq_zero := _}, dist_eq := _}

source

@[protected, instance]

def add_subgroup.normed_add_comm_group {E : Type u_3} [normed_add_comm_group E] (s : add_subgroup E) :

normed_add_comm_group ↥s

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

Equations

s.normed_add_comm_group = normed_add_comm_group.induced s.subtype _

source

@[protected, instance]

def submodule.normed_add_comm_group {𝕜 : Type u_1} {E : Type u_2} {_x : ring 𝕜} [normed_add_comm_group E] {_x_1 : module 𝕜 E} (s : submodule 𝕜 E) :

normed_add_comm_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

s.normed_add_comm_group = {to_has_norm := seminormed_add_comm_group.to_has_norm s.seminormed_add_comm_group, to_add_comm_group := seminormed_add_comm_group.to_add_comm_group s.seminormed_add_comm_group, to_metric_space := subtype.metric_space normed_add_comm_group.to_metric_space, dist_eq := _}

source

@[protected, instance]

def ulift.normed_add_comm_group {E : Type u_3} [normed_add_comm_group E] :

normed_add_comm_group (ulift E)

Equations

ulift.normed_add_comm_group = {to_has_norm := seminormed_add_comm_group.to_has_norm ulift.seminormed_add_comm_group, to_add_comm_group := seminormed_add_comm_group.to_add_comm_group ulift.seminormed_add_comm_group, to_metric_space := ulift.metric_space normed_add_comm_group.to_metric_space, dist_eq := _}

source

@[protected, instance]

noncomputable def prod.normed_add_comm_group {E : Type u_3} {F : Type u_4} [normed_add_comm_group E] [normed_add_comm_group F] :

normed_add_comm_group (E × F)

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

Equations

prod.normed_add_comm_group = {to_has_norm := seminormed_add_comm_group.to_has_norm prod.seminormed_add_comm_group, to_add_comm_group := seminormed_add_comm_group.to_add_comm_group prod.seminormed_add_comm_group, to_metric_space := prod.metric_space_max normed_add_comm_group.to_metric_space, dist_eq := _}

source

@[protected, instance]

noncomputable def pi.normed_add_comm_group {ι : Type u_2} {π : ι → Type u_1} [fintype ι] [Π (i : ι), normed_add_comm_group (π i)] :

normed_add_comm_group (Π (i : ι), π i)

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

Equations

pi.normed_add_comm_group = {to_has_norm := seminormed_add_comm_group.to_has_norm pi.seminormed_add_comm_group, to_add_comm_group := seminormed_add_comm_group.to_add_comm_group pi.seminormed_add_comm_group, to_metric_space := metric_space_pi (λ (b : ι), normed_add_comm_group.to_metric_space), dist_eq := _}

source

theorem tendsto_norm_sub_self_punctured_nhds {E : Type u_3} [normed_add_comm_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_add_comm_group E] :

filter.tendsto has_norm.norm (nhds_within 0 {0}ᶜ) (nhds_within 0 (set.Ioi 0))

source

theorem has_compact_support_norm_iff {α : Type u_1} {E : Type u_3} [normed_add_comm_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_add_comm_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_add_comm_group E] [topological_space α] {f : α → E} (hf : continuous f) (hsupp : has_compact_support f) :

∃ (C : ℝ), ∀ (x : α), ∥f x∥ ≤ C

mathlib documentation

Normed (semi)groups #

Tags #