mathlib documentation

analysis.normed_space.basic

Normed spaces

@[class]
structure has_norm  :
Type u_5Type u_5
  • norm : α →

Auxiliary class, endowing a type α with a function norm : α → ℝ. This class is designed to be extended in more interesting classes specifying the properties of the norm.

Instances
@[class]
structure normed_group  :
Type u_5Type u_5

A normed group is an additive group endowed with a norm for which dist x y = ∥x - y∥ defines a metric space structure.

Instances
def normed_group.of_add_dist {α : Type u_1} [has_norm α] [add_comm_group α] [metric_space α] :
(∀ (x : α), x = dist x 0)(∀ (x y z : α), dist x y dist (x + z) (y + z))normed_group α

Construct a normed group from a translation invariant distance

Equations
def normed_group.of_add_dist' {α : Type u_1} [has_norm α] [add_comm_group α] [metric_space α] :
(∀ (x : α), x = dist x 0)(∀ (x y z : α), dist (x + z) (y + z) dist x y)normed_group α

Construct a normed group from a translation invariant distance

Equations
structure normed_group.core (α : Type u_5) [add_comm_group α] [has_norm α] :
Prop

A normed group can be built from a norm that satisfies algebraic properties. This is formalised in this structure.

def normed_group.of_core (α : Type u_1) [add_comm_group α] [has_norm α] :

Constructing a normed group from core properties of a norm, i.e., registering the distance and the metric space structure from the norm properties.

Equations
theorem dist_eq_norm {α : Type u_1} [normed_group α] (g h : α) :
dist g h = g - h

@[simp]
theorem dist_zero_right {α : Type u_1} [normed_group α] (g : α) :

theorem norm_sub_rev {α : Type u_1} [normed_group α] (g h : α) :
g - h = h - g

@[simp]
theorem norm_neg {α : Type u_1} [normed_group α] (g : α) :

@[simp]
theorem dist_add_left {α : Type u_1} [normed_group α] (g h₁ h₂ : α) :
dist (g + h₁) (g + h₂) = dist h₁ h₂

@[simp]
theorem dist_add_right {α : Type u_1} [normed_group α] (g₁ g₂ h : α) :
dist (g₁ + h) (g₂ + h) = dist g₁ g₂

@[simp]
theorem dist_neg_neg {α : Type u_1} [normed_group α] (g h : α) :
dist (-g) (-h) = dist g h

@[simp]
theorem dist_sub_left {α : Type u_1} [normed_group α] (g h₁ h₂ : α) :
dist (g - h₁) (g - h₂) = dist h₁ h₂

@[simp]
theorem dist_sub_right {α : Type u_1} [normed_group α] (g₁ g₂ h : α) :
dist (g₁ - h) (g₂ - h) = dist g₁ g₂

theorem norm_add_le {α : Type u_1} [normed_group α] (g h : α) :

Triangle inequality for the norm.

theorem norm_add_le_of_le {α : Type u_1} [normed_group α] {g₁ g₂ : α} {n₁ n₂ : } :
g₁ n₁g₂ n₂g₁ + g₂ n₁ + n₂

theorem dist_add_add_le {α : Type u_1} [normed_group α] (g₁ g₂ h₁ h₂ : α) :
dist (g₁ + g₂) (h₁ + h₂) dist g₁ h₁ + dist g₂ h₂

theorem dist_add_add_le_of_le {α : Type u_1} [normed_group α] {g₁ g₂ h₁ h₂ : α} {d₁ d₂ : } :
dist g₁ h₁ d₁dist g₂ h₂ d₂dist (g₁ + g₂) (h₁ + h₂) d₁ + d₂

theorem dist_sub_sub_le {α : Type u_1} [normed_group α] (g₁ g₂ h₁ h₂ : α) :
dist (g₁ - g₂) (h₁ - h₂) dist g₁ h₁ + dist g₂ h₂

theorem dist_sub_sub_le_of_le {α : Type u_1} [normed_group α] {g₁ g₂ h₁ h₂ : α} {d₁ d₂ : } :
dist g₁ h₁ d₁dist g₂ h₂ d₂dist (g₁ - g₂) (h₁ - h₂) d₁ + d₂

theorem abs_dist_sub_le_dist_add_add {α : Type u_1} [normed_group α] (g₁ g₂ h₁ h₂ : α) :
abs (dist g₁ h₁ - dist g₂ h₂) dist (g₁ + g₂) (h₁ + h₂)

@[simp]
theorem norm_nonneg {α : Type u_1} [normed_group α] (g : α) :

@[simp]
theorem norm_eq_zero {α : Type u_1} [normed_group α] {g : α} :
g = 0 g = 0

@[simp]
theorem norm_zero {α : Type u_1} [normed_group α] :

theorem norm_of_subsingleton {α : Type u_1} [normed_group α] [subsingleton α] (x : α) :

theorem norm_sum_le {α : Type u_1} [normed_group α] {β : Type u_2} (s : finset β) (f : β → α) :
∑ (a : β) in s, f a ∑ (a : β) in s, f a

theorem norm_sum_le_of_le {α : Type u_1} [normed_group α] {β : Type u_2} (s : finset β) {f : β → α} {n : β → } :
(∀ (b : β), b sf b n b)∑ (b : β) in s, f b ∑ (b : β) in s, n b

@[simp]
theorem norm_pos_iff {α : Type u_1} [normed_group α] {g : α} :
0 < g g 0

@[simp]
theorem norm_le_zero_iff {α : Type u_1} [normed_group α] {g : α} :
g 0 g = 0

theorem norm_sub_le {α : Type u_1} [normed_group α] (g h : α) :

theorem norm_sub_le_of_le {α : Type u_1} [normed_group α] {g₁ g₂ : α} {n₁ n₂ : } :
g₁ n₁g₂ n₂g₁ - g₂ n₁ + n₂

theorem dist_le_norm_add_norm {α : Type u_1} [normed_group α] (g h : α) :

theorem abs_norm_sub_norm_le {α : Type u_1} [normed_group α] (g h : α) :

theorem norm_sub_norm_le {α : Type u_1} [normed_group α] (g h : α) :

theorem dist_norm_norm_le {α : Type u_1} [normed_group α] (g h : α) :

theorem eq_of_norm_sub_eq_zero {α : Type u_1} [normed_group α] {u v : α} :
u - v = 0u = v

theorem norm_le_insert {α : Type u_1} [normed_group α] (u v : α) :

theorem ball_0_eq {α : Type u_1} [normed_group α] (ε : ) :
metric.ball 0 ε = {x : α | x < ε}

theorem norm_le_of_mem_closed_ball {α : Type u_1} [normed_group α] {g h : α} {r : } :

theorem norm_lt_of_mem_ball {α : Type u_1} [normed_group α] {g h : α} {r : } :
h metric.ball g rh < g + r

theorem normed_group.tendsto_nhds_zero {α : Type u_1} {γ : Type u_3} [normed_group α] {f : γ → α} {l : filter γ} :
filter.tendsto f l (𝓝 0) ∀ (ε : ), ε > 0(∀ᶠ (x : γ) in l, f x < ε)

theorem normed_group.tendsto_nhds_nhds {α : Type u_1} {β : Type u_2} [normed_group α] [normed_group β] {f : α → β} {x : α} {y : β} :
filter.tendsto f (𝓝 x) (𝓝 y) ∀ (ε : ), ε > 0(∃ (δ : ) (H : δ > 0), ∀ (x' : α), x' - x < δf x' - y < ε)

theorem add_monoid_hom.lipschitz_of_bound {α : Type u_1} {β : Type u_2} [normed_group α] [normed_group β] (f : α →+ β) (C : ) :
(∀ (x : α), f x C * x)lipschitz_with (nnreal.of_real C) f

A homomorphism f of normed groups is Lipschitz, if there exists a constant C such that for all x, one has ∥f x∥ ≤ C * ∥x∥. The analogous condition for a linear map of normed spaces is in normed_space.operator_norm.

theorem lipschitz_on_with_iff_norm_sub_le {α : Type u_1} {β : Type u_2} [normed_group α] [normed_group β] {f : α → β} {C : ℝ≥0} {s : set α} :
lipschitz_on_with C f s ∀ (x : α), x s∀ (y : α), y sf x - f y (C) * x - y

theorem lipschitz_on_with.norm_sub_le {α : Type u_1} {β : Type u_2} [normed_group α] [normed_group β] {f : α → β} {C : ℝ≥0} {s : set α} (h : lipschitz_on_with C f s) {x y : α} :
x sy sf x - f y (C) * x - y

theorem add_monoid_hom.continuous_of_bound {α : Type u_1} {β : Type u_2} [normed_group α] [normed_group β] (f : α →+ β) (C : ) :
(∀ (x : α), f x C * x)continuous f

A homomorphism f of normed groups is continuous, if there exists a constant C such that for all x, one has ∥f x∥ ≤ C * ∥x∥. The analogous condition for a linear map of normed spaces is in normed_space.operator_norm.

def nnnorm {α : Type u_1} [normed_group α] :
α → ℝ≥0

Version of the norm taking values in nonnegative reals.

Equations
@[simp]
theorem coe_nnnorm {α : Type u_1} [normed_group α] (a : α) :

theorem nndist_eq_nnnorm {α : Type u_1} [normed_group α] (a b : α) :
nndist a b = nnnorm (a - b)

@[simp]
theorem nnnorm_eq_zero {α : Type u_1} [normed_group α] {a : α} :
nnnorm a = 0 a = 0

@[simp]
theorem nnnorm_zero {α : Type u_1} [normed_group α] :
nnnorm 0 = 0

theorem nnnorm_add_le {α : Type u_1} [normed_group α] (g h : α) :

@[simp]
theorem nnnorm_neg {α : Type u_1} [normed_group α] (g : α) :

theorem nndist_nnnorm_nnnorm_le {α : Type u_1} [normed_group α] (g h : α) :
nndist (nnnorm g) (nnnorm h) nnnorm (g - h)

theorem of_real_norm_eq_coe_nnnorm {β : Type u_2} [normed_group β] (x : β) :

theorem edist_eq_coe_nnnorm_sub {β : Type u_2} [normed_group β] (x y : β) :
edist x y = (nnnorm (x - y))

theorem edist_eq_coe_nnnorm {β : Type u_2} [normed_group β] (x : β) :
edist x 0 = (nnnorm x)

theorem nndist_add_add_le {α : Type u_1} [normed_group α] (g₁ g₂ h₁ h₂ : α) :
nndist (g₁ + g₂) (h₁ + h₂) nndist g₁ h₁ + nndist g₂ h₂

theorem edist_add_add_le {α : Type u_1} [normed_group α] (g₁ g₂ h₁ h₂ : α) :
edist (g₁ + g₂) (h₁ + h₂) edist g₁ h₁ + edist g₂ h₂

theorem nnnorm_sum_le {α : Type u_1} [normed_group α] {β : Type u_2} (s : finset β) (f : β → α) :
nnnorm (∑ (a : β) in s, f a) ∑ (a : β) in s, nnnorm (f a)

theorem lipschitz_with.neg {β : Type u_2} [normed_group β] {α : Type u_1} [emetric_space α] {K : ℝ≥0} {f : α → β} :
lipschitz_with K flipschitz_with K (λ (x : α), -f x)

theorem lipschitz_with.add {β : Type u_2} [normed_group β] {α : Type u_1} [emetric_space α] {Kf : ℝ≥0} {f : α → β} (hf : lipschitz_with Kf f) {Kg : ℝ≥0} {g : α → β} :
lipschitz_with Kg glipschitz_with (Kf + Kg) (λ (x : α), f x + g x)

theorem lipschitz_with.sub {β : Type u_2} [normed_group β] {α : Type u_1} [emetric_space α] {Kf : ℝ≥0} {f : α → β} (hf : lipschitz_with Kf f) {Kg : ℝ≥0} {g : α → β} :
lipschitz_with Kg glipschitz_with (Kf + Kg) (λ (x : α), f x - g x)

theorem antilipschitz_with.add_lipschitz_with {β : Type u_2} [normed_group β] {α : Type u_1} [metric_space α] {Kf : ℝ≥0} {f : α → β} (hf : antilipschitz_with Kf f) {Kg : ℝ≥0} {g : α → β} :
lipschitz_with Kg gKg < Kf⁻¹antilipschitz_with (Kf⁻¹ - Kg)⁻¹ (λ (x : α), f x + g x)

@[instance]
def submodule.normed_group {𝕜 : Type u_1} {_x : ring 𝕜} {E : Type u_2} [normed_group E] {_x_1 : module 𝕜 E} (s : submodule 𝕜 E) :

A submodule of a normed group is also a normed group, with the restriction of the norm. As all instances can be inferred from the submodule s, they are put as implicit instead of typeclasses.

Equations
@[instance]
def prod.normed_group {α : Type u_1} {β : Type u_2} [normed_group α] [normed_group β] :

normed group instance on the product of two normed groups, using the sup norm.

Equations
theorem prod.norm_def {α : Type u_1} {β : Type u_2} [normed_group α] [normed_group β] (x : α × β) :

theorem prod.nnnorm_def {α : Type u_1} {β : Type u_2} [normed_group α] [normed_group β] (x : α × β) :

theorem norm_fst_le {α : Type u_1} {β : Type u_2} [normed_group α] [normed_group β] (x : α × β) :

theorem norm_snd_le {α : Type u_1} {β : Type u_2} [normed_group α] [normed_group β] (x : α × β) :

theorem norm_prod_le_iff {α : Type u_1} {β : Type u_2} [normed_group α] [normed_group β] {x : α × β} {r : } :

@[instance]
def pi.normed_group {ι : Type u_4} {π : ι → Type u_1} [fintype ι] [Π (i : ι), normed_group («π» i)] :
normed_group (Π (i : ι), «π» i)

normed group instance on the product of finitely many normed groups, using the sup norm.

Equations
theorem pi_norm_le_iff {ι : Type u_4} {π : ι → Type u_1} [fintype ι] [Π (i : ι), normed_group («π» i)] {r : } (hr : 0 r) {x : Π (i : ι), «π» i} :
x r ∀ (i : ι), x i r

The norm of an element in a product space is ≤ r if and only if the norm of each component is.

theorem norm_le_pi_norm {ι : Type u_4} {π : ι → Type u_1} [fintype ι] [Π (i : ι), normed_group («π» i)] (x : Π (i : ι), «π» i) (i : ι) :

theorem tendsto_iff_norm_tendsto_zero {β : Type u_2} {ι : Type u_4} [normed_group β] {f : ι → β} {a : filter ι} {b : β} :
filter.tendsto f a (𝓝 b) filter.tendsto (λ (e : ι), f e - b) a (𝓝 0)

theorem tendsto_zero_iff_norm_tendsto_zero {β : Type u_2} {γ : Type u_3} [normed_group β] {f : γ → β} {a : filter γ} :
filter.tendsto f a (𝓝 0) filter.tendsto (λ (e : γ), f e) a (𝓝 0)

theorem squeeze_zero_norm' {α : Type u_1} {γ : Type u_3} [normed_group α] {f : γ → α} {g : γ → } {t₀ : filter γ} :
(∀ᶠ (n : γ) in t₀, f n g n)filter.tendsto g t₀ (𝓝 0)filter.tendsto f t₀ (𝓝 0)

Special case of the sandwich theorem: if the norm of f is eventually bounded by a real function g which tends to 0, then f tends to 0. In this pair of lemmas (squeeze_zero_norm' and squeeze_zero_norm), following a convention of similar lemmas in topology.metric_space.basic and topology.algebra.ordered, the ' version is phrased using "eventually" and the non-' version is phrased absolutely.

theorem squeeze_zero_norm {α : Type u_1} {γ : Type u_3} [normed_group α] {f : γ → α} {g : γ → } {t₀ : filter γ} :
(∀ (n : γ), f n g n)filter.tendsto g t₀ (𝓝 0)filter.tendsto f t₀ (𝓝 0)

Special case of the sandwich theorem: if the norm of f is bounded by a real function g which tends to 0, then f tends to 0.

theorem lim_norm {α : Type u_1} [normed_group α] (x : α) :
filter.tendsto (λ (g : α), g - x) (𝓝 x) (𝓝 0)

theorem lim_norm_zero {α : Type u_1} [normed_group α] :
filter.tendsto (λ (g : α), g) (𝓝 0) (𝓝 0)

theorem continuous_norm {α : Type u_1} [normed_group α] :
continuous (λ (g : α), g)

theorem filter.tendsto.norm {α : Type u_1} [normed_group α] {β : Type u_2} {l : filter β} {f : β → α} {a : α} :
filter.tendsto f l (𝓝 a)filter.tendsto (λ (x : β), f x) l (𝓝 a)

theorem continuous.norm {α : Type u_1} {γ : Type u_3} [normed_group α] [topological_space γ] {f : γ → α} :
continuous fcontinuous (λ (x : γ), f x)

theorem continuous_nnnorm {α : Type u_1} [normed_group α] :

theorem filter.tendsto.nnnorm {α : Type u_1} [normed_group α] {β : Type u_2} {l : filter β} {f : β → α} {a : α} :
filter.tendsto f l (𝓝 a)filter.tendsto (λ (x : β), nnnorm (f x)) l (𝓝 (nnnorm a))

theorem eventually_ne_of_tendsto_norm_at_top {α : Type u_1} {γ : Type u_3} [normed_group α] {l : filter γ} {f : γ → α} (h : filter.tendsto (λ (y : γ), f y) l filter.at_top) (x : α) :
∀ᶠ (y : γ) in l, f y x

If ∥y∥→∞, then we can assume y≠x for any fixed x.

@[instance]
def normed_uniform_group {α : Type u_1} [normed_group α] :

A normed group is a uniform additive group, i.e., addition and subtraction are uniformly continuous.

@[instance]
def normed_top_monoid {α : Type u_1} [normed_group α] :

@[instance]
def normed_top_group {α : Type u_1} [normed_group α] :

@[class]
structure normed_ring  :
Type u_5Type u_5

A normed ring is a ring endowed with a norm which satisfies the inequality ∥x y∥ ≤ ∥x∥ ∥y∥.

Instances
@[class]
structure normed_comm_ring  :
Type u_5Type 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
@[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
@[simp]
theorem nnnorm_one {α : Type u_1} [normed_group α] [has_one α] [norm_one_class α] :
nnnorm 1 = 1

@[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 β] :

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

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

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

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

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

theorem norm_pow_le' {α : Type u_1} [normed_ring α] (a : α) {n : } :
0 < na ^ n a ^ n

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

theorem norm_pow_le {α : Type u_1} [normed_ring α] [norm_one_class α] (a : α) (n : ) :

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

theorem eventually_norm_pow_le {α : Type u_1} [normed_ring α] (a : α) :
∀ᶠ (n : ) in filter.at_top, a ^ n a ^ n

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

theorem mul_left_bound {α : Type u_1} [normed_ring α] (x y : α) :

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

theorem mul_right_bound {α : Type u_1} [normed_ring α] (x y : α) :

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

@[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
@[instance]
def normed_ring_top_monoid {α : Type u_1} [normed_ring α] :

@[instance]
def normed_top_ring {α : Type u_1} [normed_ring α] :

A normed ring is a topological ring.

@[class]
structure normed_field  :
Type u_5Type u_5

A normed field is a field with a norm satisfying ∥x y∥ = ∥x∥ ∥y∥.

Instances
@[class]
structure nondiscrete_normed_field  :
Type u_5Type 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
@[simp]
theorem normed_field.norm_mul {α : Type u_1} [normed_field α] (a b : α) :

@[instance]

@[simp]
theorem normed_field.norm_hom_to_fun {α : Type u_1} [normed_field α] (a : α) :

@[simp]
theorem normed_field.norm_pow {α : Type u_1} [normed_field α] (a : α) (n : ) :
a ^ n = a ^ n

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

@[simp]
theorem normed_field.norm_div {α : Type u_1} [normed_field α] (a b : α) :

@[simp]
theorem normed_field.norm_inv {α : Type u_1} [normed_field α] (a : α) :

@[simp]
theorem normed_field.nnnorm_inv {α : Type u_1} [normed_field α] (a : α) :

@[simp]
theorem normed_field.norm_fpow {α : Type u_1} [normed_field α] (a : α) (n : ) :
a ^ n = a ^ n

theorem normed_field.tendsto_inv {α : Type u_1} [normed_field α] {r : α} :
r 0filter.tendsto (λ (q : α), q⁻¹) (𝓝 r) (𝓝 r⁻¹)

theorem normed_field.continuous_on_inv {α : Type u_1} [normed_field α] :
continuous_on (λ (x : α), x⁻¹) {x : α | x 0}

theorem normed_field.exists_one_lt_norm (α : Type u_1) [nondiscrete_normed_field α] :
∃ (x : α), 1 < x

theorem normed_field.exists_norm_lt_one (α : Type u_1) [nondiscrete_normed_field α] :
∃ (x : α), 0 < x x < 1

theorem normed_field.exists_lt_norm (α : Type u_1) [nondiscrete_normed_field α] (r : ) :
∃ (x : α), r < x

theorem normed_field.exists_norm_lt (α : Type u_1) [nondiscrete_normed_field α] {r : } :
0 < r(∃ (x : α), 0 < x x < r)

@[instance]
theorem normed_field.punctured_nhds_ne_bot {α : Type u_1} [nondiscrete_normed_field α] (x : α) :

@[instance]

@[instance]

Equations
theorem filter.tendsto.inv' {α : Type u_1} {β : Type u_2} [normed_field α] {l : filter β} {f : β → α} {y : α} :
y 0filter.tendsto f l (𝓝 y)filter.tendsto (λ (x : β), (f x)⁻¹) l (𝓝 y⁻¹)

If a function converges to a nonzero value, its inverse converges to the inverse of this value. We use the name tendsto.inv' as tendsto.inv is already used in multiplicative topological groups.

theorem continuous_at.inv' {α : Type u_1} {β : Type u_2} [topological_space α] [normed_field β] {f : α → β} {x : α} :
continuous_at f xf x 0continuous_at (λ (x : α), (f x)⁻¹) x

theorem continuous_within_at.inv' {α : Type u_1} {β : Type u_2} [topological_space α] [normed_field β] {f : α → β} {x : α} {s : set α} :
continuous_within_at f s xf x 0continuous_within_at (λ (x : α), (f x)⁻¹) s x

theorem continuous.inv' {α : Type u_1} {β : Type u_2} [topological_space α] [normed_field β] {f : α → β} :
continuous f(∀ (x : α), f x 0)continuous (λ (x : α), (f x)⁻¹)

theorem continuous_on.inv' {α : Type u_1} {β : Type u_2} [topological_space α] [normed_field β] {f : α → β} {s : set α} :
continuous_on f s(∀ (x : α), x sf x 0)continuous_on (λ (x : α), (f x)⁻¹) s

theorem filter.tendsto.div_const {α : Type u_1} {β : Type u_2} [normed_field α] {l : filter β} {f : β → α} {x y : α} :
filter.tendsto f l (𝓝 x)filter.tendsto (λ (a : β), f a / y) l (𝓝 (x / y))

theorem filter.tendsto.div {α : Type u_1} {β : Type u_2} [normed_field α] {l : filter β} {f g : β → α} {x y : α} :
filter.tendsto f l (𝓝 x)filter.tendsto g l (𝓝 y)y 0filter.tendsto (λ (a : β), f a / g a) l (𝓝 (x / y))

theorem continuous_within_at.div {α : Type u_1} {β : Type u_2} [topological_space α] [normed_field β] {f g : α → β} {s : set α} {x : α} :
continuous_within_at f s xcontinuous_within_at g s xg x 0continuous_within_at (λ (x : α), f x / g x) s x

theorem continuous_on.div {α : Type u_1} {β : Type u_2} [topological_space α] [normed_field β] {f g : α → β} {s : set α} :
continuous_on f scontinuous_on g s(∀ (x : α), x sg x 0)continuous_on (λ (x : α), f x / g x) s

theorem continuous_at.div {α : Type u_1} {β : Type u_2} [topological_space α] [normed_field β] {f g : α → β} {x : α} :
continuous_at f xcontinuous_at g xg x 0continuous_at (λ (x : α), f x / g x) x

Continuity at a point of the result of dividing two functions continuous at that point, where the denominator is nonzero.

theorem continuous.div {α : Type u_1} {β : Type u_2} [topological_space α] [normed_field β] {f g : α → β} :
continuous fcontinuous g(∀ (x : α), g x 0)continuous (λ (x : α), f x / g x)

theorem real.norm_eq_abs (r : ) :

theorem real.norm_of_nonneg {x : } :
0 xx = x

@[simp]
theorem real.norm_coe_nat (n : ) :

@[simp]
theorem real.nnnorm_coe_nat (n : ) :

@[simp]
theorem real.norm_two  :

@[simp]
theorem real.nnnorm_two  :
nnnorm 2 = 2

@[simp]

theorem real.nnnorm_of_nonneg {x : } (hx : 0 x) :
nnnorm x = x, hx⟩

@[simp]
theorem norm_norm {α : Type u_1} [normed_group α] (x : α) :

@[simp]
theorem nnnorm_norm {α : Type u_1} [normed_group α] (a : α) :

@[instance]

Equations
@[instance]

Equations
@[simp]
theorem rat.norm_cast_real (r : ) :

@[simp]
theorem int.norm_cast_rat (m : ) :

@[class]
structure normed_space (α : Type u_5) (β : Type u_6) [normed_field α] [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.

Instances
theorem norm_smul {α : Type u_1} {β : Type u_2} [normed_field α] [normed_group β] [normed_space α β] (s : α) (x : β) :

@[simp]
theorem abs_norm_eq_norm {β : Type u_2} [normed_group β] (z : β) :

theorem dist_smul {α : Type u_1} {β : Type u_2} [normed_field α] [normed_group β] [normed_space α β] (s : α) (x y : β) :
dist (s x) (s y) = s * dist x y

theorem nnnorm_smul {α : Type u_1} {β : Type u_2} [normed_field α] [normed_group β] [normed_space α β] (s : α) (x : β) :
nnnorm (s x) = (nnnorm s) * nnnorm x

theorem nndist_smul {α : Type u_1} {β : Type u_2} [normed_field α] [normed_group β] [normed_space α β] (s : α) (x y : β) :
nndist (s x) (s y) = (nnnorm s) * nndist x y

theorem norm_smul_of_nonneg {β : Type u_2} [normed_group β] [normed_space β] {t : } (ht : 0 t) (x : β) :

@[instance]
def normed_space.topological_vector_space {α : Type u_1} [normed_field α] {E : Type u_5} [normed_group E] [normed_space α E] :

theorem closure_ball {E : Type u_5} [normed_group E] [normed_space E] (x : E) {r : } :

theorem frontier_ball {E : Type u_5} [normed_group E] [normed_space E] (x : E) {r : } :

theorem interior_closed_ball {E : Type u_5} [normed_group E] [normed_space E] (x : E) {r : } :

theorem interior_closed_ball' {E : Type u_5} [normed_group E] [normed_space E] [nontrivial E] (x : E) (r : ) :

theorem frontier_closed_ball {E : Type u_5} [normed_group E] [normed_space E] (x : E) {r : } :

theorem frontier_closed_ball' {E : Type u_5} [normed_group E] [normed_space E] [nontrivial E] (x : E) (r : ) :

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} :
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.

@[instance]
def prod.normed_space {α : Type u_1} [normed_field α] {E : Type u_5} {F : Type u_6} [normed_group E] [normed_space α E] [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
@[instance]
def pi.normed_space {α : Type u_1} {ι : Type u_4} [normed_field α] {E : ι → Type u_2} [fintype ι] [Π (i : ι), 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
@[instance]
def submodule.normed_space {𝕜 : Type u_1} [normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] (s : submodule 𝕜 E) :

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

Equations
@[class]
structure normed_algebra (𝕜 : Type u_5) (𝕜' : Type u_6) [normed_field 𝕜] [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
@[simp]
theorem norm_algebra_map_eq {𝕜 : Type u_1} (𝕜' : Type u_2) [normed_field 𝕜] [normed_ring 𝕜'] [h : normed_algebra 𝕜 𝕜'] (x : 𝕜) :
(algebra_map 𝕜 𝕜') x = x

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

Equations
@[simp]
theorem normed_algebra.norm_one (𝕜 : Type u_5) [normed_field 𝕜] {𝕜' : Type u_6} [normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] :

theorem normed_algebra.norm_one_class (𝕜 : Type u_5) [normed_field 𝕜] {𝕜' : Type u_6} [normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] :

theorem normed_algebra.zero_ne_one (𝕜 : Type u_5) [normed_field 𝕜] {𝕜' : Type u_6} [normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] :
0 1

theorem normed_algebra.nontrivial (𝕜 : Type u_5) [normed_field 𝕜] {𝕜' : Type u_6} [normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] :

def normed_space.restrict_scalars (𝕜 : Type u_5) (𝕜' : Type u_6) [normed_field 𝕜] [normed_field 𝕜'] [normed_algebra 𝕜 𝕜'] (E : Type u_7) [normed_group 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 semimodule.restrict_scalars 𝕜 𝕜' E will be endowed with this instance by default.

Equations
@[instance]
def restrict_scalars.normed_group {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [I : normed_group E] :

Equations
@[instance]
def semimodule.restrict_scalars.normed_space_orig {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [normed_field 𝕜'] [normed_group E] [I : normed_space 𝕜' E] :
normed_space 𝕜' (restrict_scalars 𝕜 𝕜' E)

Equations
@[instance]
def restrict_scalars.normed_space (𝕜 : Type u_5) (𝕜' : Type u_6) [normed_field 𝕜] [normed_field 𝕜'] [normed_algebra 𝕜 𝕜'] (E : Type u_7) [normed_group E] [normed_space 𝕜' E] :
normed_space 𝕜 (restrict_scalars 𝕜 𝕜' E)

Equations
theorem cauchy_seq_finset_iff_vanishing_norm {α : Type u_1} {ι : Type u_4} [normed_group α] {f : ι → α} :
cauchy_seq (λ (s : finset ι), ∑ (i : ι) in s, f i) ∀ (ε : ), ε > 0(∃ (s : finset ι), ∀ (t : finset ι), disjoint t s∑ (i : ι) in t, f i < ε)

theorem summable_iff_vanishing_norm {α : Type u_1} {ι : Type u_4} [normed_group α] [complete_space α] {f : ι → α} :
summable f ∀ (ε : ), ε > 0(∃ (s : finset ι), ∀ (t : finset ι), disjoint t s∑ (i : ι) in t, f i < ε)

theorem cauchy_seq_finset_of_norm_bounded {α : Type u_1} {ι : Type u_4} [normed_group α] {f : ι → α} (g : ι → ) :
summable g(∀ (i : ι), f i g i)cauchy_seq (λ (s : finset ι), ∑ (i : ι) in s, f i)

theorem cauchy_seq_finset_of_summable_norm {α : Type u_1} {ι : Type u_4} [normed_group α] {f : ι → α} :
summable (λ (a : ι), f a)cauchy_seq (λ (s : finset ι), ∑ (a : ι) in s, f a)

theorem has_sum_of_subseq_of_summable {α : Type u_1} {γ : Type u_3} {ι : Type u_4} [normed_group α] {f : ι → α} (hf : summable (λ (a : ι), f a)) {s : γ → finset ι} {p : filter γ} [p.ne_bot] (hs : filter.tendsto s p filter.at_top) {a : α} :
filter.tendsto (λ (b : γ), ∑ (i : ι) in s b, f i) p (𝓝 a)has_sum f a

If a function f is summable in norm, and along some sequence of finsets exhausting the space its sum is converging to a limit a, then this holds along all finsets, i.e., f is summable with sum a.

theorem norm_tsum_le_tsum_norm {α : Type u_1} {ι : Type u_4} [normed_group α] {f : ι → α} :
summable (λ (i : ι), f i)((∑' (i : ι), f i) ∑' (i : ι), f i)

If ∑' i, ∥f i∥ is summable, then ∥(∑' i, f i)∥ ≤ (∑' i, ∥f i∥). Note that we do not assume that ∑' i, f i is summable, and it might not be the case if α is not a complete space.

theorem has_sum_iff_tendsto_nat_of_summable_norm {α : Type u_1} [normed_group α] {f : → α} {a : α} :
summable (λ (i : ), f i)(has_sum f a filter.tendsto (λ (n : ), ∑ (i : ) in finset.range n, f i) filter.at_top (𝓝 a))

theorem summable_of_norm_bounded {α : Type u_1} {ι : Type u_4} [normed_group α] [complete_space α] {f : ι → α} (g : ι → ) :
summable g(∀ (i : ι), f i g i)summable f

The direct comparison test for series: if the norm of f is bounded by a real function g which is summable, then f is summable.

theorem tsum_of_norm_bounded {α : Type u_1} {ι : Type u_4} [normed_group α] {f : ι → α} {g : ι → } {a : } :
has_sum g a(∀ (i : ι), f i g i)(∑' (i : ι), f i) a

Quantitative result associated to the direct comparison test for series: If ∑' i, g i is summable, and for all i, ∥f i∥ ≤ g i, then ∥(∑' i, f i)∥ ≤ (∑' i, g i). Note that we do not assume that ∑' i, f i is summable, and it might not be the case if α is not a complete space.

theorem summable_of_norm_bounded_eventually {α : Type u_1} {ι : Type u_4} [normed_group α] [complete_space α] {f : ι → α} (g : ι → ) :
summable g(∀ᶠ (i : ι) in filter.cofinite, f i g i)summable f

Variant of the direct comparison test for series: if the norm of f is eventually bounded by a real function g which is summable, then f is summable.

theorem summable_of_nnnorm_bounded {α : Type u_1} {ι : Type u_4} [normed_group α] [complete_space α] {f : ι → α} (g : ι → ℝ≥0) :
summable g(∀ (i : ι), nnnorm (f i) g i)summable f

theorem summable_of_summable_norm {α : Type u_1} {ι : Type u_4} [normed_group α] [complete_space α] {f : ι → α} :
summable (λ (a : ι), f a)summable f

theorem summable_of_summable_nnnorm {α : Type u_1} {ι : Type u_4} [normed_group α] [complete_space α] {f : ι → α} :
summable (λ (a : ι), nnnorm (f a))summable f