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.

source
@[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
source
@[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
source
@[protected, instance]
def normed_ring.to_semi_normed_ring {α : Type u_1} [β : normed_ring α] :
semi_normed_ring α

A normed ring is a seminormed ring.

Equations
source
@[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
source
@[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
source
@[protected, instance]
def normed_comm_ring.to_semi_normed_comm_ring {α : Type u_1} [β : normed_comm_ring α] :
semi_normed_comm_ring α

A normed commutative ring is a seminormed commutative ring.

Equations
source
@[protected, instance]
def punit.normed_comm_ring  :
normed_comm_ring punit
Equations
source
@[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
source
@[simp]
theorem nnnorm_one {α : Type u_1} [semi_normed_group α] [has_one α] [norm_one_class α] :
∥1∥₊ = 1
source
@[protected, instance]
def semi_normed_comm_ring.to_comm_ring {α : Type u_1} [β : semi_normed_comm_ring α] :
comm_ring α
Equations
source
@[protected, instance]
def normed_ring.to_normed_group {α : Type u_1} [β : normed_ring α] :
normed_group α
Equations
source
@[protected, instance]
def semi_normed_ring.to_semi_normed_group {α : Type u_1} [β : semi_normed_ring α] :
semi_normed_group α
Equations
source
@[protected, 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 (α × β)
source
theorem norm_mul_le {α : Type u_1} [semi_normed_ring α] (a b : α) :
∥a * b∥ ≤ ∥a∥ * ∥b∥
source
@[protected, 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) :
semi_normed_ring ↥s

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

See note [implicit instance arguments].

Equations
source
@[protected, 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) :
normed_ring ↥s

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

See note [implicit instance arguments].

Equations
source
theorem list.norm_prod_le' {α : Type u_1} [semi_normed_ring α] {l : list α} :
l ≠ list.nil → ∥l.prod∥ ≤ (list.map norm l).prod
source
theorem list.norm_prod_le {α : Type u_1} [semi_normed_ring α] [norm_one_class α] (l : list α) :
∥l.prod∥ ≤ (list.map norm l).prod
source
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∥
source
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∥
source
theorem norm_pow_le' {α : Type u_1} [semi_normed_ring α] (a : α) {n : ℕ} :
0 < n → ∥a ^ n∥ ≤ ∥a∥ ^ n

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

source
theorem norm_pow_le {α : Type u_1} [semi_normed_ring α] [norm_one_class α] (a : α) (n : ℕ) :
∥a ^ n∥ ≤ ∥a∥ ^ n

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

source
theorem eventually_norm_pow_le {α : Type u_1} [semi_normed_ring α] (a : α) :
∀ᶠ (n : ℕ) in filter.at_top, ∥a ^ n∥ ≤ ∥a∥ ^ n
source
theorem mul_left_bound {α : Type u_1} [semi_normed_ring α] (x y : α) :
∥⇑(add_monoid_hom.mul_left x) y∥ ≤ ∥x∥ * ∥y∥

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

source
theorem mul_right_bound {α : Type u_1} [semi_normed_ring α] (x y : α) :
∥⇑(add_monoid_hom.mul_right x) y∥ ≤ ∥x∥ * ∥y∥

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

source
@[protected, instance]
noncomputable def prod.semi_normed_ring {α : Type u_1} {β : Type u_2} [semi_normed_ring α] [semi_normed_ring β] :
semi_normed_ring (α × β)

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

Equations
source
noncomputable def matrix.semi_normed_group {α : Type u_1} [semi_normed_ring α] {n : Type u_2} {m : Type u_3} [fintype n] [fintype m] :
semi_normed_group (matrix n 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
source
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
source
theorem units.norm_pos {α : Type u_1} [normed_ring α] [nontrivial α] (x : αˣ) :
0 < ∥↑x∥
source
@[protected, instance]
noncomputable 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
source
noncomputable def matrix.normed_group {α : Type u_1} [normed_ring α] {n : Type u_2} {m : Type u_3} [fintype n] [fintype m] :
normed_group (matrix n 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
source
@[protected, instance]
def semi_normed_ring_top_monoid {α : Type u_1} [semi_normed_ring α] :
has_continuous_mul α
source
@[protected, instance]
def semi_normed_top_ring {α : Type u_1} [semi_normed_ring α] :
topological_ring α

A seminormed ring is a topological ring.

source
@[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
source
@[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
source
@[simp]
theorem normed_field.norm_mul {α : Type u_1} [normed_field α] (a b : α) :
∥a * b∥ = ∥a∥ * ∥b∥
source
@[protected, instance]
def normed_field.to_normed_comm_ring {α : Type u_1} [normed_field α] :
normed_comm_ring α
Equations
source
@[protected, instance]
def normed_field.to_norm_one_class {α : Type u_1} [normed_field α] :
norm_one_class α
source
@[simp]
theorem normed_field.nnnorm_mul {α : Type u_1} [normed_field α] (a b : α) :
∥a * b∥₊ = ∥a∥₊ * ∥b∥₊
source
@[simp]
theorem normed_field.norm_hom_apply {α : Type u_1} [normed_field α] (ᾰ : α) :
⇑normed_field.norm_hom ᾰ = ∥ᾰ∥
source
def normed_field.norm_hom {α : Type u_1} [normed_field α] :
monoid_with_zero_hom α ℝ

norm as a monoid_hom.

Equations
source
@[simp]
theorem normed_field.nnnorm_hom_apply {α : Type u_1} [normed_field α] (ᾰ : α) :
⇑normed_field.nnnorm_hom ᾰ = ∥ᾰ∥₊
source
def normed_field.nnnorm_hom {α : Type u_1} [normed_field α] :
monoid_with_zero_hom α ℝ≥0

nnnorm as a monoid_hom.

Equations
source
@[simp]
theorem normed_field.norm_pow {α : Type u_1} [normed_field α] (a : α) (n : ℕ) :
∥a ^ n∥ = ∥a∥ ^ n
source
@[simp]
theorem normed_field.nnnorm_pow {α : Type u_1} [normed_field α] (a : α) (n : ℕ) :
∥a ^ n∥₊ = ∥a∥₊ ^ n
source
@[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∥
source
@[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∥₊
source
@[simp]
theorem normed_field.norm_div {α : Type u_1} [normed_field α] (a b : α) :
∥a / b∥ = ∥a∥ / ∥b∥
source
@[simp]
theorem normed_field.nnnorm_div {α : Type u_1} [normed_field α] (a b : α) :
∥a / b∥₊ = ∥a∥₊ / ∥b∥₊
source
@[simp]
theorem normed_field.norm_inv {α : Type u_1} [normed_field α] (a : α) :
∥a⁻¹∥ = ∥a∥⁻¹
source
@[simp]
theorem normed_field.nnnorm_inv {α : Type u_1} [normed_field α] (a : α) :
∥a⁻¹∥₊ = ∥a∥₊⁻¹
source
@[simp]
theorem normed_field.norm_zpow {α : Type u_1} [normed_field α] (a : α) (n : ℤ) :
∥a ^ n∥ = ∥a∥ ^ n
source
@[simp]
theorem normed_field.nnnorm_zpow {α : Type u_1} [normed_field α] (a : α) (n : ℤ) :
∥a ^ n∥₊ = ∥a∥₊ ^ n
source
@[protected, instance]
def normed_field.has_continuous_inv₀ {α : Type u_1} [normed_field α] :
has_continuous_inv₀ α
Equations
source
theorem normed_field.exists_one_lt_norm (α : Type u_1) [nondiscrete_normed_field α] :
∃ (x : α), 1 < ∥x∥
source
theorem normed_field.exists_norm_lt_one (α : Type u_1) [nondiscrete_normed_field α] :
∃ (x : α), 0 < ∥x∥ ∧ ∥x∥ < 1
source
theorem normed_field.exists_lt_norm (α : Type u_1) [nondiscrete_normed_field α] (r : ℝ) :
∃ (x : α), r < ∥x∥
source
theorem normed_field.exists_norm_lt (α : Type u_1) [nondiscrete_normed_field α] {r : ℝ} (hr : 0 < r) :
∃ (x : α), 0 < ∥x∥ ∧ ∥x∥ < r
source
@[instance]
theorem normed_field.punctured_nhds_ne_bot {α : Type u_1} [nondiscrete_normed_field α] (x : α) :
(𝓝[{x}ᶜ] x).ne_bot
source
@[instance]
theorem normed_field.nhds_within_is_unit_ne_bot {α : Type u_1} [nondiscrete_normed_field α] :
(𝓝[{x : α | is_unit x}] 0).ne_bot
source
@[protected, instance]
noncomputable def real.normed_field  :
normed_field ℝ
Equations
source
@[protected, instance]
noncomputable def real.nondiscrete_normed_field  :
nondiscrete_normed_field ℝ
Equations
source
theorem real.norm_of_nonneg {x : ℝ} (hx : 0 ≤ x) :
∥x∥ = x
source
theorem real.norm_of_nonpos {x : ℝ} (hx : x ≤ 0) :
∥x∥ = -x
source
@[simp]
theorem real.norm_coe_nat (n : ℕ) :
∥↑n∥ = ↑n
source
@[simp]
theorem real.nnnorm_coe_nat (n : ℕ) :
∥↑n∥₊ = ↑n
source
@[simp]
theorem real.norm_two  :
∥2∥ = 2
source
@[simp]
theorem real.nnnorm_two  :
∥2∥₊ = 2
source
theorem real.nnnorm_of_nonneg {x : ℝ} (hx : 0 ≤ x) :
∥x∥₊ = ⟨x, hx⟩
source
theorem real.ennnorm_eq_of_real {x : ℝ} (hx : 0 ≤ x) :
↑∥x∥₊ = ennreal.of_real x
source
theorem real.of_real_le_ennnorm (x : ℝ) :
ennreal.of_real x ≤ ↑∥x∥₊
source
@[protected, instance]
def real.punctured_nhds_module_ne_bot {E : Type u_1} [add_comm_group E] [topological_space E] [has_continuous_add E] [nontrivial E] [module ℝ E] [has_continuous_smul ℝ E] (x : E) :
(𝓝[{x}ᶜ] x).ne_bot

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.

source
@[simp]
theorem nnreal.norm_eq (x : ℝ≥0) :
∥↑x∥ = ↑x
source
@[simp]
theorem nnreal.nnnorm_eq (x : ℝ≥0) :
∥↑x∥₊ = x
source
@[simp]
theorem norm_norm {α : Type u_1} [semi_normed_group α] (x : α) :
∥∥x∥∥ = ∥x∥
source
@[simp]
theorem nnnorm_norm {α : Type u_1} [semi_normed_group α] (a : α) :
∥∥a∥∥₊ = ∥a∥₊
source
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 ≤ n → ∥f n - b∥ < ε)

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

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

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

source
@[protected, instance]
noncomputable def int.normed_comm_ring  :
normed_comm_ring ℤ
Equations
source
@[norm_cast]
theorem int.norm_cast_real (m : ℤ) :
∥↑m∥ = ∥m∥
source
theorem int.norm_eq_abs (n : ℤ) :
∥n∥ = |↑n|
source
theorem nnreal.coe_nat_abs (n : ℤ) :
↑(n.nat_abs) = ∥n∥₊
source
@[protected, instance]
def int.norm_one_class  :
norm_one_class ℤ
source
@[protected, instance]
noncomputable def rat.normed_field  :
normed_field ℚ
Equations
source
@[protected, instance]
noncomputable def rat.nondiscrete_normed_field  :
nondiscrete_normed_field ℚ
Equations
source
@[simp, norm_cast]
theorem rat.norm_cast_real (r : ℚ) :
∥↑r∥ = ∥r∥
source
@[simp, norm_cast]
theorem int.norm_cast_rat (m : ℤ) :
∥↑m∥ = ∥m∥
source
theorem norm_nsmul_le {α : Type u_1} [semi_normed_group α] (n : ℕ) (a : α) :
∥n • a∥ ≤ (↑n) * ∥a∥
source
theorem norm_zsmul_le {α : Type u_1} [semi_normed_group α] (n : ℤ) (a : α) :
∥n • a∥ ≤ ∥n∥ * ∥a∥
source
theorem nnnorm_nsmul_le {α : Type u_1} [semi_normed_group α] (n : ℕ) (a : α) :
∥n • a∥₊ ≤ (↑n) * ∥a∥₊
source
theorem nnnorm_zsmul_le {α : Type u_1} [semi_normed_group α] (n : ℤ) (a : α) :
∥n • a∥₊ ≤ ∥n∥₊ * ∥a∥₊
source
@[class]
structure normed_space (α : Type u_5) (β : Type u_6) [normed_field α] [semi_normed_group β] :
Type (max u_5 u_6)

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.

Note that since this requires semi_normed_group and not normed_group, this typeclass can be used for "semi normed spaces" too, just as module can be used for "semi modules".

Instances
source
@[protected, instance]
def normed_space.has_bounded_smul {α : Type u_1} {β : Type u_2} [normed_field α] [semi_normed_group β] [normed_space α β] :
has_bounded_smul α β
source
@[protected, instance]
def normed_field.to_normed_space {α : Type u_1} [normed_field α] :
normed_space α α
Equations
source
theorem norm_smul {α : Type u_1} {β : Type u_2} [normed_field α] [semi_normed_group β] [normed_space α β] (s : α) (x : β) :
∥s • x∥ = ∥s∥ * ∥x∥
source
@[simp]
theorem abs_norm_eq_norm {β : Type u_2} [semi_normed_group β] (z : β) :
|∥z∥| = ∥z∥
source
theorem dist_smul {α : Type u_1} {β : Type u_2} [normed_field α] [semi_normed_group β] [normed_space α β] (s : α) (x y : β) :
dist (s • x) (s • y) = ∥s∥ * dist x y
source
theorem nnnorm_smul {α : Type u_1} {β : Type u_2} [normed_field α] [semi_normed_group β] [normed_space α β] (s : α) (x : β) :
∥s • x∥₊ = ∥s∥₊ * ∥x∥₊
source
theorem nndist_smul {α : Type u_1} {β : Type u_2} [normed_field α] [semi_normed_group β] [normed_space α β] (s : α) (x y : β) :
nndist (s • x) (s • y) = ∥s∥₊ * nndist x y
source
theorem norm_smul_of_nonneg {β : Type u_2} [semi_normed_group β] [normed_space ℝ β] {t : ℝ} (ht : 0 ≤ t) (x : β) :
∥t • x∥ = t * ∥x∥
source
theorem eventually_nhds_norm_smul_sub_lt {α : Type u_1} [normed_field α] {E : Type u_5} [semi_normed_group E] [normed_space α E] (c : α) (x : E) {ε : ℝ} (h : 0 < ε) :
∀ᶠ (y : E) in 𝓝 x, ∥c • (y - x)∥ < ε
source
theorem closure_ball {E : Type u_5} [semi_normed_group E] [normed_space ℝ E] (x : E) {r : ℝ} (hr : 0 < r) :
closure (metric.ball x r) = metric.closed_ball x r
source
theorem frontier_ball {E : Type u_5} [semi_normed_group E] [normed_space ℝ E] (x : E) {r : ℝ} (hr : 0 < r) :
frontier (metric.ball x r) = metric.sphere x r
source
theorem interior_closed_ball {E : Type u_5} [semi_normed_group E] [normed_space ℝ E] (x : E) {r : ℝ} (hr : 0 < r) :
interior (metric.closed_ball x r) = metric.ball x r
source
theorem frontier_closed_ball {E : Type u_5} [semi_normed_group E] [normed_space ℝ E] (x : E) {r : ℝ} (hr : 0 < r) :
frontier (metric.closed_ball x r) = metric.sphere x r
source
theorem homeomorph_unit_ball_apply_coe {E : Type u_1} [semi_normed_group E] [normed_space ℝ E] (x : E) :
↑(⇑homeomorph_unit_ball x) = (1 + ∥x∥)⁻¹ • x
source
noncomputable def homeomorph_unit_ball {E : Type u_1} [semi_normed_group E] [normed_space ℝ E] :
E ≃ₜ ↥(metric.ball 0 1)

A (semi) normed real vector space is homeomorphic to the unit ball in the same space. This homeomorphism sends x : E to (1 + ∥x∥)⁻¹ • x.

In many cases the actual implementation is not important, so we don't mark the projection lemmas homeomorph_unit_ball_apply_coe and homeomorph_unit_ball_symm_apply as @[simp].

Equations
source
theorem homeomorph_unit_ball_symm_apply {E : Type u_1} [semi_normed_group E] [normed_space ℝ E] (x : ↥(metric.ball 0 1)) :
⇑(homeomorph_unit_ball.symm) x = (1 - ∥↑x∥)⁻¹ • ↑x
source
theorem ne_neg_of_mem_sphere (α : Type u_1) [normed_field α] {E : Type u_5} [semi_normed_group E] [normed_space α E] [char_zero α] {r : ℝ} (hr : 0 < r) (x : ↥(metric.sphere 0 r)) :
x ≠ -x
source
theorem ne_neg_of_mem_unit_sphere (α : Type u_1) [normed_field α] {E : Type u_5} [semi_normed_group E] [normed_space α E] [char_zero α] (x : ↥(metric.sphere 0 1)) :
x ≠ -x
source
@[protected, instance]
noncomputable def prod.normed_space {α : Type u_1} [normed_field α] {E : Type u_5} [semi_normed_group E] [normed_space α E] {F : Type u_6} [semi_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
source
@[protected, instance]
noncomputable def pi.normed_space {α : Type u_1} {ι : Type u_4} [normed_field α] {E : ι → Type u_2} [fintype ι] [Π (i : ι), semi_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
source
@[protected, instance]
def submodule.normed_space {𝕜 : Type u_1} {R : Type u_2} [has_scalar 𝕜 R] [normed_field 𝕜] [ring R] {E : Type u_3} [semi_normed_group E] [normed_space 𝕜 E] [module R E] [is_scalar_tower 𝕜 R E] (s : submodule R E) :
normed_space 𝕜 ↥s

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

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

source
@[protected, instance]
def normed_space.to_module' {α : Type u_1} [normed_field α] {F : Type u_6} [normed_group F] [normed_space α F] :
module α F

While this may appear identical to normed_space.to_module, it contains an implicit argument involving normed_group.to_semi_normed_group that typeclass inference has trouble inferring.

Specifically, the following instance cannot be found without this normed_space.to_module':

example
  (𝕜 ι : Type*) (E : ι → Type*)
  [normed_field 𝕜] [Π i, normed_group (E i)] [Π i, normed_space 𝕜 (E i)] :
  Π i, module 𝕜 (E i) := by apply_instance

This Zulip thread gives some more context.

Equations
source
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
source
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
source
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.

source
noncomputable 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
source
theorem normed_space.exists_lt_norm (𝕜 : Type u_5) (E : Type u_6) [nondiscrete_normed_field 𝕜] [normed_group E] [normed_space 𝕜 E] [nontrivial E] (c : ℝ) :
∃ (x : E), c < ∥x∥

If E is a nontrivial normed space over a nondiscrete normed field 𝕜, then E is unbounded: for any c : ℝ, there exists a vector x : E with norm strictly greater than c.

source
@[protected]
theorem normed_space.unbounded_univ (𝕜 : Type u_5) (E : Type u_6) [nondiscrete_normed_field 𝕜] [normed_group E] [normed_space 𝕜 E] [nontrivial E] :
¬metric.bounded set.univ
source
@[protected]
theorem normed_space.noncompact_space (𝕜 : Type u_5) (E : Type u_6) [nondiscrete_normed_field 𝕜] [normed_group E] [normed_space 𝕜 E] [nontrivial E] :
noncompact_space E

A normed vector space over a nondiscrete normed field is a noncompact space. This cannot be an instance because in order to apply it, Lean would have to search for normed_space 𝕜 E with unknown 𝕜. We register this as an instance in two cases: 𝕜 = E and 𝕜 = ℝ.

source
@[protected, instance]
def nondiscrete_normed_field.noncompact_space (𝕜 : Type u_5) [nondiscrete_normed_field 𝕜] :
noncompact_space 𝕜
source
@[protected, instance]
def real_normed_space.noncompact_space (E : Type u_6) [normed_group E] [nontrivial E] [normed_space ℝ E] :
noncompact_space E
source
@[class]
structure normed_algebra (𝕜 : Type u_5) (𝕜' : Type u_6) [normed_field 𝕜] [semi_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
source
@[simp]
theorem norm_algebra_map_eq {𝕜 : Type u_1} (𝕜' : Type u_2) [normed_field 𝕜] [semi_normed_ring 𝕜'] [h : normed_algebra 𝕜 𝕜'] (x : 𝕜) :
∥⇑(algebra_map 𝕜 𝕜') x∥ = ∥x∥
source
theorem algebra_map_isometry (𝕜 : Type u_1) (𝕜' : Type u_2) [normed_field 𝕜] [semi_normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] :
isometry ⇑(algebra_map 𝕜 𝕜')

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

source
@[protected, instance]
def normed_algebra.to_normed_space (𝕜 : Type u_5) (𝕜' : Type u_6) [normed_field 𝕜] [semi_normed_ring 𝕜'] [h : normed_algebra 𝕜 𝕜'] :
normed_space 𝕜 𝕜'
Equations
source
@[protected, instance]
def normed_algebra.to_normed_space' (𝕜 : Type u_5) (𝕜' : Type u_6) [normed_field 𝕜] [normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] :
normed_space 𝕜 𝕜'

While this may appear identical to normed_algebra.to_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 normed_space.to_module':

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

See normed_space.to_module' for a similar situation.

Equations
source
@[protected, instance]
def normed_algebra.id (𝕜 : Type u_5) [normed_field 𝕜] :
normed_algebra 𝕜 𝕜
Equations
source
theorem normed_algebra.norm_one (𝕜 : Type u_5) (𝕜' : Type u_6) [normed_field 𝕜] [semi_normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] :
∥1∥ = 1
source
theorem normed_algebra.norm_one_class (𝕜 : Type u_5) (𝕜' : Type u_6) [normed_field 𝕜] [semi_normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] :
norm_one_class 𝕜'
source
theorem normed_algebra.zero_ne_one (𝕜 : Type u_5) (𝕜' : Type u_6) [normed_field 𝕜] [semi_normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] :
0 ≠ 1
source
theorem normed_algebra.nontrivial (𝕜 : Type u_5) (𝕜' : Type u_6) [normed_field 𝕜] [semi_normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] :
nontrivial 𝕜'
source
def normed_space.restrict_scalars (𝕜 : Type u_5) (𝕜' : Type u_6) [normed_field 𝕜] [normed_field 𝕜'] [normed_algebra 𝕜 𝕜'] (E : Type u_7) [semi_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 restrict_scalars 𝕜 𝕜' E will be endowed with this instance by default.

Equations
source
@[protected, instance]
def restrict_scalars.semi_normed_group {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [I : semi_normed_group E] :
semi_normed_group (restrict_scalars 𝕜 𝕜' E)
Equations
source
@[protected, 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
source
@[protected, instance]
def module.restrict_scalars.normed_space_orig {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [normed_field 𝕜'] [semi_normed_group E] [I : normed_space 𝕜' E] :
normed_space 𝕜' (restrict_scalars 𝕜 𝕜' E)
Equations
source
@[protected, instance]
def restrict_scalars.normed_space (𝕜 : Type u_5) (𝕜' : Type u_6) [normed_field 𝕜] [normed_field 𝕜'] [normed_algebra 𝕜 𝕜'] (E : Type u_7) [semi_normed_group E] [normed_space 𝕜' E] :
normed_space 𝕜 (restrict_scalars 𝕜 𝕜' E)
Equations

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 #

source
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)
source
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∥)
source
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)
source
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.

source
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∥)
source
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.

source
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)∥)
source
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.

source
@[class]
structure ring_hom_isometric {R₁ : Type u_5} {R₂ : Type u_6} [semiring R₁] [semiring R₂] [has_norm R₁] [has_norm R₂] (σ : R₁ →+* R₂) :
Prop

This class states that a ring homomorphism is isometric. This is a sufficient assumption for a continuous semilinear map to be bounded and this is the main use for this typeclass.

Instances
source
@[protected, instance]
def ring_hom_isometric.ids {R₁ : Type u_5} [semi_normed_ring R₁] :
ring_hom_isometric (ring_hom.id R₁)