analysis.normed.field.basic

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)

source

@[protected, instance]

def mul_opposite.norm_one_class {α : Type u_1} [seminormed_add_comm_group α] [has_one α] [norm_one_class α] :

norm_one_class αᵐᵒᵖ

source

theorem norm_mul_le {α : Type u_1} [non_unital_semi_normed_ring α] (a b : α) :

‖a * b‖ ≤ ‖a‖ * ‖b‖

source

theorem nnnorm_mul_le {α : Type u_1} [non_unital_semi_normed_ring α] (a b : α) :

‖a * b‖₊ ≤ ‖a‖₊ * ‖b‖₊

source

theorem one_le_norm_one (β : Type u_1) [normed_ring β] [nontrivial β] :

1 ≤ ‖1‖

source

theorem one_le_nnnorm_one (β : Type u_1) [normed_ring β] [nontrivial β] :

1 ≤ ‖1‖₊

source

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)

source

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)

source

theorem mul_left_bound {α : Type u_1} [non_unital_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} [non_unital_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]

def ulift.non_unital_semi_normed_ring {α : Type u_1} [non_unital_semi_normed_ring α] :

non_unital_semi_normed_ring (ulift α)

Equations

ulift.non_unital_semi_normed_ring = {to_has_norm := seminormed_add_comm_group.to_has_norm ulift.seminormed_add_comm_group, to_non_unital_ring := ulift.non_unital_ring non_unital_semi_normed_ring.to_non_unital_ring, to_pseudo_metric_space := seminormed_add_comm_group.to_pseudo_metric_space ulift.seminormed_add_comm_group, dist_eq := _, norm_mul := _}

source

@[protected, instance]

def prod.non_unital_semi_normed_ring {α : Type u_1} {β : Type u_2} [non_unital_semi_normed_ring α] [non_unital_semi_normed_ring β] :

non_unital_semi_normed_ring (α × β)

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

Equations

prod.non_unital_semi_normed_ring = {to_has_norm := seminormed_add_comm_group.to_has_norm prod.seminormed_add_comm_group, to_non_unital_ring := prod.non_unital_ring non_unital_semi_normed_ring.to_non_unital_ring, to_pseudo_metric_space := seminormed_add_comm_group.to_pseudo_metric_space prod.seminormed_add_comm_group, dist_eq := _, norm_mul := _}

source

@[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_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

pi.non_unital_semi_normed_ring = {to_has_norm := seminormed_add_comm_group.to_has_norm pi.seminormed_add_comm_group, to_non_unital_ring := pi.non_unital_ring (λ (i : ι), non_unital_semi_normed_ring.to_non_unital_ring), to_pseudo_metric_space := seminormed_add_comm_group.to_pseudo_metric_space pi.seminormed_add_comm_group, dist_eq := _, norm_mul := _}

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

s.semi_normed_ring = {to_has_norm := seminormed_add_comm_group.to_has_norm (⇑subalgebra.to_submodule s).seminormed_add_comm_group, to_ring := s.to_ring, to_pseudo_metric_space := seminormed_add_comm_group.to_pseudo_metric_space (⇑subalgebra.to_submodule s).seminormed_add_comm_group, dist_eq := _, norm_mul := _}

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

s.normed_ring = {to_has_norm := semi_normed_ring.to_has_norm s.semi_normed_ring, to_ring := semi_normed_ring.to_ring s.semi_normed_ring, to_metric_space := subtype.metric_space normed_ring.to_metric_space, dist_eq := _, norm_mul := _}

source

theorem nat.norm_cast_le {α : Type u_1} [semi_normed_ring α] (n : ℕ) :

‖↑n‖ ≤ ↑n * ‖1‖

source

theorem list.norm_prod_le' {α : Type u_1} [semi_normed_ring α] {l : list α} :

l ≠ list.nil → ‖l.prod ‖ ≤ (list.map has_norm.norm l).prod

source

theorem list.nnnorm_prod_le' {α : Type u_1} [semi_normed_ring α] {l : list α} (hl : l ≠ list.nil) :

‖l.prod ‖₊ ≤ (list.map has_nnnorm.nnnorm l).prod

source

theorem list.norm_prod_le {α : Type u_1} [semi_normed_ring α] [norm_one_class α] (l : list α) :

‖l.prod ‖ ≤ (list.map has_norm.norm l).prod

source

theorem list.nnnorm_prod_le {α : Type u_1} [semi_normed_ring α] [norm_one_class α] (l : list α) :

‖l.prod ‖₊ ≤ (list.map has_nnnorm.nnnorm l).prod

source

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‖)

source

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‖₊)

source

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‖)

source

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‖₊)

source

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

source

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

source

theorem norm_pow_le' {α : Type u_1} [semi_normed_ring α] (a : α) {n : ℕ} (h : 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

@[protected, instance]

def ulift.semi_normed_ring {α : Type u_1} [semi_normed_ring α] :

semi_normed_ring (ulift α)

Equations

ulift.semi_normed_ring = {to_has_norm := non_unital_semi_normed_ring.to_has_norm ulift.non_unital_semi_normed_ring, to_ring := ulift.ring semi_normed_ring.to_ring, to_pseudo_metric_space := non_unital_semi_normed_ring.to_pseudo_metric_space ulift.non_unital_semi_normed_ring, dist_eq := _, norm_mul := _}

source

@[protected, instance]

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

prod.semi_normed_ring = {to_has_norm := non_unital_semi_normed_ring.to_has_norm prod.non_unital_semi_normed_ring, to_ring := prod.ring semi_normed_ring.to_ring, to_pseudo_metric_space := non_unital_semi_normed_ring.to_pseudo_metric_space prod.non_unital_semi_normed_ring, dist_eq := _, norm_mul := _}

source

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

pi.semi_normed_ring = {to_has_norm := non_unital_semi_normed_ring.to_has_norm pi.non_unital_semi_normed_ring, to_ring := pi.ring (λ (i : ι), semi_normed_ring.to_ring), to_pseudo_metric_space := non_unital_semi_normed_ring.to_pseudo_metric_space pi.non_unital_semi_normed_ring, dist_eq := _, norm_mul := _}

source

@[protected, instance]

def mul_opposite.semi_normed_ring {α : Type u_1} [semi_normed_ring α] :

semi_normed_ring αᵐᵒᵖ

Equations

mul_opposite.semi_normed_ring = {to_has_norm := non_unital_semi_normed_ring.to_has_norm mul_opposite.non_unital_semi_normed_ring, to_ring := mul_opposite.ring α semi_normed_ring.to_ring, to_pseudo_metric_space := non_unital_semi_normed_ring.to_pseudo_metric_space mul_opposite.non_unital_semi_normed_ring, dist_eq := _, norm_mul := _}

source

@[protected, instance]

def ulift.non_unital_normed_ring {α : Type u_1} [non_unital_normed_ring α] :

non_unital_normed_ring (ulift α)

Equations

ulift.non_unital_normed_ring = {to_has_norm := non_unital_semi_normed_ring.to_has_norm ulift.non_unital_semi_normed_ring, to_non_unital_ring := non_unital_semi_normed_ring.to_non_unital_ring ulift.non_unital_semi_normed_ring, to_metric_space := ulift.metric_space non_unital_normed_ring.to_metric_space, dist_eq := _, norm_mul := _}

source

@[protected, instance]

def prod.non_unital_normed_ring {α : Type u_1} {β : Type u_2} [non_unital_normed_ring α] [non_unital_normed_ring β] :

non_unital_normed_ring (α × β)

Non-unital normed ring structure on the product of two non-unital normed rings, using the sup norm.

Equations

prod.non_unital_normed_ring = {to_has_norm := seminormed_add_comm_group.to_has_norm prod.seminormed_add_comm_group, to_non_unital_ring := prod.non_unital_ring non_unital_normed_ring.to_non_unital_ring, to_metric_space := prod.metric_space_max non_unital_normed_ring.to_metric_space, dist_eq := _, norm_mul := _}

source

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

pi.non_unital_normed_ring = {to_has_norm := normed_add_comm_group.to_has_norm pi.normed_add_comm_group, to_non_unital_ring := pi.non_unital_ring (λ (i : ι), non_unital_normed_ring.to_non_unital_ring), to_metric_space := normed_add_comm_group.to_metric_space pi.normed_add_comm_group, dist_eq := _, norm_mul := _}

source

@[protected, instance]

def mul_opposite.non_unital_normed_ring {α : Type u_1} [non_unital_normed_ring α] :

non_unital_normed_ring αᵐᵒᵖ

Equations

mul_opposite.non_unital_normed_ring = {to_has_norm := normed_add_comm_group.to_has_norm mul_opposite.normed_add_comm_group, to_non_unital_ring := mul_opposite.non_unital_ring α non_unital_normed_ring.to_non_unital_ring, to_metric_space := normed_add_comm_group.to_metric_space mul_opposite.normed_add_comm_group, dist_eq := _, norm_mul := _}

source

theorem units.norm_pos {α : Type u_1} [normed_ring α] [nontrivial α] (x : αˣ) :

0 < ‖↑x‖

source

theorem units.nnnorm_pos {α : Type u_1} [normed_ring α] [nontrivial α] (x : αˣ) :

0 < ‖↑x‖₊

source

@[protected, instance]

def ulift.normed_ring {α : Type u_1} [normed_ring α] :

normed_ring (ulift α)

Equations

ulift.normed_ring = {to_has_norm := semi_normed_ring.to_has_norm ulift.semi_normed_ring, to_ring := semi_normed_ring.to_ring ulift.semi_normed_ring, to_metric_space := normed_add_comm_group.to_metric_space ulift.normed_add_comm_group, dist_eq := _, norm_mul := _}

source

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

prod.normed_ring = {to_has_norm := normed_add_comm_group.to_has_norm prod.normed_add_comm_group, to_ring := prod.ring normed_ring.to_ring, to_metric_space := normed_add_comm_group.to_metric_space prod.normed_add_comm_group, dist_eq := _, norm_mul := _}

source

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

pi.normed_ring = {to_has_norm := normed_add_comm_group.to_has_norm pi.normed_add_comm_group, to_ring := pi.ring (λ (i : ι), normed_ring.to_ring), to_metric_space := normed_add_comm_group.to_metric_space pi.normed_add_comm_group, dist_eq := _, norm_mul := _}

source

@[protected, instance]

def mul_opposite.normed_ring {α : Type u_1} [normed_ring α] :

normed_ring αᵐᵒᵖ

Equations

mul_opposite.normed_ring = {to_has_norm := normed_add_comm_group.to_has_norm mul_opposite.normed_add_comm_group, to_ring := mul_opposite.ring α normed_ring.to_ring, to_metric_space := normed_add_comm_group.to_metric_space mul_opposite.normed_add_comm_group, dist_eq := _, norm_mul := _}

source

@[protected, instance]

def semi_normed_ring_top_monoid {α : Type u_1} [non_unital_semi_normed_ring α] :

has_continuous_mul α

source

@[protected, instance]

def semi_normed_top_ring {α : Type u_1} [non_unital_semi_normed_ring α] :

topological_ring α

A seminormed ring is a topological ring.

source

@[simp]

theorem norm_mul {α : Type u_1} [normed_division_ring α] (a b : α) :

‖a * b‖ = ‖a‖ * ‖b‖

source

@[protected, instance]

def normed_division_ring.to_norm_one_class {α : Type u_1} [normed_division_ring α] :

norm_one_class α

source

@[protected, instance]

def is_absolute_value_norm {α : Type u_1} [normed_division_ring α] :

is_absolute_value has_norm.norm

source

@[simp]

theorem nnnorm_mul {α : Type u_1} [normed_division_ring α] (a b : α) :

‖a * b‖₊ = ‖a‖₊ * ‖b‖₊

source

@[simp]

theorem norm_hom_apply {α : Type u_1} [normed_division_ring α] (ᾰ : α) :

⇑norm_hom ᾰ = ‖ᾰ‖

source

def norm_hom {α : Type u_1} [normed_division_ring α] :

α →*₀ ℝ

norm as a monoid_with_zero_hom.

Equations

norm_hom = {to_fun := has_norm.norm normed_division_ring.to_has_norm, map_zero' := _, map_one' := _, map_mul' := _}

source

@[simp]

theorem nnnorm_hom_apply {α : Type u_1} [normed_division_ring α] (ᾰ : α) :

⇑nnnorm_hom ᾰ = ‖ᾰ‖₊

source

def nnnorm_hom {α : Type u_1} [normed_division_ring α] :

α →*₀ nnreal

nnnorm as a monoid_with_zero_hom.

Equations

nnnorm_hom = {to_fun := has_nnnorm.nnnorm seminormed_add_group.to_has_nnnorm, map_zero' := _, map_one' := _, map_mul' := _}

source

@[simp]

theorem norm_pow {α : Type u_1} [normed_division_ring α] (a : α) (n : ℕ) :

‖a ^ n‖ = ‖a‖ ^ n

source

@[simp]

theorem nnnorm_pow {α : Type u_1} [normed_division_ring α] (a : α) (n : ℕ) :

‖a ^ n‖₊ = ‖a‖₊ ^ n

source

@[protected]

theorem list.norm_prod {α : Type u_1} [normed_division_ring α] (l : list α) :

‖l.prod ‖ = (list.map has_norm.norm l).prod

source

@[protected]

theorem list.nnnorm_prod {α : Type u_1} [normed_division_ring α] (l : list α) :

‖l.prod ‖₊ = (list.map has_nnnorm.nnnorm l).prod

source

@[simp]

theorem norm_div {α : Type u_1} [normed_division_ring α] (a b : α) :

‖a / b‖ = ‖a‖ / ‖b‖

source

@[simp]

theorem nnnorm_div {α : Type u_1} [normed_division_ring α] (a b : α) :

‖a / b‖₊ = ‖a‖₊ / ‖b‖₊

source

@[simp]

theorem norm_inv {α : Type u_1} [normed_division_ring α] (a : α) :

‖a⁻¹ ‖ = ‖a‖⁻¹

source

@[simp]

theorem nnnorm_inv {α : Type u_1} [normed_division_ring α] (a : α) :

‖a⁻¹ ‖₊ = ‖a‖₊⁻¹

source

@[simp]

theorem norm_zpow {α : Type u_1} [normed_division_ring α] (a : α) (n : ℤ) :

‖a ^ n‖ = ‖a‖ ^ n

source

@[simp]

theorem nnnorm_zpow {α : Type u_1} [normed_division_ring α] (a : α) (n : ℤ) :

‖a ^ n‖₊ = ‖a‖₊ ^ n

source

theorem dist_inv_inv₀ {α : Type u_1} [normed_division_ring α] {z w : α} (hz : z ≠ 0) (hw : w ≠ 0) :

has_dist.dist z⁻¹ w⁻¹ = has_dist.dist z w / (‖z‖ * ‖w‖)

source

theorem nndist_inv_inv₀ {α : Type u_1} [normed_division_ring α] {z w : α} (hz : z ≠ 0) (hw : w ≠ 0) :

has_nndist.nndist z⁻¹ w⁻¹ = has_nndist.nndist z w / (‖z‖₊ * ‖w‖₊)

source

theorem filter.tendsto_mul_left_cobounded {α : Type u_1} [normed_division_ring α] {a : α} (ha : a ≠ 0) :

filter.tendsto (has_mul.mul a) (filter.comap has_norm.norm filter.at_top) (filter.comap has_norm.norm filter.at_top)

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.

source

theorem filter.tendsto_mul_right_cobounded {α : Type u_1} [normed_division_ring α] {a : α} (ha : a ≠ 0) :

filter.tendsto (λ (x : α), x * a) (filter.comap has_norm.norm filter.at_top) (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.

source

@[protected, instance]

def normed_division_ring.to_has_continuous_inv₀ {α : Type u_1} [normed_division_ring α] :

has_continuous_inv₀ α

source

@[protected, instance]

def normed_division_ring.to_topological_division_ring {α : Type u_1} [normed_division_ring α] :

topological_division_ring α

A normed division ring is a topological division ring.

source

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

source

theorem norm_one_of_pow_eq_one {α : Type u_1} [normed_division_ring α] {x : α} {k : ℕ+} (h : x ^ ↑k = 1) :

‖x‖ = 1

source

@[class]

structure normed_field (α : Type u_5) :

Type u_5

to_has_norm : has_norm α
to_field : field α
to_metric_space : metric_space α
dist_eq : ∀ (x y : α), has_dist.dist x y = ‖x - y‖
norm_mul' : ∀ (a b : α), ‖a * b‖ = ‖a‖ * ‖b‖

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

source

@[class]

structure nontrivially_normed_field (α : Type u_5) :

Type u_5

to_normed_field : normed_field α
non_trivial : ∃ (x : α), 1 < ‖x‖

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

densely_normed_field.to_nontrivially_normed_field

Instances of other typeclasses for nontrivially_normed_field

nontrivially_normed_field.has_sizeof_inst

source

@[class]

structure densely_normed_field (α : Type u_5) :

Type u_5

to_normed_field : normed_field α
lt_norm_lt : ∀ (x y : ℝ), 0 ≤ x → x < y → (∃ (a : α), x < ‖a‖ ∧ ‖a‖ < y)

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

source

@[protected, instance]

def densely_normed_field.to_nontrivially_normed_field {α : Type u_1} [densely_normed_field α] :

nontrivially_normed_field α

A densely normed field is always a nontrivially normed field. See note [lower instance priority].

Equations

densely_normed_field.to_nontrivially_normed_field = {to_normed_field := densely_normed_field.to_normed_field _inst_1, non_trivial := _}

source

@[protected, instance]

def normed_field.to_normed_division_ring {α : Type u_1} [normed_field α] :

normed_division_ring α

Equations

normed_field.to_normed_division_ring = {to_has_norm := normed_field.to_has_norm _inst_1, to_division_ring := {add := field.add normed_field.to_field, add_assoc := _, zero := field.zero normed_field.to_field, zero_add := _, add_zero := _, nsmul := field.nsmul normed_field.to_field, nsmul_zero' := _, nsmul_succ' := _, neg := field.neg normed_field.to_field, sub := field.sub normed_field.to_field, sub_eq_add_neg := _, zsmul := field.zsmul normed_field.to_field, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := field.int_cast normed_field.to_field, nat_cast := field.nat_cast normed_field.to_field, one := field.one normed_field.to_field, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := field.mul normed_field.to_field, mul_assoc := _, one_mul := _, mul_one := _, npow := field.npow normed_field.to_field, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, inv := field.inv normed_field.to_field, div := field.div normed_field.to_field, div_eq_mul_inv := _, zpow := field.zpow normed_field.to_field, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, rat_cast := field.rat_cast normed_field.to_field, mul_inv_cancel := _, inv_zero := _, rat_cast_mk := _, qsmul := field.qsmul normed_field.to_field, qsmul_eq_mul' := _}, to_metric_space := normed_field.to_metric_space _inst_1, dist_eq := _, norm_mul' := _}

source

@[protected, instance]

def normed_field.to_normed_comm_ring {α : Type u_1} [normed_field α] :

normed_comm_ring α

Equations

normed_field.to_normed_comm_ring = {to_normed_ring := {to_has_norm := normed_field.to_has_norm _inst_1, to_ring := {add := field.add normed_field.to_field, add_assoc := _, zero := field.zero normed_field.to_field, zero_add := _, add_zero := _, nsmul := field.nsmul normed_field.to_field, nsmul_zero' := _, nsmul_succ' := _, neg := field.neg normed_field.to_field, sub := field.sub normed_field.to_field, sub_eq_add_neg := _, zsmul := field.zsmul normed_field.to_field, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := field.int_cast normed_field.to_field, nat_cast := field.nat_cast normed_field.to_field, one := field.one normed_field.to_field, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := field.mul normed_field.to_field, mul_assoc := _, one_mul := _, mul_one := _, npow := field.npow normed_field.to_field, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _}, to_metric_space := normed_field.to_metric_space _inst_1, dist_eq := _, norm_mul := _}, mul_comm := _}

source

@[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‖)

source

@[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‖₊)

source

theorem normed_field.exists_one_lt_norm (α : Type u_1) [nontrivially_normed_field α] :

∃ (x : α), 1 < ‖x‖

source

theorem normed_field.exists_lt_norm (α : Type u_1) [nontrivially_normed_field α] (r : ℝ) :

∃ (x : α), r < ‖x‖

source

theorem normed_field.exists_norm_lt (α : Type u_1) [nontrivially_normed_field α] {r : ℝ} (hr : 0 < r) :

∃ (x : α), 0 < ‖x‖ ∧ ‖x‖ < r

source

theorem normed_field.exists_norm_lt_one (α : Type u_1) [nontrivially_normed_field α] :

∃ (x : α), 0 < ‖x‖ ∧ ‖x‖ < 1

source

@[instance]

theorem normed_field.punctured_nhds_ne_bot {α : Type u_1} [nontrivially_normed_field α] (x : α) :

(nhds_within x {x}ᶜ).ne_bot

source

@[instance]

theorem normed_field.nhds_within_is_unit_ne_bot {α : Type u_1} [nontrivially_normed_field α] :

(nhds_within 0 {x : α | is_unit x}).ne_bot

source

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₂

source

theorem normed_field.exists_lt_nnnorm_lt (α : Type u_1) [densely_normed_field α] {r₁ r₂ : nnreal} (h : r₁ < r₂) :

∃ (x : α), r₁ < ‖x‖₊ ∧ ‖x‖₊ < r₂

source

@[protected, instance]

def normed_field.densely_ordered_range_norm (α : Type u_1) [densely_normed_field α] :

densely_ordered ↥(set.range has_norm.norm)

source

@[protected, instance]

def normed_field.densely_ordered_range_nnnorm (α : Type u_1) [densely_normed_field α] :

densely_ordered ↥(set.range has_nnnorm.nnnorm)

source

theorem normed_field.dense_range_nnnorm (α : Type u_1) [densely_normed_field α] :

dense_range has_nnnorm.nnnorm

source

@[protected, instance]

def real.normed_comm_ring :

normed_comm_ring ℝ

Equations

real.normed_comm_ring = {to_normed_ring := {to_has_norm := normed_add_comm_group.to_has_norm real.normed_add_comm_group, to_ring := {add := add_comm_group.add normed_add_comm_group.to_add_comm_group, add_assoc := real.normed_comm_ring._proof_1, zero := add_comm_group.zero normed_add_comm_group.to_add_comm_group, zero_add := real.normed_comm_ring._proof_2, add_zero := real.normed_comm_ring._proof_3, nsmul := add_comm_group.nsmul normed_add_comm_group.to_add_comm_group, nsmul_zero' := real.normed_comm_ring._proof_4, nsmul_succ' := real.normed_comm_ring._proof_5, neg := add_comm_group.neg normed_add_comm_group.to_add_comm_group, sub := add_comm_group.sub normed_add_comm_group.to_add_comm_group, sub_eq_add_neg := real.normed_comm_ring._proof_6, zsmul := add_comm_group.zsmul normed_add_comm_group.to_add_comm_group, zsmul_zero' := real.normed_comm_ring._proof_7, zsmul_succ' := real.normed_comm_ring._proof_8, zsmul_neg' := real.normed_comm_ring._proof_9, add_left_neg := real.normed_comm_ring._proof_10, add_comm := real.normed_comm_ring._proof_11, int_cast := comm_ring.int_cast real.comm_ring, nat_cast := comm_ring.nat_cast real.comm_ring, one := comm_ring.one real.comm_ring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := comm_ring.mul real.comm_ring, mul_assoc := _, one_mul := _, mul_one := _, npow := comm_ring.npow real.comm_ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _}, to_metric_space := normed_add_comm_group.to_metric_space real.normed_add_comm_group, dist_eq := _, norm_mul := real.normed_comm_ring._proof_12}, mul_comm := _}

source

@[protected, instance]

noncomputable def real.normed_field :

normed_field ℝ

Equations

real.normed_field = {to_has_norm := normed_add_comm_group.to_has_norm real.normed_add_comm_group, to_field := real.field, to_metric_space := normed_add_comm_group.to_metric_space real.normed_add_comm_group, dist_eq := _, norm_mul' := _}

source

@[protected, instance]

noncomputable def real.densely_normed_field :

densely_normed_field ℝ

Equations

real.densely_normed_field = {to_normed_field := real.normed_field, lt_norm_lt := real.densely_normed_field._proof_1}

source

theorem real.to_nnreal_mul_nnnorm {x : ℝ} (y : ℝ) (hx : 0 ≤ x) :

x.to_nnreal * ‖y‖₊ = ‖x * y‖₊

source

theorem real.nnnorm_mul_to_nnreal (x : ℝ) {y : ℝ} (hy : 0 ≤ y) :

‖x‖₊ * y.to_nnreal = ‖x * y‖₊

source

@[simp]

theorem nnreal.norm_eq (x : nnreal) :

‖↑x‖ = ↑x

source

@[simp]

theorem nnreal.nnnorm_eq (x : nnreal) :

‖↑x‖₊ = x

source

@[simp]

theorem norm_norm {α : Type u_1} [seminormed_add_comm_group α] (x : α) :

‖‖x‖‖ = ‖x‖

source

@[simp]

theorem nnnorm_norm {α : Type u_1} [seminormed_add_comm_group α] (a : α) :

‖‖a‖‖₊ = ‖a‖₊

source

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.

source

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, ...

source

@[protected, instance]

def int.normed_comm_ring :

normed_comm_ring ℤ

Equations

int.normed_comm_ring = {to_normed_ring := {to_has_norm := normed_add_comm_group.to_has_norm int.normed_add_comm_group, to_ring := int.ring, to_metric_space := normed_add_comm_group.to_metric_space int.normed_add_comm_group, dist_eq := _, norm_mul := int.normed_comm_ring._proof_1}, mul_comm := _}

source

@[protected, instance]

def int.norm_one_class :

norm_one_class ℤ

source

@[protected, instance]

def rat.normed_field :

normed_field ℚ

Equations

rat.normed_field = {to_has_norm := normed_add_comm_group.to_has_norm rat.normed_add_comm_group, to_field := rat.field, to_metric_space := normed_add_comm_group.to_metric_space rat.normed_add_comm_group, dist_eq := _, norm_mul' := rat.normed_field._proof_1}

source

@[protected, instance]

def rat.densely_normed_field :

densely_normed_field ℚ

Equations

rat.densely_normed_field = {to_normed_field := rat.normed_field, lt_norm_lt := rat.densely_normed_field._proof_1}

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

is_iso : ∀ {x : R₁}, ‖⇑σ x‖ = ‖x‖

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

source

@[protected, instance]

def ring_hom_isometric.ids {R₁ : Type u_5} [semi_normed_ring R₁] :

ring_hom_isometric (ring_hom.id R₁)

source

@[reducible]

def non_unital_semi_normed_ring.induced {F : Type u_5} (R : Type u_6) (S : Type u_7) [non_unital_ring R] [non_unital_semi_normed_ring S] [non_unital_ring_hom_class F R S] (f : F) :

non_unital_semi_normed_ring R

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

See note [reducible non-instances]

Equations

non_unital_semi_normed_ring.induced R S f = {to_has_norm := seminormed_add_comm_group.to_has_norm (seminormed_add_comm_group.induced R S f), to_non_unital_ring := _inst_1, to_pseudo_metric_space := seminormed_add_comm_group.to_pseudo_metric_space (seminormed_add_comm_group.induced R S f), dist_eq := _, norm_mul := _}

source

@[reducible]

def non_unital_normed_ring.induced {F : Type u_5} (R : Type u_6) (S : Type u_7) [non_unital_ring R] [non_unital_normed_ring S] [non_unital_ring_hom_class F R S] (f : F) (hf : function.injective ⇑f) :

non_unital_normed_ring R

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

See note [reducible non-instances]

Equations

non_unital_normed_ring.induced R S f hf = {to_has_norm := non_unital_semi_normed_ring.to_has_norm (non_unital_semi_normed_ring.induced R S f), to_non_unital_ring := non_unital_semi_normed_ring.to_non_unital_ring (non_unital_semi_normed_ring.induced R S f), to_metric_space := normed_add_comm_group.to_metric_space (normed_add_comm_group.induced R S f hf), dist_eq := _, norm_mul := _}

source

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

semi_normed_ring R

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

semi_normed_ring.induced R S f = {to_has_norm := non_unital_semi_normed_ring.to_has_norm (non_unital_semi_normed_ring.induced R S f), to_ring := _inst_1, to_pseudo_metric_space := non_unital_semi_normed_ring.to_pseudo_metric_space (non_unital_semi_normed_ring.induced R S f), dist_eq := _, norm_mul := _}

source

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

normed_ring R

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

normed_ring.induced R S f hf = {to_has_norm := non_unital_semi_normed_ring.to_has_norm (non_unital_semi_normed_ring.induced R S f), to_ring := _inst_1, to_metric_space := normed_add_comm_group.to_metric_space (normed_add_comm_group.induced R S f hf), dist_eq := _, norm_mul := _}

source

@[reducible]

def semi_normed_comm_ring.induced {F : Type u_5} (R : Type u_6) (S : Type u_7) [comm_ring R] [semi_normed_ring S] [non_unital_ring_hom_class F R S] (f : F) :

semi_normed_comm_ring R

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

See note [reducible non-instances]

Equations

semi_normed_comm_ring.induced R S f = {to_semi_normed_ring := {to_has_norm := non_unital_semi_normed_ring.to_has_norm (non_unital_semi_normed_ring.induced R S f), to_ring := comm_ring.to_ring R _inst_1, to_pseudo_metric_space := non_unital_semi_normed_ring.to_pseudo_metric_space (non_unital_semi_normed_ring.induced R S f), dist_eq := _, norm_mul := _}, mul_comm := _}

source

@[reducible]

def normed_comm_ring.induced {F : Type u_5} (R : Type u_6) (S : Type u_7) [comm_ring R] [normed_ring S] [non_unital_ring_hom_class F R S] (f : F) (hf : function.injective ⇑f) :

normed_comm_ring R

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

See note [reducible non-instances]

Equations

normed_comm_ring.induced R S f hf = {to_normed_ring := {to_has_norm := semi_normed_ring.to_has_norm semi_normed_comm_ring.to_semi_normed_ring, to_ring := semi_normed_ring.to_ring semi_normed_comm_ring.to_semi_normed_ring, to_metric_space := normed_add_comm_group.to_metric_space (normed_add_comm_group.induced R S f hf), dist_eq := _, norm_mul := _}, mul_comm := _}

source

@[reducible]

def normed_division_ring.induced {F : Type u_5} (R : Type u_6) (S : Type u_7) [division_ring R] [normed_division_ring S] [non_unital_ring_hom_class F R S] (f : F) (hf : function.injective ⇑f) :

normed_division_ring R

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

normed_division_ring.induced R S f hf = {to_has_norm := normed_add_comm_group.to_has_norm (normed_add_comm_group.induced R S f hf), to_division_ring := _inst_1, to_metric_space := normed_add_comm_group.to_metric_space (normed_add_comm_group.induced R S f hf), dist_eq := _, norm_mul' := _}

source

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

normed_field R

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

normed_field.induced R S f hf = {to_has_norm := normed_division_ring.to_has_norm (normed_division_ring.induced R S f hf), to_field := _inst_1, to_metric_space := normed_division_ring.to_metric_space (normed_division_ring.induced R S f hf), dist_eq := _, norm_mul' := _}

source

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) :

norm_one_class R

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.

source

@[protected, instance]