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

structure seminorm (π•œ : Type u_8) (E : Type u_9) [semi_normed_ring π•œ] [add_monoid E] [has_scalar π•œ 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
@[protected, instance]
def seminorm.fun_like {π•œ : Type u_3} {E : Type u_4} [semi_normed_ring π•œ] [add_monoid E] [has_scalar π•œ E] :
fun_like (seminorm π•œ E) E (Ξ» (_x : E), ℝ)
Equations
@[protected, instance]
def seminorm.has_coe_to_fun {π•œ : Type u_3} {E : Type u_4} [semi_normed_ring π•œ] [add_monoid E] [has_scalar π•œ 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_monoid E] [has_scalar π•œ 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_monoid E] [has_scalar π•œ E] :
has_zero (seminorm π•œ E)
Equations
@[simp]
theorem seminorm.coe_zero {π•œ : Type u_3} {E : Type u_4} [semi_normed_ring π•œ] [add_monoid E] [has_scalar π•œ E] :
@[simp]
theorem seminorm.zero_apply {π•œ : Type u_3} {E : Type u_4} [semi_normed_ring π•œ] [add_monoid E] [has_scalar π•œ E] (x : E) :
⇑0 x = 0
@[protected, instance]
def seminorm.inhabited {π•œ : Type u_3} {E : Type u_4} [semi_normed_ring π•œ] [add_monoid E] [has_scalar π•œ E] :
inhabited (seminorm π•œ E)
Equations
@[protected]
theorem seminorm.smul {π•œ : Type u_3} {E : Type u_4} [semi_normed_ring π•œ] [add_monoid E] [has_scalar π•œ E] (p : seminorm π•œ E) (c : π•œ) (x : E) :
@[protected]
theorem seminorm.triangle {π•œ : Type u_3} {E : Type u_4} [semi_normed_ring π•œ] [add_monoid E] [has_scalar π•œ E] (p : seminorm π•œ E) (x y : E) :
⇑p (x + y) ≀ ⇑p x + ⇑p y
@[protected, instance]
def seminorm.has_scalar {R : Type u_1} {π•œ : Type u_3} {E : Type u_4} [semi_normed_ring π•œ] [add_monoid E] [has_scalar π•œ E] [has_scalar R ℝ] [has_scalar R nnreal] [is_scalar_tower R nnreal ℝ] :
has_scalar 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_monoid E] [has_scalar π•œ E] [has_scalar R ℝ] [has_scalar R nnreal] [is_scalar_tower R nnreal ℝ] [has_scalar R' ℝ] [has_scalar R' nnreal] [is_scalar_tower R' nnreal ℝ] [has_scalar R R'] [is_scalar_tower R R' ℝ] :
is_scalar_tower R R' (seminorm π•œ E)
theorem seminorm.coe_smul {R : Type u_1} {π•œ : Type u_3} {E : Type u_4} [semi_normed_ring π•œ] [add_monoid E] [has_scalar π•œ E] [has_scalar R ℝ] [has_scalar R nnreal] [is_scalar_tower R nnreal ℝ] (r : R) (p : seminorm π•œ E) :
@[simp]
theorem seminorm.smul_apply {R : Type u_1} {π•œ : Type u_3} {E : Type u_4} [semi_normed_ring π•œ] [add_monoid E] [has_scalar π•œ E] [has_scalar R ℝ] [has_scalar R nnreal] [is_scalar_tower R nnreal ℝ] (r : R) (p : seminorm π•œ E) (x : E) :
@[protected, instance]
def seminorm.has_add {π•œ : Type u_3} {E : Type u_4} [semi_normed_ring π•œ] [add_monoid E] [has_scalar π•œ E] :
has_add (seminorm π•œ E)
Equations
theorem seminorm.coe_add {π•œ : Type u_3} {E : Type u_4} [semi_normed_ring π•œ] [add_monoid E] [has_scalar π•œ E] (p q : seminorm π•œ E) :
@[simp]
theorem seminorm.add_apply {π•œ : Type u_3} {E : Type u_4} [semi_normed_ring π•œ] [add_monoid E] [has_scalar π•œ 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_monoid E] [has_scalar π•œ E] :
add_monoid (seminorm π•œ E)
Equations
@[protected, instance]
def seminorm.ordered_cancel_add_comm_monoid {π•œ : Type u_3} {E : Type u_4} [semi_normed_ring π•œ] [add_monoid E] [has_scalar π•œ E] :
Equations
@[protected, instance]
def seminorm.mul_action {R : Type u_1} {π•œ : Type u_3} {E : Type u_4} [semi_normed_ring π•œ] [add_monoid E] [has_scalar π•œ E] [monoid R] [mul_action R ℝ] [has_scalar 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_monoid E] [has_scalar π•œ 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_monoid E] [has_scalar π•œ E] (x : seminorm π•œ E) (αΎ° : E) :
⇑(seminorm.coe_fn_add_monoid_hom π•œ E) x αΎ° = ⇑x αΎ°
theorem seminorm.coe_fn_add_monoid_hom_injective (π•œ : Type u_3) (E : Type u_4) [semi_normed_ring π•œ] [add_monoid E] [has_scalar π•œ E] :
@[protected, instance]
def seminorm.distrib_mul_action {R : Type u_1} {π•œ : Type u_3} {E : Type u_4} [semi_normed_ring π•œ] [add_monoid E] [has_scalar π•œ E] [monoid R] [distrib_mul_action R ℝ] [has_scalar 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_monoid E] [has_scalar π•œ E] [semiring R] [module R ℝ] [has_scalar 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_monoid E] [has_scalar π•œ E] :
has_sup (seminorm π•œ E)
Equations
@[simp]
theorem seminorm.coe_sup {π•œ : Type u_3} {E : Type u_4} [semi_normed_ring π•œ] [add_monoid E] [has_scalar π•œ E] (p q : seminorm π•œ E) :
theorem seminorm.sup_apply {π•œ : Type u_3} {E : Type u_4} [semi_normed_ring π•œ] [add_monoid E] [has_scalar π•œ E] (p q : seminorm π•œ E) (x : E) :
theorem seminorm.smul_sup {R : Type u_1} {π•œ : Type u_3} {E : Type u_4} [semi_normed_ring π•œ] [add_monoid E] [has_scalar π•œ E] [has_scalar R ℝ] [has_scalar R nnreal] [is_scalar_tower R nnreal ℝ] (r : R) (p q : seminorm π•œ E) :
@[protected, instance]
def seminorm.partial_order {π•œ : Type u_3} {E : Type u_4} [semi_normed_ring π•œ] [add_monoid E] [has_scalar π•œ E] :
partial_order (seminorm π•œ E)
Equations
theorem seminorm.le_def {π•œ : Type u_3} {E : Type u_4} [semi_normed_ring π•œ] [add_monoid E] [has_scalar π•œ E] (p q : seminorm π•œ E) :
theorem seminorm.lt_def {π•œ : Type u_3} {E : Type u_4} [semi_normed_ring π•œ] [add_monoid E] [has_scalar π•œ E] (p q : seminorm π•œ E) :
@[protected, instance]
noncomputable def seminorm.semilattice_sup {π•œ : Type u_3} {E : Type u_4} [semi_normed_ring π•œ] [add_monoid E] [has_scalar π•œ E] :
Equations
@[protected, simp]
theorem seminorm.zero {π•œ : Type u_3} {E : Type u_4} [semi_normed_ring π•œ] [add_monoid E] [smul_with_zero π•œ E] (p : seminorm π•œ E) :
⇑p 0 = 0
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) :
@[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_triangle {π•œ : 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_scalar R ℝ] [has_scalar 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] [norm_one_class π•œ] (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] [norm_one_class π•œ] (p : seminorm π•œ E) (x y : E) :
⇑p (x - y) ≀ ⇑p x + ⇑p y
theorem seminorm.nonneg {π•œ : Type u_3} {E : Type u_4} [semi_normed_ring π•œ] [add_comm_group E] [module π•œ E] [norm_one_class π•œ] (p : seminorm π•œ E) (x : E) :
theorem seminorm.sub_rev {π•œ : Type u_3} {E : Type u_4} [semi_normed_ring π•œ] [add_comm_group E] [module π•œ E] [norm_one_class π•œ] (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] [norm_one_class π•œ] (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] [norm_one_class π•œ] (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] [norm_one_class π•œ] :
order_bot (seminorm π•œ E)
Equations
@[simp]
theorem seminorm.coe_bot {π•œ : Type u_3} {E : Type u_4} [semi_normed_ring π•œ] [add_comm_group E] [module π•œ E] [norm_one_class π•œ] :
theorem seminorm.bot_eq_zero {π•œ : Type u_3} {E : Type u_4} [semi_normed_ring π•œ] [add_comm_group E] [module π•œ E] [norm_one_class π•œ] :
theorem seminorm.smul_le_smul {π•œ : Type u_3} {E : Type u_4} [semi_normed_ring π•œ] [add_comm_group E] [module π•œ E] [norm_one_class π•œ] {p q : seminorm π•œ E} {a b : nnreal} (hpq : p ≀ q) (hab : a ≀ b) :
theorem seminorm.finset_sup_apply {π•œ : Type u_3} {E : Type u_4} {ΞΉ : Type u_7} [semi_normed_ring π•œ] [add_comm_group E] [module π•œ E] [norm_one_class π•œ] (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] [norm_one_class π•œ] (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] [norm_one_class π•œ] {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] [norm_one_class π•œ] {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 : π•œ) :
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) :
@[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)
@[protected, instance]
noncomputable def seminorm.lattice {π•œ : Type u_3} {E : Type u_4} [normed_field π•œ] [add_comm_group E] [module π•œ E] :
lattice (seminorm π•œ E)
Equations
theorem seminorm.smul_inf {R : Type u_1} {π•œ : Type u_3} {E : Type u_4} [normed_field π•œ] [add_comm_group E] [module π•œ E] [has_scalar R ℝ] [has_scalar R nnreal] [is_scalar_tower R nnreal ℝ] (r : R) (p q : seminorm π•œ E) :

Seminorm ball #

def seminorm.ball {π•œ : Type u_3} {E : Type u_4} [semi_normed_ring π•œ] [add_comm_group E] [has_scalar π•œ 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_scalar π•œ 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_scalar π•œ 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_scalar π•œ 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_scalar π•œ 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_scalar π•œ 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_scalar π•œ 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_scalar π•œ 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_scalar π•œ 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_scalar π•œ 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_scalar π•œ 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] [norm_one_class π•œ] (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] [norm_one_class π•œ] {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] [norm_one_class π•œ] (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] [norm_one_class π•œ] (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] [norm_one_class π•œ] (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] [norm_one_class π•œ] (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] [norm_one_class π•œ] (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_scalar ℝ 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 : ℝ) :

Seminorm-balls are convex.

The norm as a seminorm #

def norm_seminorm (π•œ : Type u_3) (E : Type u_4) [normed_field π•œ] [semi_normed_group E] [normed_space π•œ E] :
seminorm π•œ E

The norm of a seminormed group as a seminorm.

Equations
Instances for norm_seminorm
@[simp]
theorem coe_norm_seminorm (π•œ : Type u_3) (E : Type u_4) [normed_field π•œ] [semi_normed_group E] [normed_space π•œ E] :
@[simp]
theorem ball_norm_seminorm (π•œ : Type u_3) (E : Type u_4) [normed_field π•œ] [semi_normed_group E] [normed_space π•œ E] :
theorem absorbent_ball_zero {π•œ : Type u_3} {E : Type u_4} [normed_field π•œ] [semi_normed_group E] [normed_space π•œ E] {r : ℝ} (hr : 0 < r) :
absorbent π•œ (metric.ball 0 r)

Balls at the origin are absorbent.

theorem absorbent_ball {π•œ : Type u_3} {E : Type u_4} [normed_field π•œ] [semi_normed_group E] [normed_space π•œ E] {r : ℝ} {x : E} (hx : βˆ₯xβˆ₯ < r) :
absorbent π•œ (metric.ball x r)

Balls containing the origin are absorbent.

theorem balanced_ball_zero {π•œ : Type u_3} {E : Type u_4} [normed_field π•œ] [semi_normed_group E] [normed_space π•œ E] {r : ℝ} [norm_one_class π•œ] :
balanced π•œ (metric.ball 0 r)

Balls at the origin are balanced.