Seminorms #
This file defines seminorms.
A seminorm is a function to the reals which is positive-semidefinite, absolutely homogeneous, and subadditive. They are closely related to convex sets and a topological vector space is locally convex if and only if its topology is induced by a family of seminorms.
Main declarations #
For a module over a normed ring:
seminorm
: A function to the reals that is positive-semidefinite, absolutely homogeneous, and subadditive.norm_seminorm 𝕜 E
: The norm onE
as a seminorm.
References #
Tags #
seminorm, locally convex, LCTVS
- to_fun : E → ℝ
- map_zero' : self.to_fun 0 = 0
- add_le' : ∀ (r s : E), self.to_fun (r + s) ≤ self.to_fun r + self.to_fun s
- neg' : ∀ (r : E), self.to_fun (-r) = self.to_fun r
- smul' : ∀ (a : 𝕜) (x : E), self.to_fun (a • x) = ∥a∥ * self.to_fun x
A seminorm on a module over a normed ring is a function to the reals that is positive semidefinite, positive homogeneous, and subadditive.
Instances for seminorm
- seminorm.has_sizeof_inst
- seminorm.zero_hom_class
- seminorm.has_coe_to_fun
- seminorm.has_zero
- seminorm.inhabited
- seminorm.has_smul
- seminorm.is_scalar_tower
- seminorm.has_add
- seminorm.add_monoid
- seminorm.ordered_cancel_add_comm_monoid
- seminorm.mul_action
- seminorm.distrib_mul_action
- seminorm.module
- seminorm.has_sup
- seminorm.partial_order
- seminorm.semilattice_sup
- seminorm.order_bot
- seminorm.has_inf
- seminorm.lattice
Alternative constructor for a seminorm
on an add_comm_group E
that is a module over a
semi_norm_ring 𝕜
.
Alternative constructor for a seminorm
over a normed field 𝕜
that only assumes f 0 = 0
and an inequality for the scalar multiplication.
Equations
- seminorm.of_smul_le f map_zero add_le smul_le = seminorm.of f add_le _
Equations
- seminorm.zero_hom_class = {coe := λ (f : seminorm 𝕜 E), f.to_fun, coe_injective' := _, map_zero := _}
Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun
.
Equations
- seminorm.inhabited = {default := 0}
Any action on ℝ
which factors through ℝ≥0
applies to a seminorm.
Equations
- seminorm.add_monoid = function.injective.add_monoid coe_fn seminorm.add_monoid._proof_2 seminorm.add_monoid._proof_3 seminorm.coe_add seminorm.add_monoid._proof_4
Equations
- seminorm.ordered_cancel_add_comm_monoid = function.injective.ordered_cancel_add_comm_monoid coe_fn seminorm.ordered_cancel_add_comm_monoid._proof_2 seminorm.ordered_cancel_add_comm_monoid._proof_3 seminorm.coe_add seminorm.ordered_cancel_add_comm_monoid._proof_4
Equations
- seminorm.mul_action = function.injective.mul_action coe_fn seminorm.mul_action._proof_1 seminorm.mul_action._proof_2
coe_fn
as an add_monoid_hom
. Helper definition for showing that seminorm 𝕜 E
is
a module.
Equations
- seminorm.coe_fn_add_monoid_hom 𝕜 E = {to_fun := coe_fn seminorm.has_coe_to_fun, map_zero' := _, map_add' := _}
Equations
- seminorm.distrib_mul_action = function.injective.distrib_mul_action (seminorm.coe_fn_add_monoid_hom 𝕜 E) _ seminorm.distrib_mul_action._proof_1
Equations
- seminorm.module = function.injective.module R (seminorm.coe_fn_add_monoid_hom 𝕜 E) _ seminorm.module._proof_1
Equations
- seminorm.partial_order = partial_order.lift coe_fn seminorm.partial_order._proof_1
Equations
- seminorm.semilattice_sup = function.injective.semilattice_sup coe_fn seminorm.semilattice_sup._proof_1 seminorm.coe_sup
Composition of a seminorm with a linear map is a seminorm.
The composition as an add_monoid_hom
.
The direct path from 0 to y is shorter than the path with x "inserted" in between.
The direct path from 0 to x is shorter than the path with y "inserted" in between.
Equations
- seminorm.order_bot = {bot := 0, bot_le := _}
Equations
- seminorm.lattice = {sup := semilattice_sup.sup seminorm.semilattice_sup, le := semilattice_sup.le seminorm.semilattice_sup, lt := semilattice_sup.lt seminorm.semilattice_sup, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := has_inf.inf seminorm.has_inf, inf_le_left := _, inf_le_right := _, le_inf := _}
Seminorm ball #
The ball of radius r
at x
with respect to seminorm p
is the set of elements y
with
p (y - x) <
r`.
Seminorm-balls at the origin are balanced.
Seminorm-balls at the origin are absorbent.
Seminorm-balls containing the origin are absorbent.
A seminorm is convex. Also see convex_on_norm
.
Seminorm-balls are convex.
The norm as a seminorm #
The norm of a seminormed group as a seminorm.
Equations
- norm_seminorm 𝕜 E = {to_fun := (norm_add_group_seminorm E).to_fun, map_zero' := _, add_le' := _, neg' := _, smul' := _}
Balls at the origin are absorbent.
Balls containing the origin are absorbent.
Balls at the origin are balanced.