mathlib documentation

analysis.normed_space.basic

Normed spaces #

In this file we define (semi)normed rings, fields, spaces, and algebras. We also prove some theorems about these definitions.

@[class]
structure semi_normed_ring (α : Type u_5) :
Type u_5

A seminormed ring is a ring endowed with a seminorm which satisfies the inequality ∥x y∥ ≤ ∥x∥ ∥y∥.

Instances
@[class]
structure normed_ring (α : Type u_5) :
Type u_5

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

Instances
@[class]
structure semi_normed_comm_ring (α : Type u_5) :
Type u_5

A seminormed commutative ring is a commutative ring endowed with a seminorm 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
@[instance]
Equations
@[class]
structure norm_one_class (α : Type u_5) [has_norm α] [has_one α] :
Prop

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} [semi_normed_group α] [has_one α] [norm_one_class α] :
@[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 β] :
theorem norm_mul_le {α : Type u_1} [semi_normed_ring α] (a b : α) :
@[instance]
def subalgebra.semi_normed_ring {𝕜 : Type u_1} {_x : comm_ring 𝕜} {E : Type u_2} [semi_normed_ring E] {_x_1 : algebra 𝕜 E} (s : subalgebra 𝕜 E) :

A subalgebra of a seminormed ring is also a seminormed ring, with the restriction of the norm.

See note [implicit instance arguments].

Equations
@[instance]
def subalgebra.normed_ring {𝕜 : Type u_1} {_x : comm_ring 𝕜} {E : Type u_2} [normed_ring E] {_x_1 : algebra 𝕜 E} (s : subalgebra 𝕜 E) :

A subalgebra of a normed ring is also a normed ring, with the restriction of the norm.

See note [implicit instance arguments].

Equations
theorem list.norm_prod_le' {α : Type u_1} [semi_normed_ring α] {l : list α} :
theorem list.norm_prod_le {α : Type u_1} [semi_normed_ring α] [norm_one_class α] (l : list α) :
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} [semi_normed_ring α] (a : α) {n : } :
0 < na ^ n a ^ n

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

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

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

theorem eventually_norm_pow_le {α : Type u_1} [semi_normed_ring α] (a : α) :
∀ᶠ (n : ) in filter.at_top, a ^ n a ^ n
theorem mul_left_bound {α : Type u_1} [semi_normed_ring α] (x y : α) :

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

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

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

@[instance]
def prod.semi_normed_ring {α : Type u_1} {β : Type u_2} [semi_normed_ring α] [semi_normed_ring β] :

Seminormed ring structure on the product of two seminormed rings, using the sup norm.

Equations
def matrix.semi_normed_group {α : Type u_1} [semi_normed_ring α] {n : Type u_2} {m : Type u_3} [fintype n] [fintype m] :

Seminormed group instance (using sup norm of sup norm) for matrices over a seminormed ring. Not declared as an instance because there are several natural choices for defining the norm of a matrix.

Equations
theorem semi_norm_matrix_le_iff {α : Type u_1} [semi_normed_ring α] {n : Type u_2} {m : Type u_3} [fintype n] [fintype m] {r : } (hr : 0 r) {A : matrix n m α} :
A r ∀ (i : n) (j : m), A i j r
theorem units.norm_pos {α : Type u_1} [normed_ring α] [nontrivial α] (x : units α) :
@[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
def matrix.normed_group {α : Type u_1} [normed_ring α] {n : Type u_2} {m : Type u_3} [fintype n] [fintype m] :

Normed group instance (using sup norm of sup norm) for matrices over a normed ring. Not declared as an instance because there are several natural choices for defining the norm of a matrix.

Equations
@[instance]
@[instance]
def semi_normed_top_ring {α : Type u_1} [semi_normed_ring α] :

A seminormed ring is a topological ring.

@[class]
structure normed_field (α : Type u_5) :
Type u_5

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

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 : α) :
@[instance]
@[simp]
theorem normed_field.nnnorm_mul {α : Type u_1} [normed_field α] (a b : α) :
@[simp]
theorem normed_field.norm_hom_apply {α : Type u_1} [normed_field α] (ᾰ : α) :
@[simp]
theorem normed_field.nnnorm_hom_apply {α : Type u_1} [normed_field α] (ᾰ : α) :
@[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 : ) :
@[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 : β → α) :
∏ (b : β) in s, f b∥₊ = ∏ (b : β) in s, f b∥₊
@[simp]
theorem normed_field.norm_div {α : Type u_1} [normed_field α] (a b : α) :
@[simp]
theorem normed_field.nnnorm_div {α : Type u_1} [normed_field α] (a b : α) :
@[simp]
theorem normed_field.norm_inv {α : Type u_1} [normed_field α] (a : α) :
@[simp]
theorem normed_field.nnnorm_inv {α : Type u_1} [normed_field α] (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 : ) :
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 : α) :
@[instance]
theorem real.norm_of_nonneg {x : } (hx : 0 x) :
theorem real.norm_of_nonpos {x : } (hx : x 0) :
@[simp]
theorem real.norm_coe_nat (n : ) :
@[simp]
@[simp]
theorem real.norm_two  :
@[simp]
theorem real.nnnorm_two  :
theorem real.nnnorm_of_nonneg {x : } (hx : 0 x) :
x∥₊ = x, hx⟩
@[instance]

If E is a nontrivial topological module over , then E has no isolated points. This is a particular case of module.punctured_nhds_ne_bot.

@[simp]
theorem nnreal.norm_eq (x : ℝ≥0) :
@[simp]
theorem nnreal.nnnorm_eq (x : ℝ≥0) :
@[simp]
theorem norm_norm {α : Type u_1} [semi_normed_group α] (x : α) :
@[simp]
theorem nnnorm_norm {α : Type u_1} [semi_normed_group α] (a : α) :
theorem normed_group.tendsto_at_top {α : Type u_1} [nonempty α] [semilattice_sup α] {β : Type u_2} [semi_normed_group β] {f : α → β} {b : β} :
filter.tendsto f filter.at_top (𝓝 b) ∀ (ε : ), 0 < ε(∃ (N : α), ∀ (n : α), N nf n - b < ε)

A restatement of metric_space.tendsto_at_top in terms of the norm.

theorem normed_group.tendsto_at_top' {α : Type u_1} [nonempty α] [semilattice_sup α] [no_top_order α] {β : Type u_2} [semi_normed_group β] {f : α → β} {b : β} :
filter.tendsto f filter.at_top (𝓝 b) ∀ (ε : ), 0 < ε(∃ (N : α), ∀ (n : α), N < nf n - b < ε)

A variant of normed_group.tendsto_at_top that uses ∃ N, ∀ n > N, ... rather than ∃ N, ∀ n ≥ N, ...

@[instance]
Equations
theorem int.norm_eq_abs (n : ) :
@[instance]
Equations
@[simp]
theorem rat.norm_cast_real (r : ) :
@[simp]
theorem int.norm_cast_rat (m : ) :
theorem norm_nsmul_le {α : Type u_1} [semi_normed_group α] (n : ) (a : α) :
theorem norm_gsmul_le {α : Type u_1} [semi_normed_group α] (n : ) (a : α) :
theorem nnnorm_nsmul_le {α : Type u_1} [semi_normed_group α] (n : ) (a : α) :
theorem nnnorm_gsmul_le {α : Type u_1} [semi_normed_group α] (n : ) (a : α) :
@[class]
structure semi_normed_space (α : Type u_5) (β : Type u_6) [normed_field α] [semi_normed_group β] :
Type (max u_5 u_6)

A seminormed space over a normed field is a vector space endowed with a seminorm 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_space.to_semi_normed_space {α : Type u_1} {β : Type u_2} [normed_field α] [normed_group β] [γ : normed_space α β] :

A normed space is a seminormed space.

Equations
@[instance]
def semi_normed_space.has_bounded_smul {α : Type u_1} {β : Type u_2} [normed_field α] [semi_normed_group β] [semi_normed_space α β] :
theorem norm_smul {α : Type u_1} {β : Type u_2} [normed_field α] [semi_normed_group β] [semi_normed_space α β] (s : α) (x : β) :
@[simp]
theorem abs_norm_eq_norm {β : Type u_2} [semi_normed_group β] (z : β) :
theorem dist_smul {α : Type u_1} {β : Type u_2} [normed_field α] [semi_normed_group β] [semi_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 α] [semi_normed_group β] [semi_normed_space α β] (s : α) (x : β) :
theorem nndist_smul {α : Type u_1} {β : Type u_2} [normed_field α] [semi_normed_group β] [semi_normed_space α β] (s : α) (x y : β) :
nndist (s x) (s y) = s∥₊ * nndist x y
theorem norm_smul_of_nonneg {β : Type u_2} [semi_normed_group β] [semi_normed_space β] {t : } (ht : 0 t) (x : β) :
theorem eventually_nhds_norm_smul_sub_lt {α : Type u_1} [normed_field α] {E : Type u_5} [semi_normed_group E] [semi_normed_space α E] (c : α) (x : E) {ε : } (h : 0 < ε) :
∀ᶠ (y : E) in 𝓝 x, c (y - x) < ε
theorem closure_ball {E : Type u_5} [semi_normed_group E] [semi_normed_space E] (x : E) {r : } (hr : 0 < r) :
theorem frontier_ball {E : Type u_5} [semi_normed_group E] [semi_normed_space E] (x : E) {r : } (hr : 0 < r) :
theorem interior_closed_ball {E : Type u_5} [semi_normed_group E] [semi_normed_space E] (x : E) {r : } (hr : 0 < r) :
theorem frontier_closed_ball {E : Type u_5} [semi_normed_group E] [semi_normed_space E] (x : E) {r : } (hr : 0 < r) :
theorem smul_ball {α : Type u_1} [normed_field α] {E : Type u_5} [semi_normed_group E] [semi_normed_space α E] {c : α} (hc : c 0) (x : E) (r : ) :
theorem smul_closed_ball' {α : Type u_1} [normed_field α] {E : Type u_5} [semi_normed_group E] [semi_normed_space α E] {c : α} (hc : c 0) (x : E) (r : ) :
theorem smul_closed_ball {α : Type u_1} [normed_field α] {E : Type u_2} [normed_group E] [normed_space α E] (c : α) (x : E) {r : } (hr : 0 r) :
theorem ne_neg_of_mem_sphere (α : Type u_1) [normed_field α] {E : Type u_5} [semi_normed_group E] [semi_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} [semi_normed_group E] [semi_normed_space α E] [char_zero α] (x : (metric.sphere 0 1)) :
x -x
@[instance]
def prod.semi_normed_space {α : Type u_1} [normed_field α] {E : Type u_5} [semi_normed_group E] [semi_normed_space α E] {F : Type u_6} [semi_normed_group F] [semi_normed_space α F] :

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

Equations
@[instance]
def pi.semi_normed_space {α : Type u_1} {ι : Type u_4} [normed_field α] {E : ι → Type u_2} [fintype ι] [Π (i : ι), semi_normed_group (E i)] [Π (i : ι), semi_normed_space α (E i)] :
semi_normed_space α (Π (i : ι), E i)

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

Equations
@[instance]
def submodule.semi_normed_space {𝕜 : Type u_1} {R : Type u_2} [has_scalar 𝕜 R] [normed_field 𝕜] [ring R] {E : Type u_3} [semi_normed_group E] [semi_normed_space 𝕜 E] [module R E] [is_scalar_tower 𝕜 R E] (s : submodule R E) :

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

Equations
theorem rescale_to_shell_semi_normed {α : Type u_1} [normed_field α] {E : Type u_5} [semi_normed_group E] [semi_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 with nonzero norm 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.

theorem interior_closed_ball' {E : Type u_5} [normed_group E] [normed_space E] [nontrivial E] (x : E) (r : ) :
theorem frontier_closed_ball' {E : Type u_5} [normed_group E] [normed_space E] [nontrivial E] (x : E) (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} [normed_group E] [normed_space α E] {F : Type u_6} [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
@[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
def matrix.normed_space {α : Type u_1} [normed_field α] {n : Type u_2} {m : Type u_3} [fintype n] [fintype m] :
normed_space α (matrix n m α)

Normed space instance (using sup norm of sup norm) for matrices over a normed field. Not declared as an instance because there are several natural choices for defining the norm of a matrix.

Equations
@[instance]
def submodule.normed_space {𝕜 : Type u_1} {R : Type u_2} [has_scalar 𝕜 R] [normed_field 𝕜] [ring R] {E : Type u_3} [normed_group E] [normed_space 𝕜 E] [module R E] [is_scalar_tower 𝕜 R E] (s : submodule R E) :

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

Equations
@[class]
structure semi_normed_algebra (𝕜 : Type u_5) (𝕜' : Type u_6) [normed_field 𝕜] [semi_normed_ring 𝕜'] :
Type (max u_5 u_6)

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

Instances
@[class]
structure normed_algebra (𝕜 : Type u_5) (𝕜' : Type u_6) [normed_field 𝕜] [normed_ring 𝕜'] :
Type (max u_5 u_6)

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

Instances
@[instance]
def normed_algebra.to_semi_normed_algebra (𝕜 : Type u_1) (𝕜' : Type u_2) [normed_field 𝕜] [normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] :

A normed algebra is a seminormed algebra.

Equations
@[simp]
theorem norm_algebra_map_eq {𝕜 : Type u_1} (𝕜' : Type u_2) [normed_field 𝕜] [semi_normed_ring 𝕜'] [h : semi_normed_algebra 𝕜 𝕜'] (x : 𝕜) :
(algebra_map 𝕜 𝕜') x = x
theorem algebra_map_isometry (𝕜 : Type u_1) (𝕜' : Type u_2) [normed_field 𝕜] [semi_normed_ring 𝕜'] [semi_normed_algebra 𝕜 𝕜'] :

In a normed algebra, the inclusion of the base field in the extended field is an isometry.

@[instance]
def semi_normed_algebra.to_semi_normed_space' (𝕜 : Type u_1) [normed_field 𝕜] (𝕜' : Type u_2) [normed_ring 𝕜'] [semi_normed_algebra 𝕜 𝕜'] :

While this may appear identical to semi_normed_algebra.to_semi_normed_space, it contains an implicit argument involving normed_ring.to_semi_normed_ring that typeclass inference has trouble inferring.

Specifically, the following instance cannot be found without this semi_normed_algebra.to_semi_normed_space':

example
  (𝕜 ι : Type*) (E : ι  Type*)
  [normed_field 𝕜] [Π i, normed_ring (E i)] [Π i, normed_algebra 𝕜 (E i)] :
  Π i, module 𝕜 (E i) := by apply_instance

See semi_normed_space.to_module' for a similar situation.

Equations
@[instance]
def normed_algebra.to_normed_space (𝕜 : Type u_1) [normed_field 𝕜] (𝕜' : Type u_2) [normed_ring 𝕜'] [h : normed_algebra 𝕜 𝕜'] :
normed_space 𝕜 𝕜'
Equations
theorem normed_algebra.norm_one (𝕜 : Type u_5) [normed_field 𝕜] (𝕜' : Type u_6) [semi_normed_ring 𝕜'] [semi_normed_algebra 𝕜 𝕜'] :
theorem normed_algebra.norm_one_class (𝕜 : Type u_5) [normed_field 𝕜] (𝕜' : Type u_6) [semi_normed_ring 𝕜'] [semi_normed_algebra 𝕜 𝕜'] :
theorem normed_algebra.zero_ne_one (𝕜 : Type u_5) [normed_field 𝕜] (𝕜' : Type u_6) [semi_normed_ring 𝕜'] [semi_normed_algebra 𝕜 𝕜'] :
0 1
theorem normed_algebra.nontrivial (𝕜 : Type u_5) [normed_field 𝕜] (𝕜' : Type u_6) [semi_normed_ring 𝕜'] [semi_normed_algebra 𝕜 𝕜'] :
def semi_normed_space.restrict_scalars (𝕜 : Type u_5) (𝕜' : Type u_6) [normed_field 𝕜] [normed_field 𝕜'] [normed_algebra 𝕜 𝕜'] (F : Type u_8) [semi_normed_group F] [semi_normed_space 𝕜' F] :

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

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

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

Equations
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] :

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 restrict_scalars 𝕜 𝕜' E will be endowed with this instance by default.

Equations
@[instance]
def restrict_scalars.semi_normed_group {𝕜 : Type u_1} {𝕜' : Type u_2} {F : Type u_3} [I : semi_normed_group F] :
Equations
@[instance]
def restrict_scalars.normed_group {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [I : normed_group E] :
Equations
@[instance]
def module.restrict_scalars.semi_normed_space_orig {𝕜 : Type u_1} {𝕜' : Type u_2} {F : Type u_3} [normed_field 𝕜'] [semi_normed_group F] [I : semi_normed_space 𝕜' F] :
semi_normed_space 𝕜' (restrict_scalars 𝕜 𝕜' F)
Equations
@[instance]
def module.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
@[instance]
def restrict_scalars.semi_normed_space (𝕜 : Type u_5) (𝕜' : Type u_6) [normed_field 𝕜] [normed_field 𝕜'] [normed_algebra 𝕜 𝕜'] (F : Type u_8) [semi_normed_group F] [semi_normed_space 𝕜' F] :
Equations
@[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
theorem cauchy_seq_finset_iff_vanishing_norm {α : Type u_1} {ι : Type u_4} [semi_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} [semi_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} [semi_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} [semi_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} [semi_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)) :

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 has_sum_iff_tendsto_nat_of_summable_norm {α : Type u_1} [semi_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} [semi_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 has_sum.norm_le_of_bounded {α : Type u_1} {ι : Type u_4} [semi_normed_group α] {f : ι → α} {g : ι → } {a : α} {b : } (hf : has_sum f a) (hg : has_sum g b) (h : ∀ (i : ι), f i g i) :
theorem tsum_of_norm_bounded {α : Type u_1} {ι : Type u_4} [semi_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 norm_tsum_le_tsum_norm {α : Type u_1} {ι : Type u_4} [semi_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 tsum_of_nnnorm_bounded {α : Type u_1} {ι : Type u_4} [semi_normed_group α] {f : ι → α} {g : ι → ℝ≥0} {a : ℝ≥0} (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, nnnorm (f i) ≤ g i, then nnnorm (∑' 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 nnnorm_tsum_le {α : Type u_1} {ι : Type u_4} [semi_normed_group α] {f : ι → α} (hf : summable (λ (i : ι), f i∥₊)) :
∑' (i : ι), f i∥₊ ∑' (i : ι), f i∥₊

If ∑' i, nnnorm (f i) is summable, then nnnorm (∑' i, f i) ≤ ∑' i, nnnorm (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 summable_of_norm_bounded_eventually {α : Type u_1} {ι : Type u_4} [semi_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} [semi_normed_group α] [complete_space α] {f : ι → α} (g : ι → ℝ≥0) (hg : summable g) (h : ∀ (i : ι), f i∥₊ g i) :
theorem summable_of_summable_norm {α : Type u_1} {ι : Type u_4} [semi_normed_group α] [complete_space α] {f : ι → α} (hf : summable (λ (a : ι), f a)) :
theorem summable_of_summable_nnnorm {α : Type u_1} {ι : Type u_4} [semi_normed_group α] [complete_space α] {f : ι → α} (hf : summable (λ (a : ι), f a∥₊)) :

Multiplying two infinite sums in a normed ring #

In this section, we prove various results about (∑' x : ι, f x) * (∑' y : ι', g y) in a normed ring. There are similar results proven in topology/algebra/infinite_sum (e.g tsum_mul_tsum), but in a normed ring we get summability results which aren't true in general.

We first establish results about arbitrary index types, β and γ, and then we specialize to β = γ = ℕ to prove the Cauchy product formula (see tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm).

Arbitrary index types #

theorem summable.mul_of_nonneg {ι : Type u_4} {ι' : Type u_5} {f : ι → } {g : ι' → } (hf : summable f) (hg : summable g) (hf' : 0 f) (hg' : 0 g) :
summable (λ (x : ι × ι'), (f x.fst) * g x.snd)
theorem summable.mul_norm {α : Type u_1} {ι : Type u_4} {ι' : Type u_5} [normed_ring α] {f : ι → α} {g : ι' → α} (hf : summable (λ (x : ι), f x)) (hg : summable (λ (x : ι'), g x)) :
summable (λ (x : ι × ι'), (f x.fst) * g x.snd)
theorem summable_mul_of_summable_norm {α : Type u_1} {ι : Type u_4} {ι' : Type u_5} [normed_ring α] [complete_space α] {f : ι → α} {g : ι' → α} (hf : summable (λ (x : ι), f x)) (hg : summable (λ (x : ι'), g x)) :
summable (λ (x : ι × ι'), (f x.fst) * g x.snd)
theorem tsum_mul_tsum_of_summable_norm {α : Type u_1} {ι : Type u_4} {ι' : Type u_5} [normed_ring α] [complete_space α] {f : ι → α} {g : ι' → α} (hf : summable (λ (x : ι), f x)) (hg : summable (λ (x : ι'), g x)) :
(∑' (x : ι), f x) * ∑' (y : ι'), g y = ∑' (z : ι × ι'), (f z.fst) * g z.snd

Product of two infinites sums indexed by arbitrary types. See also tsum_mul_tsum if f and g are not absolutely summable.

-indexed families (Cauchy product) #

We prove two versions of the Cauchy product formula. The first one is tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm, where the n-th term is a sum over finset.range (n+1) involving nat substraction. In order to avoid nat substraction, we also provide tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm, where the n-th term is a sum over all pairs (k, l) such that k+l=n, which corresponds to the finset finset.nat.antidiagonal n.

theorem summable_norm_sum_mul_antidiagonal_of_summable_norm {α : Type u_1} [normed_ring α] {f g : → α} (hf : summable (λ (x : ), f x)) (hg : summable (λ (x : ), g x)) :
summable (λ (n : ), ∑ (kl : × ) in finset.nat.antidiagonal n, (f kl.fst) * g kl.snd)
theorem tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm {α : Type u_1} [normed_ring α] [complete_space α] {f g : → α} (hf : summable (λ (x : ), f x)) (hg : summable (λ (x : ), g x)) :
(∑' (n : ), f n) * ∑' (n : ), g n = ∑' (n : ), ∑ (kl : × ) in finset.nat.antidiagonal n, (f kl.fst) * g kl.snd

The Cauchy product formula for the product of two infinite sums indexed by , expressed by summing on finset.nat.antidiagonal. See also tsum_mul_tsum_eq_tsum_sum_antidiagonal if f and g are not absolutely summable.

theorem summable_norm_sum_mul_range_of_summable_norm {α : Type u_1} [normed_ring α] {f g : → α} (hf : summable (λ (x : ), f x)) (hg : summable (λ (x : ), g x)) :
summable (λ (n : ), ∑ (k : ) in finset.range (n + 1), (f k) * g (n - k))
theorem tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm {α : Type u_1} [normed_ring α] [complete_space α] {f g : → α} (hf : summable (λ (x : ), f x)) (hg : summable (λ (x : ), g x)) :
(∑' (n : ), f n) * ∑' (n : ), g n = ∑' (n : ), ∑ (k : ) in finset.range (n + 1), (f k) * g (n - k)

The Cauchy product formula for the product of two infinite sums indexed by , expressed by summing on finset.range. See also tsum_mul_tsum_eq_tsum_sum_range if f and g are not absolutely summable.

@[simp]
theorem uniform_space.completion.norm_coe {V : Type u_1} [semi_normed_group V] (v : V) :