mathlib documentation

@[class]

structure normed_group (α : Type u_5) :

Type u_5

to_has_norm : has_norm α
to_add_comm_group : add_comm_group α
to_metric_space : metric_space α
dist_eq : ∀ (x y : α), 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

def normed_group.of_add_dist {α : Type u_1} [has_norm α] [add_comm_group α] [metric_space α] (H1 : ∀ (x : α), ∥x∥ = dist x 0) (H2 : ∀ (x y z : α), dist x y ≤ dist (x + z) (y + z)) :

Construct a normed group from a translation invariant distance

Equations

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

def normed_group.of_add_dist' {α : Type u_1} [has_norm α] [add_comm_group α] [metric_space α] (H1 : ∀ (x : α), ∥x∥ = dist x 0) (H2 : ∀ (x y z : α), dist (x + z) (y + z) ≤ dist x y) :

Construct a normed group from a translation invariant distance

Equations

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

structure normed_group.core (α : Type u_5) [add_comm_group α] [has_norm α] :

Prop

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

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

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

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_group.of_core α C = {to_has_norm := _inst_2, to_add_comm_group := _inst_1, to_metric_space := {to_has_dist := {dist := λ (x y : α), ∥x - y∥}, dist_self := _, eq_of_dist_eq_zero := _, dist_comm := _, dist_triangle := _, edist := λ (x y : α), ennreal.of_real ((λ (x y : α), ∥x - y∥) x y), edist_dist := _, to_uniform_space := uniform_space_of_dist (λ (x y : α), ∥x - y∥) _ _ _, uniformity_dist := _}, dist_eq := _}

theorem dist_eq_norm {α : Type u_1} [normed_group α] (g h : α) :

dist g h = ∥g - h∥

@[simp]

theorem dist_zero_right {α : Type u_1} [normed_group α] (g : α) :

dist g 0 = ∥g∥

theorem norm_sub_rev {α : Type u_1} [normed_group α] (g h : α) :

∥g - h∥ = ∥h - g∥

@[simp]

theorem norm_neg {α : Type u_1} [normed_group α] (g : α) :

∥-g∥ = ∥g∥

@[simp]

theorem dist_add_left {α : Type u_1} [normed_group α] (g h₁ h₂ : α) :

dist (g + h₁) (g + h₂) = dist h₁ h₂

@[simp]

theorem dist_add_right {α : Type u_1} [normed_group α] (g₁ g₂ h : α) :

dist (g₁ + h) (g₂ + h) = dist g₁ g₂

@[simp]

theorem dist_neg_neg {α : Type u_1} [normed_group α] (g h : α) :

dist (-g) (-h) = dist g h

@[simp]

theorem dist_sub_left {α : Type u_1} [normed_group α] (g h₁ h₂ : α) :

dist (g - h₁) (g - h₂) = dist h₁ h₂

@[simp]

theorem dist_sub_right {α : Type u_1} [normed_group α] (g₁ g₂ h : α) :

dist (g₁ - h) (g₂ - h) = dist g₁ g₂

theorem norm_add_le {α : Type u_1} [normed_group α] (g h : α) :

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

Triangle inequality for the norm.

theorem norm_add_le_of_le {α : Type u_1} [normed_group α] {g₁ g₂ : α} {n₁ n₂ : ℝ} (H₁ : ∥g₁∥ ≤ n₁) (H₂ : ∥g₂∥ ≤ n₂) :

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

theorem dist_add_add_le {α : Type u_1} [normed_group α] (g₁ g₂ h₁ h₂ : α) :

dist (g₁ + g₂) (h₁ + h₂) ≤ dist g₁ h₁ + dist g₂ h₂

theorem dist_add_add_le_of_le {α : Type u_1} [normed_group α] {g₁ g₂ h₁ h₂ : α} {d₁ d₂ : ℝ} (H₁ : dist g₁ h₁ ≤ d₁) (H₂ : dist g₂ h₂ ≤ d₂) :

dist (g₁ + g₂) (h₁ + h₂) ≤ d₁ + d₂

theorem dist_sub_sub_le {α : Type u_1} [normed_group α] (g₁ g₂ h₁ h₂ : α) :

dist (g₁ - g₂) (h₁ - h₂) ≤ dist g₁ h₁ + dist g₂ h₂

theorem dist_sub_sub_le_of_le {α : Type u_1} [normed_group α] {g₁ g₂ h₁ h₂ : α} {d₁ d₂ : ℝ} (H₁ : dist g₁ h₁ ≤ d₁) (H₂ : dist g₂ h₂ ≤ d₂) :

dist (g₁ - g₂) (h₁ - h₂) ≤ d₁ + d₂

theorem abs_dist_sub_le_dist_add_add {α : Type u_1} [normed_group α] (g₁ g₂ h₁ h₂ : α) :

abs (dist g₁ h₁ - dist g₂ h₂) ≤ dist (g₁ + g₂) (h₁ + h₂)

@[simp]

theorem norm_nonneg {α : Type u_1} [normed_group α] (g : α) :

0 ≤ ∥g∥

@[simp]

theorem norm_eq_zero {α : Type u_1} [normed_group α] {g : α} :

∥g∥ = 0 ↔ g = 0

@[simp]

theorem norm_zero {α : Type u_1} [normed_group α] :

∥0∥ = 0

theorem norm_sum_le {α : Type u_1} [normed_group α] {β : Type u_2} (s : finset β) (f : β → α) :

∥∑ (a : β) in s, f a∥ ≤ ∑ (a : β) in s, ∥f a∥

theorem norm_sum_le_of_le {α : Type u_1} [normed_group α] {β : Type u_2} (s : finset β) {f : β → α} {n : β → ℝ} (h : ∀ (b : β), b ∈ s → ∥f b∥ ≤ n b) :

∥∑ (b : β) in s, f b∥ ≤ ∑ (b : β) in s, n b

theorem norm_pos_iff {α : Type u_1} [normed_group α] {g : α} :

0 < ∥g∥ ↔ g ≠ 0

theorem norm_le_zero_iff {α : Type u_1} [normed_group α] {g : α} :

∥g∥ ≤ 0 ↔ g = 0

theorem norm_sub_le {α : Type u_1} [normed_group α] (g h : α) :

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

theorem norm_sub_le_of_le {α : Type u_1} [normed_group α] {g₁ g₂ : α} {n₁ n₂ : ℝ} (H₁ : ∥g₁∥ ≤ n₁) (H₂ : ∥g₂∥ ≤ n₂) :

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

theorem dist_le_norm_add_norm {α : Type u_1} [normed_group α] (g h : α) :

dist g h ≤ ∥g∥ + ∥h∥

theorem abs_norm_sub_norm_le {α : Type u_1} [normed_group α] (g h : α) :

abs (∥g∥ - ∥h∥) ≤ ∥g - h∥

theorem norm_sub_norm_le {α : Type u_1} [normed_group α] (g h : α) :

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

theorem dist_norm_norm_le {α : Type u_1} [normed_group α] (g h : α) :

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

theorem eq_of_norm_sub_eq_zero {α : Type u_1} [normed_group α] {u v : α} (h : ∥u - v∥ = 0) :

u = v

theorem norm_le_insert {α : Type u_1} [normed_group α] (u v : α) :

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

theorem ball_0_eq {α : Type u_1} [normed_group α] (ε : ℝ) :

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

theorem norm_le_of_mem_closed_ball {α : Type u_1} [normed_group α] {g h : α} {r : ℝ} (H : h ∈ metric.closed_ball g r) :

∥h∥ ≤ ∥g∥ + r

theorem norm_lt_of_mem_ball {α : Type u_1} [normed_group α] {g h : α} {r : ℝ} (H : h ∈ metric.ball g r) :

∥h∥ < ∥g∥ + r

theorem normed_group.tendsto_nhds_zero {α : Type u_1} {γ : Type u_3} [normed_group α] {f : γ → α} {l : filter γ} :

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

theorem normed_group.tendsto_nhds_nhds {α : Type u_1} {β : Type u_2} [normed_group α] [normed_group β] {f : α → β} {x : α} {y : β} :

(f→_{x}y) ↔ ∀ (ε : ℝ), ε > 0 → (∃ (δ : ℝ) (H : δ > 0), ∀ (x' : α), ∥x' - x∥ < δ → ∥f x' - y∥ < ε)

theorem add_monoid_hom.lipschitz_of_bound {α : Type u_1} {β : Type u_2} [normed_group α] [normed_group β] (f : α →+ β) (C : ℝ) (h : ∀ (x : α), ∥⇑f x∥ ≤ C * ∥x∥) :

lipschitz_with (nnreal.of_real C) ⇑f

A homomorphism f of normed 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 normed spaces is in normed_space.operator_norm.

theorem lipschitz_on_with_iff_norm_sub_le {α : Type u_1} {β : Type u_2} [normed_group α] [normed_group β] {f : α → β} {C : ℝ≥0} {s : set α} :

lipschitz_on_with C f s ↔ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → ∥f x - f y∥ ≤ (↑C) * ∥x - y∥

theorem lipschitz_on_with.norm_sub_le {α : Type u_1} {β : Type u_2} [normed_group α] [normed_group β] {f : α → β} {C : ℝ≥0} {s : set α} (h : lipschitz_on_with C f s) {x y : α} (x_in : x ∈ s) (y_in : y ∈ s) :

∥f x - f y∥ ≤ (↑C) * ∥x - y∥

theorem add_monoid_hom.continuous_of_bound {α : Type u_1} {β : Type u_2} [normed_group α] [normed_group β] (f : α →+ β) (C : ℝ) (h : ∀ (x : α), ∥⇑f x∥ ≤ C * ∥x∥) :

continuous ⇑f

A homomorphism f of normed 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.

def nnnorm {α : Type u_1} [normed_group α] (a : α) :

ℝ≥0

Version of the norm taking values in nonnegative reals.

Equations

nnnorm a = ⟨∥a∥, _⟩

@[simp]

theorem coe_nnnorm {α : Type u_1} [normed_group α] (a : α) :

↑(nnnorm a) = ∥a∥

theorem nndist_eq_nnnorm {α : Type u_1} [normed_group α] (a b : α) :

nndist a b = nnnorm (a - b)

@[simp]

theorem nnnorm_eq_zero {α : Type u_1} [normed_group α] {a : α} :

nnnorm a = 0 ↔ a = 0

@[simp]

theorem nnnorm_zero {α : Type u_1} [normed_group α] :

nnnorm 0 = 0

theorem nnnorm_add_le {α : Type u_1} [normed_group α] (g h : α) :

nnnorm (g + h) ≤ nnnorm g + nnnorm h

@[simp]

theorem nnnorm_neg {α : Type u_1} [normed_group α] (g : α) :

nnnorm (-g) = nnnorm g

theorem nndist_nnnorm_nnnorm_le {α : Type u_1} [normed_group α] (g h : α) :

nndist (nnnorm g) (nnnorm h) ≤ nnnorm (g - h)

theorem of_real_norm_eq_coe_nnnorm {β : Type u_2} [normed_group β] (x : β) :

ennreal.of_real ∥x∥ = ↑(nnnorm x)

theorem edist_eq_coe_nnnorm_sub {β : Type u_2} [normed_group β] (x y : β) :

edist x y = ↑(nnnorm (x - y))

theorem edist_eq_coe_nnnorm {β : Type u_2} [normed_group β] (x : β) :

edist x 0 = ↑(nnnorm x)

theorem nndist_add_add_le {α : Type u_1} [normed_group α] (g₁ g₂ h₁ h₂ : α) :

nndist (g₁ + g₂) (h₁ + h₂) ≤ nndist g₁ h₁ + nndist g₂ h₂

theorem edist_add_add_le {α : Type u_1} [normed_group α] (g₁ g₂ h₁ h₂ : α) :

edist (g₁ + g₂) (h₁ + h₂) ≤ edist g₁ h₁ + edist g₂ h₂

theorem nnnorm_sum_le {α : Type u_1} [normed_group α] {β : Type u_2} (s : finset β) (f : β → α) :

nnnorm (∑ (a : β) in s, f a) ≤ ∑ (a : β) in s, nnnorm (f a)

theorem lipschitz_with.neg {β : Type u_2} [normed_group β] {α : Type u_1} [emetric_space α] {K : ℝ≥0} {f : α → β} (hf : lipschitz_with K f) :

lipschitz_with K (λ (x : α), -f x)

theorem lipschitz_with.add {β : Type u_2} [normed_group β] {α : Type u_1} [emetric_space α] {Kf : ℝ≥0} {f : α → β} (hf : lipschitz_with Kf f) {Kg : ℝ≥0} {g : α → β} (hg : lipschitz_with Kg g) :

lipschitz_with (Kf + Kg) (λ (x : α), f x + g x)

theorem lipschitz_with.sub {β : Type u_2} [normed_group β] {α : Type u_1} [emetric_space α] {Kf : ℝ≥0} {f : α → β} (hf : lipschitz_with Kf f) {Kg : ℝ≥0} {g : α → β} (hg : lipschitz_with Kg g) :

lipschitz_with (Kf + Kg) (λ (x : α), f x - g x)

theorem antilipschitz_with.add_lipschitz_with {β : Type u_2} [normed_group β] {α : Type u_1} [metric_space α] {Kf : ℝ≥0} {f : α → β} (hf : antilipschitz_with Kf f) {Kg : ℝ≥0} {g : α → β} (hg : lipschitz_with Kg g) (hK : Kg < Kf⁻¹) :

antilipschitz_with (Kf⁻¹ - Kg)⁻¹ (λ (x : α), f x + g x)

@[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. As all instances can be inferred from the submodule s, they are put as implicit instead of typeclasses.

Equations

s.normed_group = {to_has_norm := {norm := λ (x : ↥s), ∥↑x∥}, to_add_comm_group := s.add_comm_group, to_metric_space := subtype.metric_space normed_group.to_metric_space, dist_eq := _}

@[instance]

def prod.normed_group {α : Type u_1} {β : Type u_2} [normed_group α] [normed_group β] :

normed_group (α × β)

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

Equations

prod.normed_group = {to_has_norm := {norm := λ (x : α × β), max ∥x.fst ∥ ∥x.snd ∥}, to_add_comm_group := prod.add_comm_group normed_group.to_add_comm_group, to_metric_space := prod.metric_space_max normed_group.to_metric_space, dist_eq := _}

theorem prod.norm_def {α : Type u_1} {β : Type u_2} [normed_group α] [normed_group β] (x : α × β) :

∥x∥ = max ∥x.fst ∥ ∥x.snd ∥

theorem prod.nnnorm_def {α : Type u_1} {β : Type u_2} [normed_group α] [normed_group β] (x : α × β) :

nnnorm x = max (nnnorm x.fst) (nnnorm x.snd)

theorem norm_fst_le {α : Type u_1} {β : Type u_2} [normed_group α] [normed_group β] (x : α × β) :

∥x.fst ∥ ≤ ∥x∥

theorem norm_snd_le {α : Type u_1} {β : Type u_2} [normed_group α] [normed_group β] (x : α × β) :

∥x.snd ∥ ≤ ∥x∥

theorem norm_prod_le_iff {α : Type u_1} {β : Type u_2} [normed_group α] [normed_group β] {x : α × β} {r : ℝ} :

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

@[instance]

def pi.normed_group {ι : Type u_4} {π : ι → 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

pi.normed_group = {to_has_norm := {norm := λ (f : Π (i : ι), «π» i), ↑(finset.univ.sup (λ (b : ι), nnnorm (f b)))}, to_add_comm_group := pi.add_comm_group (λ (i : ι), normed_group.to_add_comm_group), to_metric_space := metric_space_pi (λ (b : ι), normed_group.to_metric_space), dist_eq := _}

theorem pi_norm_le_iff {ι : Type u_4} {π : ι → Type u_1} [fintype ι] [Π (i : ι), normed_group («π» i)] {r : ℝ} (hr : 0 ≤ r) {x : Π (i : ι), «π» i} :

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

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

theorem norm_le_pi_norm {ι : Type u_4} {π : ι → Type u_1} [fintype ι] [Π (i : ι), normed_group («π» i)] (x : Π (i : ι), «π» i) (i : ι) :

∥x i∥ ≤ ∥x∥

theorem tendsto_iff_norm_tendsto_zero {β : Type u_2} {ι : Type u_4} [normed_group β] {f : ι → β} {a : filter ι} {b : β} :

filter.tendsto f a (𝓝 b) ↔ filter.tendsto (λ (e : ι), ∥f e - b∥) a (𝓝 0)

theorem tendsto_zero_iff_norm_tendsto_zero {β : Type u_2} {γ : Type u_3} [normed_group β] {f : γ → β} {a : filter γ} :

filter.tendsto f a (𝓝 0) ↔ filter.tendsto (λ (e : γ), ∥f e∥) a (𝓝 0)

theorem squeeze_zero_norm' {α : Type u_1} {γ : Type u_3} [normed_group α] {f : γ → α} {g : γ → ℝ} {t₀ : filter γ} (h : ∀ᶠ (n : γ) in t₀, ∥f n∥ ≤ g n) (h' : filter.tendsto g t₀ (𝓝 0)) :

filter.tendsto f t₀ (𝓝 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.ordered, the ' version is phrased using "eventually" and the non-' version is phrased absolutely.

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

filter.tendsto f t₀ (𝓝 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.

theorem lim_norm {α : Type u_1} [normed_group α] (x : α) :

(λ (g : α), ∥g - x∥)→_{x}0

theorem lim_norm_zero {α : Type u_1} [normed_group α] :

(λ (g : α), ∥g∥)→_{0}0

theorem continuous_norm {α : Type u_1} [normed_group α] :

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

theorem filter.tendsto.norm {α : Type u_1} [normed_group α] {β : Type u_2} {l : filter β} {f : β → α} {a : α} (h : filter.tendsto f l (𝓝 a)) :

filter.tendsto (λ (x : β), ∥f x∥) l (𝓝 ∥a∥)

theorem continuous_nnnorm {α : Type u_1} [normed_group α] :

continuous nnnorm

theorem filter.tendsto.nnnorm {α : Type u_1} [normed_group α] {β : Type u_2} {l : filter β} {f : β → α} {a : α} (h : filter.tendsto f l (𝓝 a)) :

filter.tendsto (λ (x : β), nnnorm (f x)) l (𝓝 (nnnorm a))

theorem eventually_ne_of_tendsto_norm_at_top {α : Type u_1} {γ : Type u_3} [normed_group α] {l : filter γ} {f : γ → α} (h : filter.tendsto (λ (y : γ), ∥f y∥) l filter.at_top) (x : α) :

∀ᶠ (y : γ) in l, f y ≠ x

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

@[instance]

def normed_uniform_group {α : Type u_1} [normed_group α] :

uniform_add_group α

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

@[instance]

def normed_top_monoid {α : Type u_1} [normed_group α] :

has_continuous_add α

@[instance]

def normed_top_group {α : Type u_1} [normed_group α] :

topological_add_group α

@[class]

structure normed_ring (α : Type u_5) :

Type u_5

to_has_norm : has_norm α
to_ring : ring α
to_metric_space : metric_space α
dist_eq : ∀ (x y : α), dist x y = ∥x - y∥
norm_mul : ∀ (a b : α), ∥a * b∥ ≤ ∥a∥ * ∥b∥

A normed ring is a ring endowed with a norm which satisfies the inequality ∥x y∥ ≤ ∥x∥ ∥y∥.

Instances

@[class]

structure normed_comm_ring (α : Type u_5) :

Type u_5

to_normed_ring : normed_ring α
mul_comm : ∀ (x y : α), x * y = y * x

A normed commutative ring is a commutative ring endowed with a norm which satisfies the inequality ∥x y∥ ≤ ∥x∥ ∥y∥.

Instances

normed_field.to_normed_comm_ring

@[instance]

def normed_comm_ring.to_comm_ring {α : Type u_1} [β : normed_comm_ring α] :

comm_ring α

Equations

normed_comm_ring.to_comm_ring = {add := ring.add normed_ring.to_ring, add_assoc := _, zero := ring.zero normed_ring.to_ring, zero_add := _, add_zero := _, neg := ring.neg normed_ring.to_ring, add_left_neg := _, add_comm := _, mul := ring.mul normed_ring.to_ring, mul_assoc := _, one := ring.one normed_ring.to_ring, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _}

@[instance]

def normed_ring.to_normed_group {α : Type u_1} [β : normed_ring α] :

Equations

normed_ring.to_normed_group = {to_has_norm := normed_ring.to_has_norm β, to_add_comm_group := {add := ring.add normed_ring.to_ring, add_assoc := _, zero := ring.zero normed_ring.to_ring, zero_add := _, add_zero := _, neg := ring.neg normed_ring.to_ring, add_left_neg := _, add_comm := _}, to_metric_space := normed_ring.to_metric_space β, dist_eq := _}

theorem norm_mul_le {α : Type u_1} [normed_ring α] (a b : α) :

∥a * b∥ ≤ ∥a∥ * ∥b∥

theorem norm_pow_le {α : Type u_1} [normed_ring α] (a : α) {n : ℕ} (a_1 : 0 < n) :

∥a ^ n∥ ≤ ∥a∥ ^ n

theorem eventually_norm_pow_le {α : Type u_1} [normed_ring α] (a : α) :

∀ᶠ (n : ℕ) in filter.at_top, ∥a ^ n∥ ≤ ∥a∥ ^ n

theorem units.norm_pos {α : Type u_1} [normed_ring α] [nontrivial α] (x : units α) :

0 < ∥↑x∥

theorem mul_left_bound {α : Type u_1} [normed_ring α] (x y : α) :

∥⇑(add_monoid_hom.mul_left x) y∥ ≤ ∥x∥ * ∥y∥

In a normed ring, the left-multiplication add_monoid_hom is bounded.

theorem mul_right_bound {α : Type u_1} [normed_ring α] (x y : α) :

∥⇑(add_monoid_hom.mul_right x) y∥ ≤ ∥x∥ * ∥y∥

In a normed ring, the right-multiplication add_monoid_hom is bounded.

@[instance]

def prod.normed_ring {α : Type u_1} {β : Type u_2} [normed_ring α] [normed_ring β] :

normed_ring (α × β)

Normed ring structure on the product of two normed rings, using the sup norm.

Equations

prod.normed_ring = {to_has_norm := normed_group.to_has_norm prod.normed_group, to_ring := prod.ring normed_ring.to_ring, to_metric_space := normed_group.to_metric_space prod.normed_group, dist_eq := _, norm_mul := _}

@[instance]

def normed_ring_top_monoid {α : Type u_1} [normed_ring α] :

has_continuous_mul α

@[instance]

def normed_top_ring {α : Type u_1} [normed_ring α] :

topological_ring α

A normed ring is a topological ring.

@[class]

structure normed_field (α : Type u_5) :

Type u_5

to_has_norm : has_norm α
to_field : field α
to_metric_space : metric_space α
dist_eq : ∀ (x y : α), dist x y = ∥x - y∥
norm_mul' : ∀ (a b : α), ∥a * b∥ = ∥a∥ * ∥b∥

A normed field is a field with a norm satisfying ∥x y∥ = ∥x∥ ∥y∥.

Instances

@[class]

structure nondiscrete_normed_field (α : Type u_5) :

Type u_5

to_normed_field : normed_field α
non_trivial : ∃ (x : α), 1 < ∥x∥

A nondiscrete normed field is a normed field in which there is an element of norm different from 0 and 1. This makes it possible to bring any element arbitrarily close to 0 by multiplication by the powers of any element, and thus to relate algebra and topology.

Instances

@[simp]

theorem normed_field.norm_mul {α : Type u_1} [normed_field α] (a b : α) :

∥a * b∥ = ∥a∥ * ∥b∥

@[instance]

def normed_field.to_normed_comm_ring {α : Type u_1} [normed_field α] :

normed_comm_ring α

Equations

normed_field.to_normed_comm_ring = {to_normed_ring := {to_has_norm := normed_field.to_has_norm _inst_1, to_ring := {add := field.add normed_field.to_field, add_assoc := _, zero := field.zero normed_field.to_field, zero_add := _, add_zero := _, neg := field.neg normed_field.to_field, add_left_neg := _, add_comm := _, mul := field.mul normed_field.to_field, mul_assoc := _, one := field.one normed_field.to_field, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _}, to_metric_space := normed_field.to_metric_space _inst_1, dist_eq := _, norm_mul := _}, mul_comm := _}

@[simp]

theorem normed_field.norm_one {α : Type u_1} [normed_field α] :

∥1∥ = 1

@[simp]

theorem normed_field.nnnorm_one {α : Type u_1} [normed_field α] :

nnnorm 1 = 1

def normed_field.norm_hom {α : Type u_1} [normed_field α] :

α →* ℝ

norm as a monoid_hom.

Equations

normed_field.norm_hom = {to_fun := norm normed_field.to_has_norm, map_one' := _, map_mul' := _}

@[simp]

theorem normed_field.norm_hom_to_fun {α : Type u_1} [normed_field α] (a : α) :

⇑normed_field.norm_hom a = ∥a∥

@[simp]

theorem normed_field.norm_pow {α : Type u_1} [normed_field α] (a : α) (n : ℕ) :

∥a ^ n∥ = ∥a∥ ^ n

@[simp]

theorem normed_field.norm_prod {α : Type u_1} {β : Type u_2} [normed_field α] (s : finset β) (f : β → α) :

∥∏ (b : β) in s, f b∥ = ∏ (b : β) in s, ∥f b∥

@[simp]

theorem normed_field.norm_div {α : Type u_1} [normed_field α] (a b : α) :

∥a / b∥ = ∥a∥ / ∥b∥

@[simp]

theorem normed_field.norm_inv {α : Type u_1} [normed_field α] (a : α) :

∥a⁻¹ ∥ = ∥a∥⁻¹

@[simp]

theorem normed_field.nnnorm_inv {α : Type u_1} [normed_field α] (a : α) :

nnnorm a⁻¹ = (nnnorm a)⁻¹

@[simp]

theorem normed_field.norm_fpow {α : Type u_1} [normed_field α] (a : α) (n : ℤ) :

∥a ^ n∥ = ∥a∥ ^ n

theorem normed_field.tendsto_inv {α : Type u_1} [normed_field α] {r : α} (r0 : r ≠ 0) :

(λ (q : α), q⁻¹)→_{r}r⁻¹

theorem normed_field.continuous_on_inv {α : Type u_1} [normed_field α] :

continuous_on (λ (x : α), x⁻¹) {x : α | x ≠ 0}

theorem normed_field.exists_one_lt_norm (α : Type u_1) [nondiscrete_normed_field α] :

∃ (x : α), 1 < ∥x∥

theorem normed_field.exists_norm_lt_one (α : Type u_1) [nondiscrete_normed_field α] :

∃ (x : α), 0 < ∥x∥ ∧ ∥x∥ < 1

theorem normed_field.exists_lt_norm (α : Type u_1) [nondiscrete_normed_field α] (r : ℝ) :

∃ (x : α), r < ∥x∥

theorem normed_field.exists_norm_lt (α : Type u_1) [nondiscrete_normed_field α] {r : ℝ} (hr : 0 < r) :

∃ (x : α), 0 < ∥x∥ ∧ ∥x∥ < r

@[instance]

theorem normed_field.punctured_nhds_ne_bot {α : Type u_1} [nondiscrete_normed_field α] (x : α) :

(𝓝[{x}ᶜ ] x).ne_bot

@[instance]

theorem normed_field.nhds_within_is_unit_ne_bot {α : Type u_1} [nondiscrete_normed_field α] :

(𝓝[{x : α | is_unit x}] 0).ne_bot

@[instance]

def real.normed_field :

normed_field ℝ

Equations

real.normed_field = {to_has_norm := {norm := λ (x : ℝ), abs x}, to_field := real.field, to_metric_space := real.metric_space, dist_eq := real.normed_field._proof_1, norm_mul' := _}

nondiscrete_normed_field ℝ

@[instance]

def real.nondiscrete_normed_field :

Equations

real.nondiscrete_normed_field = {to_normed_field := real.normed_field, non_trivial := real.nondiscrete_normed_field._proof_1}

theorem filter.tendsto.inv' {α : Type u_1} {β : Type u_2} [normed_field α] {l : filter β} {f : β → α} {y : α} (hy : y ≠ 0) (h : filter.tendsto f l (𝓝 y)) :

filter.tendsto (λ (x : β), (f x)⁻¹) l (𝓝 y⁻¹)

If a function converges to a nonzero value, its inverse converges to the inverse of this value. We use the name tendsto.inv' as tendsto.inv is already used in multiplicative topological groups.

theorem filter.tendsto.div {α : Type u_1} {β : Type u_2} [normed_field α] {l : filter β} {f g : β → α} {x y : α} (hf : filter.tendsto f l (𝓝 x)) (hg : filter.tendsto g l (𝓝 y)) (hy : y ≠ 0) :

filter.tendsto (λ (a : β), f a / g a) l (𝓝 (x / y))

theorem filter.tendsto.div_const {α : Type u_1} {β : Type u_2} [normed_field α] {l : filter β} {f : β → α} {x y : α} (hf : filter.tendsto f l (𝓝 x)) :

filter.tendsto (λ (a : β), f a / y) l (𝓝 (x / y))

theorem continuous_at.div {α : Type u_1} {β : Type u_2} [topological_space α] [normed_field β] {f g : α → β} {x : α} (hf : continuous_at f x) (hg : continuous_at g x) (hnz : g x ≠ 0) :

continuous_at (λ (x : α), f x / g x) x

Continuity at a point of the result of dividing two functions continuous at that point, where the denominator is nonzero.

theorem real.norm_eq_abs (r : ℝ) :

∥r∥ = abs r

theorem real.norm_of_nonneg {x : ℝ} (hx : 0 ≤ x) :

∥x∥ = x

@[simp]

theorem real.norm_coe_nat (n : ℕ) :

∥↑n∥ = ↑n

@[simp]

theorem real.nnnorm_coe_nat (n : ℕ) :

nnnorm ↑n = ↑n

@[simp]

theorem real.norm_two :

∥2∥ = 2

@[simp]

theorem real.nnnorm_two :

nnnorm 2 = 2

@[simp]

theorem real.nnreal.norm_eq (x : ℝ≥0) :

∥↑x∥ = ↑x

theorem real.nnnorm_coe_eq_self {x : ℝ≥0} :

nnnorm ↑x = x

theorem real.nnnorm_of_nonneg {x : ℝ} (hx : 0 ≤ x) :

nnnorm x = ⟨x, hx⟩

theorem real.ennnorm_eq_of_real {x : ℝ} (hx : 0 ≤ x) :

↑(nnnorm x) = ennreal.of_real x

@[simp]

theorem norm_norm {α : Type u_1} [normed_group α] (x : α) :

∥∥x∥∥ = ∥x∥

@[simp]

theorem nnnorm_norm {α : Type u_1} [normed_group α] (a : α) :

nnnorm ∥a∥ = nnnorm a

@[instance]

def int.normed_ring :

normed_ring ℤ

Equations

int.normed_ring = {to_has_norm := {norm := λ (n : ℤ), ∥↑n∥}, to_ring := int.ring, to_metric_space := int.metric_space, dist_eq := int.normed_ring._proof_1, norm_mul := int.normed_ring._proof_2}

theorem int.norm_cast_real (m : ℤ) :

∥↑m∥ = ∥m∥

@[instance]

def rat.normed_field :

normed_field ℚ

Equations

rat.normed_field = {to_has_norm := {norm := λ (r : ℚ), ∥↑r∥}, to_field := rat.field, to_metric_space := rat.metric_space, dist_eq := rat.normed_field._proof_1, norm_mul' := rat.normed_field._proof_2}

nondiscrete_normed_field ℚ

@[instance]

def rat.nondiscrete_normed_field :

Equations

rat.nondiscrete_normed_field = {to_normed_field := rat.normed_field, non_trivial := rat.nondiscrete_normed_field._proof_1}

@[simp]

theorem rat.norm_cast_real (r : ℚ) :

∥↑r∥ = ∥r∥

@[simp]

theorem int.norm_cast_rat (m : ℤ) :

∥↑m∥ = ∥m∥

@[class]

structure normed_space (α : Type u_5) (β : Type u_6) [normed_field α] [normed_group β] :

Type (max u_5 u_6)

to_semimodule : semimodule α β
norm_smul_le : ∀ (a : α) (b : β), ∥a • b∥ ≤ ∥a∥ * ∥b∥

A normed space over a normed field is a vector space endowed with a norm which satisfies the equality ∥c • x∥ = ∥c∥ ∥x∥. We require only ∥c • x∥ ≤ ∥c∥ ∥x∥ in the definition, then prove ∥c • x∥ = ∥c∥ ∥x∥ in norm_smul.

Instances

@[instance]

def normed_field.to_normed_space {α : Type u_1} [normed_field α] :

normed_space α α

Equations

normed_field.to_normed_space = {to_semimodule := semiring.to_semimodule ring.to_semiring, norm_smul_le := _}

theorem norm_smul {α : Type u_1} {β : Type u_2} [normed_field α] [normed_group β] [normed_space α β] (s : α) (x : β) :

∥s • x∥ = ∥s∥ * ∥x∥

theorem dist_smul {α : Type u_1} {β : Type u_2} [normed_field α] [normed_group β] [normed_space α β] (s : α) (x y : β) :

dist (s • x) (s • y) = ∥s∥ * dist x y

theorem nnnorm_smul {α : Type u_1} {β : Type u_2} [normed_field α] [normed_group β] [normed_space α β] (s : α) (x : β) :

nnnorm (s • x) = (nnnorm s) * nnnorm x

theorem nndist_smul {α : Type u_1} {β : Type u_2} [normed_field α] [normed_group β] [normed_space α β] (s : α) (x y : β) :

nndist (s • x) (s • y) = (nnnorm s) * nndist x y

theorem norm_smul_of_nonneg {β : Type u_2} [normed_group β] [normed_space ℝ β] {t : ℝ} (ht : 0 ≤ t) (x : β) :

∥t • x∥ = t * ∥x∥

@[instance]

def normed_space.topological_vector_space {α : Type u_1} [normed_field α] {E : Type u_5} [normed_group E] [normed_space α E] :

topological_vector_space α E

theorem closure_ball {E : Type u_5} [normed_group E] [normed_space ℝ E] (x : E) {r : ℝ} (hr : 0 < r) :

closure (metric.ball x r) = metric.closed_ball x r

theorem frontier_ball {E : Type u_5} [normed_group E] [normed_space ℝ E] (x : E) {r : ℝ} (hr : 0 < r) :

frontier (metric.ball x r) = metric.sphere x r

theorem interior_closed_ball {E : Type u_5} [normed_group E] [normed_space ℝ E] (x : E) {r : ℝ} (hr : 0 < r) :

interior (metric.closed_ball x r) = metric.ball x r

theorem interior_closed_ball' {E : Type u_5} [normed_group E] [normed_space ℝ E] [nontrivial E] (x : E) (r : ℝ) :

interior (metric.closed_ball x r) = metric.ball x r

theorem frontier_closed_ball {E : Type u_5} [normed_group E] [normed_space ℝ E] (x : E) {r : ℝ} (hr : 0 < r) :

frontier (metric.closed_ball x r) = metric.sphere x r

theorem frontier_closed_ball' {E : Type u_5} [normed_group E] [normed_space ℝ E] [nontrivial E] (x : E) (r : ℝ) :

frontier (metric.closed_ball x r) = metric.sphere x r

theorem rescale_to_shell {α : Type u_1} [normed_field α] {E : Type u_5} [normed_group E] [normed_space α E] {c : α} (hc : 1 < ∥c∥) {ε : ℝ} (εpos : 0 < ε) {x : E} (hx : x ≠ 0) :

∃ (d : α), d ≠ 0 ∧ ∥d • x∥ ≤ ε ∧ ε / ∥c∥ ≤ ∥d • x∥ ∧ ∥d∥⁻¹ ≤ (ε⁻¹ * ∥c∥) * ∥x∥

If there is a scalar c with ∥c∥>1, then any element can be moved by scalar multiplication to any shell of width ∥c∥. Also recap information on the norm of the rescaling element that shows up in applications.

@[instance]

def prod.normed_space {α : Type u_1} [normed_field α] {E : Type u_5} {F : Type u_6} [normed_group E] [normed_space α E] [normed_group F] [normed_space α F] :

normed_space α (E × F)

The product of two normed spaces is a normed space, with the sup norm.

Equations

prod.normed_space = {to_semimodule := {to_distrib_mul_action := {to_mul_action := distrib_mul_action.to_mul_action semimodule.to_distrib_mul_action, smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}, norm_smul_le := _}

@[instance]

def pi.normed_space {α : Type u_1} {ι : Type u_4} [normed_field α] {E : ι → Type u_2} [fintype ι] [Π (i : ι), normed_group (E i)] [Π (i : ι), normed_space α (E i)] :

normed_space α (Π (i : ι), E i)

The product of finitely many normed spaces is a normed space, with the sup norm.

Equations

pi.normed_space = {to_semimodule := pi.semimodule ι (λ (i : ι), E i) α (λ (i : ι), normed_space.to_semimodule), norm_smul_le := _}

@[instance]

def submodule.normed_space {𝕜 : Type u_1} [normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] (s : submodule 𝕜 E) :

normed_space 𝕜 ↥s

A subspace of a normed space is also a normed space, with the restriction of the norm.

Equations

s.normed_space = {to_semimodule := s.semimodule, norm_smul_le := _}

@[class]

structure normed_algebra (𝕜 : Type u_5) (𝕜' : Type u_6) [normed_field 𝕜] [normed_ring 𝕜'] :

Type (max u_5 u_6)

to_algebra : algebra 𝕜 𝕜'
norm_algebra_map_eq : ∀ (x : 𝕜), ∥⇑(algebra_map 𝕜 𝕜') x∥ = ∥x∥

A normed algebra 𝕜' over 𝕜 is an algebra endowed with a norm for which the embedding of 𝕜 in 𝕜' is an isometry.

Instances

@[simp]

theorem norm_algebra_map_eq {𝕜 : Type u_1} (𝕜' : Type u_2) [normed_field 𝕜] [normed_ring 𝕜'] [h : normed_algebra 𝕜 𝕜'] (x : 𝕜) :

∥⇑(algebra_map 𝕜 𝕜') x∥ = ∥x∥

@[instance]

def normed_algebra.to_normed_space (𝕜 : Type u_5) [normed_field 𝕜] (𝕜' : Type u_6) [normed_ring 𝕜'] [h : normed_algebra 𝕜 𝕜'] :

normed_space 𝕜 𝕜'

Equations

normed_algebra.to_normed_space 𝕜 𝕜' = {to_semimodule := algebra.to_semimodule normed_algebra.to_algebra, norm_smul_le := _}

@[instance]

def normed_algebra.id (𝕜 : Type u_5) [normed_field 𝕜] :

normed_algebra 𝕜 𝕜

Equations

normed_algebra.id 𝕜 = {to_algebra := {to_has_scalar := algebra.to_has_scalar (algebra.id 𝕜), to_ring_hom := algebra.to_ring_hom (algebra.id 𝕜), commutes' := _, smul_def' := _}, norm_algebra_map_eq := _}

@[simp]

theorem normed_algebra.norm_one (𝕜 : Type u_5) [normed_field 𝕜] {𝕜' : Type u_6} [normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] :

∥1∥ = 1

theorem normed_algebra.zero_ne_one (𝕜 : Type u_5) [normed_field 𝕜] {𝕜' : Type u_6} [normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] :

0 ≠ 1

theorem normed_algebra.to_nonzero (𝕜 : Type u_5) [normed_field 𝕜] {𝕜' : Type u_6} [normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] :

nontrivial 𝕜'

def normed_space.restrict_scalars' (𝕜 : Type u_5) (𝕜' : Type u_6) [normed_field 𝕜] [normed_field 𝕜'] [normed_algebra 𝕜 𝕜'] (E : Type u_7) [normed_group E] [normed_space 𝕜' E] :

normed_space 𝕜 E

𝕜-normed space structure induced by a 𝕜'-normed space structure when 𝕜' is a normed algebra over 𝕜. Not registered as an instance as 𝕜' can not be inferred.

The type synonym semimodule.restrict_scalars 𝕜 𝕜' E will be endowed with this instance by default.

Equations

normed_space.restrict_scalars' 𝕜 𝕜' E = {to_semimodule := {to_distrib_mul_action := semimodule.to_distrib_mul_action (semimodule.restrict_scalars' 𝕜 𝕜' E), add_smul := _, zero_smul := _}, norm_smul_le := _}

@[instance]

def semimodule.restrict_scalars.normed_group {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [I : normed_group E] :

normed_group (semimodule.restrict_scalars 𝕜 𝕜' E)

Equations

semimodule.restrict_scalars.normed_group = I

@[instance]

def semimodule.restrict_scalars.normed_space_orig {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [normed_field 𝕜'] [normed_group E] [I : normed_space 𝕜' E] :

normed_space 𝕜' (semimodule.restrict_scalars 𝕜 𝕜' E)

Equations

semimodule.restrict_scalars.normed_space_orig = I

@[instance]

def semimodule.restrict_scalars.normed_space (𝕜 : Type u_5) (𝕜' : Type u_6) [normed_field 𝕜] [normed_field 𝕜'] [normed_algebra 𝕜 𝕜'] (E : Type u_7) [normed_group E] [normed_space 𝕜' E] :

normed_space 𝕜 (semimodule.restrict_scalars 𝕜 𝕜' E)

Equations

semimodule.restrict_scalars.normed_space 𝕜 𝕜' E = normed_space.restrict_scalars' 𝕜 𝕜' E

theorem has_sum_of_bounded_monoid_hom_of_has_sum {α : Type u_1} {β : Type u_2} {ι : Type u_4} [normed_group α] [normed_group β] {f : ι → α} {φ : α →+ β} {x : α} (hf : has_sum f x) (C : ℝ) (hφ : ∀ (x : α), ∥⇑φ x∥ ≤ C * ∥x∥) :

has_sum (λ (b : ι), ⇑φ (f b)) (⇑φ x)

theorem has_sum_of_bounded_monoid_hom_of_summable {α : Type u_1} {β : Type u_2} {ι : Type u_4} [normed_group α] [normed_group β] {f : ι → α} {φ : α →+ β} (hf : summable f) (C : ℝ) (hφ : ∀ (x : α), ∥⇑φ x∥ ≤ C * ∥x∥) :

has_sum (λ (b : ι), ⇑φ (f b)) (⇑φ (∑' (b : ι), f b))

theorem cauchy_seq_finset_iff_vanishing_norm {α : Type u_1} {ι : Type u_4} [normed_group α] {f : ι → α} :

cauchy_seq (λ (s : finset ι), ∑ (i : ι) in s, f i) ↔ ∀ (ε : ℝ), ε > 0 → (∃ (s : finset ι), ∀ (t : finset ι), disjoint t s → ∥∑ (i : ι) in t, f i∥ < ε)

theorem summable_iff_vanishing_norm {α : Type u_1} {ι : Type u_4} [normed_group α] [complete_space α] {f : ι → α} :

summable f ↔ ∀ (ε : ℝ), ε > 0 → (∃ (s : finset ι), ∀ (t : finset ι), disjoint t s → ∥∑ (i : ι) in t, f i∥ < ε)

theorem cauchy_seq_finset_of_norm_bounded {α : Type u_1} {ι : Type u_4} [normed_group α] {f : ι → α} (g : ι → ℝ) (hg : summable g) (h : ∀ (i : ι), ∥f i∥ ≤ g i) :

cauchy_seq (λ (s : finset ι), ∑ (i : ι) in s, f i)

theorem cauchy_seq_finset_of_summable_norm {α : Type u_1} {ι : Type u_4} [normed_group α] {f : ι → α} (hf : summable (λ (a : ι), ∥f a∥)) :

cauchy_seq (λ (s : finset ι), ∑ (a : ι) in s, f a)

theorem has_sum_of_subseq_of_summable {α : Type u_1} {γ : Type u_3} {ι : Type u_4} [normed_group α] {f : ι → α} (hf : summable (λ (a : ι), ∥f a∥)) {s : γ → finset ι} {p : filter γ} [p.ne_bot] (hs : filter.tendsto s p filter.at_top) {a : α} (ha : filter.tendsto (λ (b : γ), ∑ (i : ι) in s b, f i) p (𝓝 a)) :

has_sum f a

If a function f is summable in norm, and along some sequence of finsets exhausting the space its sum is converging to a limit a, then this holds along all finsets, i.e., f is summable with sum a.

theorem norm_tsum_le_tsum_norm {α : Type u_1} {ι : Type u_4} [normed_group α] {f : ι → α} (hf : summable (λ (i : ι), ∥f i∥)) :

∥(∑' (i : ι), f i)∥ ≤ ∑' (i : ι), ∥f i∥

If ∑' i, ∥f i∥ is summable, then ∥(∑' i, f i)∥ ≤ (∑' i, ∥f i∥). Note that we do not assume that ∑' i, f i is summable, and it might not be the case if α is not a complete space.

theorem has_sum_iff_tendsto_nat_of_summable_norm {α : Type u_1} [normed_group α] {f : ℕ → α} {a : α} (hf : summable (λ (i : ℕ), ∥f i∥)) :

has_sum f a ↔ filter.tendsto (λ (n : ℕ), ∑ (i : ℕ) in finset.range n, f i) filter.at_top (𝓝 a)

theorem summable_of_norm_bounded {α : Type u_1} {ι : Type u_4} [normed_group α] [complete_space α] {f : ι → α} (g : ι → ℝ) (hg : summable g) (h : ∀ (i : ι), ∥f i∥ ≤ g i) :

The direct comparison test for series: if the norm of f is bounded by a real function g which is summable, then f is summable.

theorem tsum_of_norm_bounded {α : Type u_1} {ι : Type u_4} [normed_group α] {f : ι → α} {g : ι → ℝ} {a : ℝ} (hg : has_sum g a) (h : ∀ (i : ι), ∥f i∥ ≤ g i) :

∥(∑' (i : ι), f i)∥ ≤ a

Quantitative result associated to the direct comparison test for series: If ∑' i, g i is summable, and for all i, ∥f i∥ ≤ g i, then ∥(∑' i, f i)∥ ≤ (∑' i, g i). Note that we do not assume that ∑' i, f i is summable, and it might not be the case if α is not a complete space.

theorem summable_of_norm_bounded_eventually {α : Type u_1} {ι : Type u_4} [normed_group α] [complete_space α] {f : ι → α} (g : ι → ℝ) (hg : summable g) (h : ∀ᶠ (i : ι) in filter.cofinite, ∥f i∥ ≤ g i) :

Variant of the direct comparison test for series: if the norm of f is eventually bounded by a real function g which is summable, then f is summable.

theorem summable_of_nnnorm_bounded {α : Type u_1} {ι : Type u_4} [normed_group α] [complete_space α] {f : ι → α} (g : ι → ℝ≥0) (hg : summable g) (h : ∀ (i : ι), nnnorm (f i) ≤ g i) :

theorem summable_of_summable_norm {α : Type u_1} {ι : Type u_4} [normed_group α] [complete_space α] {f : ι → α} (hf : summable (λ (a : ι), ∥f a∥)) :

theorem summable_of_summable_nnnorm {α : Type u_1} {ι : Type u_4} [normed_group α] [complete_space α] {f : ι → α} (hf : summable (λ (a : ι), nnnorm (f a))) :