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_13} {E : Type u_14} [semi_normed_ring π•œ] [add_group E] [has_smul π•œ E] (self : seminorm π•œ E) :
structure seminorm (π•œ : Type u_13) (E : Type u_14) [semi_normed_ring π•œ] [add_group E] [has_smul π•œ E] :
Type u_14

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_13) (π•œ : out_param (Type u_14)) (E : out_param (Type u_15)) [semi_normed_ring π•œ] [add_group E] [has_smul π•œ E] [self : seminorm_class F π•œ E] :
@[class]
structure seminorm_class (F : Type u_13) (π•œ : out_param (Type u_14)) (E : out_param (Type u_15)) [semi_normed_ring π•œ] [add_group E] [has_smul π•œ E] :
Type (max u_13 u_15)

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_7} [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_7} [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_7} [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_7} [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_7} [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_7} [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_7} [semi_normed_ring π•œ] [add_group E] [has_smul π•œ E] :
@[simp]
theorem seminorm.zero_apply {π•œ : Type u_3} {E : Type u_7} [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_7} [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_7} [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_7} [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_7} [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_7} [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_7} [semi_normed_ring π•œ] [add_group E] [has_smul π•œ E] :
has_add (seminorm π•œ E)
Equations
theorem seminorm.coe_add {π•œ : Type u_3} {E : Type u_7} [semi_normed_ring π•œ] [add_group E] [has_smul π•œ E] (p q : seminorm π•œ E) :
@[simp]
theorem seminorm.add_apply {π•œ : Type u_3} {E : Type u_7} [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_7} [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_7} [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_7} [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_7) [semi_normed_ring π•œ] [add_group E] [has_smul π•œ 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_7) [semi_normed_ring π•œ] [add_group E] [has_smul π•œ E] (x : seminorm π•œ E) (αΎ° : E) :
⇑(seminorm.coe_fn_add_monoid_hom π•œ E) x αΎ° = ⇑x αΎ°
@[protected, instance]
def seminorm.distrib_mul_action {R : Type u_1} {π•œ : Type u_3} {E : Type u_7} [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_7} [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_7} [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_7} [semi_normed_ring π•œ] [add_group E] [has_smul π•œ E] (p q : seminorm π•œ E) :
theorem seminorm.sup_apply {π•œ : Type u_3} {E : Type u_7} [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_7} [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_7} [semi_normed_ring π•œ] [add_group E] [has_smul π•œ E] :
partial_order (seminorm π•œ E)
Equations
theorem seminorm.le_def {π•œ : Type u_3} {E : Type u_7} [semi_normed_ring π•œ] [add_group E] [has_smul π•œ E] (p q : seminorm π•œ E) :
theorem seminorm.lt_def {π•œ : Type u_3} {E : Type u_7} [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_7} [semi_normed_ring π•œ] [add_group E] [has_smul π•œ E] :
Equations
def seminorm.comp {π•œ : Type u_3} {π•œβ‚‚ : Type u_4} {E : Type u_7} {Eβ‚‚ : Type u_8} [semi_normed_ring π•œ] [semi_normed_ring π•œβ‚‚] {σ₁₂ : π•œ β†’+* π•œβ‚‚} [ring_hom_isometric σ₁₂] [add_comm_group E] [add_comm_group Eβ‚‚] [module π•œ E] [module π•œβ‚‚ Eβ‚‚] (p : seminorm π•œβ‚‚ Eβ‚‚) (f : E β†’β‚›β‚—[σ₁₂] Eβ‚‚) :
seminorm π•œ E

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

Equations
theorem seminorm.coe_comp {π•œ : Type u_3} {π•œβ‚‚ : Type u_4} {E : Type u_7} {Eβ‚‚ : Type u_8} [semi_normed_ring π•œ] [semi_normed_ring π•œβ‚‚] {σ₁₂ : π•œ β†’+* π•œβ‚‚} [ring_hom_isometric σ₁₂] [add_comm_group E] [add_comm_group Eβ‚‚] [module π•œ E] [module π•œβ‚‚ Eβ‚‚] (p : seminorm π•œβ‚‚ Eβ‚‚) (f : E β†’β‚›β‚—[σ₁₂] Eβ‚‚) :
@[simp]
theorem seminorm.comp_apply {π•œ : Type u_3} {π•œβ‚‚ : Type u_4} {E : Type u_7} {Eβ‚‚ : Type u_8} [semi_normed_ring π•œ] [semi_normed_ring π•œβ‚‚] {σ₁₂ : π•œ β†’+* π•œβ‚‚} [ring_hom_isometric σ₁₂] [add_comm_group E] [add_comm_group Eβ‚‚] [module π•œ E] [module π•œβ‚‚ Eβ‚‚] (p : seminorm π•œβ‚‚ Eβ‚‚) (f : E β†’β‚›β‚—[σ₁₂] Eβ‚‚) (x : E) :
⇑(p.comp f) x = ⇑p (⇑f x)
@[simp]
theorem seminorm.comp_id {π•œ : Type u_3} {E : Type u_7} [semi_normed_ring π•œ] [add_comm_group E] [module π•œ E] (p : seminorm π•œ E) :
@[simp]
theorem seminorm.comp_zero {π•œ : Type u_3} {π•œβ‚‚ : Type u_4} {E : Type u_7} {Eβ‚‚ : Type u_8} [semi_normed_ring π•œ] [semi_normed_ring π•œβ‚‚] {σ₁₂ : π•œ β†’+* π•œβ‚‚} [ring_hom_isometric σ₁₂] [add_comm_group E] [add_comm_group Eβ‚‚] [module π•œ E] [module π•œβ‚‚ Eβ‚‚] (p : seminorm π•œβ‚‚ Eβ‚‚) :
p.comp 0 = 0
@[simp]
theorem seminorm.zero_comp {π•œ : Type u_3} {π•œβ‚‚ : Type u_4} {E : Type u_7} {Eβ‚‚ : Type u_8} [semi_normed_ring π•œ] [semi_normed_ring π•œβ‚‚] {σ₁₂ : π•œ β†’+* π•œβ‚‚} [ring_hom_isometric σ₁₂] [add_comm_group E] [add_comm_group Eβ‚‚] [module π•œ E] [module π•œβ‚‚ Eβ‚‚] (f : E β†’β‚›β‚—[σ₁₂] Eβ‚‚) :
0.comp f = 0
theorem seminorm.comp_comp {π•œ : Type u_3} {π•œβ‚‚ : Type u_4} {π•œβ‚ƒ : Type u_5} {E : Type u_7} {Eβ‚‚ : Type u_8} {E₃ : Type u_9} [semi_normed_ring π•œ] [semi_normed_ring π•œβ‚‚] [semi_normed_ring π•œβ‚ƒ] {σ₁₂ : π•œ β†’+* π•œβ‚‚} [ring_hom_isometric σ₁₂] {σ₂₃ : π•œβ‚‚ β†’+* π•œβ‚ƒ} [ring_hom_isometric σ₂₃] {σ₁₃ : π•œ β†’+* π•œβ‚ƒ} [ring_hom_isometric σ₁₃] [add_comm_group E] [add_comm_group Eβ‚‚] [add_comm_group E₃] [module π•œ E] [module π•œβ‚‚ Eβ‚‚] [module π•œβ‚ƒ E₃] [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] (p : seminorm π•œβ‚ƒ E₃) (g : Eβ‚‚ β†’β‚›β‚—[σ₂₃] E₃) (f : E β†’β‚›β‚—[σ₁₂] Eβ‚‚) :
p.comp (g.comp f) = (p.comp g).comp f
theorem seminorm.add_comp {π•œ : Type u_3} {π•œβ‚‚ : Type u_4} {E : Type u_7} {Eβ‚‚ : Type u_8} [semi_normed_ring π•œ] [semi_normed_ring π•œβ‚‚] {σ₁₂ : π•œ β†’+* π•œβ‚‚} [ring_hom_isometric σ₁₂] [add_comm_group E] [add_comm_group Eβ‚‚] [module π•œ E] [module π•œβ‚‚ Eβ‚‚] (p q : seminorm π•œβ‚‚ Eβ‚‚) (f : E β†’β‚›β‚—[σ₁₂] Eβ‚‚) :
(p + q).comp f = p.comp f + q.comp f
theorem seminorm.comp_add_le {π•œ : Type u_3} {π•œβ‚‚ : Type u_4} {E : Type u_7} {Eβ‚‚ : Type u_8} [semi_normed_ring π•œ] [semi_normed_ring π•œβ‚‚] {σ₁₂ : π•œ β†’+* π•œβ‚‚} [ring_hom_isometric σ₁₂] [add_comm_group E] [add_comm_group Eβ‚‚] [module π•œ E] [module π•œβ‚‚ Eβ‚‚] (p : seminorm π•œβ‚‚ Eβ‚‚) (f g : E β†’β‚›β‚—[σ₁₂] Eβ‚‚) :
p.comp (f + g) ≀ p.comp f + p.comp g
theorem seminorm.smul_comp {R : Type u_1} {π•œ : Type u_3} {π•œβ‚‚ : Type u_4} {E : Type u_7} {Eβ‚‚ : Type u_8} [semi_normed_ring π•œ] [semi_normed_ring π•œβ‚‚] {σ₁₂ : π•œ β†’+* π•œβ‚‚} [ring_hom_isometric σ₁₂] [add_comm_group E] [add_comm_group Eβ‚‚] [module π•œ E] [module π•œβ‚‚ Eβ‚‚] [has_smul R ℝ] [has_smul R nnreal] [is_scalar_tower R nnreal ℝ] (p : seminorm π•œβ‚‚ Eβ‚‚) (f : E β†’β‚›β‚—[σ₁₂] Eβ‚‚) (c : R) :
(c β€’ p).comp f = c β€’ p.comp f
theorem seminorm.comp_mono {π•œ : Type u_3} {π•œβ‚‚ : Type u_4} {E : Type u_7} {Eβ‚‚ : Type u_8} [semi_normed_ring π•œ] [semi_normed_ring π•œβ‚‚] {σ₁₂ : π•œ β†’+* π•œβ‚‚} [ring_hom_isometric σ₁₂] [add_comm_group E] [add_comm_group Eβ‚‚] [module π•œ E] [module π•œβ‚‚ Eβ‚‚] {p q : seminorm π•œβ‚‚ Eβ‚‚} (f : E β†’β‚›β‚—[σ₁₂] Eβ‚‚) (hp : p ≀ q) :
p.comp f ≀ q.comp f
def seminorm.pullback {π•œ : Type u_3} {π•œβ‚‚ : Type u_4} {E : Type u_7} {Eβ‚‚ : Type u_8} [semi_normed_ring π•œ] [semi_normed_ring π•œβ‚‚] {σ₁₂ : π•œ β†’+* π•œβ‚‚} [ring_hom_isometric σ₁₂] [add_comm_group E] [add_comm_group Eβ‚‚] [module π•œ E] [module π•œβ‚‚ Eβ‚‚] (f : E β†’β‚›β‚—[σ₁₂] Eβ‚‚) :
seminorm π•œβ‚‚ Eβ‚‚ β†’+ seminorm π•œ E

The composition as an add_monoid_hom.

Equations
@[simp]
theorem seminorm.pullback_apply {π•œ : Type u_3} {π•œβ‚‚ : Type u_4} {E : Type u_7} {Eβ‚‚ : Type u_8} [semi_normed_ring π•œ] [semi_normed_ring π•œβ‚‚] {σ₁₂ : π•œ β†’+* π•œβ‚‚} [ring_hom_isometric σ₁₂] [add_comm_group E] [add_comm_group Eβ‚‚] [module π•œ E] [module π•œβ‚‚ Eβ‚‚] (f : E β†’β‚›β‚—[σ₁₂] Eβ‚‚) (p : seminorm π•œβ‚‚ Eβ‚‚) :
@[protected, instance]
def seminorm.order_bot {π•œ : Type u_3} {E : Type u_7} [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_7} [semi_normed_ring π•œ] [add_comm_group E] [module π•œ E] :
theorem seminorm.bot_eq_zero {π•œ : Type u_3} {E : Type u_7} [semi_normed_ring π•œ] [add_comm_group E] [module π•œ E] :
theorem seminorm.smul_le_smul {π•œ : Type u_3} {E : Type u_7} [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_7} {ΞΉ : Type u_12} [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_7} {ΞΉ : Type u_12} [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_7} {ΞΉ : Type u_12} [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_7} {ΞΉ : Type u_12} [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_7} [semi_normed_ring π•œ] [add_comm_group E] [module π•œ E] (p : seminorm π•œ E) (x y : E) :
theorem seminorm.comp_smul {π•œ : Type u_3} {π•œβ‚‚ : Type u_4} {E : Type u_7} {Eβ‚‚ : Type u_8} [semi_normed_ring π•œ] [semi_normed_comm_ring π•œβ‚‚] {σ₁₂ : π•œ β†’+* π•œβ‚‚} [ring_hom_isometric σ₁₂] [add_comm_group E] [add_comm_group Eβ‚‚] [module π•œ E] [module π•œβ‚‚ Eβ‚‚] (p : seminorm π•œβ‚‚ Eβ‚‚) (f : E β†’β‚›β‚—[σ₁₂] Eβ‚‚) (c : π•œβ‚‚) :
theorem seminorm.comp_smul_apply {π•œ : Type u_3} {π•œβ‚‚ : Type u_4} {E : Type u_7} {Eβ‚‚ : Type u_8} [semi_normed_ring π•œ] [semi_normed_comm_ring π•œβ‚‚] {σ₁₂ : π•œ β†’+* π•œβ‚‚} [ring_hom_isometric σ₁₂] [add_comm_group E] [add_comm_group Eβ‚‚] [module π•œ E] [module π•œβ‚‚ Eβ‚‚] (p : seminorm π•œβ‚‚ Eβ‚‚) (f : E β†’β‚›β‚—[σ₁₂] Eβ‚‚) (c : π•œβ‚‚) (x : E) :
theorem seminorm.bdd_below_range_add {π•œ : Type u_3} {E : Type u_7} [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_7} [normed_field π•œ] [add_comm_group E] [module π•œ E] :
has_inf (seminorm π•œ E)
Equations
@[simp]
theorem seminorm.inf_apply {π•œ : Type u_3} {E : Type u_7} [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_7} [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) :
@[protected, instance]
noncomputable def seminorm.has_Sup {π•œ : Type u_3} {E : Type u_7} [normed_field π•œ] [add_comm_group E] [module π•œ E] :
has_Sup (seminorm π•œ E)

We define the supremum of an arbitrary subset of seminorm π•œ E as follows:

  • if s is bdd_above as a set of functions E β†’ ℝ (that is, if s is pointwise bounded above), we take the pointwise supremum of all elements of s, and we prove that it is indeed a seminorm.
  • otherwise, we take the zero seminorm βŠ₯.

There are two things worth mentionning here:

  • First, it is not trivial at first that s being bounded above by a function implies being bounded above as a seminorm. We show this in seminorm.bdd_above_iff by using that the Sup s as defined here is then a bounding seminorm for s. So it is important to make the case disjunction on bdd_above (coe_fn '' s : set (E β†’ ℝ)) and not bdd_above s.
  • Since the pointwise Sup already gives 0 at points where a family of functions is not bounded above, one could hope that just using the pointwise Sup would work here, without the need for an additional case disjunction. As discussed on Zulip, this doesn't work because this can give a function which does not satisfy the seminorm axioms (typically sub-additivity).
Equations
@[protected]
theorem seminorm.coe_Sup_eq' {π•œ : Type u_3} {E : Type u_7} [normed_field π•œ] [add_comm_group E] [module π•œ E] {s : set (seminorm π•œ E)} (hs : bdd_above (coe_fn '' s)) :
@[protected]
theorem seminorm.bdd_above_iff {π•œ : Type u_3} {E : Type u_7} [normed_field π•œ] [add_comm_group E] [module π•œ E] {s : set (seminorm π•œ E)} :
@[protected]
theorem seminorm.coe_Sup_eq {π•œ : Type u_3} {E : Type u_7} [normed_field π•œ] [add_comm_group E] [module π•œ E] {s : set (seminorm π•œ E)} (hs : bdd_above s) :
@[protected]
theorem seminorm.coe_supr_eq {π•œ : Type u_3} {E : Type u_7} [normed_field π•œ] [add_comm_group E] [module π•œ E] {ΞΉ : Type u_1} {p : ΞΉ β†’ seminorm π•œ E} (hp : bdd_above (set.range p)) :
(⇑⨆ (i : ΞΉ), p i) = ⨆ (i : ΞΉ), ⇑(p i)
@[protected, instance]
noncomputable def seminorm.conditionally_complete_lattice {π•œ : Type u_3} {E : Type u_7} [normed_field π•œ] [add_comm_group E] [module π•œ E] :

seminorm π•œ E is a conditionally complete lattice.

Note that, while inf, sup and Sup have good definitional properties (corresponding to seminorm.has_inf, seminorm.has_sup and seminorm.has_Sup respectively), Inf s is just defined as the supremum of the lower bounds of s, which is not really useful in practice. If you need to use Inf on seminorms, then you should probably provide a more workable definition first, but this is unlikely to happen so we keep the "bad" definition for now.

Equations

Seminorm ball #

def seminorm.ball {π•œ : Type u_3} {E : Type u_7} [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
def seminorm.closed_ball {π•œ : Type u_3} {E : Type u_7} [semi_normed_ring π•œ] [add_comm_group E] [has_smul π•œ E] (p : seminorm π•œ E) (x : E) (r : ℝ) :
set E

The closed 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_7} [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
@[simp]
theorem seminorm.mem_closed_ball {π•œ : Type u_3} {E : Type u_7} [semi_normed_ring π•œ] [add_comm_group E] [has_smul π•œ E] (p : seminorm π•œ E) {x y : E} {r : ℝ} :
theorem seminorm.mem_ball_self {π•œ : Type u_3} {E : Type u_7} [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_closed_ball_self {π•œ : Type u_3} {E : Type u_7} [semi_normed_ring π•œ] [add_comm_group E] [has_smul π•œ E] (p : seminorm π•œ E) {x : E} {r : ℝ} (hr : 0 ≀ r) :
theorem seminorm.mem_ball_zero {π•œ : Type u_3} {E : Type u_7} [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.mem_closed_ball_zero {π•œ : Type u_3} {E : Type u_7} [semi_normed_ring π•œ] [add_comm_group E] [has_smul π•œ E] (p : seminorm π•œ E) {y : E} {r : ℝ} :
theorem seminorm.ball_zero_eq {π•œ : Type u_3} {E : Type u_7} [semi_normed_ring π•œ] [add_comm_group E] [has_smul π•œ E] (p : seminorm π•œ E) {r : ℝ} :
p.ball 0 r = {y : E | ⇑p y < r}
theorem seminorm.closed_ball_zero_eq {π•œ : Type u_3} {E : Type u_7} [semi_normed_ring π•œ] [add_comm_group E] [has_smul π•œ E] (p : seminorm π•œ E) {r : ℝ} :
p.closed_ball 0 r = {y : E | ⇑p y ≀ r}
theorem seminorm.ball_subset_closed_ball {π•œ : Type u_3} {E : Type u_7} [semi_normed_ring π•œ] [add_comm_group E] [has_smul π•œ E] (p : seminorm π•œ E) (x : E) (r : ℝ) :
p.ball x r βŠ† p.closed_ball x r
theorem seminorm.closed_ball_eq_bInter_ball {π•œ : Type u_3} {E : Type u_7} [semi_normed_ring π•œ] [add_comm_group E] [has_smul π•œ E] (p : seminorm π•œ E) (x : E) (r : ℝ) :
p.closed_ball x r = β‹‚ (ρ : ℝ) (H : ρ > r), p.ball x ρ
@[simp]
theorem seminorm.ball_zero' {π•œ : Type u_3} {E : Type u_7} [semi_normed_ring π•œ] [add_comm_group E] [has_smul π•œ E] {r : ℝ} (x : E) (hr : 0 < r) :
@[simp]
theorem seminorm.closed_ball_zero' {π•œ : Type u_3} {E : Type u_7} [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_7} [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.closed_ball_smul {π•œ : Type u_3} {E : Type u_7} [semi_normed_ring π•œ] [add_comm_group E] [has_smul π•œ E] (p : seminorm π•œ E) {c : nnreal} (hc : 0 < c) (r : ℝ) (x : E) :
theorem seminorm.ball_sup {π•œ : Type u_3} {E : Type u_7} [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.closed_ball_sup {π•œ : Type u_3} {E : Type u_7} [semi_normed_ring π•œ] [add_comm_group E] [has_smul π•œ E] (p q : seminorm π•œ E) (e : E) (r : ℝ) :
theorem seminorm.ball_finset_sup' {π•œ : Type u_3} {E : Type u_7} {ΞΉ : Type u_12} [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.closed_ball_finset_sup' {π•œ : Type u_3} {E : Type u_7} {ΞΉ : Type u_12} [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).closed_ball e r = s.inf' H (Ξ» (i : ΞΉ), (p i).closed_ball e r)
theorem seminorm.ball_mono {π•œ : Type u_3} {E : Type u_7} [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.closed_ball_mono {π•œ : Type u_3} {E : Type u_7} [semi_normed_ring π•œ] [add_comm_group E] [has_smul π•œ E] {x : E} {p : seminorm π•œ E} {r₁ rβ‚‚ : ℝ} (h : r₁ ≀ rβ‚‚) :
p.closed_ball x r₁ βŠ† p.closed_ball x rβ‚‚
theorem seminorm.ball_antitone {π•œ : Type u_3} {E : Type u_7} [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.closed_ball_antitone {π•œ : Type u_3} {E : Type u_7} [semi_normed_ring π•œ] [add_comm_group E] [has_smul π•œ E] {x : E} {r : ℝ} {p q : seminorm π•œ E} (h : q ≀ p) :
theorem seminorm.ball_add_ball_subset {π•œ : Type u_3} {E : Type u_7} [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.closed_ball_add_closed_ball_subset {π•œ : Type u_3} {E : Type u_7} [semi_normed_ring π•œ] [add_comm_group E] [has_smul π•œ E] (p : seminorm π•œ E) (r₁ rβ‚‚ : ℝ) (x₁ xβ‚‚ : E) :
p.closed_ball x₁ r₁ + p.closed_ball xβ‚‚ rβ‚‚ βŠ† p.closed_ball (x₁ + xβ‚‚) (r₁ + rβ‚‚)
theorem seminorm.sub_mem_ball {π•œ : Type u_3} {E : Type u_7} [semi_normed_ring π•œ] [add_comm_group E] [has_smul π•œ E] (p : seminorm π•œ E) (x₁ xβ‚‚ y : E) (r : ℝ) :
x₁ - xβ‚‚ ∈ p.ball y r ↔ x₁ ∈ p.ball (xβ‚‚ + y) r
theorem seminorm.vadd_ball {π•œ : Type u_3} {E : Type u_7} [semi_normed_ring π•œ] [add_comm_group E] [has_smul π•œ E] {x y : E} {r : ℝ} (p : seminorm π•œ E) :
x +α΅₯ p.ball y r = p.ball (x +α΅₯ y) r

The image of a ball under addition with a singleton is another ball.

theorem seminorm.vadd_closed_ball {π•œ : Type u_3} {E : Type u_7} [semi_normed_ring π•œ] [add_comm_group E] [has_smul π•œ E] {x y : E} {r : ℝ} (p : seminorm π•œ E) :

The image of a closed ball under addition with a singleton is another closed ball.

theorem seminorm.ball_comp {π•œ : Type u_3} {π•œβ‚‚ : Type u_4} {E : Type u_7} {Eβ‚‚ : Type u_8} [semi_normed_ring π•œ] [add_comm_group E] [module π•œ E] [semi_normed_ring π•œβ‚‚] [add_comm_group Eβ‚‚] [module π•œβ‚‚ Eβ‚‚] {σ₁₂ : π•œ β†’+* π•œβ‚‚} [ring_hom_isometric σ₁₂] (p : seminorm π•œβ‚‚ Eβ‚‚) (f : E β†’β‚›β‚—[σ₁₂] Eβ‚‚) (x : E) (r : ℝ) :
(p.comp f).ball x r = ⇑f ⁻¹' p.ball (⇑f x) r
theorem seminorm.closed_ball_comp {π•œ : Type u_3} {π•œβ‚‚ : Type u_4} {E : Type u_7} {Eβ‚‚ : Type u_8} [semi_normed_ring π•œ] [add_comm_group E] [module π•œ E] [semi_normed_ring π•œβ‚‚] [add_comm_group Eβ‚‚] [module π•œβ‚‚ Eβ‚‚] {σ₁₂ : π•œ β†’+* π•œβ‚‚} [ring_hom_isometric σ₁₂] (p : seminorm π•œβ‚‚ Eβ‚‚) (f : E β†’β‚›β‚—[σ₁₂] Eβ‚‚) (x : E) (r : ℝ) :
theorem seminorm.preimage_metric_ball {π•œ : Type u_3} {E : Type u_7} [semi_normed_ring π•œ] [add_comm_group E] [module π•œ E] (p : seminorm π•œ E) {r : ℝ} :
⇑p ⁻¹' metric.ball 0 r = {x : E | ⇑p x < r}
theorem seminorm.preimage_metric_closed_ball {π•œ : Type u_3} {E : Type u_7} [semi_normed_ring π•œ] [add_comm_group E] [module π•œ E] (p : seminorm π•œ E) {r : ℝ} :
theorem seminorm.ball_zero_eq_preimage_ball {π•œ : Type u_3} {E : Type u_7} [semi_normed_ring π•œ] [add_comm_group E] [module π•œ E] (p : seminorm π•œ E) {r : ℝ} :
theorem seminorm.closed_ball_zero_eq_preimage_closed_ball {π•œ : Type u_3} {E : Type u_7} [semi_normed_ring π•œ] [add_comm_group E] [module π•œ E] (p : seminorm π•œ E) {r : ℝ} :
@[simp]
theorem seminorm.ball_bot {π•œ : Type u_3} {E : Type u_7} [semi_normed_ring π•œ] [add_comm_group E] [module π•œ E] {r : ℝ} (x : E) (hr : 0 < r) :
@[simp]
theorem seminorm.closed_ball_bot {π•œ : Type u_3} {E : Type u_7} [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_7} [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.balanced_closed_ball_zero {π•œ : Type u_3} {E : Type u_7} [semi_normed_ring π•œ] [add_comm_group E] [module π•œ E] (p : seminorm π•œ E) (r : ℝ) :
balanced π•œ (p.closed_ball 0 r)

Closed seminorm-balls at the origin are balanced.

theorem seminorm.ball_finset_sup_eq_Inter {π•œ : Type u_3} {E : Type u_7} {ΞΉ : Type u_12} [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.closed_ball_finset_sup_eq_Inter {π•œ : Type u_3} {E : Type u_7} {ΞΉ : Type u_12} [semi_normed_ring π•œ] [add_comm_group E] [module π•œ E] (p : ΞΉ β†’ seminorm π•œ E) (s : finset ΞΉ) (x : E) {r : ℝ} (hr : 0 ≀ r) :
(s.sup p).closed_ball x r = β‹‚ (i : ΞΉ) (H : i ∈ s), (p i).closed_ball x r
theorem seminorm.ball_finset_sup {π•œ : Type u_3} {E : Type u_7} {ΞΉ : Type u_12} [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.closed_ball_finset_sup {π•œ : Type u_3} {E : Type u_7} {ΞΉ : Type u_12} [semi_normed_ring π•œ] [add_comm_group E] [module π•œ E] (p : ΞΉ β†’ seminorm π•œ E) (s : finset ΞΉ) (x : E) {r : ℝ} (hr : 0 ≀ r) :
(s.sup p).closed_ball x r = s.inf (Ξ» (i : ΞΉ), (p i).closed_ball x r)
theorem seminorm.ball_smul_ball {π•œ : Type u_3} {E : Type u_7} [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β‚‚)
theorem seminorm.closed_ball_smul_closed_ball {π•œ : Type u_3} {E : Type u_7} [semi_normed_ring π•œ] [add_comm_group E] [module π•œ E] (p : seminorm π•œ E) (r₁ rβ‚‚ : ℝ) :
metric.closed_ball 0 r₁ β€’ p.closed_ball 0 rβ‚‚ βŠ† p.closed_ball 0 (r₁ * rβ‚‚)
@[simp]
theorem seminorm.ball_eq_emptyset {π•œ : Type u_3} {E : Type u_7} [semi_normed_ring π•œ] [add_comm_group E] [module π•œ E] (p : seminorm π•œ E) {x : E} {r : ℝ} (hr : r ≀ 0) :
p.ball x r = βˆ…
@[simp]
theorem seminorm.closed_ball_eq_emptyset {π•œ : Type u_3} {E : Type u_7} [semi_normed_ring π•œ] [add_comm_group E] [module π•œ E] (p : seminorm π•œ E) {x : E} {r : ℝ} (hr : r < 0) :
theorem seminorm.ball_norm_mul_subset {π•œ : Type u_3} {E : Type u_7} [normed_field π•œ] [add_comm_group E] [module π•œ E] {p : seminorm π•œ E} {k : π•œ} {r : ℝ} :
theorem seminorm.smul_ball_zero {π•œ : Type u_3} {E : Type u_7} [normed_field π•œ] [add_comm_group E] [module π•œ E] {p : seminorm π•œ E} {k : π•œ} {r : ℝ} (hk : k β‰  0) :
k β€’ p.ball 0 r = p.ball 0 (β€–kβ€– * r)
theorem seminorm.smul_closed_ball_subset {π•œ : Type u_3} {E : Type u_7} [normed_field π•œ] [add_comm_group E] [module π•œ E] {p : seminorm π•œ E} {k : π•œ} {r : ℝ} :
theorem seminorm.smul_closed_ball_zero {π•œ : Type u_3} {E : Type u_7} [normed_field π•œ] [add_comm_group E] [module π•œ E] {p : seminorm π•œ E} {k : π•œ} {r : ℝ} (hk : 0 < β€–kβ€–) :
theorem seminorm.ball_zero_absorbs_ball_zero {π•œ : Type u_3} {E : Type u_7} [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_7} [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_closed_ball_zero {π•œ : Type u_3} {E : Type u_7} [normed_field π•œ] [add_comm_group E] [module π•œ E] (p : seminorm π•œ E) {r : ℝ} (hr : 0 < r) :
absorbent π•œ (p.closed_ball 0 r)

Closed seminorm-balls at the origin are absorbent.

@[protected]
theorem seminorm.absorbent_ball {π•œ : Type u_3} {E : Type u_7} [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.

@[protected]
theorem seminorm.absorbent_closed_ball {π•œ : Type u_3} {E : Type u_7} [normed_field π•œ] [add_comm_group E] [module π•œ E] (p : seminorm π•œ E) {r : ℝ} {x : E} (hpr : ⇑p x < r) :
absorbent π•œ (p.closed_ball x r)

Seminorm-balls containing the origin are absorbent.

theorem seminorm.symmetric_ball_zero {π•œ : Type u_3} {E : Type u_7} [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_7} [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_7} [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_7} [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_7} [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.

theorem seminorm.convex_closed_ball {π•œ : Type u_3} {E : Type u_7} [normed_field π•œ] [add_comm_group E] [normed_space ℝ π•œ] [module π•œ E] [module ℝ E] [is_scalar_tower ℝ π•œ E] (p : seminorm π•œ E) (x : E) (r : ℝ) :

Closed seminorm-balls are convex.

@[protected]
def seminorm.restrict_scalars (π•œ : Type u_3) {E : Type u_7} {π•œ' : Type u_13} [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_7} {π•œ' : Type u_13} [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_7} {π•œ' : Type u_13} [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_closed_ball (π•œ : Type u_3) {E : Type u_7} {π•œ' : Type u_13} [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_7} [nontrivially_normed_field π•œ] [add_comm_group E] [module π•œ E] [topological_space E] [has_continuous_const_smul π•œ E] {p : seminorm π•œ E} {r : ℝ} (hr : 0 < r) (hp : p.closed_ball 0 r ∈ nhds 0) :
theorem seminorm.continuous_at_zero {π•œ : Type u_3} {E : Type u_7} [nontrivially_normed_field π•œ] [add_comm_group E] [module π•œ E] [topological_space E] [has_continuous_const_smul π•œ E] {p : seminorm π•œ E} {r : ℝ} (hr : 0 < r) (hp : p.ball 0 r ∈ nhds 0) :
@[protected]
theorem seminorm.uniform_continuous_of_continuous_at_zero {𝕝 : Type u_6} {E : Type u_7} [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_6} {E : Type u_7} [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_7} [nontrivially_normed_field π•œ] [add_comm_group E] [module π•œ E] [uniform_space E] [uniform_add_group E] [has_continuous_const_smul π•œ E] {p : seminorm π•œ E} {r : ℝ} (hr : 0 < r) (hp : p.ball 0 r ∈ nhds 0) :
@[protected]
theorem seminorm.uniform_continuous' {π•œ : Type u_3} {E : Type u_7} [nontrivially_normed_field π•œ] [add_comm_group E] [module π•œ E] [uniform_space E] [uniform_add_group E] [has_continuous_const_smul π•œ E] {p : seminorm π•œ E} {r : ℝ} (hr : 0 < r) (hp : p.closed_ball 0 r ∈ nhds 0) :
@[protected]
theorem seminorm.continuous {π•œ : Type u_3} {E : Type u_7} [nontrivially_normed_field π•œ] [add_comm_group E] [module π•œ E] [topological_space E] [topological_add_group E] [has_continuous_const_smul π•œ E] {p : seminorm π•œ E} {r : ℝ} (hr : 0 < r) (hp : p.ball 0 r ∈ nhds 0) :
@[protected]
theorem seminorm.continuous' {π•œ : Type u_3} {E : Type u_7} [nontrivially_normed_field π•œ] [add_comm_group E] [module π•œ E] [topological_space E] [topological_add_group E] [has_continuous_const_smul π•œ E] {p : seminorm π•œ E} {r : ℝ} (hr : 0 < r) (hp : p.closed_ball 0 r ∈ nhds 0) :
theorem seminorm.continuous_of_le {π•œ : Type u_3} {E : Type u_7} [nontrivially_normed_field π•œ] [add_comm_group E] [module π•œ 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_7) [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_7) [normed_field π•œ] [seminormed_add_comm_group E] [normed_space π•œ E] :
@[simp]
theorem ball_norm_seminorm (π•œ : Type u_3) (E : Type u_7) [normed_field π•œ] [seminormed_add_comm_group E] [normed_space π•œ E] :
theorem absorbent_ball_zero {π•œ : Type u_3} {E : Type u_7} [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_7} [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_7} [normed_field π•œ] [seminormed_add_comm_group E] [normed_space π•œ E] {r : ℝ} :
balanced π•œ (metric.ball 0 r)

Balls at the origin are balanced.