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
@[nolint, instance]
def seminorm_class.to_add_group_seminorm_class (F : Type u_8) (π•œ : out_param (Type u_9)) (E : out_param (Type u_10)) [semi_normed_ring π•œ] [add_group E] [has_smul π•œ E] [self : seminorm_class F π•œ E] :
@[class]
structure seminorm_class (F : Type u_8) (π•œ : out_param (Type u_9)) (E : out_param (Type u_10)) [semi_normed_ring π•œ] [add_group E] [has_smul π•œ E] :
Type (max u_10 u_8)

seminorm_class F π•œ E states that F is a type of seminorms on the π•œ-module E.

You should extend this class when you extend seminorm.

Instances of this typeclass
Instances of other typeclasses for seminorm_class
  • seminorm_class.has_sizeof_inst
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.seminorm_class {π•œ : Type u_3} {E : Type u_4} [semi_normed_ring π•œ] [add_group E] [has_smul π•œ E] :
seminorm_class (seminorm π•œ E) π•œ 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] :
has_zero (seminorm π•œ E)
Equations
@[simp]
theorem seminorm.coe_zero {π•œ : Type u_3} {E : Type u_4} [semi_normed_ring π•œ] [add_group E] [has_smul π•œ E] :
@[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] :
inhabited (seminorm π•œ E)
Equations
@[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' ℝ] :
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_group E] [has_smul π•œ E] [has_smul R ℝ] [has_smul 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_group E] [has_smul π•œ E] [has_smul R ℝ] [has_smul 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_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) :
@[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] :
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_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) :
⇑(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_group E] [has_smul π•œ 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]
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) :
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) :
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) :
@[protected, instance]
def seminorm.partial_order {π•œ : Type u_3} {E : Type u_4} [semi_normed_ring π•œ] [add_group E] [has_smul π•œ E] :
partial_order (seminorm π•œ 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) :
theorem seminorm.lt_def {π•œ : Type u_3} {E : Type u_4} [semi_normed_ring π•œ] [add_group E] [has_smul π•œ E] (p q : seminorm π•œ E) :
@[protected, instance]
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) :
@[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, instance]
def seminorm.order_bot {π•œ : Type u_3} {E : Type u_4} [semi_normed_ring π•œ] [add_comm_group E] [module π•œ E] :
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] :
theorem seminorm.bot_eq_zero {π•œ : Type u_3} {E : Type u_4} [semi_normed_ring π•œ] [add_comm_group E] [module π•œ E] :
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) :
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.norm_sub_map_le_sub {π•œ : Type u_3} {E : Type u_4} [semi_normed_ring π•œ] [add_comm_group E] [module π•œ E] (p : seminorm π•œ E) (x y : E) :
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) :
theorem seminorm.bdd_below_range_add {π•œ : Type u_3} {E : Type u_4} [normed_field π•œ] [add_comm_group E] [module π•œ E] {p q : seminorm π•œ E} {x : E} :
bdd_below (set.range (Ξ» (u : E), ⇑p u + ⇑q (x - u)))

Auxiliary lemma to show that the infimum of seminorms is well-defined.

@[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_smul R ℝ] [has_smul 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_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_self {π•œ : Type u_3} {E : Type u_4} [semi_normed_ring π•œ] [add_comm_group E] [has_smul π•œ E] (p : seminorm π•œ E) {x : E} {r : ℝ} (hr : 0 < r) :
x ∈ p.ball 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 : ℝ) :

Seminorm-balls are convex.

@[protected]
def seminorm.restrict_scalars (π•œ : Type u_3) {E : Type u_4} {π•œ' : Type u_8} [normed_field π•œ] [semi_normed_ring π•œ'] [normed_algebra π•œ π•œ'] [norm_one_class π•œ'] [add_comm_group E] [module π•œ' E] [has_smul π•œ E] [is_scalar_tower π•œ π•œ' E] (p : seminorm π•œ' E) :
seminorm π•œ E

Reinterpret a seminorm over a field π•œ' as a seminorm over a smaller field π•œ. This will typically be used with is_R_or_C π•œ' and π•œ = ℝ.

Equations
@[simp]
theorem seminorm.coe_restrict_scalars (π•œ : Type u_3) {E : Type u_4} {π•œ' : Type u_8} [normed_field π•œ] [semi_normed_ring π•œ'] [normed_algebra π•œ π•œ'] [norm_one_class π•œ'] [add_comm_group E] [module π•œ' E] [has_smul π•œ E] [is_scalar_tower π•œ π•œ' E] (p : seminorm π•œ' E) :
@[simp]
theorem seminorm.restrict_scalars_ball (π•œ : Type u_3) {E : Type u_4} {π•œ' : Type u_8} [normed_field π•œ] [semi_normed_ring π•œ'] [normed_algebra π•œ π•œ'] [norm_one_class π•œ'] [add_comm_group E] [module π•œ' E] [has_smul π•œ E] [is_scalar_tower π•œ π•œ' E] (p : seminorm π•œ' E) :

Continuity criterions for seminorms #

theorem seminorm.continuous_at_zero {π•œ : Type u_3} {E : Type u_4} [semi_normed_ring π•œ] [add_comm_group E] [module π•œ E] [norm_one_class π•œ] [normed_algebra ℝ π•œ] [module ℝ E] [is_scalar_tower ℝ π•œ E] [topological_space E] [has_continuous_const_smul ℝ E] {p : seminorm π•œ E} (hp : p.ball 0 1 ∈ nhds 0) :
@[protected]
theorem seminorm.uniform_continuous_of_continuous_at_zero {π•œ : Type u_3} {E : Type u_4} [semi_normed_ring π•œ] [add_comm_group E] [module π•œ E] [uniform_space E] [uniform_add_group E] {p : seminorm π•œ E} (hp : continuous_at ⇑p 0) :
@[protected]
theorem seminorm.continuous_of_continuous_at_zero {π•œ : Type u_3} {E : Type u_4} [semi_normed_ring π•œ] [add_comm_group E] [module π•œ E] [topological_space E] [topological_add_group E] {p : seminorm π•œ E} (hp : continuous_at ⇑p 0) :
@[protected]
theorem seminorm.uniform_continuous {π•œ : Type u_3} {E : Type u_4} [semi_normed_ring π•œ] [add_comm_group E] [module π•œ E] [norm_one_class π•œ] [normed_algebra ℝ π•œ] [module ℝ E] [is_scalar_tower ℝ π•œ E] [uniform_space E] [uniform_add_group E] [has_continuous_const_smul ℝ E] {p : seminorm π•œ E} (hp : p.ball 0 1 ∈ nhds 0) :
@[protected]
theorem seminorm.continuous {π•œ : Type u_3} {E : Type u_4} [semi_normed_ring π•œ] [add_comm_group E] [module π•œ E] [norm_one_class π•œ] [normed_algebra ℝ π•œ] [module ℝ E] [is_scalar_tower ℝ π•œ E] [topological_space E] [topological_add_group E] [has_continuous_const_smul ℝ E] {p : seminorm π•œ E} (hp : p.ball 0 1 ∈ nhds 0) :
theorem seminorm.continuous_of_le {π•œ : Type u_3} {E : Type u_4} [semi_normed_ring π•œ] [add_comm_group E] [module π•œ E] [norm_one_class π•œ] [normed_algebra ℝ π•œ] [module ℝ E] [is_scalar_tower ℝ π•œ E] [topological_space E] [topological_add_group E] [has_continuous_const_smul ℝ E] {p q : seminorm π•œ E} (hq : continuous ⇑q) (hpq : p ≀ q) :

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) :
absorbent π•œ (metric.ball 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) :
absorbent π•œ (metric.ball 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 : ℝ} :
balanced π•œ (metric.ball 0 r)

Balls at the origin are balanced.