# 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:

- `Seminorm`: A function to the reals that is positive-semidefinite, absolutely homogeneous, and subadditive.
- `normSeminorm 𝕜 E`: The norm on `E` as a seminorm.

## References #

- [H. H. Schaefer, Topological Vector Spaces][schaefer1966]

## Tags #

seminorm, locally convex, LCTVS

source
structure Seminorm (𝕜 : Type u_12) (E : Type u_13) [SeminormedRing 𝕜] [AddGroup E] [SMul 𝕜 E] extends AddGroupSeminorm E :
Type u_13

A seminorm on a module over a normed ring is a function to the reals that is positive semidefinite, positive homogeneous, and subadditive.

- toFun : E → ℝ
- map_zero' : self.toFun 0 = 0
- add_le' (r s : E) : self.toFun (r + s) ≤ self.toFun r + self.toFun s
- neg' (r : E) : self.toFun (-r) = self.toFun r
- smul' (a : 𝕜) (x : E) : self.toFun (a • x) = ‖a‖ * self.toFun x

  The seminorm of a scalar multiplication is the product of the absolute value of the scalar and the original seminorm.

Instances For

source
class SeminormClass (F : Type u_12) (𝕜 : outParam (Type u_13)) (E : outParam (Type u_14)) [SeminormedRing 𝕜] [AddGroup E] [SMul 𝕜 E] [FunLike F E ℝ] extends AddGroupSeminormClass F E ℝ :
Prop

`SeminormClass F 𝕜 E` states that `F` is a type of seminorms on the `𝕜`-module `E`.

You should extend this class when you extend `Seminorm`.

- map_add_le_add (f : F) (a b : E) : f (a + b) ≤ f a + f b
- map_zero (f : F) : f 0 = 0
- map_neg_eq_map (f : F) (a : E) : f (-a) = f a
- map_smul_eq_mul (f : F) (a : 𝕜) (x : E) : f (a • x) = ‖a‖ * f x

  The seminorm of a scalar multiplication is the product of the absolute value of the scalar and the original seminorm.

Instances

source
def Seminorm.of {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddCommGroup 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 `AddCommGroup E` that is a module over a `SeminormedRing 𝕜`.

Equations

- Seminorm.of f add_le smul = { toFun := f, map_zero' := ⋯, add_le' := add_le, neg' := ⋯, smul' := smul }

Instances For

source
def Seminorm.ofSMulLE {𝕜 : Type u_3} {E : Type u_7} [NormedField 𝕜] [AddCommGroup 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

- Seminorm.ofSMulLE f map_zero add_le smul_le = Seminorm.of f add_le ⋯

Instances For

source
instance Seminorm.instFunLike {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddGroup E] [SMul 𝕜 E] :
FunLike (Seminorm 𝕜 E) E ℝ
Equations

- Seminorm.instFunLike = { coe := fun (f : Seminorm 𝕜 E) => f.toFun, coe_injective' := ⋯ }

source
instance Seminorm.instSeminormClass {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddGroup E] [SMul 𝕜 E] :
SeminormClass (Seminorm 𝕜 E) 𝕜 E
source
theorem Seminorm.ext {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddGroup E] [SMul 𝕜 E] {p q : Seminorm 𝕜 E} (h : ∀ (x : E), p x = q x) :
p = q
source
theorem Seminorm.ext_iff {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddGroup E] [SMul 𝕜 E] {p q : Seminorm 𝕜 E} :
p = q ↔ ∀ (x : E), p x = q x
source
instance Seminorm.instZero {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddGroup E] [SMul 𝕜 E] :
Zero (Seminorm 𝕜 E)
Equations

- Seminorm.instZero = { zero := let __src := Zero.zero; { toAddGroupSeminorm := __src, smul' := ⋯ } }

source
@[simp]
theorem Seminorm.coe_zero {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddGroup E] [SMul 𝕜 E] :
⇑0 = 0
source
@[simp]
theorem Seminorm.zero_apply {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddGroup E] [SMul 𝕜 E] (x : E) :
0 x = 0
source
instance Seminorm.instInhabited {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddGroup E] [SMul 𝕜 E] :
Inhabited (Seminorm 𝕜 E)
Equations

- Seminorm.instInhabited = { default := 0 }

source
instance Seminorm.instSMul {R : Type u_1} {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddGroup E] [SMul 𝕜 E] [SMul R ℝ] [SMul R NNReal] [IsScalarTower R NNReal ℝ] :
SMul R (Seminorm 𝕜 E)

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

Equations

- One or more equations did not get rendered due to their size.

source
instance Seminorm.instIsScalarTowerOfReal {R : Type u_1} {R' : Type u_2} {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddGroup E] [SMul 𝕜 E] [SMul R ℝ] [SMul R NNReal] [IsScalarTower R NNReal ℝ] [SMul R' ℝ] [SMul R' NNReal] [IsScalarTower R' NNReal ℝ] [SMul R R'] [IsScalarTower R R' ℝ] :
IsScalarTower R R' (Seminorm 𝕜 E)
source
theorem Seminorm.coe_smul {R : Type u_1} {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddGroup E] [SMul 𝕜 E] [SMul R ℝ] [SMul R NNReal] [IsScalarTower 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_7} [SeminormedRing 𝕜] [AddGroup E] [SMul 𝕜 E] [SMul R ℝ] [SMul R NNReal] [IsScalarTower R NNReal ℝ] (r : R) (p : Seminorm 𝕜 E) (x : E) :
(r • p) x = r • p x
source
instance Seminorm.instAdd {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddGroup E] [SMul 𝕜 E] :
Add (Seminorm 𝕜 E)
Equations

- One or more equations did not get rendered due to their size.

source
theorem Seminorm.coe_add {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddGroup E] [SMul 𝕜 E] (p q : Seminorm 𝕜 E) :
⇑(p + q) = ⇑p + ⇑q
source
@[simp]
theorem Seminorm.add_apply {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddGroup E] [SMul 𝕜 E] (p q : Seminorm 𝕜 E) (x : E) :
(p + q) x = p x + q x
source
instance Seminorm.instAddMonoid {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddGroup E] [SMul 𝕜 E] :
AddMonoid (Seminorm 𝕜 E)
Equations

- Seminorm.instAddMonoid = Function.Injective.addMonoid (fun (f : Seminorm 𝕜 E) => ⇑f) ⋯ ⋯ ⋯ ⋯

source
instance Seminorm.instAddCommMonoid {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddGroup E] [SMul 𝕜 E] :
AddCommMonoid (Seminorm 𝕜 E)
Equations

- Seminorm.instAddCommMonoid = Function.Injective.addCommMonoid (fun (f : Seminorm 𝕜 E) => ⇑f) ⋯ ⋯ ⋯ ⋯

source
instance Seminorm.instPartialOrder {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddGroup E] [SMul 𝕜 E] :
PartialOrder (Seminorm 𝕜 E)
Equations

- Seminorm.instPartialOrder = PartialOrder.lift (fun (f : Seminorm 𝕜 E) => ⇑f) ⋯

source
instance Seminorm.instIsOrderedCancelAddMonoid {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddGroup E] [SMul 𝕜 E] :
IsOrderedCancelAddMonoid (Seminorm 𝕜 E)
source
instance Seminorm.instMulAction {R : Type u_1} {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddGroup E] [SMul 𝕜 E] [Monoid R] [MulAction R ℝ] [SMul R NNReal] [IsScalarTower R NNReal ℝ] :
MulAction R (Seminorm 𝕜 E)
Equations

- Seminorm.instMulAction = Function.Injective.mulAction (fun (f : Seminorm 𝕜 E) => ⇑f) ⋯ ⋯

source
def Seminorm.coeFnAddMonoidHom (𝕜 : Type u_3) (E : Type u_7) [SeminormedRing 𝕜] [AddGroup E] [SMul 𝕜 E] :
Seminorm 𝕜 E →+ E → ℝ

`coeFn` as an `AddMonoidHom`. Helper definition for showing that `Seminorm 𝕜 E` is a module.

Equations

- Seminorm.coeFnAddMonoidHom 𝕜 E = { toFun := DFunLike.coe, map_zero' := ⋯, map_add' := ⋯ }

Instances For

source
@[simp]
theorem Seminorm.coeFnAddMonoidHom_apply (𝕜 : Type u_3) (E : Type u_7) [SeminormedRing 𝕜] [AddGroup E] [SMul 𝕜 E] (a✝ : Seminorm 𝕜 E) (a : E) :
(coeFnAddMonoidHom 𝕜 E) a✝ a = a✝ a
source
theorem Seminorm.coeFnAddMonoidHom_injective (𝕜 : Type u_3) (E : Type u_7) [SeminormedRing 𝕜] [AddGroup E] [SMul 𝕜 E] :
Function.Injective ⇑(coeFnAddMonoidHom 𝕜 E)
source
instance Seminorm.instDistribMulAction {R : Type u_1} {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddGroup E] [SMul 𝕜 E] [Monoid R] [DistribMulAction R ℝ] [SMul R NNReal] [IsScalarTower R NNReal ℝ] :
DistribMulAction R (Seminorm 𝕜 E)
Equations

- Seminorm.instDistribMulAction = Function.Injective.distribMulAction (Seminorm.coeFnAddMonoidHom 𝕜 E) ⋯ ⋯

source
instance Seminorm.instModule {R : Type u_1} {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddGroup E] [SMul 𝕜 E] [Semiring R] [Module R ℝ] [SMul R NNReal] [IsScalarTower R NNReal ℝ] :
Module R (Seminorm 𝕜 E)
Equations

- Seminorm.instModule = Function.Injective.module R (Seminorm.coeFnAddMonoidHom 𝕜 E) ⋯ ⋯

source
instance Seminorm.instSup {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddGroup E] [SMul 𝕜 E] :
Max (Seminorm 𝕜 E)
Equations

- One or more equations did not get rendered due to their size.

source
@[simp]
theorem Seminorm.coe_sup {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddGroup E] [SMul 𝕜 E] (p q : Seminorm 𝕜 E) :
⇑(p ⊔ q) = ⇑p ⊔ ⇑q
source
theorem Seminorm.sup_apply {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddGroup E] [SMul 𝕜 E] (p q : Seminorm 𝕜 E) (x : E) :
(p ⊔ q) x = max (p x) (q x)
source
theorem Seminorm.smul_sup {R : Type u_1} {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddGroup E] [SMul 𝕜 E] [SMul R ℝ] [SMul R NNReal] [IsScalarTower R NNReal ℝ] (r : R) (p q : Seminorm 𝕜 E) :
r • (p ⊔ q) = r • p ⊔ r • q
source
@[simp]
theorem Seminorm.coe_le_coe {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddGroup E] [SMul 𝕜 E] {p q : Seminorm 𝕜 E} :
⇑p ≤ ⇑q ↔ p ≤ q
source
@[simp]
theorem Seminorm.coe_lt_coe {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddGroup E] [SMul 𝕜 E] {p q : Seminorm 𝕜 E} :
⇑p < ⇑q ↔ p < q
source
theorem Seminorm.le_def {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddGroup E] [SMul 𝕜 E] {p q : Seminorm 𝕜 E} :
p ≤ q ↔ ∀ (x : E), p x ≤ q x
source
theorem Seminorm.lt_def {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddGroup E] [SMul 𝕜 E] {p q : Seminorm 𝕜 E} :
p < q ↔ p ≤ q ∧ ∃ (x : E), p x < q x
source
instance Seminorm.instSemilatticeSup {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddGroup E] [SMul 𝕜 E] :
SemilatticeSup (Seminorm 𝕜 E)
Equations

- Seminorm.instSemilatticeSup = Function.Injective.semilatticeSup (fun (f : Seminorm 𝕜 E) => ⇑f) ⋯ ⋯

source
def Seminorm.comp {𝕜 : Type u_3} {𝕜₂ : Type u_4} {E : Type u_7} {E₂ : Type u_8} [SeminormedRing 𝕜] [SeminormedRing 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] [AddCommGroup E] [AddCommGroup 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

- p.comp f = { toFun := fun (x : E) => p (f x), map_zero' := ⋯, add_le' := ⋯, neg' := ⋯, smul' := ⋯ }

Instances For

source
theorem Seminorm.coe_comp {𝕜 : Type u_3} {𝕜₂ : Type u_4} {E : Type u_7} {E₂ : Type u_8} [SeminormedRing 𝕜] [SeminormedRing 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] [AddCommGroup E] [AddCommGroup E₂] [Module 𝕜 E] [Module 𝕜₂ E₂] (p : Seminorm 𝕜₂ E₂) (f : E →ₛₗ[σ₁₂] E₂) :
⇑(p.comp f) = ⇑p ∘ ⇑f
source
@[simp]
theorem Seminorm.comp_apply {𝕜 : Type u_3} {𝕜₂ : Type u_4} {E : Type u_7} {E₂ : Type u_8} [SeminormedRing 𝕜] [SeminormedRing 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] [AddCommGroup E] [AddCommGroup E₂] [Module 𝕜 E] [Module 𝕜₂ E₂] (p : Seminorm 𝕜₂ E₂) (f : E →ₛₗ[σ₁₂] E₂) (x : E) :
(p.comp f) x = p (f x)
source
@[simp]
theorem Seminorm.comp_id {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (p : Seminorm 𝕜 E) :
p.comp LinearMap.id = p
source
@[simp]
theorem Seminorm.comp_zero {𝕜 : Type u_3} {𝕜₂ : Type u_4} {E : Type u_7} {E₂ : Type u_8} [SeminormedRing 𝕜] [SeminormedRing 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] [AddCommGroup E] [AddCommGroup E₂] [Module 𝕜 E] [Module 𝕜₂ E₂] (p : Seminorm 𝕜₂ E₂) :
p.comp 0 = 0
source
@[simp]
theorem Seminorm.zero_comp {𝕜 : Type u_3} {𝕜₂ : Type u_4} {E : Type u_7} {E₂ : Type u_8} [SeminormedRing 𝕜] [SeminormedRing 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] [AddCommGroup E] [AddCommGroup E₂] [Module 𝕜 E] [Module 𝕜₂ E₂] (f : E →ₛₗ[σ₁₂] E₂) :
comp 0 f = 0
source
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} [SeminormedRing 𝕜] [SeminormedRing 𝕜₂] [SeminormedRing 𝕜₃] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] {σ₂₃ : 𝕜₂ →+* 𝕜₃} [RingHomIsometric σ₂₃] {σ₁₃ : 𝕜 →+* 𝕜₃} [RingHomIsometric σ₁₃] [AddCommGroup E] [AddCommGroup E₂] [AddCommGroup E₃] [Module 𝕜 E] [Module 𝕜₂ E₂] [Module 𝕜₃ E₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (p : Seminorm 𝕜₃ E₃) (g : E₂ →ₛₗ[σ₂₃] E₃) (f : E →ₛₗ[σ₁₂] E₂) :
p.comp (g ∘ₛₗ f) = (p.comp g).comp f
source
theorem Seminorm.add_comp {𝕜 : Type u_3} {𝕜₂ : Type u_4} {E : Type u_7} {E₂ : Type u_8} [SeminormedRing 𝕜] [SeminormedRing 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] [AddCommGroup E] [AddCommGroup E₂] [Module 𝕜 E] [Module 𝕜₂ E₂] (p q : Seminorm 𝕜₂ E₂) (f : E →ₛₗ[σ₁₂] E₂) :
(p + q).comp f = p.comp f + q.comp f
source
theorem Seminorm.comp_add_le {𝕜 : Type u_3} {𝕜₂ : Type u_4} {E : Type u_7} {E₂ : Type u_8} [SeminormedRing 𝕜] [SeminormedRing 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] [AddCommGroup E] [AddCommGroup E₂] [Module 𝕜 E] [Module 𝕜₂ E₂] (p : Seminorm 𝕜₂ E₂) (f g : E →ₛₗ[σ₁₂] E₂) :
p.comp (f + g) ≤ p.comp f + p.comp g
source
theorem Seminorm.smul_comp {R : Type u_1} {𝕜 : Type u_3} {𝕜₂ : Type u_4} {E : Type u_7} {E₂ : Type u_8} [SeminormedRing 𝕜] [SeminormedRing 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] [AddCommGroup E] [AddCommGroup E₂] [Module 𝕜 E] [Module 𝕜₂ E₂] [SMul R ℝ] [SMul R NNReal] [IsScalarTower R NNReal ℝ] (p : Seminorm 𝕜₂ E₂) (f : E →ₛₗ[σ₁₂] E₂) (c : R) :
(c • p).comp f = c • p.comp f
source
theorem Seminorm.comp_mono {𝕜 : Type u_3} {𝕜₂ : Type u_4} {E : Type u_7} {E₂ : Type u_8} [SeminormedRing 𝕜] [SeminormedRing 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] [AddCommGroup E] [AddCommGroup E₂] [Module 𝕜 E] [Module 𝕜₂ E₂] {p q : Seminorm 𝕜₂ E₂} (f : E →ₛₗ[σ₁₂] E₂) (hp : p ≤ q) :
p.comp f ≤ q.comp f
source
def Seminorm.pullback {𝕜 : Type u_3} {𝕜₂ : Type u_4} {E : Type u_7} {E₂ : Type u_8} [SeminormedRing 𝕜] [SeminormedRing 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] [AddCommGroup E] [AddCommGroup E₂] [Module 𝕜 E] [Module 𝕜₂ E₂] (f : E →ₛₗ[σ₁₂] E₂) :
Seminorm 𝕜₂ E₂ →+ Seminorm 𝕜 E

The composition as an `AddMonoidHom`.

Equations

- Seminorm.pullback f = { toFun := fun (p : Seminorm 𝕜₂ E₂) => p.comp f, map_zero' := ⋯, map_add' := ⋯ }

Instances For

source
@[simp]
theorem Seminorm.pullback_apply {𝕜 : Type u_3} {𝕜₂ : Type u_4} {E : Type u_7} {E₂ : Type u_8} [SeminormedRing 𝕜] [SeminormedRing 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] [AddCommGroup E] [AddCommGroup E₂] [Module 𝕜 E] [Module 𝕜₂ E₂] (f : E →ₛₗ[σ₁₂] E₂) (p : Seminorm 𝕜₂ E₂) :
(pullback f) p = p.comp f
source
instance Seminorm.instOrderBot {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] :
OrderBot (Seminorm 𝕜 E)
Equations

- Seminorm.instOrderBot = { bot := 0, bot_le := ⋯ }

source
@[simp]
theorem Seminorm.coe_bot {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] :
⇑⊥ = 0
source
theorem Seminorm.bot_eq_zero {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] :
⊥ = 0
source
theorem Seminorm.smul_le_smul {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddCommGroup 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_7} {ι : Type u_11} [SeminormedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (p : ι → Seminorm 𝕜 E) (s : Finset ι) (x : E) :
(s.sup p) x = ↑(s.sup fun (i : ι) => ⟨(p i) x, ⋯⟩)
source
theorem Seminorm.exists_apply_eq_finset_sup {𝕜 : Type u_3} {E : Type u_7} {ι : Type u_11} [SeminormedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (p : ι → Seminorm 𝕜 E) {s : Finset ι} (hs : s.Nonempty) (x : E) :
∃ i ∈ s, (s.sup p) x = (p i) x
source
theorem Seminorm.zero_or_exists_apply_eq_finset_sup {𝕜 : Type u_3} {E : Type u_7} {ι : Type u_11} [SeminormedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (p : ι → Seminorm 𝕜 E) (s : Finset ι) (x : E) :
(s.sup p) x = 0 ∨ ∃ i ∈ s, (s.sup p) x = (p i) x
source
theorem Seminorm.finset_sup_smul {𝕜 : Type u_3} {E : Type u_7} {ι : Type u_11} [SeminormedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (p : ι → Seminorm 𝕜 E) (s : Finset ι) (C : NNReal) :
s.sup (C • p) = C • s.sup p
source
theorem Seminorm.finset_sup_le_sum {𝕜 : Type u_3} {E : Type u_7} {ι : Type u_11} [SeminormedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (p : ι → Seminorm 𝕜 E) (s : Finset ι) :
s.sup p ≤ ∑ i ∈ s, p i
source
theorem Seminorm.finset_sup_apply_le {𝕜 : Type u_3} {E : Type u_7} {ι : Type u_11} [SeminormedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {p : ι → Seminorm 𝕜 E} {s : Finset ι} {x : E} {a : ℝ} (ha : 0 ≤ a) (h : ∀ i ∈ s, (p i) x ≤ a) :
(s.sup p) x ≤ a
source
theorem Seminorm.le_finset_sup_apply {𝕜 : Type u_3} {E : Type u_7} {ι : Type u_11} [SeminormedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {p : ι → Seminorm 𝕜 E} {s : Finset ι} {x : E} {i : ι} (hi : i ∈ s) :
(p i) x ≤ (s.sup p) x
source
theorem Seminorm.finset_sup_apply_lt {𝕜 : Type u_3} {E : Type u_7} {ι : Type u_11} [SeminormedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {p : ι → Seminorm 𝕜 E} {s : Finset ι} {x : E} {a : ℝ} (ha : 0 < a) (h : ∀ 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_7} [SeminormedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (p : Seminorm 𝕜 E) (x y : E) :
‖p x - p y‖ ≤ p (x - y)
source
theorem Seminorm.comp_smul {𝕜 : Type u_3} {𝕜₂ : Type u_4} {E : Type u_7} {E₂ : Type u_8} [SeminormedRing 𝕜] [SeminormedCommRing 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] [AddCommGroup E] [AddCommGroup E₂] [Module 𝕜 E] [Module 𝕜₂ E₂] (p : Seminorm 𝕜₂ E₂) (f : E →ₛₗ[σ₁₂] E₂) (c : 𝕜₂) :
p.comp (c • f) = ‖c‖₊ • p.comp f
source
theorem Seminorm.comp_smul_apply {𝕜 : Type u_3} {𝕜₂ : Type u_4} {E : Type u_7} {E₂ : Type u_8} [SeminormedRing 𝕜] [SeminormedCommRing 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] [AddCommGroup E] [AddCommGroup E₂] [Module 𝕜 E] [Module 𝕜₂ E₂] (p : Seminorm 𝕜₂ E₂) (f : E →ₛₗ[σ₁₂] E₂) (c : 𝕜₂) (x : E) :
(p.comp (c • f)) x = ‖c‖ * p (f x)
source
theorem Seminorm.bddBelow_range_add {𝕜 : Type u_3} {E : Type u_7} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {p q : Seminorm 𝕜 E} {x : E} :
BddBelow (Set.range fun (u : E) => p u + q (x - u))

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

source
noncomputable instance Seminorm.instInf {𝕜 : Type u_3} {E : Type u_7} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] :
Min (Seminorm 𝕜 E)
Equations

- One or more equations did not get rendered due to their size.

source
@[simp]
theorem Seminorm.inf_apply {𝕜 : Type u_3} {E : Type u_7} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] (p q : Seminorm 𝕜 E) (x : E) :
(p ⊓ q) x = ⨅ (u : E), p u + q (x - u)
source
noncomputable instance Seminorm.instLattice {𝕜 : Type u_3} {E : Type u_7} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] :
Lattice (Seminorm 𝕜 E)
Equations

- Seminorm.instLattice = { toSemilatticeSup := Seminorm.instSemilatticeSup, inf := fun (x1 x2 : Seminorm 𝕜 E) => x1 ⊓ x2, inf_le_left := ⋯, inf_le_right := ⋯, le_inf := ⋯ }

source
theorem Seminorm.smul_inf {R : Type u_1} {𝕜 : Type u_3} {E : Type u_7} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [SMul R ℝ] [SMul R NNReal] [IsScalarTower R NNReal ℝ] (r : R) (p q : Seminorm 𝕜 E) :
r • (p ⊓ q) = r • p ⊓ r • q
source
noncomputable instance Seminorm.instSupSet {𝕜 : Type u_3} {E : Type u_7} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] :
SupSet (Seminorm 𝕜 E)

We define the supremum of an arbitrary subset of `Seminorm 𝕜 E` as follows:

- if `s` is `BddAbove` 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 mentioning 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.bddAbove_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 `BddAbove ((↑) '' s : Set (E → ℝ))` and not `BddAbove 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

- One or more equations did not get rendered due to their size.

source
theorem Seminorm.coe_sSup_eq' {𝕜 : Type u_3} {E : Type u_7} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set (Seminorm 𝕜 E)} (hs : BddAbove (DFunLike.coe '' s)) :
⇑(sSup s) = ⨆ (p : ↑s), ⇑↑p
source
theorem Seminorm.bddAbove_iff {𝕜 : Type u_3} {E : Type u_7} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set (Seminorm 𝕜 E)} :
BddAbove s ↔ BddAbove (DFunLike.coe '' s)
source
theorem Seminorm.bddAbove_range_iff {𝕜 : Type u_3} {E : Type u_7} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {ι : Sort u_12} {p : ι → Seminorm 𝕜 E} :
BddAbove (Set.range p) ↔ ∀ (x : E), BddAbove (Set.range fun (i : ι) => (p i) x)
source
theorem Seminorm.coe_sSup_eq {𝕜 : Type u_3} {E : Type u_7} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set (Seminorm 𝕜 E)} (hs : BddAbove s) :
⇑(sSup s) = ⨆ (p : ↑s), ⇑↑p
source
theorem Seminorm.coe_iSup_eq {𝕜 : Type u_3} {E : Type u_7} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {ι : Sort u_12} {p : ι → Seminorm 𝕜 E} (hp : BddAbove (Set.range p)) :
⇑(⨆ (i : ι), p i) = ⨆ (i : ι), ⇑(p i)
source
theorem Seminorm.sSup_apply {𝕜 : Type u_3} {E : Type u_7} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set (Seminorm 𝕜 E)} (hp : BddAbove s) {x : E} :
(sSup s) x = ⨆ (p : ↑s), ↑p x
source
theorem Seminorm.iSup_apply {𝕜 : Type u_3} {E : Type u_7} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {ι : Sort u_12} {p : ι → Seminorm 𝕜 E} (hp : BddAbove (Set.range p)) {x : E} :
(⨆ (i : ι), p i) x = ⨆ (i : ι), (p i) x
source
theorem Seminorm.sSup_empty {𝕜 : Type u_3} {E : Type u_7} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] :
sSup ∅ = ⊥
source
noncomputable instance Seminorm.instConditionallyCompleteLattice {𝕜 : Type u_3} {E : Type u_7} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] :
ConditionallyCompleteLattice (Seminorm 𝕜 E)

`Seminorm 𝕜 E` is a conditionally complete lattice.

Note that, while `inf`, `sup` and `sSup` have good definitional properties (corresponding to the instances given here for `Inf`, `Sup` and `SupSet` respectively), `sInf 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 `sInf` 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.instConditionallyCompleteLattice = conditionallyCompleteLatticeOfLatticeOfsSup (Seminorm 𝕜 E) ⋯

### Seminorm ball #

source
def Seminorm.ball {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddCommGroup E] [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

- p.ball x r = {y : E | p (y - x) < r}

Instances For

source
def Seminorm.closedBall {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddCommGroup E] [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

- p.closedBall x r = {y : E | p (y - x) ≤ r}

Instances For

source
@[simp]
theorem Seminorm.mem_ball {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddCommGroup E] [SMul 𝕜 E] (p : Seminorm 𝕜 E) {x y : E} {r : ℝ} :
y ∈ p.ball x r ↔ p (y - x) < r
source
@[simp]
theorem Seminorm.mem_closedBall {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddCommGroup E] [SMul 𝕜 E] (p : Seminorm 𝕜 E) {x y : E} {r : ℝ} :
y ∈ p.closedBall x r ↔ p (y - x) ≤ r
source
theorem Seminorm.mem_ball_self {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddCommGroup E] [SMul 𝕜 E] (p : Seminorm 𝕜 E) {x : E} {r : ℝ} (hr : 0 < r) :
x ∈ p.ball x r
source
theorem Seminorm.mem_closedBall_self {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddCommGroup E] [SMul 𝕜 E] (p : Seminorm 𝕜 E) {x : E} {r : ℝ} (hr : 0 ≤ r) :
x ∈ p.closedBall x r
source
theorem Seminorm.mem_ball_zero {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddCommGroup E] [SMul 𝕜 E] (p : Seminorm 𝕜 E) {y : E} {r : ℝ} :
y ∈ p.ball 0 r ↔ p y < r
source
theorem Seminorm.mem_closedBall_zero {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddCommGroup E] [SMul 𝕜 E] (p : Seminorm 𝕜 E) {y : E} {r : ℝ} :
y ∈ p.closedBall 0 r ↔ p y ≤ r
source
theorem Seminorm.ball_zero_eq {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddCommGroup E] [SMul 𝕜 E] (p : Seminorm 𝕜 E) {r : ℝ} :
p.ball 0 r = {y : E | p y < r}
source
theorem Seminorm.closedBall_zero_eq {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddCommGroup E] [SMul 𝕜 E] (p : Seminorm 𝕜 E) {r : ℝ} :
p.closedBall 0 r = {y : E | p y ≤ r}
source
theorem Seminorm.ball_subset_closedBall {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddCommGroup E] [SMul 𝕜 E] (p : Seminorm 𝕜 E) (x : E) (r : ℝ) :
p.ball x r ⊆ p.closedBall x r
source
theorem Seminorm.closedBall_eq_biInter_ball {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddCommGroup E] [SMul 𝕜 E] (p : Seminorm 𝕜 E) (x : E) (r : ℝ) :
p.closedBall x r = ⋂ (ρ : ℝ), ⋂ (_ : ρ > r), p.ball x ρ
source
@[simp]
theorem Seminorm.ball_zero' {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddCommGroup E] [SMul 𝕜 E] {r : ℝ} (x : E) (hr : 0 < r) :
ball 0 x r = Set.univ
source
@[simp]
theorem Seminorm.closedBall_zero' {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddCommGroup E] [SMul 𝕜 E] {r : ℝ} (x : E) (hr : 0 < r) :
closedBall 0 x r = Set.univ
source
theorem Seminorm.ball_smul {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddCommGroup E] [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.closedBall_smul {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddCommGroup E] [SMul 𝕜 E] (p : Seminorm 𝕜 E) {c : NNReal} (hc : 0 < c) (r : ℝ) (x : E) :
(c • p).closedBall x r = p.closedBall x (r / ↑c)
source
theorem Seminorm.ball_sup {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddCommGroup E] [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.closedBall_sup {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddCommGroup E] [SMul 𝕜 E] (p q : Seminorm 𝕜 E) (e : E) (r : ℝ) :
(p ⊔ q).closedBall e r = p.closedBall e r ∩ q.closedBall e r
source
theorem Seminorm.ball_finset_sup' {𝕜 : Type u_3} {E : Type u_7} {ι : Type u_11} [SeminormedRing 𝕜] [AddCommGroup E] [SMul 𝕜 E] (p : ι → Seminorm 𝕜 E) (s : Finset ι) (H : s.Nonempty) (e : E) (r : ℝ) :
(s.sup' H p).ball e r = s.inf' H fun (i : ι) => (p i).ball e r
source
theorem Seminorm.closedBall_finset_sup' {𝕜 : Type u_3} {E : Type u_7} {ι : Type u_11} [SeminormedRing 𝕜] [AddCommGroup E] [SMul 𝕜 E] (p : ι → Seminorm 𝕜 E) (s : Finset ι) (H : s.Nonempty) (e : E) (r : ℝ) :
(s.sup' H p).closedBall e r = s.inf' H fun (i : ι) => (p i).closedBall e r
source
theorem Seminorm.ball_mono {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddCommGroup E] [SMul 𝕜 E] {x : E} {p : Seminorm 𝕜 E} {r₁ r₂ : ℝ} (h : r₁ ≤ r₂) :
p.ball x r₁ ⊆ p.ball x r₂
source
theorem Seminorm.closedBall_mono {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddCommGroup E] [SMul 𝕜 E] {x : E} {p : Seminorm 𝕜 E} {r₁ r₂ : ℝ} (h : r₁ ≤ r₂) :
p.closedBall x r₁ ⊆ p.closedBall x r₂
source
theorem Seminorm.ball_antitone {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddCommGroup E] [SMul 𝕜 E] {x : E} {r : ℝ} {p q : Seminorm 𝕜 E} (h : q ≤ p) :
p.ball x r ⊆ q.ball x r
source
theorem Seminorm.closedBall_antitone {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddCommGroup E] [SMul 𝕜 E] {x : E} {r : ℝ} {p q : Seminorm 𝕜 E} (h : q ≤ p) :
p.closedBall x r ⊆ q.closedBall x r
source
theorem Seminorm.ball_add_ball_subset {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddCommGroup E] [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.closedBall_add_closedBall_subset {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddCommGroup E] [SMul 𝕜 E] (p : Seminorm 𝕜 E) (r₁ r₂ : ℝ) (x₁ x₂ : E) :
p.closedBall x₁ r₁ + p.closedBall x₂ r₂ ⊆ p.closedBall (x₁ + x₂) (r₁ + r₂)
source
theorem Seminorm.sub_mem_ball {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddCommGroup E] [SMul 𝕜 E] (p : Seminorm 𝕜 E) (x₁ x₂ y : E) (r : ℝ) :
x₁ - x₂ ∈ p.ball y r ↔ x₁ ∈ p.ball (x₂ + y) r
source
theorem Seminorm.sub_mem_closedBall {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddCommGroup E] [SMul 𝕜 E] (p : Seminorm 𝕜 E) (x₁ x₂ y : E) (r : ℝ) :
x₁ - x₂ ∈ p.closedBall y r ↔ x₁ ∈ p.closedBall (x₂ + y) r
source
theorem Seminorm.vadd_ball {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddCommGroup E] [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.

source
theorem Seminorm.vadd_closedBall {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddCommGroup E] [SMul 𝕜 E] {x y : E} {r : ℝ} (p : Seminorm 𝕜 E) :
x +ᵥ p.closedBall y r = p.closedBall (x +ᵥ y) r

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

source
theorem Seminorm.ball_comp {𝕜 : Type u_3} {𝕜₂ : Type u_4} {E : Type u_7} {E₂ : Type u_8} [SeminormedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [SeminormedRing 𝕜₂] [AddCommGroup E₂] [Module 𝕜₂ E₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (p : Seminorm 𝕜₂ E₂) (f : E →ₛₗ[σ₁₂] E₂) (x : E) (r : ℝ) :
(p.comp f).ball x r = ⇑f ⁻¹' p.ball (f x) r
source
theorem Seminorm.closedBall_comp {𝕜 : Type u_3} {𝕜₂ : Type u_4} {E : Type u_7} {E₂ : Type u_8} [SeminormedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [SeminormedRing 𝕜₂] [AddCommGroup E₂] [Module 𝕜₂ E₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (p : Seminorm 𝕜₂ E₂) (f : E →ₛₗ[σ₁₂] E₂) (x : E) (r : ℝ) :
(p.comp f).closedBall x r = ⇑f ⁻¹' p.closedBall (f x) r
source
theorem Seminorm.preimage_metric_ball {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (p : Seminorm 𝕜 E) {r : ℝ} :
⇑p ⁻¹' Metric.ball 0 r = {x : E | p x < r}
source
theorem Seminorm.preimage_metric_closedBall {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (p : Seminorm 𝕜 E) {r : ℝ} :
⇑p ⁻¹' Metric.closedBall 0 r = {x : E | p x ≤ r}
source
theorem Seminorm.ball_zero_eq_preimage_ball {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (p : Seminorm 𝕜 E) {r : ℝ} :
p.ball 0 r = ⇑p ⁻¹' Metric.ball 0 r
source
theorem Seminorm.closedBall_zero_eq_preimage_closedBall {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (p : Seminorm 𝕜 E) {r : ℝ} :
p.closedBall 0 r = ⇑p ⁻¹' Metric.closedBall 0 r
source
@[simp]
theorem Seminorm.ball_bot {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {r : ℝ} (x : E) (hr : 0 < r) :
⊥.ball x r = Set.univ
source
@[simp]
theorem Seminorm.closedBall_bot {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {r : ℝ} (x : E) (hr : 0 < r) :
⊥.closedBall x r = Set.univ
source
theorem Seminorm.balanced_ball_zero {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (p : Seminorm 𝕜 E) (r : ℝ) :
Balanced 𝕜 (p.ball 0 r)

Seminorm-balls at the origin are balanced.

source
theorem Seminorm.balanced_closedBall_zero {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (p : Seminorm 𝕜 E) (r : ℝ) :
Balanced 𝕜 (p.closedBall 0 r)

Closed seminorm-balls at the origin are balanced.

source
theorem Seminorm.ball_finset_sup_eq_iInter {𝕜 : Type u_3} {E : Type u_7} {ι : Type u_11} [SeminormedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (p : ι → Seminorm 𝕜 E) (s : Finset ι) (x : E) {r : ℝ} (hr : 0 < r) :
(s.sup p).ball x r = ⋂ i ∈ s, (p i).ball x r
source
theorem Seminorm.closedBall_finset_sup_eq_iInter {𝕜 : Type u_3} {E : Type u_7} {ι : Type u_11} [SeminormedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (p : ι → Seminorm 𝕜 E) (s : Finset ι) (x : E) {r : ℝ} (hr : 0 ≤ r) :
(s.sup p).closedBall x r = ⋂ i ∈ s, (p i).closedBall x r
source
theorem Seminorm.ball_finset_sup {𝕜 : Type u_3} {E : Type u_7} {ι : Type u_11} [SeminormedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (p : ι → Seminorm 𝕜 E) (s : Finset ι) (x : E) {r : ℝ} (hr : 0 < r) :
(s.sup p).ball x r = s.inf fun (i : ι) => (p i).ball x r
source
theorem Seminorm.closedBall_finset_sup {𝕜 : Type u_3} {E : Type u_7} {ι : Type u_11} [SeminormedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (p : ι → Seminorm 𝕜 E) (s : Finset ι) (x : E) {r : ℝ} (hr : 0 ≤ r) :
(s.sup p).closedBall x r = s.inf fun (i : ι) => (p i).closedBall x r
source
@[simp]
theorem Seminorm.ball_eq_emptyset {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (p : Seminorm 𝕜 E) {x : E} {r : ℝ} (hr : r ≤ 0) :
p.ball x r = ∅
source
@[simp]
theorem Seminorm.closedBall_eq_emptyset {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (p : Seminorm 𝕜 E) {x : E} {r : ℝ} (hr : r < 0) :
p.closedBall x r = ∅
source
theorem Seminorm.closedBall_smul_ball {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (p : Seminorm 𝕜 E) {r₁ : ℝ} (hr₁ : r₁ ≠ 0) (r₂ : ℝ) :
Metric.closedBall 0 r₁ • p.ball 0 r₂ ⊆ p.ball 0 (r₁ * r₂)
source
theorem Seminorm.ball_smul_closedBall {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (p : Seminorm 𝕜 E) (r₁ : ℝ) {r₂ : ℝ} (hr₂ : r₂ ≠ 0) :
Metric.ball 0 r₁ • p.closedBall 0 r₂ ⊆ p.ball 0 (r₁ * r₂)
source
theorem Seminorm.ball_smul_ball {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (p : Seminorm 𝕜 E) (r₁ r₂ : ℝ) :
Metric.ball 0 r₁ • p.ball 0 r₂ ⊆ p.ball 0 (r₁ * r₂)
source
theorem Seminorm.closedBall_smul_closedBall {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (p : Seminorm 𝕜 E) (r₁ r₂ : ℝ) :
Metric.closedBall 0 r₁ • p.closedBall 0 r₂ ⊆ p.closedBall 0 (r₁ * r₂)
source
theorem Seminorm.neg_mem_ball_zero {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (p : Seminorm 𝕜 E) {r : ℝ} {x : E} :
-x ∈ p.ball 0 r ↔ x ∈ p.ball 0 r
source
theorem Seminorm.neg_mem_closedBall_zero {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (p : Seminorm 𝕜 E) {r : ℝ} {x : E} :
-x ∈ p.closedBall 0 r ↔ x ∈ p.closedBall 0 r
source
@[simp]
theorem Seminorm.neg_ball {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (p : Seminorm 𝕜 E) (r : ℝ) (x : E) :
-p.ball x r = p.ball (-x) r
source
@[simp]
theorem Seminorm.neg_closedBall {𝕜 : Type u_3} {E : Type u_7} [SeminormedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (p : Seminorm 𝕜 E) (r : ℝ) (x : E) :
-p.closedBall x r = p.closedBall (-x) r
source
theorem Seminorm.closedBall_iSup {𝕜 : Type u_3} {E : Type u_7} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {ι : Sort u_12} {p : ι → Seminorm 𝕜 E} (hp : BddAbove (Set.range p)) (e : E) {r : ℝ} (hr : 0 < r) :
(⨆ (i : ι), p i).closedBall e r = ⋂ (i : ι), (p i).closedBall e r
source
theorem Seminorm.ball_norm_mul_subset {𝕜 : Type u_3} {E : Type u_7} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {p : Seminorm 𝕜 E} {k : 𝕜} {r : ℝ} :
p.ball 0 (‖k‖ * r) ⊆ k • p.ball 0 r
source
theorem Seminorm.smul_ball_zero {𝕜 : Type u_3} {E : Type u_7} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {p : Seminorm 𝕜 E} {k : 𝕜} {r : ℝ} (hk : k ≠ 0) :
k • p.ball 0 r = p.ball 0 (‖k‖ * r)
source
theorem Seminorm.smul_closedBall_subset {𝕜 : Type u_3} {E : Type u_7} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {p : Seminorm 𝕜 E} {k : 𝕜} {r : ℝ} :
k • p.closedBall 0 r ⊆ p.closedBall 0 (‖k‖ * r)
source
theorem Seminorm.smul_closedBall_zero {𝕜 : Type u_3} {E : Type u_7} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {p : Seminorm 𝕜 E} {k : 𝕜} {r : ℝ} (hk : 0 < ‖k‖) :
k • p.closedBall 0 r = p.closedBall 0 (‖k‖ * r)
source
theorem Seminorm.ball_zero_absorbs_ball_zero {𝕜 : Type u_3} {E : Type u_7} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] (p : Seminorm 𝕜 E) {r₁ r₂ : ℝ} (hr₁ : 0 < r₁) :
Absorbs 𝕜 (p.ball 0 r₁) (p.ball 0 r₂)
source
theorem Seminorm.absorbent_ball_zero {𝕜 : Type u_3} {E : Type u_7} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] (p : Seminorm 𝕜 E) {r : ℝ} (hr : 0 < r) :
Absorbent 𝕜 (p.ball 0 r)

Seminorm-balls at the origin are absorbent.

source
theorem Seminorm.absorbent_closedBall_zero {𝕜 : Type u_3} {E : Type u_7} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] (p : Seminorm 𝕜 E) {r : ℝ} (hr : 0 < r) :
Absorbent 𝕜 (p.closedBall 0 r)

Closed seminorm-balls at the origin are absorbent.

source
theorem Seminorm.absorbent_ball {𝕜 : Type u_3} {E : Type u_7} [NormedField 𝕜] [AddCommGroup 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.absorbent_closedBall {𝕜 : Type u_3} {E : Type u_7} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] (p : Seminorm 𝕜 E) {r : ℝ} {x : E} (hpr : p x < r) :
Absorbent 𝕜 (p.closedBall x r)

Seminorm-balls containing the origin are absorbent.

source
@[simp]
theorem Seminorm.smul_ball_preimage {𝕜 : Type u_3} {E : Type u_7} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] (p : Seminorm 𝕜 E) (y : E) (r : ℝ) (a : 𝕜) (ha : a ≠ 0) :
(fun (x : E) => a • x) ⁻¹' p.ball y r = p.ball (a⁻¹ • y) (r / ‖a‖)
source
@[simp]
theorem Seminorm.smul_closedBall_preimage {𝕜 : Type u_3} {E : Type u_7} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] (p : Seminorm 𝕜 E) (y : E) (r : ℝ) (a : 𝕜) (ha : a ≠ 0) :
(fun (x : E) => a • x) ⁻¹' p.closedBall y r = p.closedBall (a⁻¹ • y) (r / ‖a‖)
source
theorem Seminorm.convexOn {𝕜 : Type u_3} {E : Type u_7} [NormedField 𝕜] [AddCommGroup E] [NormedSpace ℝ 𝕜] [Module 𝕜 E] [SMul ℝ E] [IsScalarTower ℝ 𝕜 E] (p : Seminorm 𝕜 E) :
ConvexOn ℝ Set.univ ⇑p

A seminorm is convex. Also see `convexOn_norm`.

source
theorem Seminorm.convex_ball {𝕜 : Type u_3} {E : Type u_7} [NormedField 𝕜] [AddCommGroup E] [NormedSpace ℝ 𝕜] [Module 𝕜 E] [Module ℝ E] [IsScalarTower ℝ 𝕜 E] (p : Seminorm 𝕜 E) (x : E) (r : ℝ) :
Convex ℝ (p.ball x r)

Seminorm-balls are convex.

source
theorem Seminorm.convex_closedBall {𝕜 : Type u_3} {E : Type u_7} [NormedField 𝕜] [AddCommGroup E] [NormedSpace ℝ 𝕜] [Module 𝕜 E] [Module ℝ E] [IsScalarTower ℝ 𝕜 E] (p : Seminorm 𝕜 E) (x : E) (r : ℝ) :
Convex ℝ (p.closedBall x r)

Closed seminorm-balls are convex.

source
def Seminorm.restrictScalars (𝕜 : Type u_3) {E : Type u_7} {𝕜' : Type u_12} [NormedField 𝕜] [SeminormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormOneClass 𝕜'] [AddCommGroup E] [Module 𝕜' E] [SMul 𝕜 E] [IsScalarTower 𝕜 𝕜' 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 `RCLike 𝕜'` and `𝕜 = ℝ`.

Equations

- Seminorm.restrictScalars 𝕜 p = { toAddGroupSeminorm := p.toAddGroupSeminorm, smul' := ⋯ }

Instances For

source
@[simp]
theorem Seminorm.coe_restrictScalars (𝕜 : Type u_3) {E : Type u_7} {𝕜' : Type u_12} [NormedField 𝕜] [SeminormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormOneClass 𝕜'] [AddCommGroup E] [Module 𝕜' E] [SMul 𝕜 E] [IsScalarTower 𝕜 𝕜' E] (p : Seminorm 𝕜' E) :
⇑(Seminorm.restrictScalars 𝕜 p) = ⇑p
source
@[simp]
theorem Seminorm.restrictScalars_ball (𝕜 : Type u_3) {E : Type u_7} {𝕜' : Type u_12} [NormedField 𝕜] [SeminormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormOneClass 𝕜'] [AddCommGroup E] [Module 𝕜' E] [SMul 𝕜 E] [IsScalarTower 𝕜 𝕜' E] (p : Seminorm 𝕜' E) :
(Seminorm.restrictScalars 𝕜 p).ball = p.ball
source
@[simp]
theorem Seminorm.restrictScalars_closedBall (𝕜 : Type u_3) {E : Type u_7} {𝕜' : Type u_12} [NormedField 𝕜] [SeminormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormOneClass 𝕜'] [AddCommGroup E] [Module 𝕜' E] [SMul 𝕜 E] [IsScalarTower 𝕜 𝕜' E] (p : Seminorm 𝕜' E) :
(Seminorm.restrictScalars 𝕜 p).closedBall = p.closedBall

### Continuity criteria for seminorms #

source
theorem Seminorm.continuousAt_zero_of_forall' {𝕝 : Type u_6} {E : Type u_7} [SeminormedRing 𝕝] [AddCommGroup E] [Module 𝕝 E] [TopologicalSpace E] {p : Seminorm 𝕝 E} (hp : ∀ r > 0, p.closedBall 0 r ∈ nhds 0) :
ContinuousAt (⇑p) 0

A seminorm is continuous at `0` if `p.closedBall 0 r ∈ 𝓝 0` for all `r > 0`. Over a `NontriviallyNormedField` it is actually enough to check that this is true for some `r`, see `Seminorm.continuousAt_zero'`.

source
theorem Seminorm.continuousAt_zero' {𝕜 : Type u_3} {E : Type u_7} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousConstSMul 𝕜 E] {p : Seminorm 𝕜 E} {r : ℝ} (hp : p.closedBall 0 r ∈ nhds 0) :
ContinuousAt (⇑p) 0
source
theorem Seminorm.continuousAt_zero_of_forall {𝕝 : Type u_6} {E : Type u_7} [SeminormedRing 𝕝] [AddCommGroup E] [Module 𝕝 E] [TopologicalSpace E] {p : Seminorm 𝕝 E} (hp : ∀ r > 0, p.ball 0 r ∈ nhds 0) :
ContinuousAt (⇑p) 0

A seminorm is continuous at `0` if `p.ball 0 r ∈ 𝓝 0` for all `r > 0`. Over a `NontriviallyNormedField` it is actually enough to check that this is true for some `r`, see `Seminorm.continuousAt_zero'`.

source
theorem Seminorm.continuousAt_zero {𝕜 : Type u_3} {E : Type u_7} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousConstSMul 𝕜 E] {p : Seminorm 𝕜 E} {r : ℝ} (hp : p.ball 0 r ∈ nhds 0) :
ContinuousAt (⇑p) 0
source
theorem Seminorm.uniformContinuous_of_continuousAt_zero {𝕝 : Type u_6} {E : Type u_7} [SeminormedRing 𝕝] [AddCommGroup E] [Module 𝕝 E] [UniformSpace E] [IsUniformAddGroup E] {p : Seminorm 𝕝 E} (hp : ContinuousAt (⇑p) 0) :
UniformContinuous ⇑p
source
theorem Seminorm.continuous_of_continuousAt_zero {𝕝 : Type u_6} {E : Type u_7} [SeminormedRing 𝕝] [AddCommGroup E] [Module 𝕝 E] [TopologicalSpace E] [IsTopologicalAddGroup E] {p : Seminorm 𝕝 E} (hp : ContinuousAt (⇑p) 0) :
Continuous ⇑p
source
theorem Seminorm.uniformContinuous_of_forall {𝕝 : Type u_6} {E : Type u_7} [SeminormedRing 𝕝] [AddCommGroup E] [Module 𝕝 E] [UniformSpace E] [IsUniformAddGroup E] {p : Seminorm 𝕝 E} (hp : ∀ r > 0, p.ball 0 r ∈ nhds 0) :
UniformContinuous ⇑p

A seminorm is uniformly continuous if `p.ball 0 r ∈ 𝓝 0` for all `r > 0`. Over a `NontriviallyNormedField` it is actually enough to check that this is true for some `r`, see `Seminorm.uniformContinuous`.

source
theorem Seminorm.uniformContinuous {𝕜 : Type u_3} {E : Type u_7} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [UniformSpace E] [IsUniformAddGroup E] [ContinuousConstSMul 𝕜 E] {p : Seminorm 𝕜 E} {r : ℝ} (hp : p.ball 0 r ∈ nhds 0) :
UniformContinuous ⇑p
source
theorem Seminorm.uniformContinuous_of_forall' {𝕝 : Type u_6} {E : Type u_7} [SeminormedRing 𝕝] [AddCommGroup E] [Module 𝕝 E] [UniformSpace E] [IsUniformAddGroup E] {p : Seminorm 𝕝 E} (hp : ∀ r > 0, p.closedBall 0 r ∈ nhds 0) :
UniformContinuous ⇑p

A seminorm is uniformly continuous if `p.closedBall 0 r ∈ 𝓝 0` for all `r > 0`. Over a `NontriviallyNormedField` it is actually enough to check that this is true for some `r`, see `Seminorm.uniformContinuous'`.

source
theorem Seminorm.uniformContinuous' {𝕜 : Type u_3} {E : Type u_7} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [UniformSpace E] [IsUniformAddGroup E] [ContinuousConstSMul 𝕜 E] {p : Seminorm 𝕜 E} {r : ℝ} (hp : p.closedBall 0 r ∈ nhds 0) :
UniformContinuous ⇑p
source
theorem Seminorm.continuous_of_forall {𝕝 : Type u_6} {E : Type u_7} [SeminormedRing 𝕝] [AddCommGroup E] [Module 𝕝 E] [TopologicalSpace E] [IsTopologicalAddGroup E] {p : Seminorm 𝕝 E} (hp : ∀ r > 0, p.ball 0 r ∈ nhds 0) :
Continuous ⇑p

A seminorm is continuous if `p.ball 0 r ∈ 𝓝 0` for all `r > 0`. Over a `NontriviallyNormedField` it is actually enough to check that this is true for some `r`, see `Seminorm.continuous`.

source
theorem Seminorm.continuous {𝕜 : Type u_3} {E : Type u_7} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {p : Seminorm 𝕜 E} {r : ℝ} (hp : p.ball 0 r ∈ nhds 0) :
Continuous ⇑p
source
theorem Seminorm.continuous_iff {𝕜 : Type u_3} {E : Type u_7} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {p : Seminorm 𝕜 E} {r : ℝ} (hr : 0 < r) :
Continuous ⇑p ↔ p.ball 0 r ∈ nhds 0
source
theorem Seminorm.continuous_of_forall' {𝕝 : Type u_6} {E : Type u_7} [SeminormedRing 𝕝] [AddCommGroup E] [Module 𝕝 E] [TopologicalSpace E] [IsTopologicalAddGroup E] {p : Seminorm 𝕝 E} (hp : ∀ r > 0, p.closedBall 0 r ∈ nhds 0) :
Continuous ⇑p

A seminorm is continuous if `p.closedBall 0 r ∈ 𝓝 0` for all `r > 0`. Over a `NontriviallyNormedField` it is actually enough to check that this is true for some `r`, see `Seminorm.continuous'`.

source
theorem Seminorm.continuous' {𝕜 : Type u_3} {E : Type u_7} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {p : Seminorm 𝕜 E} {r : ℝ} (hp : p.closedBall 0 r ∈ nhds 0) :
Continuous ⇑p
source
theorem Seminorm.continuous_of_le {𝕝 : Type u_6} {E : Type u_7} [SeminormedRing 𝕝] [AddCommGroup E] [Module 𝕝 E] [TopologicalSpace E] [IsTopologicalAddGroup E] {p q : Seminorm 𝕝 E} (hq : Continuous ⇑q) (hpq : p ≤ q) :
Continuous ⇑p
source
theorem Seminorm.ball_mem_nhds {𝕝 : Type u_6} {E : Type u_7} [SeminormedRing 𝕝] [AddCommGroup E] [Module 𝕝 E] [TopologicalSpace E] {p : Seminorm 𝕝 E} (hp : Continuous ⇑p) {r : ℝ} (hr : 0 < r) :
p.ball 0 r ∈ nhds 0
source
theorem Seminorm.uniformSpace_eq_of_hasBasis {𝕜 : Type u_3} {E : Type u_7} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {ι : Sort u_12} [UniformSpace E] [IsUniformAddGroup E] [ContinuousConstSMul 𝕜 E] {p' : ι → Prop} {s : ι → Set E} (p : Seminorm 𝕜 E) (hb : (nhds 0).HasBasis p' s) (h₁ : ∃ (r : ℝ), p.closedBall 0 r ∈ nhds 0) (h₂ : ∀ (i : ι), p' i → ∃ r > 0, p.ball 0 r ⊆ s i) :
inst✝ = PseudoMetricSpace.toUniformSpace
source
theorem Seminorm.uniformity_eq_of_hasBasis {𝕜 : Type u_3} {E : Type u_7} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {ι : Sort u_12} [UniformSpace E] [IsUniformAddGroup E] [ContinuousConstSMul 𝕜 E] {p' : ι → Prop} {s : ι → Set E} (p : Seminorm 𝕜 E) (hb : (nhds 0).HasBasis p' s) (h₁ : ∃ (r : ℝ), p.closedBall 0 r ∈ nhds 0) (h₂ : ∀ (i : ι), p' i → ∃ r > 0, p.ball 0 r ⊆ s i) :
uniformity E = ⨅ (r : ℝ), ⨅ (_ : r > 0), Filter.principal {x : E × E | p (x.1 - x.2) < r}
source
theorem Seminorm.rescale_to_shell_zpow {𝕜 : Type u_3} {E : Type u_7} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] (p : Seminorm 𝕜 E) {c : 𝕜} (hc : 1 < ‖c‖) {ε : ℝ} (εpos : 0 < ε) {x : E} (hx : p x ≠ 0) :
∃ (n : ℤ), c ^ n ≠ 0 ∧ p (c ^ n • x) < ε ∧ ε / ‖c‖ ≤ p (c ^ n • x) ∧ ‖c ^ n‖⁻¹ ≤ ε⁻¹ * ‖c‖ * p x

Let `p` be a seminorm on a vector space over a `NormedField`. If there is a scalar `c` with `‖c‖>1`, then any `x` such that `p x ≠ 0` can be moved by scalar multiplication to any `p`-shell of width `‖c‖`. Also recap information on the value of `p` on the rescaling element that shows up in applications.

source
theorem Seminorm.rescale_to_shell {𝕜 : Type u_3} {E : Type u_7} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] (p : Seminorm 𝕜 E) {c : 𝕜} (hc : 1 < ‖c‖) {ε : ℝ} (εpos : 0 < ε) {x : E} (hx : p x ≠ 0) :
∃ (d : 𝕜), d ≠ 0 ∧ p (d • x) < ε ∧ ε / ‖c‖ ≤ p (d • x) ∧ ‖d‖⁻¹ ≤ ε⁻¹ * ‖c‖ * p x

Let `p` be a seminorm on a vector space over a `NormedField`. If there is a scalar `c` with `‖c‖>1`, then any `x` such that `p x ≠ 0` can be moved by scalar multiplication to any `p`-shell of width `‖c‖`. Also recap information on the value of `p` on the rescaling element that shows up in applications.

source
theorem Seminorm.bound_of_shell {𝕜 : Type u_3} {E : Type u_7} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] (p q : Seminorm 𝕜 E) {ε C : ℝ} (ε_pos : 0 < ε) {c : 𝕜} (hc : 1 < ‖c‖) (hf : ∀ (x : E), ε / ‖c‖ ≤ p x → p x < ε → q x ≤ C * p x) {x : E} (hx : p x ≠ 0) :
q x ≤ C * p x

Let `p` and `q` be two seminorms on a vector space over a `NontriviallyNormedField`. If we have `q x ≤ C * p x` on some shell of the form `{x | ε/‖c‖ ≤ p x < ε}` (where `ε > 0` and `‖c‖ > 1`), then we also have `q x ≤ C * p x` for all `x` such that `p x ≠ 0`.

source
theorem Seminorm.bound_of_shell_smul {𝕜 : Type u_3} {E : Type u_7} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] (p q : Seminorm 𝕜 E) {ε : ℝ} {C : NNReal} (ε_pos : 0 < ε) {c : 𝕜} (hc : 1 < ‖c‖) (hf : ∀ (x : E), ε / ‖c‖ ≤ p x → p x < ε → q x ≤ (C • p) x) {x : E} (hx : p x ≠ 0) :
q x ≤ (C • p) x

A version of `Seminorm.bound_of_shell` expressed using pointwise scalar multiplication of seminorms.

source
theorem Seminorm.bound_of_shell_sup {𝕜 : Type u_3} {E : Type u_7} {ι : Type u_11} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] (p : ι → Seminorm 𝕜 E) (s : Finset ι) (q : Seminorm 𝕜 E) {ε : ℝ} {C : NNReal} (ε_pos : 0 < ε) {c : 𝕜} (hc : 1 < ‖c‖) (hf : ∀ (x : E), (∀ i ∈ s, (p i) x < ε) → ∀ j ∈ s, ε / ‖c‖ ≤ (p j) x → q x ≤ (C • p j) x) {x : E} (hx : ∃ j ∈ s, (p j) x ≠ 0) :
q x ≤ (C • s.sup p) x
source
theorem Seminorm.bddAbove_of_absorbent {𝕜 : Type u_3} {E : Type u_7} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {ι : Sort u_12} {p : ι → Seminorm 𝕜 E} {s : Set E} (hs : Absorbent 𝕜 s) (h : ∀ x ∈ s, BddAbove (Set.range fun (x_1 : ι) => (p x_1) x)) :
BddAbove (Set.range p)

Let `p i` be a family of seminorms on `E`. Let `s` be an absorbent set in `𝕜`. If all seminorms are uniformly bounded at every point of `s`, then they are bounded in the space of seminorms.

### The norm as a seminorm #

source
def normSeminorm (𝕜 : Type u_3) (E : Type u_7) [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] :
Seminorm 𝕜 E

The norm of a seminormed group as a seminorm.

Equations

- normSeminorm 𝕜 E = { toAddGroupSeminorm := normAddGroupSeminorm E, smul' := ⋯ }

Instances For

source
@[simp]
theorem coe_normSeminorm (𝕜 : Type u_3) (E : Type u_7) [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] :
⇑(normSeminorm 𝕜 E) = norm
source
@[simp]
theorem ball_normSeminorm (𝕜 : Type u_3) (E : Type u_7) [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] :
(normSeminorm 𝕜 E).ball = Metric.ball
source
@[simp]
theorem closedBall_normSeminorm (𝕜 : Type u_3) (E : Type u_7) [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] :
(normSeminorm 𝕜 E).closedBall = Metric.closedBall
source
theorem absorbent_ball_zero {𝕜 : Type u_3} {E : Type u_7} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 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_7} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 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_7} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {r : ℝ} :
Balanced 𝕜 (Metric.ball 0 r)

Balls at the origin are balanced.

source
theorem balanced_closedBall_zero {𝕜 : Type u_3} {E : Type u_7} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {r : ℝ} :
Balanced 𝕜 (Metric.closedBall 0 r)

Closed balls at the origin are balanced.

source
theorem rescale_to_shell_semi_normed_zpow {𝕜 : Type u_3} {E : Type u_7} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {c : 𝕜} (hc : 1 < ‖c‖) {ε : ℝ} (εpos : 0 < ε) {x : E} (hx : ‖x‖ ≠ 0) :
∃ (n : ℤ), c ^ n ≠ 0 ∧ ‖c ^ n • x‖ < ε ∧ ε / ‖c‖ ≤ ‖c ^ n • x‖ ∧ ‖c ^ n‖⁻¹ ≤ ε⁻¹ * ‖c‖ * ‖x‖

If there is a scalar `c` with `‖c‖>1`, then any element with nonzero norm can be moved by scalar multiplication to any shell of width `‖c‖`. Also recap information on the norm of the rescaling element that shows up in applications.

source
theorem rescale_to_shell_semi_normed {𝕜 : Type u_3} {E : Type u_7} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {c : 𝕜} (hc : 1 < ‖c‖) {ε : ℝ} (εpos : 0 < ε) {x : E} (hx : ‖x‖ ≠ 0) :
∃ (d : 𝕜), d ≠ 0 ∧ ‖d • x‖ < ε ∧ ε / ‖c‖ ≤ ‖d • x‖ ∧ ‖d‖⁻¹ ≤ ε⁻¹ * ‖c‖ * ‖x‖

If there is a scalar `c` with `‖c‖>1`, then any element with nonzero norm can be moved by scalar multiplication to any shell of width `‖c‖`. Also recap information on the norm of the rescaling element that shows up in applications.

source
theorem rescale_to_shell_zpow {𝕜 : Type u_3} {F : Type u_10} [NormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {c : 𝕜} (hc : 1 < ‖c‖) {ε : ℝ} (εpos : 0 < ε) {x : F} (hx : x ≠ 0) :
∃ (n : ℤ), c ^ n ≠ 0 ∧ ‖c ^ n • x‖ < ε ∧ ε / ‖c‖ ≤ ‖c ^ n • x‖ ∧ ‖c ^ n‖⁻¹ ≤ ε⁻¹ * ‖c‖ * ‖x‖
source
theorem rescale_to_shell {𝕜 : Type u_3} {F : Type u_10} [NormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {c : 𝕜} (hc : 1 < ‖c‖) {ε : ℝ} (εpos : 0 < ε) {x : F} (hx : x ≠ 0) :
∃ (d : 𝕜), d ≠ 0 ∧ ‖d • x‖ < ε ∧ ε / ‖c‖ ≤ ‖d • x‖ ∧ ‖d‖⁻¹ ≤ ε⁻¹ * ‖c‖ * ‖x‖

If there is a scalar `c` with `‖c‖>1`, then any element can be moved by scalar multiplication to any shell of width `‖c‖`. Also recap information on the norm of the rescaling element that shows up in applications.