mathlib documentation

analysis.normed.field.basic

Normed fields #

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

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

A non-unital seminormed ring is a not-necessarily-unital ring endowed with a seminorm which satisfies the inequality ∥x y∥ ≤ ∥x∥ ∥y∥.

Instances of this typeclass
Instances of other typeclasses for non_unital_semi_normed_ring
  • non_unital_semi_normed_ring.has_sizeof_inst
@[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 of this typeclass
Instances of other typeclasses for semi_normed_ring
  • semi_normed_ring.has_sizeof_inst
@[class]
structure non_unital_normed_ring (α : Type u_5) :
Type u_5

A non-unital normed ring is a not-necessarily-unital ring endowed with a norm which satisfies the inequality ∥x y∥ ≤ ∥x∥ ∥y∥.

Instances of this typeclass
Instances of other typeclasses for non_unital_normed_ring
  • non_unital_normed_ring.has_sizeof_inst
@[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 of this typeclass
Instances of other typeclasses for normed_ring
  • normed_ring.has_sizeof_inst
@[class]
structure normed_division_ring (α : Type u_5) :
Type u_5

A normed division ring is a division ring endowed with a seminorm which satisfies the equality ∥x y∥ = ∥x∥ ∥y∥.

Instances of this typeclass
Instances of other typeclasses for normed_division_ring
  • normed_division_ring.has_sizeof_inst
@[protected, instance]

A normed division ring is a normed ring.

Equations
@[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 of this typeclass
Instances of other typeclasses for semi_normed_comm_ring
  • semi_normed_comm_ring.has_sizeof_inst
@[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 of this typeclass
Instances of other typeclasses for normed_comm_ring
  • normed_comm_ring.has_sizeof_inst
@[protected, instance]
Equations
@[simp]
theorem nnnorm_one {α : Type u_1} [seminormed_add_comm_group α] [has_one α] [norm_one_class α] :
@[protected, instance]
@[protected, instance]
def prod.norm_one_class {α : Type u_1} {β : Type u_2} [seminormed_add_comm_group α] [has_one α] [norm_one_class α] [seminormed_add_comm_group β] [has_one β] [norm_one_class β] :
@[protected, instance]
def pi.norm_one_class {ι : Type u_1} {α : ι → Type u_2} [nonempty ι] [fintype ι] [Π (i : ι), seminormed_add_comm_group (α i)] [Π (i : ι), has_one (α i)] [∀ (i : ι), norm_one_class (α i)] :
norm_one_class (Π (i : ι), α i)
theorem norm_mul_le {α : Type u_1} [non_unital_semi_normed_ring α] (a b : α) :
theorem nnnorm_mul_le {α : Type u_1} [non_unital_semi_normed_ring α] (a b : α) :
theorem one_le_norm_one (β : Type u_1) [normed_ring β] [nontrivial β] :
theorem one_le_nnnorm_one (β : Type u_1) [normed_ring β] [nontrivial β] :
theorem filter.tendsto.zero_mul_is_bounded_under_le {α : Type u_1} {ι : Type u_4} [non_unital_semi_normed_ring α] {f g : ι → α} {l : filter ι} (hf : filter.tendsto f l (nhds 0)) (hg : filter.is_bounded_under has_le.le l (has_norm.norm g)) :
filter.tendsto (λ (x : ι), f x * g x) l (nhds 0)
theorem filter.is_bounded_under_le.mul_tendsto_zero {α : Type u_1} {ι : Type u_4} [non_unital_semi_normed_ring α] {f g : ι → α} {l : filter ι} (hf : filter.is_bounded_under has_le.le l (has_norm.norm f)) (hg : filter.tendsto g l (nhds 0)) :
filter.tendsto (λ (x : ι), f x * g x) l (nhds 0)

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

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

@[protected, instance]
noncomputable def pi.non_unital_semi_normed_ring {ι : Type u_4} {π : ι → Type u_1} [fintype ι] [Π (i : ι), non_unital_semi_normed_ring (π i)] :
non_unital_semi_normed_ring (Π (i : ι), π i)

Non-unital seminormed ring structure on the product of finitely many non-unital seminormed rings, using the sup norm.

Equations
@[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) :

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

See note [implicit instance arguments].

Equations
@[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) :

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

See note [implicit instance arguments].

Equations
theorem nat.norm_cast_le {α : Type u_1} [semi_normed_ring α] (n : ) :
theorem list.norm_prod_le' {α : Type u_1} [semi_normed_ring α] {l : list α} :
theorem list.nnnorm_prod_le' {α : Type u_1} [semi_normed_ring α] {l : list α} (hl : l list.nil) :
theorem finset.norm_prod_le' {ι : Type u_4} {α : Type u_1} [normed_comm_ring α] (s : finset ι) (hs : s.nonempty) (f : ι → α) :
s.prod (λ (i : ι), f i) s.prod (λ (i : ι), f i)
theorem finset.nnnorm_prod_le' {ι : Type u_4} {α : Type u_1} [normed_comm_ring α] (s : finset ι) (hs : s.nonempty) (f : ι → α) :
s.prod (λ (i : ι), f i)∥₊ s.prod (λ (i : ι), f i∥₊)
theorem finset.norm_prod_le {ι : Type u_4} {α : Type u_1} [normed_comm_ring α] [norm_one_class α] (s : finset ι) (f : ι → α) :
s.prod (λ (i : ι), f i) s.prod (λ (i : ι), f i)
theorem finset.nnnorm_prod_le {ι : Type u_4} {α : Type u_1} [normed_comm_ring α] [norm_one_class α] (s : finset ι) (f : ι → α) :
s.prod (λ (i : ι), f i)∥₊ s.prod (λ (i : ι), f i∥₊)
theorem nnnorm_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 nnnorm_pow_le.

theorem nnnorm_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 nnnorm_pow_le'.

theorem norm_pow_le' {α : Type u_1} [semi_normed_ring α] (a : α) {n : } (h : 0 < 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
@[protected, instance]
noncomputable 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
@[protected, instance]
noncomputable def pi.semi_normed_ring {ι : Type u_4} {π : ι → Type u_1} [fintype ι] [Π (i : ι), semi_normed_ring (π i)] :
semi_normed_ring (Π (i : ι), π i)

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

Equations
@[protected, instance]
noncomputable def pi.non_unital_normed_ring {ι : Type u_4} {π : ι → Type u_1} [fintype ι] [Π (i : ι), non_unital_normed_ring (π i)] :
non_unital_normed_ring (Π (i : ι), π i)

Normed ring structure on the product of finitely many non-unital normed rings, using the sup norm.

Equations
theorem units.norm_pos {α : Type u_1} [normed_ring α] [nontrivial α] (x : αˣ) :
theorem units.nnnorm_pos {α : Type u_1} [normed_ring α] [nontrivial α] (x : αˣ) :
@[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
@[protected, instance]
noncomputable def pi.normed_ring {ι : Type u_4} {π : ι → Type u_1} [fintype ι] [Π (i : ι), normed_ring (π i)] :
normed_ring (Π (i : ι), π i)

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

Equations
@[protected, instance]
@[protected, instance]

A seminormed ring is a topological ring.

@[simp]
theorem norm_mul {α : Type u_1} [normed_division_ring α] (a b : α) :
@[protected, instance]
@[simp]
theorem nnnorm_mul {α : Type u_1} [normed_division_ring α] (a b : α) :
@[simp]
theorem norm_hom_apply {α : Type u_1} [normed_division_ring α] (ᾰ : α) :
@[simp]
theorem nnnorm_hom_apply {α : Type u_1} [normed_division_ring α] (ᾰ : α) :
@[simp]
theorem norm_pow {α : Type u_1} [normed_division_ring α] (a : α) (n : ) :
a ^ n = a ^ n
@[simp]
theorem nnnorm_pow {α : Type u_1} [normed_division_ring α] (a : α) (n : ) :
@[protected]
theorem list.norm_prod {α : Type u_1} [normed_division_ring α] (l : list α) :
@[protected]
theorem list.nnnorm_prod {α : Type u_1} [normed_division_ring α] (l : list α) :
@[simp]
theorem norm_div {α : Type u_1} [normed_division_ring α] (a b : α) :
@[simp]
theorem nnnorm_div {α : Type u_1} [normed_division_ring α] (a b : α) :
@[simp]
theorem norm_inv {α : Type u_1} [normed_division_ring α] (a : α) :
@[simp]
theorem nnnorm_inv {α : Type u_1} [normed_division_ring α] (a : α) :
@[simp]
theorem norm_zpow {α : Type u_1} [normed_division_ring α] (a : α) (n : ) :
a ^ n = a ^ n
@[simp]
theorem nnnorm_zpow {α : Type u_1} [normed_division_ring α] (a : α) (n : ) :

Multiplication on the left by a nonzero element of a normed division ring tends to infinity at infinity. TODO: use bornology.cobounded instead of filter.comap has_norm.norm filter.at_top.

Multiplication on the right by a nonzero element of a normed division ring tends to infinity at infinity. TODO: use bornology.cobounded instead of filter.comap has_norm.norm filter.at_top.

@[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 of this typeclass
Instances of other typeclasses for normed_field
  • normed_field.has_sizeof_inst
@[class]
structure nontrivially_normed_field (α : Type u_5) :
Type u_5

A nontrivially 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 of this typeclass
Instances of other typeclasses for nontrivially_normed_field
  • nontrivially_normed_field.has_sizeof_inst
@[class]
structure densely_normed_field (α : Type u_5) :
Type u_5

A densely normed field is a normed field for which the image of the norm is dense in ℝ≥0, which means it is also nontrivially normed. However, not all nontrivally normed fields are densely normed; in particular, the padics exhibit this fact.

Instances of this typeclass
Instances of other typeclasses for densely_normed_field
  • densely_normed_field.has_sizeof_inst
@[protected, instance]
Equations
@[simp]
theorem norm_prod {α : Type u_1} {β : Type u_2} [normed_field α] (s : finset β) (f : β → α) :
s.prod (λ (b : β), f b) = s.prod (λ (b : β), f b)
@[simp]
theorem nnnorm_prod {α : Type u_1} {β : Type u_2} [normed_field α] (s : finset β) (f : β → α) :
s.prod (λ (b : β), f b)∥₊ = s.prod (λ (b : β), f b∥₊)
theorem normed_field.exists_one_lt_norm (α : Type u_1) [nontrivially_normed_field α] :
∃ (x : α), 1 < x
theorem normed_field.exists_lt_norm (α : Type u_1) [nontrivially_normed_field α] (r : ) :
∃ (x : α), r < x
theorem normed_field.exists_norm_lt (α : Type u_1) [nontrivially_normed_field α] {r : } (hr : 0 < r) :
∃ (x : α), 0 < x x < r
theorem normed_field.exists_norm_lt_one (α : Type u_1) [nontrivially_normed_field α] :
∃ (x : α), 0 < x x < 1
@[instance]
theorem normed_field.punctured_nhds_ne_bot {α : Type u_1} [nontrivially_normed_field α] (x : α) :
@[instance]
theorem normed_field.exists_lt_norm_lt (α : Type u_1) [densely_normed_field α] {r₁ r₂ : } (h₀ : 0 r₁) (h : r₁ < r₂) :
∃ (x : α), r₁ < x x < r₂
theorem normed_field.exists_lt_nnnorm_lt (α : Type u_1) [densely_normed_field α] {r₁ r₂ : nnreal} (h : r₁ < r₂) :
∃ (x : α), r₁ < x∥₊ x∥₊ < r₂
@[protected, instance]
Equations
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⟩
@[protected, 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 : nnreal) :
@[simp]
theorem nnreal.nnnorm_eq (x : nnreal) :
@[simp]
theorem norm_norm {α : Type u_1} [seminormed_add_comm_group α] (x : α) :
@[simp]
theorem nnnorm_norm {α : Type u_1} [seminormed_add_comm_group α] (a : α) :
theorem normed_add_comm_group.tendsto_at_top {α : Type u_1} [nonempty α] [semilattice_sup α] {β : Type u_2} [seminormed_add_comm_group β] {f : α → β} {b : β} :
filter.tendsto f filter.at_top (nhds b) ∀ (ε : ), 0 < ε(∃ (N : α), ∀ (n : α), N nf n - b < ε)

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

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

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

@[protected, instance]
noncomputable def int.normed_comm_ring  :
Equations
@[norm_cast]
theorem int.norm_cast_real (m : ) :
theorem int.norm_eq_abs (n : ) :
@[protected, instance]
@[protected, instance]
noncomputable def rat.normed_field  :
Equations
@[protected, instance]
Equations
@[simp, norm_cast]
theorem rat.norm_cast_real (r : ) :
@[simp, norm_cast]
theorem int.norm_cast_rat (m : ) :
theorem norm_nsmul_le {α : Type u_1} [seminormed_add_comm_group α] (n : ) (a : α) :
theorem norm_zsmul_le {α : Type u_1} [seminormed_add_comm_group α] (n : ) (a : α) :
theorem nnnorm_nsmul_le {α : Type u_1} [seminormed_add_comm_group α] (n : ) (a : α) :
theorem nnnorm_zsmul_le {α : Type u_1} [seminormed_add_comm_group α] (n : ) (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 : ), (finset.nat.antidiagonal n).sum (λ (kl : × ), 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 : ), (finset.nat.antidiagonal n).sum (λ (kl : × ), 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 : ), (finset.range (n + 1)).sum (λ (k : ), 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 : ), (finset.range (n + 1)).sum (λ (k : ), 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.

@[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 of this typeclass
@[protected, instance]