Normed spaces #
Since a lot of elementary properties don't require ∥x∥ = 0 → x = 0
we start setting up the
theory of semi_normed_group
and we specialize to normed_group
at the end.
- 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
- semi_normed_group.to_has_norm
- normed_group.to_has_norm
- semi_normed_ring.to_has_norm
- normed_ring.to_has_norm
- normed_field.to_has_norm
- normed_linear_ordered_group.to_has_norm
- normed_linear_ordered_field.to_has_norm
- normed_group_hom.has_op_norm
- continuous_linear_map.has_op_norm
- continuous_multilinear_map.has_op_norm
- complex.has_norm
- bounded_continuous_function.has_norm
- continuous_map.has_norm
- measure_theory.Lp.has_norm
- padic.has_norm
- padic_int.has_norm
- uniform_space.completion.has_norm
- to_has_norm : has_norm α
- to_add_comm_group : add_comm_group α
- to_pseudo_metric_space : pseudo_metric_space α
- dist_eq : ∀ (x y : α), dist x y = ∥x - y∥
A seminormed group is an additive group endowed with a norm for which dist x y = ∥x - y∥
defines a pseudometric space structure.
Instances
- normed_group.to_semi_normed_group
- semi_normed_ring.to_semi_normed_group
- add_subgroup.semi_normed_group
- submodule.semi_normed_group
- prod.semi_normed_group
- pi.semi_normed_group
- restrict_scalars.semi_normed_group
- normed_group_hom.to_semi_normed_group
- continuous_linear_map.to_semi_normed_group
- pi_Lp.semi_normed_group
- to_has_norm : has_norm α
- to_add_comm_group : add_comm_group α
- to_metric_space : metric_space α
- dist_eq : ∀ (x y : α), dist x y = ∥x - y∥
A normed group is an additive group endowed with a norm for which dist x y = ∥x - y∥
defines
a metric space structure.
Instances
- normed_ring.to_normed_group
- normed_linear_ordered_group.to_normed_group
- inner_product_space.to_normed_group
- real.normed_group
- add_subgroup.normed_group
- submodule.normed_group
- prod.normed_group
- pi.normed_group
- restrict_scalars.normed_group
- normed_group_hom.to_normed_group
- continuous_linear_map.to_normed_group
- continuous_multilinear_map.to_normed_group
- complex.normed_group
- pi_Lp.normed_group
- bounded_continuous_function.normed_group
- continuous_map.normed_group
- measure_theory.Lp.normed_group
- measure_theory.Lp.normed_group_L1
- measure_theory.Lp.normed_group_L2
- measure_theory.Lp.normed_group_Ltop
- normed_space.dual.normed_group
- enorm.finite_subspace.normed_group
- uniform_space.completion.normed_group
A normed group is a seminormed group.
Construct a seminormed group from a translation invariant pseudodistance
Equations
- semi_normed_group.of_add_dist H1 H2 = {to_has_norm := _inst_1, to_add_comm_group := _inst_2, to_pseudo_metric_space := _inst_3, dist_eq := _}
Construct a seminormed group from a translation invariant pseudodistance
Equations
- semi_normed_group.of_add_dist' H1 H2 = {to_has_norm := _inst_1, to_add_comm_group := _inst_2, to_pseudo_metric_space := _inst_3, dist_eq := _}
A seminormed group can be built from a seminorm that satisfies algebraic properties. This is formalised in this structure.
Constructing a seminormed group from core properties of a seminorm, i.e., registering the pseudodistance and the pseudometric space structure from the seminorm properties.
Equations
- semi_normed_group.of_core α C = {to_has_norm := _inst_2, to_add_comm_group := _inst_1, to_pseudo_metric_space := {to_has_dist := {dist := λ (x y : α), ∥x - y∥}, dist_self := _, dist_comm := _, dist_triangle := _, edist := λ (x y : α), ennreal.of_real ((λ (x y : α), ∥x - y∥) x y), edist_dist := _, to_uniform_space := uniform_space_of_dist (λ (x y : α), ∥x - y∥) _ _ _, uniformity_dist := _}, dist_eq := _}
Equations
- real.normed_group = {to_has_norm := {norm := λ (x : ℝ), abs x}, to_add_comm_group := real.add_comm_group, to_metric_space := real.metric_space, dist_eq := real.normed_group._proof_1}
We equip the sphere, in a seminormed group, with a formal operation of negation, namely the antipodal map.
Equations
- metric.sphere.has_neg = {neg := λ (w : ↥(metric.sphere 0 r)), ⟨-↑w, _⟩}
A homomorphism f
of seminormed 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
(semi)normed spaces is in normed_space.operator_norm
.
A homomorphism f
of seminormed 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
.
A subgroup of a seminormed group is also a seminormed group, with the restriction of the norm.
Equations
- s.semi_normed_group = {to_has_norm := {norm := λ (x : ↥s), ∥↑x∥}, to_add_comm_group := s.to_add_comm_group, to_pseudo_metric_space := subtype.psudo_metric_space semi_normed_group.to_pseudo_metric_space, dist_eq := _}
If x
is an element of a subgroup s
of a seminormed group E
, its norm in s
is equal to
its norm in E
.
A submodule of a seminormed group is also a seminormed group, with the restriction of the norm.
See note [implicit instance arguments].
Equations
- s.semi_normed_group = {to_has_norm := {norm := λ (x : ↥s), ∥↑x∥}, to_add_comm_group := s.add_comm_group, to_pseudo_metric_space := subtype.psudo_metric_space semi_normed_group.to_pseudo_metric_space, dist_eq := _}
If x
is an element of a submodule s
of a normed group E
, its norm in E
is equal to its
norm in s
.
seminormed group instance on the product of two seminormed groups, using the sup norm.
Equations
seminormed group instance on the product of finitely many seminormed groups, using the sup norm.
Equations
- pi.semi_normed_group = {to_has_norm := {norm := λ (f : Π (i : ι), «π» i), ↑(finset.univ.sup (λ (b : ι), nnnorm (f b)))}, to_add_comm_group := pi.add_comm_group (λ (i : ι), semi_normed_group.to_add_comm_group), to_pseudo_metric_space := pseudo_metric_space_pi (λ (b : ι), semi_normed_group.to_pseudo_metric_space), dist_eq := _}
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.
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
.
If ∥y∥→∞
, then we can assume y≠x
for any fixed x
.
A seminormed group is a uniform additive group, i.e., addition and subtraction are uniformly continuous.
Construct a normed group from a translation invariant distance
Equations
- normed_group.of_add_dist H1 H2 = {to_has_norm := _inst_1, to_add_comm_group := _inst_2, to_metric_space := _inst_3, dist_eq := _}
The semi_normed_group.core
induced by a normed_group.core
.
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
- normed_group.of_core α C = {to_has_norm := semi_normed_group.to_has_norm (semi_normed_group.of_core α _), to_add_comm_group := semi_normed_group.to_add_comm_group (semi_normed_group.of_core α _), to_metric_space := {to_pseudo_metric_space := semi_normed_group.to_pseudo_metric_space (semi_normed_group.of_core α _), eq_of_dist_eq_zero := _}, dist_eq := _}
A subgroup of a normed group is also a normed group, with the restriction of the norm.
A submodule of a normed group is also a normed group, with the restriction of the norm.
normed group instance on the product of two normed groups, using the sup norm.
normed group instance on the product of finitely many normed groups, using the sup norm.
A normed ring is a seminormed ring.
Equations
- to_semi_normed_ring : semi_normed_ring α
- mul_comm : ∀ (x y : α), x * y = y * x
A seminormed commutative ring is a commutative ring endowed with a seminorm which satisfies
the inequality ∥x y∥ ≤ ∥x∥ ∥y∥
.
- 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∥
.
A normed commutative ring is a seminormed commutative ring.
Equations
- normed_comm_ring.to_semi_normed_comm_ring = {to_semi_normed_ring := {to_has_norm := normed_ring.to_has_norm normed_comm_ring.to_normed_ring, to_ring := normed_ring.to_ring normed_comm_ring.to_normed_ring, to_pseudo_metric_space := metric_space.to_pseudo_metric_space normed_ring.to_metric_space, dist_eq := _, norm_mul := _}, mul_comm := _}
A mixin class with the axiom ∥1∥ = 1
. Many normed_ring
s and all normed_field
s satisfy this
axiom.
Equations
- semi_normed_comm_ring.to_comm_ring = {add := ring.add semi_normed_ring.to_ring, add_assoc := _, zero := ring.zero semi_normed_ring.to_ring, zero_add := _, add_zero := _, nsmul := ring.nsmul semi_normed_ring.to_ring, nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg semi_normed_ring.to_ring, sub := ring.sub semi_normed_ring.to_ring, sub_eq_add_neg := _, add_left_neg := _, add_comm := _, mul := ring.mul semi_normed_ring.to_ring, mul_assoc := _, one := ring.one semi_normed_ring.to_ring, one_mul := _, mul_one := _, npow := ring.npow semi_normed_ring.to_ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _}
Equations
- normed_ring.to_normed_group = {to_has_norm := normed_ring.to_has_norm β, to_add_comm_group := {add := ring.add normed_ring.to_ring, add_assoc := _, zero := ring.zero normed_ring.to_ring, zero_add := _, add_zero := _, nsmul := ring.nsmul normed_ring.to_ring, nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg normed_ring.to_ring, sub := ring.sub normed_ring.to_ring, sub_eq_add_neg := _, add_left_neg := _, add_comm := _}, to_metric_space := normed_ring.to_metric_space β, dist_eq := _}
Equations
- semi_normed_ring.to_semi_normed_group = {to_has_norm := semi_normed_ring.to_has_norm β, to_add_comm_group := {add := ring.add semi_normed_ring.to_ring, add_assoc := _, zero := ring.zero semi_normed_ring.to_ring, zero_add := _, add_zero := _, nsmul := ring.nsmul semi_normed_ring.to_ring, nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg semi_normed_ring.to_ring, sub := ring.sub semi_normed_ring.to_ring, sub_eq_add_neg := _, add_left_neg := _, add_comm := _}, to_pseudo_metric_space := semi_normed_ring.to_pseudo_metric_space β, dist_eq := _}
If α
is a seminormed ring, then ∥a^n∥≤ ∥a∥^n
for n > 0
. See also norm_pow_le
.
If α
is a seminormed ring with ∥1∥=1
, then ∥a^n∥≤ ∥a∥^n
. See also norm_pow_le'
.
In a seminormed ring, the left-multiplication add_monoid_hom
is bounded.
In a seminormed ring, the right-multiplication add_monoid_hom
is bounded.
Seminormed ring structure on the product of two seminormed rings, using the sup norm.
Normed ring structure on the product of two normed rings, using the sup norm.
A seminormed ring is a topological ring.
- to_normed_field : normed_field α
- non_trivial : ∃ (x : α), 1 < ∥x∥
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.
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 := _, add_left_neg := _, add_comm := _, mul := field.mul normed_field.to_field, mul_assoc := _, one := field.one normed_field.to_field, 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 := _}
norm
as a monoid_hom
.
Equations
- normed_field.norm_hom = {to_fun := norm normed_field.to_has_norm, map_zero' := _, map_one' := _, map_mul' := _}
nnnorm
as a monoid_hom
.
Equations
- normed_field.nnnorm_hom = {to_fun := nnnorm semi_normed_ring.to_semi_normed_group, map_zero' := _, map_one' := _, map_mul' := _}
Equations
Equations
Equations
- real.nondiscrete_normed_field = {to_normed_field := real.normed_field, non_trivial := real.nondiscrete_normed_field._proof_1}
A restatement of metric_space.tendsto_at_top
in terms of the norm.
A variant of normed_group.tendsto_at_top
that
uses ∃ N, ∀ n > N, ...
rather than ∃ N, ∀ n ≥ N, ...
Equations
- int.normed_comm_ring = {to_normed_ring := {to_has_norm := {norm := λ (n : ℤ), ∥↑n∥}, to_ring := int.ring, to_metric_space := int.metric_space, dist_eq := int.normed_comm_ring._proof_1, norm_mul := int.normed_comm_ring._proof_2}, mul_comm := _}
Equations
- rat.normed_field = {to_has_norm := {norm := λ (r : ℚ), ∥↑r∥}, to_field := rat.field, to_metric_space := rat.metric_space, dist_eq := rat.normed_field._proof_1, norm_mul' := rat.normed_field._proof_2}
Equations
- rat.nondiscrete_normed_field = {to_normed_field := rat.normed_field, non_trivial := rat.nondiscrete_normed_field._proof_1}
A seminormed space over a normed field is a vector space endowed with a seminorm 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
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
- normed_algebra.to_normed_space
- inner_product_space.to_normed_space
- normed_field.to_normed_space
- prod.normed_space
- pi.normed_space
- submodule.normed_space
- semimodule.restrict_scalars.normed_space_orig
- restrict_scalars.normed_space
- continuous_linear_map.to_normed_space
- continuous_multilinear_map.to_normed_space
- pi_Lp.normed_space
- bounded_continuous_function.normed_space
- continuous_map.normed_space
- measure_theory.Lp.normed_space
- measure_theory.Lp.normed_space_L1
- measure_theory.Lp.normed_space_L2
- measure_theory.Lp.normed_space_Ltop
- normed_space.dual.normed_space
- enorm.finite_subspace.normed_space
A normed space is a seminormed space.
Equations
Equations
The product of two seminormed spaces is a seminormed space, with the sup norm.
Equations
- prod.semi_normed_space = {to_semimodule := {to_distrib_mul_action := semimodule.to_distrib_mul_action prod.semimodule, add_smul := _, zero_smul := _}, norm_smul_le := _}
The product of finitely many seminormed spaces is a seminormed space, with the sup norm.
Equations
- pi.semi_normed_space = {to_semimodule := pi.semimodule ι (λ (i : ι), E i) α (λ (i : ι), semi_normed_space.to_semimodule), norm_smul_le := _}
A subspace of a seminormed space is also a normed space, with the restriction of the norm.
Equations
- s.semi_normed_space = {to_semimodule := s.semimodule' _inst_13, norm_smul_le := _}
If there is a scalar c
with ∥c∥>1
, then any element of with norm different from 0
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.
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.
The product of two normed spaces is a normed space, with the sup norm.
Equations
The product of finitely many normed spaces is a normed space, with the sup norm.
Equations
A subspace of a normed space is also a normed space, with the restriction of the norm.
Equations
A seminormed algebra 𝕜'
over 𝕜
is an algebra endowed with a seminorm for which the
embedding of 𝕜
in 𝕜'
is an isometry.
Instances
A normed algebra 𝕜'
over 𝕜
is an algebra endowed with a norm for which the embedding of
𝕜
in 𝕜'
is an isometry.
A normed algebra is a seminormed algebra.
Equations
- normed_algebra.to_semi_normed_algebra 𝕜 𝕜' = {to_algebra := normed_algebra.to_algebra _inst_3, norm_algebra_map_eq := _}
Equations
Equations
Equations
- normed_algebra.id 𝕜 = {to_algebra := {to_has_scalar := algebra.to_has_scalar (algebra.id 𝕜), to_ring_hom := algebra.to_ring_hom (algebra.id 𝕜), commutes' := _, smul_def' := _}, norm_algebra_map_eq := _}
Warning: This declaration should be used judiciously.
Please consider using is_scalar_tower
instead.
𝕜
-seminormed space structure induced by a 𝕜'
-seminormed space structure when 𝕜'
is a
seminormed 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
- semi_normed_space.restrict_scalars 𝕜 𝕜' F = {to_semimodule := {to_distrib_mul_action := semimodule.to_distrib_mul_action (restrict_scalars.semimodule 𝕜 𝕜' F), add_smul := _, zero_smul := _}, norm_smul_le := _}
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
- normed_space.restrict_scalars 𝕜 𝕜' E = {to_semimodule := {to_distrib_mul_action := semimodule.to_distrib_mul_action (restrict_scalars.semimodule 𝕜 𝕜' E), add_smul := _, zero_smul := _}, norm_smul_le := _}
Equations
Equations
Equations
Equations
Equations
Equations
- restrict_scalars.normed_space 𝕜 𝕜' E = normed_space.restrict_scalars 𝕜 𝕜' E
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
.
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.
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.
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.
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.