mathlib3 documentation

analysis.normed.field.basic

Normed fields #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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
@[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 of this typeclass
@[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 : ) :
theorem dist_inv_inv₀ {α : Type u_1} [normed_division_ring α] {z w : α} (hz : z 0) (hw : w 0) :
theorem nndist_inv_inv₀ {α : Type u_1} [normed_division_ring α] {z w : α} (hz : z 0) (hw : w 0) :

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.

@[protected, instance]

A normed division ring is a topological division ring.

theorem norm_map_one_of_pow_eq_one {α : Type u_1} {β : Type u_2} [normed_division_ring α] [monoid β] (φ : β →* α) {x : β} {k : ℕ+} (h : x ^ k = 1) :
φ x = 1
theorem norm_one_of_pow_eq_one {α : Type u_1} [normed_division_ring α] {x : α} {k : ℕ+} (h : x ^ k = 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) :
@[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]
@[protected, instance]
Equations
@[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 semi_normed_ring.induced {F : Type u_5} (R : Type u_6) (S : Type u_7) [ring R] [semi_normed_ring S] [non_unital_ring_hom_class F R S] (f : F) :

A non-unital ring homomorphism from an ring to a semi_normed_ring induces a semi_normed_ring structure on the domain.

See note [reducible non-instances]

Equations
@[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]

An injective non-unital ring homomorphism from an division_ring to a normed_ring induces a normed_division_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