Normed (semi)groups #
In this file we define four classes:
has_norm
,has_nnnorm
: auxiliary classes endowing a typeα
with a functionnorm : α → ℝ
(notation:∥x∥
) andnnnorm : α → ℝ≥0
(notation:∥x∥₊
), respectively;semi_normed_group
: a seminormed group is an additive group with a norm and a pseudo metric space structures that agree with each other:∀ x y, dist x y = ∥x - y∥
;normed_group
: a normed group is an additive group with a norm and a metric space structures that agree with each other:∀ x y, dist x y = ∥x - y∥
.
We also prove basic properties of (semi)normed groups and provide some instances.
Tags #
normed group
- norm : E → ℝ
Auxiliary class, endowing a type E
with a function norm : E → ℝ
with notation ∥x∥
. This
class is designed to be extended in more interesting classes specifying the properties of the norm.
Instances of this typeclass
- semi_normed_group.to_has_norm
- normed_group.to_has_norm
- non_unital_semi_normed_ring.to_has_norm
- semi_normed_ring.to_has_norm
- non_unital_normed_ring.to_has_norm
- normed_ring.to_has_norm
- normed_division_ring.to_has_norm
- normed_field.to_has_norm
- normed_linear_ordered_group.to_has_norm
- normed_linear_ordered_field.to_has_norm
- continuous_linear_map.has_op_norm
- normed_group_hom.has_op_norm
- complex.has_norm
- continuous_multilinear_map.has_op_norm
- continuous_multilinear_map.has_op_norm'
- bounded_continuous_function.has_norm
- continuous_map.has_norm
- measure_theory.Lp.has_norm
- continuous_affine_map.has_norm
- uniform_space.completion.has_norm
- lp.has_norm
- norm_on_quotient
- padic.has_norm
- padic_int.has_norm
Instances of other typeclasses for has_norm
- has_norm.has_sizeof_inst
- to_has_norm : has_norm E
- to_add_comm_group : add_comm_group E
- to_pseudo_metric_space : pseudo_metric_space E
- dist_eq : ∀ (x y : E), has_dist.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 of this typeclass
- normed_group.to_semi_normed_group
- non_unital_semi_normed_ring.to_semi_normed_group
- add_subgroup.semi_normed_group
- submodule.semi_normed_group
- ulift.semi_normed_group
- prod.semi_normed_group
- pi.semi_normed_group
- restrict_scalars.semi_normed_group
- continuous_linear_map.to_semi_normed_group
- normed_group_hom.to_semi_normed_group
- normed_space.dual.semi_normed_group
- bounded_continuous_function.semi_normed_group
- pi_Lp.semi_normed_group
- SemiNormedGroup.semi_normed_group
- SemiNormedGroup₁.semi_normed_group
- add_subgroup.semi_normed_group_quotient
Instances of other typeclasses for semi_normed_group
- semi_normed_group.has_sizeof_inst
- to_has_norm : has_norm E
- to_add_comm_group : add_comm_group E
- to_metric_space : metric_space E
- dist_eq : ∀ (x y : E), has_dist.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 of this typeclass
- non_unital_normed_ring.to_normed_group
- normed_linear_ordered_group.to_normed_group
- inner_product_space.to_normed_group
- normed_lattice_add_comm_group.to_normed_group
- order_dual.normed_group
- punit.normed_group
- real.normed_group
- add_subgroup.normed_group
- submodule.normed_group
- ulift.normed_group
- prod.normed_group
- pi.normed_group
- restrict_scalars.normed_group
- continuous_linear_map.to_normed_group
- normed_group_hom.to_normed_group
- complex.normed_group
- continuous_multilinear_map.normed_group
- continuous_multilinear_map.normed_group'
- normed_space.dual.normed_group
- bounded_continuous_function.normed_group
- continuous_map.normed_group
- measure_theory.Lp.normed_group
- continuous_affine_map.normed_group
- pi_Lp.normed_group
- uniform_space.completion.normed_group
- lp.normed_group
- add_subgroup.normed_group_quotient
- enorm.finite_subspace.normed_group
- zero_at_infty_continuous_map.normed_group
Instances of other typeclasses for normed_group
- normed_group.has_sizeof_inst
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. Note that in most
cases this instance creates bad definitional equalities (e.g., it does not take into account
a possibly existing uniform_space
instance on E
).
Equations
- semi_normed_group.of_core E C = {to_has_norm := _inst_2, to_add_comm_group := _inst_1, to_pseudo_metric_space := {to_has_dist := {dist := λ (x y : E), ∥x - y∥}, dist_self := _, dist_comm := _, dist_triangle := _, edist := λ (x y : E), ↑⟨(λ (x y : E), ∥x - y∥) x y, _⟩, edist_dist := _, to_uniform_space := uniform_space_of_dist (λ (x y : E), ∥x - y∥) _ _ _, uniformity_dist := _, to_bornology := bornology.of_dist (λ (x y : E), ∥x - y∥) _ _ _, cobounded_sets := _}, dist_eq := _}
Equations
- punit.normed_group = {to_has_norm := {norm := function.const punit 0}, to_add_comm_group := punit.add_comm_group, to_metric_space := punit.metric_space, dist_eq := punit.normed_group._proof_1}
Equations
- real.normed_group = {to_has_norm := {norm := λ (x : ℝ), |x|}, to_add_comm_group := real.add_comm_group, to_metric_space := real.metric_space, dist_eq := real.normed_group._proof_1}
In a (semi)normed group, negation x ↦ -x
tends to infinity at infinity. TODO: use
bornology.cobounded
instead of filter.comap has_norm.norm filter.at_top
.
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, _⟩}
Addition y ↦ y + x
as an isometry
.
Equations
- isometric.add_right x = {to_equiv := {to_fun := (equiv.add_right x).to_fun, inv_fun := (equiv.add_right x).inv_fun, left_inv := _, right_inv := _}, isometry_to_fun := _}
Addition y ↦ x + y
as an isometry
.
Equations
- isometric.add_left x = {to_equiv := equiv.add_left x, isometry_to_fun := _}
Negation x ↦ -x
as an isometry
.
Equations
- isometric.neg E = {to_equiv := equiv.neg E (subtraction_monoid.to_has_involutive_neg E), isometry_to_fun := _}
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
.
Alias of the forward direction of lipschitz_with_iff_norm_sub_le`.
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
.
- nnnorm : E → nnreal
Auxiliary class, endowing a type α
with a function nnnorm : α → ℝ≥0
with notation ∥x∥₊
.
Instances of this typeclass
Instances of other typeclasses for has_nnnorm
- has_nnnorm.has_sizeof_inst
A group homomorphism from an add_comm_group
to a semi_normed_group
induces a
semi_normed_group
structure on the domain.
See note [reducible non-instances]
Equations
- semi_normed_group.induced f = {to_has_norm := {norm := λ (x : E), ∥⇑f x∥}, to_add_comm_group := _inst_4, to_pseudo_metric_space := {to_has_dist := pseudo_metric_space.to_has_dist (pseudo_metric_space.induced ⇑f semi_normed_group.to_pseudo_metric_space), dist_self := _, dist_comm := _, dist_triangle := _, edist := pseudo_metric_space.edist (pseudo_metric_space.induced ⇑f semi_normed_group.to_pseudo_metric_space), edist_dist := _, to_uniform_space := pseudo_metric_space.to_uniform_space (pseudo_metric_space.induced ⇑f semi_normed_group.to_pseudo_metric_space), uniformity_dist := _, to_bornology := pseudo_metric_space.to_bornology (pseudo_metric_space.induced ⇑f semi_normed_group.to_pseudo_metric_space), cobounded_sets := _}, dist_eq := _}
A subgroup of a seminormed group is also a seminormed group, with the restriction of the norm.
Equations
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
.
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
.
This is a reversed version of the simp
lemma add_subgroup.coe_norm
for use by norm_cast
.
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.pseudo_metric_space (λ (x : E), x ∈ s), dist_eq := _}
If x
is an element of a submodule s
of a normed group E
, its norm in s
is equal to its
norm in E
.
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
.
This is a reversed version of the simp
lemma submodule.coe_norm
for use by norm_cast
.
Equations
- ulift.semi_normed_group = semi_normed_group.induced {to_fun := ulift.down E, map_zero' := _, map_add' := _}
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 : ι), ∥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 := _}
The $L^1$ norm is less than the $L^\infty$ norm scaled by the cardinality.
The $L^1$ norm is less than the $L^\infty$ norm scaled by the cardinality.
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.order
, 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
.
A helper lemma used to prove that the (scalar or usual) product of a function that tends to zero
and a bounded function tends to zero. This lemma is formulated for any binary operation
op : E → F → G
with an estimate ∥op x y∥ ≤ A * ∥x∥ * ∥y∥
for some constant A instead of
multiplication so that it can be applied to (*)
, flip (*)
, (•)
, and flip (•)
.
A helper lemma used to prove that the (scalar or usual) product of a function that tends to zero
and a bounded function tends to zero. This lemma is formulated for any binary operation
op : E → F → G
with an estimate ∥op x y∥ ≤ ∥x∥ * ∥y∥
instead of multiplication so that it
can be applied to (*)
, flip (*)
, (•)
, and flip (•)
.
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 E C = {to_has_norm := semi_normed_group.to_has_norm (semi_normed_group.of_core E _), to_add_comm_group := semi_normed_group.to_add_comm_group (semi_normed_group.of_core E _), to_metric_space := {to_pseudo_metric_space := semi_normed_group.to_pseudo_metric_space (semi_normed_group.of_core E _), eq_of_dist_eq_zero := _}, dist_eq := _}
An injective group homomorphism from an add_comm_group
to a normed_group
induces a
normed_group
structure on the domain.
See note [reducible non-instances].
Equations
- normed_group.induced f h = {to_has_norm := semi_normed_group.to_has_norm (semi_normed_group.induced f), to_add_comm_group := semi_normed_group.to_add_comm_group (semi_normed_group.induced f), to_metric_space := {to_pseudo_metric_space := semi_normed_group.to_pseudo_metric_space (semi_normed_group.induced f), eq_of_dist_eq_zero := _}, dist_eq := _}
A subgroup of a normed group is also a normed group, with the restriction of the norm.
Equations
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.
Some relations with has_compact_support
Alias of the reverse direction of has_compact_support_norm_iff`.