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∥

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

dist g h = ∥h - g∥

@[simp]

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

dist g 0 = ∥g∥

theorem tendsto_norm_cocompact_at_top {α : Type u_1} [normed_group α] [proper_space α] :

filter.tendsto norm (filter.cocompact α) filter.at_top

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_of_subsingleton {α : Type u_1} [normed_group α] [subsingleton α] (x : α) :

∥x∥ = 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

@[simp]

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

0 < ∥g∥ ↔ g ≠ 0

@[simp]

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

∥g∥ ≤ 0 ↔ g = 0

theorem eq_of_norm_sub_le_zero {α : Type u_1} [normed_group α] {g h : α} (a : ∥g - h∥ ≤ 0) :

g = h

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_sub_eq_zero_iff {α : Type u_1} [normed_group α] {u v : α} :

∥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 mem_ball_iff_norm {α : Type u_1} [normed_group α] {g h : α} {r : ℝ} :

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

theorem mem_ball_iff_norm' {α : Type u_1} [normed_group α] {g h : α} {r : ℝ} :

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

theorem mem_closed_ball_iff_norm {α : Type u_1} [normed_group α] {g h : α} {r : ℝ} :

h ∈ metric.closed_ball g r ↔ ∥h - g∥ ≤ r

theorem mem_closed_ball_iff_norm' {α : Type u_1} [normed_group α] {g h : α} {r : ℝ} :

h ∈ metric.closed_ball g r ↔ ∥g - h∥ ≤ r

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

@[simp]

theorem mem_sphere_iff_norm {α : Type u_1} [normed_group α] (v w : α) (r : ℝ) :

w ∈ metric.sphere v r ↔ ∥w - v∥ = r

@[simp]

theorem mem_sphere_zero_iff_norm {α : Type u_1} [normed_group α] {w : α} {r : ℝ} :

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

@[simp]

theorem norm_eq_of_mem_sphere {α : Type u_1} [normed_group α] {r : ℝ} (x : ↥(metric.sphere 0 r)) :

∥↑x∥ = r

theorem nonzero_of_mem_sphere {α : Type u_1} [normed_group α] {r : ℝ} (hr : 0 < r) (x : ↥(metric.sphere 0 r)) :

↑x ≠ 0

theorem nonzero_of_mem_unit_sphere {α : Type u_1} [normed_group α] (x : ↥(metric.sphere 0 1)) :

↑x ≠ 0

@[instance]

def metric.sphere.has_neg {α : Type u_1} [normed_group α] {r : ℝ} :

has_neg ↥(metric.sphere 0 r)

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

Equations

metric.sphere.has_neg = {neg := λ (w : ↥(metric.sphere 0 r)), ⟨-↑w, _⟩}

@[simp]

theorem coe_neg_sphere {α : Type u_1} [normed_group α] {r : ℝ} (v : ↥(metric.sphere 0 r)) :

↑-v = -↑v

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 : β} :

filter.tendsto 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 mem_emetric_ball_0_iff {β : Type u_2} [normed_group β] {x : β} {r : ennreal} :

x ∈ emetric.ball 0 r ↔ ↑(nnnorm x) < r

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 tendsto_norm_sub_self {α : Type u_1} [normed_group α] (x : α) :

filter.tendsto (λ (g : α), ∥g - x∥) (𝓝 x) (𝓝 0)

theorem tendsto_norm {α : Type u_1} [normed_group α] {x : α} :

filter.tendsto (λ (g : α), ∥g∥) (𝓝 x) (𝓝 ∥x∥)

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

filter.tendsto (λ (g : α), ∥g∥) (𝓝 0) (𝓝 0)

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

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

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

continuous nnnorm

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

filter.tendsto norm (𝓝[{0}ᶜ ] 0) (𝓝[set.Ioi 0] 0)

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

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

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

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

theorem continuous.norm {α : Type u_1} {γ : Type u_3} [normed_group α] [topological_space γ] {f : γ → α} (h : continuous f) :

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

theorem continuous.nnnorm {α : Type u_1} {γ : Type u_3} [normed_group α] [topological_space γ] {f : γ → α} (h : continuous f) :

continuous (λ (x : γ), nnnorm (f x))

theorem continuous_at.norm {α : Type u_1} {γ : Type u_3} [normed_group α] [topological_space γ] {f : γ → α} {a : γ} (h : continuous_at f a) :

continuous_at (λ (x : γ), ∥f x∥) a

theorem continuous_at.nnnorm {α : Type u_1} {γ : Type u_3} [normed_group α] [topological_space γ] {f : γ → α} {a : γ} (h : continuous_at f a) :

continuous_at (λ (x : γ), nnnorm (f x)) a

theorem continuous_within_at.norm {α : Type u_1} {γ : Type u_3} [normed_group α] [topological_space γ] {f : γ → α} {s : set γ} {a : γ} (h : continuous_within_at f s a) :

continuous_within_at (λ (x : γ), ∥f x∥) s a

theorem continuous_within_at.nnnorm {α : Type u_1} {γ : Type u_3} [normed_group α] [topological_space γ] {f : γ → α} {s : set γ} {a : γ} (h : continuous_within_at f s a) :

continuous_within_at (λ (x : γ), nnnorm (f x)) s a

theorem continuous_on.norm {α : Type u_1} {γ : Type u_3} [normed_group α] [topological_space γ] {f : γ → α} {s : set γ} (h : continuous_on f s) :

continuous_on (λ (x : γ), ∥f x∥) s

theorem continuous_on.nnnorm {α : Type u_1} {γ : Type u_3} [normed_group α] [topological_space γ] {f : γ → α} {s : set γ} (h : continuous_on f s) :

continuous_on (λ (x : γ), nnnorm (f x)) s

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

@[class]

structure norm_one_class (α : Type u_5) [has_norm α] [has_one α] :

Prop

norm_one : ∥1∥ = 1

A mixin class with the axiom ∥1∥ = 1. Many normed_rings and all normed_fields satisfy this axiom.

Instances

@[simp]

theorem nnnorm_one {α : Type u_1} [normed_group α] [has_one α] [norm_one_class α] :

nnnorm 1 = 1

@[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, sub := ring.sub normed_ring.to_ring, sub_eq_add_neg := _, 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, sub := ring.sub normed_ring.to_ring, sub_eq_add_neg := _, add_left_neg := _, add_comm := _}, to_metric_space := normed_ring.to_metric_space β, dist_eq := _}

@[instance]

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

norm_one_class (α × β)

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

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

theorem list.norm_prod_le' {α : Type u_1} [normed_ring α] {l : list α} :

l ≠ list.nil → ∥l.prod ∥ ≤ (list.map norm l).prod

theorem list.norm_prod_le {α : Type u_1} [normed_ring α] [norm_one_class α] (l : list α) :

∥l.prod ∥ ≤ (list.map norm l).prod

theorem finset.norm_prod_le' {ι : Type u_4} {α : Type u_1} [normed_comm_ring α] (s : finset ι) (hs : s.nonempty) (f : ι → α) :

∥∏ (i : ι) in s, f i∥ ≤ ∏ (i : ι) in s, ∥f i∥

theorem finset.norm_prod_le {ι : Type u_4} {α : Type u_1} [normed_comm_ring α] [norm_one_class α] (s : finset ι) (f : ι → α) :

∥∏ (i : ι) in s, f i∥ ≤ ∏ (i : ι) in s, ∥f i∥

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

0 < n → ∥a ^ n∥ ≤ ∥a∥ ^ n

If α is a normed ring, then ∥a^n∥≤ ∥a∥^n for n > 0. See also norm_pow_le.

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

∥a ^ n∥ ≤ ∥a∥ ^ n

If α is a normed ring with ∥1∥=1, then ∥a^n∥≤ ∥a∥^n. See also norm_pow_le'.

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, sub := field.sub normed_field.to_field, sub_eq_add_neg := _, 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 := _}

@[instance]

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

norm_one_class α

@[simp]

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

nnnorm (a * b) = (nnnorm a) * nnnorm b

@[simp]

theorem normed_field.norm_hom_apply {α : Type u_1} [normed_field α] (ᾰ : α) :

⇑normed_field.norm_hom ᾰ = ∥ᾰ∥

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

monoid_with_zero_hom α ℝ

norm as a monoid_hom.

Equations

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

@[simp]

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

⇑normed_field.nnnorm_hom a = nnnorm a

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

monoid_with_zero_hom α ℝ≥0

nnnorm as a monoid_hom.

Equations

normed_field.nnnorm_hom = {to_fun := nnnorm normed_ring.to_normed_group, map_zero' := _, map_one' := _, map_mul' := _}

@[simp]

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

∥a ^ n∥ = ∥a∥ ^ n

@[simp]

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

nnnorm (a ^ n) = nnnorm 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.nnnorm_prod {α : Type u_1} {β : Type u_2} [normed_field α] (s : finset β) (f : β → α) :

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

@[simp]

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

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

@[simp]

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

nnnorm (a / b) = nnnorm a / nnnorm 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

@[simp]

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

nnnorm (a ^ n) = nnnorm a ^ n

@[instance]

def normed_field.has_continuous_inv' {α : Type u_1} [normed_field α] :

has_continuous_inv' α

Equations

normed_field.has_continuous_inv' = {continuous_at_inv' := _}

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 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_comm_ring :

normed_comm_ring ℤ

Equations

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

theorem int.norm_cast_real (m : ℤ) :

∥↑m∥ = ∥m∥

@[instance]

def int.norm_one_class :

norm_one_class ℤ

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

@[simp]

theorem abs_norm_eq_norm {β : Type u_2} [normed_group β] (z : β) :

abs ∥z∥ = ∥z∥

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 ne_neg_of_mem_sphere (α : Type u_1) [normed_field α] {E : Type u_5} [normed_group E] [normed_space α E] [char_zero α] {r : ℝ} (hr : 0 < r) (x : ↥(metric.sphere 0 r)) :

x ≠ -x

theorem ne_neg_of_mem_unit_sphere (α : Type u_1) [normed_field α] {E : Type u_5} [normed_group E] [normed_space α E] [char_zero α] (x : ↥(metric.sphere 0 1)) :

x ≠ -x

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 := submodule.restricted_module 𝕜 𝕜 E s, 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.norm_one_class (𝕜 : Type u_5) [normed_field 𝕜] {𝕜' : Type u_6} [normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] :

norm_one_class 𝕜'

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

0 ≠ 1

theorem normed_algebra.nontrivial (𝕜 : 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

Warning: This declaration should be used judiciously. Please consider using is_scalar_tower instead.

𝕜-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 (restrict_scalars.semimodule 𝕜 𝕜' E), add_smul := _, zero_smul := _}, norm_smul_le := _}

@[instance]

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

normed_group (restrict_scalars 𝕜 𝕜' E)

Equations

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 𝕜' (restrict_scalars 𝕜 𝕜' E)

Equations

semimodule.restrict_scalars.normed_space_orig = I

@[instance]

def 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 𝕜 (restrict_scalars 𝕜 𝕜' E)

Equations

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

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