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

source
@[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) :
add_group_seminorm E
source
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
source
@[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] :
add_group_seminorm_class F E
source
@[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
source
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
source
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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[simp]
theorem seminorm.coe_zero {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_group E] [has_smul 𝕜 E] :
⇑0 = 0
source
@[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
source
@[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
source
@[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
source
@[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)
source
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
source
@[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
source
@[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
source
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
source
@[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
source
@[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
source
@[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] :
ordered_cancel_add_comm_monoid (seminorm 𝕜 E)
Equations
source
@[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
source
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
source
@[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 ᾰ
source
theorem seminorm.coe_fn_add_monoid_hom_injective (𝕜 : Type u_3) (E : Type u_4) [semi_normed_ring 𝕜] [add_group E] [has_smul 𝕜 E] :
function.injective ⇑(seminorm.coe_fn_add_monoid_hom 𝕜 E)
source
@[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 ℝ] :
distrib_mul_action R (seminorm 𝕜 E)
Equations
source
@[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
source
@[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
source
@[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
source
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
source
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
source
@[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
source
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
source
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
source
@[protected, instance]
def seminorm.semilattice_sup {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_group E] [has_smul 𝕜 E] :
semilattice_sup (seminorm 𝕜 E)
Equations
source
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
source
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
source
@[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)
source
@[simp]
theorem seminorm.comp_id {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_comm_group E] [module 𝕜 E] (p : seminorm 𝕜 E) :
p.comp linear_map.id = p
source
@[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
source
@[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
source
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
source
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
source
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
source
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
source
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
source
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
source
@[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) :
⇑(seminorm.pullback f) p = p.comp f
source
@[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
source
@[simp]
theorem seminorm.coe_bot {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_comm_group E] [module 𝕜 E] :
⇑⊥ = 0
source
theorem seminorm.bot_eq_zero {𝕜 : Type u_3} {E : Type u_4} [semi_normed_ring 𝕜] [add_comm_group E] [module 𝕜 E] :
⊥ = 0
source
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
source
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, _⟩))
source
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)
source
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
source
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
source
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) :
∥⇑p x - ⇑p y∥ ≤ ⇑p (x - y)
source
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
source
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)
source
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.

source
@[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
source
@[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)
source
@[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
source
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 #

source
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
source
@[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
source
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
source
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
source
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}
source
@[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) :
0.ball x r = set.univ
source
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)
source
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
source
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)
source
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₂
source
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
source
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₂)
source
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
source
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 : ℝ} :
p.ball 0 r = ⇑p ⁻¹' metric.ball 0 r
source
@[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) :
⊥.ball x r = set.univ
source
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.

source
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
source
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)
source
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₂)
source
@[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 = ∅
source
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)
source
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₂)
source
@[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.

source
@[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.

source
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
source
@[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
source
@[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) :
has_smul.smul a ⁻¹' p.ball y r = p.ball (a⁻¹ • y) (r / ∥a∥)
source
@[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) :
convex_on ℝ set.univ ⇑p

A seminorm is convex. Also see convex_on_norm.

source
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.

source
@[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
source
@[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) :
⇑(seminorm.restrict_scalars 𝕜 p) = ⇑p
source
@[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) :
(seminorm.restrict_scalars 𝕜 p).ball = p.ball

Continuity criterions for seminorms #

source
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) :
continuous_at ⇑p 0
source
@[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) :
uniform_continuous ⇑p
source
@[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) :
continuous ⇑p
source
@[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) :
uniform_continuous ⇑p
source
@[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) :
continuous ⇑p
source
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) :
continuous ⇑p

The norm as a seminorm #

source
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
source
@[simp]
theorem coe_norm_seminorm (𝕜 : Type u_3) (E : Type u_4) [normed_field 𝕜] [seminormed_add_comm_group E] [normed_space 𝕜 E] :
⇑(norm_seminorm 𝕜 E) = has_norm.norm
source
@[simp]
theorem ball_norm_seminorm (𝕜 : Type u_3) (E : Type u_4) [normed_field 𝕜] [seminormed_add_comm_group E] [normed_space 𝕜 E] :
(norm_seminorm 𝕜 E).ball = metric.ball
source
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.

source
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.

source
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.