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

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]
@[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 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]
def pi.non_unital_semi_normed_ring {ι : Type u_4} {π : ι Type u_1} [fintype ι] [Π (i : ι), non_unital_semi_normed_ring (π 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 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 : } :

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 : α) :
@[protected, instance]
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]
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]
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]
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]
@[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.

theorem norm_one_of_pow_eq_one {α : Type u_1} [normed_division_ring α] {x : α} {k : ℕ+} (h : x ^ k = 1) :
theorem norm_map_one_of_pow_eq_one {α : Type u_1} {β : Type u_2} [normed_division_ring α] [comm_monoid β] (φ : β →* α) {x : β} {k : ℕ+} (h : x ^ k = 1) :
φ x = 1
@[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_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
@[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
@[protected, instance]
Equations
theorem real.to_nnreal_mul_nnnorm {x : } (y : ) (hx : 0 x) :
theorem real.nnnorm_mul_to_nnreal (x : ) {y : } (hy : 0 y) :
@[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 n f 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 < n f n - b < ε)

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

@[protected, instance]
Equations
@[norm_cast]
theorem int.norm_cast_real (m : ) :
theorem int.norm_eq_abs (n : ) :
@[protected, instance]
@[protected, instance]
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]

Induced normed structures #

@[reducible]
def normed_ring.induced {F : Type u_5} (R : Type u_6) (S : Type u_7) [ring R] [normed_ring S] [non_unital_ring_hom_class F R S] (f : F) (hf : function.injective f) :

An injective non-unital ring homomorphism from an ring to a normed_ring induces a normed_ring structure on the domain.

See note [reducible non-instances]

Equations
@[reducible]
def normed_field.induced {F : Type u_5} (R : Type u_6) (S : Type u_7) [field R] [normed_field S] [non_unital_ring_hom_class F R S] (f : F) (hf : function.injective f) :

An injective non-unital ring homomorphism from an field to a normed_ring induces a normed_field structure on the domain.

See note [reducible non-instances]

Equations
theorem norm_one_class.induced {F : Type u_1} (R : Type u_2) (S : Type u_3) [ring R] [semi_normed_ring S] [norm_one_class S] [ring_hom_class F R S] (f : F) :

A ring homomorphism from a ring R to a semi_normed_ring S which induces the norm structure semi_normed_ring.induced makes R satisfy ‖(1 : R)‖ = 1 whenever ‖(1 : S)‖ = 1.

@[protected, instance]
def subring_class.to_normed_ring {S : Type u_5} {R : Type u_6} [set_like S R] [normed_ring R] [subring_class S R] (s : S) :
Equations