mathlib documentation

analysis.seminorm

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:

References #

Tags #

seminorm, locally convex, LCTVS

@[nolint]
def seminorm.to_add_group_seminorm {𝕜 : Type u_8} {E : Type u_9} [semi_normed_ring 𝕜] [add_group E] [has_smul 𝕜 E] (self : seminorm 𝕜 E) :
structure seminorm (𝕜 : Type u_8) (E : Type u_9) [semi_normed_ring 𝕜] [add_group E] [has_smul 𝕜 E] :
Type u_9

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
def seminorm.of {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_comm_group E] [module 𝕜 E] (f : E → ) (add_le : ∀ (x y : E), f (x + y) f x + f y) (smul : ∀ (a : 𝕜) (x : E), f (a x) = a * f x) :
seminorm 𝕜 E

Alternative constructor for a seminorm on an add_comm_group E that is a module over a semi_norm_ring 𝕜.

Equations
def seminorm.of_smul_le {𝕜 : Type u_3} {E : Type u_4} [normed_field 𝕜] [add_comm_group E] [module 𝕜 E] (f : E → ) (map_zero : f 0 = 0) (add_le : ∀ (x y : E), f (x + y) f x + f y) (smul_le : ∀ (r : 𝕜) (x : E), f (r x) r * f x) :
seminorm 𝕜 E

Alternative constructor for a seminorm over a normed field 𝕜 that only assumes f 0 = 0 and an inequality for the scalar multiplication.

Equations
@[protected, instance]
def seminorm.zero_hom_class {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_group E] [has_smul 𝕜 E] :
Equations
@[protected, instance]
def seminorm.has_coe_to_fun {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_group E] [has_smul 𝕜 E] :
has_coe_to_fun (seminorm 𝕜 E) (λ (_x : seminorm 𝕜 E), E → )

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun.

Equations
@[ext]
theorem seminorm.ext {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_group E] [has_smul 𝕜 E] {p q : seminorm 𝕜 E} (h : ∀ (x : E), p x = q x) :
p = q
@[protected, instance]
def seminorm.has_zero {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_group E] [has_smul 𝕜 E] :
Equations
@[simp]
theorem seminorm.coe_zero {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_group E] [has_smul 𝕜 E] :
0 = 0
@[simp]
theorem seminorm.zero_apply {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_group E] [has_smul 𝕜 E] (x : E) :
0 x = 0
@[protected, instance]
def seminorm.inhabited {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_group E] [has_smul 𝕜 E] :
Equations
@[protected]
theorem seminorm.nonneg {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_group E] [has_smul 𝕜 E] (p : seminorm 𝕜 E) (x : E) :
0 p x
@[protected]
theorem seminorm.map_zero {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_group E] [has_smul 𝕜 E] (p : seminorm 𝕜 E) :
p 0 = 0
@[protected]
theorem seminorm.smul {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_group E] [has_smul 𝕜 E] (p : seminorm 𝕜 E) (c : 𝕜) (x : E) :
p (c x) = c * p x
@[protected]
theorem seminorm.add_le {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_group E] [has_smul 𝕜 E] (p : seminorm 𝕜 E) (x y : E) :
p (x + y) p x + p y
@[protected, instance]
def seminorm.has_smul {R : Type u_1} {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_group E] [has_smul 𝕜 E] [has_smul R ] [has_smul R nnreal] [is_scalar_tower R nnreal ] :
has_smul R (seminorm 𝕜 E)

Any action on which factors through ℝ≥0 applies to a seminorm.

Equations
@[protected, instance]
def seminorm.is_scalar_tower {R : Type u_1} {R' : Type u_2} {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_group E] [has_smul 𝕜 E] [has_smul R ] [has_smul R nnreal] [is_scalar_tower R nnreal ] [has_smul R' ] [has_smul R' nnreal] [is_scalar_tower R' nnreal ] [has_smul R R'] [is_scalar_tower R R' ] :
theorem seminorm.coe_smul {R : Type u_1} {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_group E] [has_smul 𝕜 E] [has_smul R ] [has_smul R nnreal] [is_scalar_tower R nnreal ] (r : R) (p : seminorm 𝕜 E) :
(r p) = r p
@[simp]
theorem seminorm.smul_apply {R : Type u_1} {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_group E] [has_smul 𝕜 E] [has_smul R ] [has_smul R nnreal] [is_scalar_tower R nnreal ] (r : R) (p : seminorm 𝕜 E) (x : E) :
(r p) x = r p x
@[protected, instance]
def seminorm.has_add {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_group E] [has_smul 𝕜 E] :
has_add (seminorm 𝕜 E)
Equations
theorem seminorm.coe_add {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_group E] [has_smul 𝕜 E] (p q : seminorm 𝕜 E) :
(p + q) = p + q
@[simp]
theorem seminorm.add_apply {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_group E] [has_smul 𝕜 E] (p q : seminorm 𝕜 E) (x : E) :
(p + q) x = p x + q x
@[protected, instance]
def seminorm.add_monoid {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_group E] [has_smul 𝕜 E] :
Equations
@[protected, instance]
def seminorm.ordered_cancel_add_comm_monoid {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_group E] [has_smul 𝕜 E] :
Equations
@[protected, instance]
def seminorm.mul_action {R : Type u_1} {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_group E] [has_smul 𝕜 E] [monoid R] [mul_action R ] [has_smul R nnreal] [is_scalar_tower R nnreal ] :
mul_action R (seminorm 𝕜 E)
Equations
def seminorm.coe_fn_add_monoid_hom (𝕜 : Type u_3) (E : Type u_4) [semi_normed_ring 𝕜] [add_group E] [has_smul 𝕜 E] :
seminorm 𝕜 E →+ E →

coe_fn as an add_monoid_hom. Helper definition for showing that seminorm 𝕜 E is a module.

Equations
@[simp]
theorem seminorm.coe_fn_add_monoid_hom_apply (𝕜 : Type u_3) (E : Type u_4) [semi_normed_ring 𝕜] [add_group E] [has_smul 𝕜 E] (x : seminorm 𝕜 E) (ᾰ : E) :
@[protected, instance]
def seminorm.distrib_mul_action {R : Type u_1} {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_group E] [has_smul 𝕜 E] [monoid R] [distrib_mul_action R ] [has_smul R nnreal] [is_scalar_tower R nnreal ] :
Equations
@[protected, instance]
def seminorm.module {R : Type u_1} {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_group E] [has_smul 𝕜 E] [semiring R] [module R ] [has_smul R nnreal] [is_scalar_tower R nnreal ] :
module R (seminorm 𝕜 E)
Equations
@[protected, instance]
noncomputable def seminorm.has_sup {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_group E] [has_smul 𝕜 E] :
has_sup (seminorm 𝕜 E)
Equations
@[simp]
theorem seminorm.coe_sup {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_group E] [has_smul 𝕜 E] (p q : seminorm 𝕜 E) :
(p q) = p q
theorem seminorm.sup_apply {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_group E] [has_smul 𝕜 E] (p q : seminorm 𝕜 E) (x : E) :
(p q) x = p x q x
theorem seminorm.smul_sup {R : Type u_1} {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_group E] [has_smul 𝕜 E] [has_smul R ] [has_smul R nnreal] [is_scalar_tower R nnreal ] (r : R) (p q : seminorm 𝕜 E) :
r (p q) = r p r q
@[protected, instance]
def seminorm.partial_order {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_group E] [has_smul 𝕜 E] :
Equations
theorem seminorm.le_def {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_group E] [has_smul 𝕜 E] (p q : seminorm 𝕜 E) :
p q p q
theorem seminorm.lt_def {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_group E] [has_smul 𝕜 E] (p q : seminorm 𝕜 E) :
p < q p < q
@[protected, instance]
noncomputable def seminorm.semilattice_sup {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_group E] [has_smul 𝕜 E] :
Equations
def seminorm.comp {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [semi_normed_ring 𝕜] [add_comm_group E] [add_comm_group F] [module 𝕜 E] [module 𝕜 F] (p : seminorm 𝕜 F) (f : E →ₗ[𝕜] F) :
seminorm 𝕜 E

Composition of a seminorm with a linear map is a seminorm.

Equations
theorem seminorm.coe_comp {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [semi_normed_ring 𝕜] [add_comm_group E] [add_comm_group F] [module 𝕜 E] [module 𝕜 F] (p : seminorm 𝕜 F) (f : E →ₗ[𝕜] F) :
(p.comp f) = p f
@[simp]
theorem seminorm.comp_apply {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [semi_normed_ring 𝕜] [add_comm_group E] [add_comm_group F] [module 𝕜 E] [module 𝕜 F] (p : seminorm 𝕜 F) (f : E →ₗ[𝕜] F) (x : E) :
(p.comp f) x = p (f x)
@[simp]
theorem seminorm.comp_id {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_comm_group E] [module 𝕜 E] (p : seminorm 𝕜 E) :
@[simp]
theorem seminorm.comp_zero {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [semi_normed_ring 𝕜] [add_comm_group E] [add_comm_group F] [module 𝕜 E] [module 𝕜 F] (p : seminorm 𝕜 F) :
p.comp 0 = 0
@[simp]
theorem seminorm.zero_comp {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [semi_normed_ring 𝕜] [add_comm_group E] [add_comm_group F] [module 𝕜 E] [module 𝕜 F] (f : E →ₗ[𝕜] F) :
0.comp f = 0
theorem seminorm.comp_comp {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} [semi_normed_ring 𝕜] [add_comm_group E] [add_comm_group F] [add_comm_group G] [module 𝕜 E] [module 𝕜 F] [module 𝕜 G] (p : seminorm 𝕜 G) (g : F →ₗ[𝕜] G) (f : E →ₗ[𝕜] F) :
p.comp (g.comp f) = (p.comp g).comp f
theorem seminorm.add_comp {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [semi_normed_ring 𝕜] [add_comm_group E] [add_comm_group F] [module 𝕜 E] [module 𝕜 F] (p q : seminorm 𝕜 F) (f : E →ₗ[𝕜] F) :
(p + q).comp f = p.comp f + q.comp f
theorem seminorm.comp_add_le {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [semi_normed_ring 𝕜] [add_comm_group E] [add_comm_group F] [module 𝕜 E] [module 𝕜 F] (p : seminorm 𝕜 F) (f g : E →ₗ[𝕜] F) :
p.comp (f + g) p.comp f + p.comp g
theorem seminorm.smul_comp {R : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [semi_normed_ring 𝕜] [add_comm_group E] [add_comm_group F] [module 𝕜 E] [module 𝕜 F] [has_smul R ] [has_smul R nnreal] [is_scalar_tower R nnreal ] (p : seminorm 𝕜 F) (f : E →ₗ[𝕜] F) (c : R) :
(c p).comp f = c p.comp f
theorem seminorm.comp_mono {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [semi_normed_ring 𝕜] [add_comm_group E] [add_comm_group F] [module 𝕜 E] [module 𝕜 F] {p q : seminorm 𝕜 F} (f : E →ₗ[𝕜] F) (hp : p q) :
p.comp f q.comp f
def seminorm.pullback {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [semi_normed_ring 𝕜] [add_comm_group E] [add_comm_group F] [module 𝕜 E] [module 𝕜 F] (f : E →ₗ[𝕜] F) :
seminorm 𝕜 F →+ seminorm 𝕜 E

The composition as an add_monoid_hom.

Equations
@[simp]
theorem seminorm.pullback_apply {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [semi_normed_ring 𝕜] [add_comm_group E] [add_comm_group F] [module 𝕜 E] [module 𝕜 F] (f : E →ₗ[𝕜] F) (p : seminorm 𝕜 F) :
@[protected, simp]
theorem seminorm.neg {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_comm_group E] [module 𝕜 E] (p : seminorm 𝕜 E) (x : E) :
p (-x) = p x
@[protected]
theorem seminorm.sub_le {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_comm_group E] [module 𝕜 E] (p : seminorm 𝕜 E) (x y : E) :
p (x - y) p x + p y
theorem seminorm.sub_rev {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_comm_group E] [module 𝕜 E] (p : seminorm 𝕜 E) (x y : E) :
p (x - y) = p (y - x)
theorem seminorm.le_insert {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_comm_group E] [module 𝕜 E] (p : seminorm 𝕜 E) (x y : E) :
p y p x + p (x - y)

The direct path from 0 to y is shorter than the path with x "inserted" in between.

theorem seminorm.le_insert' {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_comm_group E] [module 𝕜 E] (p : seminorm 𝕜 E) (x y : E) :
p x p y + p (x - y)

The direct path from 0 to x is shorter than the path with y "inserted" in between.

@[protected, instance]
def seminorm.order_bot {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_comm_group E] [module 𝕜 E] :
Equations
@[simp]
theorem seminorm.coe_bot {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_comm_group E] [module 𝕜 E] :
theorem seminorm.bot_eq_zero {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_comm_group E] [module 𝕜 E] :
= 0
theorem seminorm.smul_le_smul {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_comm_group E] [module 𝕜 E] {p q : seminorm 𝕜 E} {a b : nnreal} (hpq : p q) (hab : a b) :
a p b q
theorem seminorm.finset_sup_apply {𝕜 : Type u_3} {E : Type u_4} {ι : Type u_7} [semi_normed_ring 𝕜] [add_comm_group E] [module 𝕜 E] (p : ι → seminorm 𝕜 E) (s : finset ι) (x : E) :
(s.sup p) x = (s.sup (λ (i : ι), (p i) x, _⟩))
theorem seminorm.finset_sup_le_sum {𝕜 : Type u_3} {E : Type u_4} {ι : Type u_7} [semi_normed_ring 𝕜] [add_comm_group E] [module 𝕜 E] (p : ι → seminorm 𝕜 E) (s : finset ι) :
s.sup p s.sum (λ (i : ι), p i)
theorem seminorm.finset_sup_apply_le {𝕜 : Type u_3} {E : Type u_4} {ι : Type u_7} [semi_normed_ring 𝕜] [add_comm_group E] [module 𝕜 E] {p : ι → seminorm 𝕜 E} {s : finset ι} {x : E} {a : } (ha : 0 a) (h : ∀ (i : ι), i s(p i) x a) :
(s.sup p) x a
theorem seminorm.finset_sup_apply_lt {𝕜 : Type u_3} {E : Type u_4} {ι : Type u_7} [semi_normed_ring 𝕜] [add_comm_group E] [module 𝕜 E] {p : ι → seminorm 𝕜 E} {s : finset ι} {x : E} {a : } (ha : 0 < a) (h : ∀ (i : ι), i s(p i) x < a) :
(s.sup p) x < a
theorem seminorm.comp_smul {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [semi_normed_comm_ring 𝕜] [add_comm_group E] [add_comm_group F] [module 𝕜 E] [module 𝕜 F] (p : seminorm 𝕜 F) (f : E →ₗ[𝕜] F) (c : 𝕜) :
p.comp (c f) = c∥₊ p.comp f
theorem seminorm.comp_smul_apply {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [semi_normed_comm_ring 𝕜] [add_comm_group E] [add_comm_group F] [module 𝕜 E] [module 𝕜 F] (p : seminorm 𝕜 F) (f : E →ₗ[𝕜] F) (c : 𝕜) (x : E) :
(p.comp (c f)) x = c * p (f x)
@[protected, instance]
noncomputable def seminorm.has_inf {𝕜 : Type u_3} {E : Type u_4} [normed_field 𝕜] [add_comm_group E] [module 𝕜 E] :
has_inf (seminorm 𝕜 E)
Equations
@[simp]
theorem seminorm.inf_apply {𝕜 : Type u_3} {E : Type u_4} [normed_field 𝕜] [add_comm_group E] [module 𝕜 E] (p q : seminorm 𝕜 E) (x : E) :
(p q) x = ⨅ (u : E), p u + q (x - u)
theorem seminorm.smul_inf {R : Type u_1} {𝕜 : Type u_3} {E : Type u_4} [normed_field 𝕜] [add_comm_group E] [module 𝕜 E] [has_smul R ] [has_smul R nnreal] [is_scalar_tower R nnreal ] (r : R) (p q : seminorm 𝕜 E) :
r (p q) = r p r q

Seminorm ball #

def seminorm.ball {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_comm_group E] [has_smul 𝕜 E] (p : seminorm 𝕜 E) (x : E) (r : ) :
set E

The ball of radius r at x with respect to seminorm p is the set of elements y with p (y - x) <r`.

Equations
@[simp]
theorem seminorm.mem_ball {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_comm_group E] [has_smul 𝕜 E] (p : seminorm 𝕜 E) {x y : E} {r : } :
y p.ball x r p (y - x) < r
theorem seminorm.mem_ball_zero {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_comm_group E] [has_smul 𝕜 E] (p : seminorm 𝕜 E) {y : E} {r : } :
y p.ball 0 r p y < r
theorem seminorm.ball_zero_eq {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_comm_group E] [has_smul 𝕜 E] (p : seminorm 𝕜 E) {r : } :
p.ball 0 r = {y : E | p y < r}
@[simp]
theorem seminorm.ball_zero' {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_comm_group E] [has_smul 𝕜 E] {r : } (x : E) (hr : 0 < r) :
theorem seminorm.ball_smul {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_comm_group E] [has_smul 𝕜 E] (p : seminorm 𝕜 E) {c : nnreal} (hc : 0 < c) (r : ) (x : E) :
(c p).ball x r = p.ball x (r / c)
theorem seminorm.ball_sup {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_comm_group E] [has_smul 𝕜 E] (p q : seminorm 𝕜 E) (e : E) (r : ) :
(p q).ball e r = p.ball e r q.ball e r
theorem seminorm.ball_finset_sup' {𝕜 : Type u_3} {E : Type u_4} {ι : Type u_7} [semi_normed_ring 𝕜] [add_comm_group E] [has_smul 𝕜 E] (p : ι → seminorm 𝕜 E) (s : finset ι) (H : s.nonempty) (e : E) (r : ) :
(s.sup' H p).ball e r = s.inf' H (λ (i : ι), (p i).ball e r)
theorem seminorm.ball_mono {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_comm_group E] [has_smul 𝕜 E] {x : E} {p : seminorm 𝕜 E} {r₁ r₂ : } (h : r₁ r₂) :
p.ball x r₁ p.ball x r₂
theorem seminorm.ball_antitone {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_comm_group E] [has_smul 𝕜 E] {x : E} {r : } {p q : seminorm 𝕜 E} (h : q p) :
p.ball x r q.ball x r
theorem seminorm.ball_add_ball_subset {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_comm_group E] [has_smul 𝕜 E] (p : seminorm 𝕜 E) (r₁ r₂ : ) (x₁ x₂ : E) :
p.ball x₁ r₁ + p.ball x₂ r₂ p.ball (x₁ + x₂) (r₁ + r₂)
theorem seminorm.ball_comp {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [semi_normed_ring 𝕜] [add_comm_group E] [module 𝕜 E] [add_comm_group F] [module 𝕜 F] (p : seminorm 𝕜 F) (f : E →ₗ[𝕜] F) (x : E) (r : ) :
(p.comp f).ball x r = f ⁻¹' p.ball (f x) r
theorem seminorm.ball_zero_eq_preimage_ball {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_comm_group E] [module 𝕜 E] (p : seminorm 𝕜 E) {r : } :
@[simp]
theorem seminorm.ball_bot {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_comm_group E] [module 𝕜 E] {r : } (x : E) (hr : 0 < r) :
theorem seminorm.balanced_ball_zero {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_comm_group E] [module 𝕜 E] (p : seminorm 𝕜 E) (r : ) :
balanced 𝕜 (p.ball 0 r)

Seminorm-balls at the origin are balanced.

theorem seminorm.ball_finset_sup_eq_Inter {𝕜 : Type u_3} {E : Type u_4} {ι : Type u_7} [semi_normed_ring 𝕜] [add_comm_group E] [module 𝕜 E] (p : ι → seminorm 𝕜 E) (s : finset ι) (x : E) {r : } (hr : 0 < r) :
(s.sup p).ball x r = ⋂ (i : ι) (H : i s), (p i).ball x r
theorem seminorm.ball_finset_sup {𝕜 : Type u_3} {E : Type u_4} {ι : Type u_7} [semi_normed_ring 𝕜] [add_comm_group E] [module 𝕜 E] (p : ι → seminorm 𝕜 E) (s : finset ι) (x : E) {r : } (hr : 0 < r) :
(s.sup p).ball x r = s.inf (λ (i : ι), (p i).ball x r)
theorem seminorm.ball_smul_ball {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_comm_group E] [module 𝕜 E] (p : seminorm 𝕜 E) (r₁ r₂ : ) :
metric.ball 0 r₁ p.ball 0 r₂ p.ball 0 (r₁ * r₂)
@[simp]
theorem seminorm.ball_eq_emptyset {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_comm_group E] [module 𝕜 E] (p : seminorm 𝕜 E) {x : E} {r : } (hr : r 0) :
p.ball x r =
theorem seminorm.smul_ball_zero {𝕜 : Type u_3} {E : Type u_4} [normed_field 𝕜] [add_comm_group E] [module 𝕜 E] {p : seminorm 𝕜 E} {k : 𝕜} {r : } (hk : 0 < k) :
k p.ball 0 r = p.ball 0 (k * r)
theorem seminorm.ball_zero_absorbs_ball_zero {𝕜 : Type u_3} {E : Type u_4} [normed_field 𝕜] [add_comm_group E] [module 𝕜 E] (p : seminorm 𝕜 E) {r₁ r₂ : } (hr₁ : 0 < r₁) :
absorbs 𝕜 (p.ball 0 r₁) (p.ball 0 r₂)
@[protected]
theorem seminorm.absorbent_ball_zero {𝕜 : Type u_3} {E : Type u_4} [normed_field 𝕜] [add_comm_group E] [module 𝕜 E] (p : seminorm 𝕜 E) {r : } (hr : 0 < r) :
absorbent 𝕜 (p.ball 0 r)

Seminorm-balls at the origin are absorbent.

@[protected]
theorem seminorm.absorbent_ball {𝕜 : Type u_3} {E : Type u_4} [normed_field 𝕜] [add_comm_group E] [module 𝕜 E] (p : seminorm 𝕜 E) {r : } {x : E} (hpr : p x < r) :
absorbent 𝕜 (p.ball x r)

Seminorm-balls containing the origin are absorbent.

theorem seminorm.symmetric_ball_zero {𝕜 : Type u_3} {E : Type u_4} [normed_field 𝕜] [add_comm_group E] [module 𝕜 E] (p : seminorm 𝕜 E) {x : E} (r : ) (hx : x p.ball 0 r) :
-x p.ball 0 r
@[simp]
theorem seminorm.neg_ball {𝕜 : Type u_3} {E : Type u_4} [normed_field 𝕜] [add_comm_group E] [module 𝕜 E] (p : seminorm 𝕜 E) (r : ) (x : E) :
-p.ball x r = p.ball (-x) r
@[simp]
theorem seminorm.smul_ball_preimage {𝕜 : Type u_3} {E : Type u_4} [normed_field 𝕜] [add_comm_group E] [module 𝕜 E] (p : seminorm 𝕜 E) (y : E) (r : ) (a : 𝕜) (ha : a 0) :
@[protected]
theorem seminorm.convex_on {𝕜 : Type u_3} {E : Type u_4} [normed_field 𝕜] [add_comm_group E] [normed_space 𝕜] [module 𝕜 E] [has_smul E] [is_scalar_tower 𝕜 E] (p : seminorm 𝕜 E) :

A seminorm is convex. Also see convex_on_norm.

theorem seminorm.convex_ball {𝕜 : Type u_3} {E : Type u_4} [normed_field 𝕜] [add_comm_group E] [normed_space 𝕜] [module 𝕜 E] [module E] [is_scalar_tower 𝕜 E] (p : seminorm 𝕜 E) (x : E) (r : ) :
convex (p.ball x r)

Seminorm-balls are convex.

The norm as a seminorm #

def norm_seminorm (𝕜 : Type u_3) (E : Type u_4) [normed_field 𝕜] [seminormed_add_comm_group E] [normed_space 𝕜 E] :
seminorm 𝕜 E

The norm of a seminormed group as a seminorm.

Equations
@[simp]
theorem coe_norm_seminorm (𝕜 : Type u_3) (E : Type u_4) [normed_field 𝕜] [seminormed_add_comm_group E] [normed_space 𝕜 E] :
@[simp]
theorem ball_norm_seminorm (𝕜 : Type u_3) (E : Type u_4) [normed_field 𝕜] [seminormed_add_comm_group E] [normed_space 𝕜 E] :
theorem absorbent_ball_zero {𝕜 : Type u_3} {E : Type u_4} [normed_field 𝕜] [seminormed_add_comm_group E] [normed_space 𝕜 E] {r : } (hr : 0 < r) :

Balls at the origin are absorbent.

theorem absorbent_ball {𝕜 : Type u_3} {E : Type u_4} [normed_field 𝕜] [seminormed_add_comm_group E] [normed_space 𝕜 E] {r : } {x : E} (hx : x < r) :

Balls containing the origin are absorbent.

theorem balanced_ball_zero {𝕜 : Type u_3} {E : Type u_4} [normed_field 𝕜] [seminormed_add_comm_group E] [normed_space 𝕜 E] {r : } :

Balls at the origin are balanced.