Seminorms and Local Convexity #
This file defines absorbent sets, balanced sets, seminorms and the Minkowski functional.
An absorbent set is one that "surrounds" the origin. The idea is made precise by requiring that any point belongs to all large enough scalings of the set. This is the vector world analog of a topological neighborhood of the origin.
A balanced set is one that is everywhere around the origin. This means that a • s ⊆ s for all a
of norm less than 1.
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.
The Minkowski functional of a set s is the function which associates each point to how much you
need to scale s for x to be inside it. When s is symmetric, convex and absorbent, its gauge is
a seminorm. Reciprocally, any seminorm arises as the gauge of some set, namely its unit ball. This
induces the equivalence of seminorms and locally convex topological vector spaces.
Main declarations #
For a vector space over a normed field:
absorbent: A setsis absorbent if every point eventually belongs to all large scalings ofs.balanced: A setsis balanced ifa • s ⊆ sfor allaof norm less than1.seminorm: A function to the reals that is positive-semidefinite, absolutely homogeneous, and subadditive.norm_seminorm 𝕜 E: The norm onEas a seminorm.gauge: Aka Minkowksi functional.gauge s xis the least (actually, an infimum)rsuch thatx ∈ r • s.gauge_seminorm: The Minkowski functional as a seminorm, whensis symmetric, convex and absorbent.
References #
TODO #
Define and show equivalence of two notions of local convexity for a topological vector space over ℝ or ℂ: that it has a local base of balanced convex absorbent sets, and that it carries the initial topology induced by a family of seminorms.
Prove the properties of balanced and absorbent sets of a real vector space.
Tags #
absorbent, balanced, seminorm, Minkowski functional, gauge, locally convex, LCTVS
Set Properties #
Absorbent and balanced sets in a vector space over a normed field.
theorem
balanced.union
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[has_scalar 𝕜 E]
{A B : set E}
(hA : balanced 𝕜 A)
(hB : balanced 𝕜 B) :
theorem
balanced.inter
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[add_comm_group E]
[module 𝕜 E]
{A B : set E}
(hA : balanced 𝕜 A)
(hB : balanced 𝕜 B) :
theorem
balanced.add
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[add_comm_group E]
[module 𝕜 E]
{A B : set E}
(hA₁ : balanced 𝕜 A)
(hA₂ : balanced 𝕜 B) :
theorem
absorbs.mono
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[add_comm_group E]
[module 𝕜 E]
{s t u v : set E}
(hs : absorbs 𝕜 s u)
(hst : s ⊆ t)
(hvu : v ⊆ u) :
absorbs 𝕜 t v
theorem
absorbs.mono_left
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[add_comm_group E]
[module 𝕜 E]
{s t u : set E}
(hs : absorbs 𝕜 s u)
(h : s ⊆ t) :
absorbs 𝕜 t u
theorem
absorbs.mono_right
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[add_comm_group E]
[module 𝕜 E]
{s u v : set E}
(hs : absorbs 𝕜 s u)
(h : v ⊆ u) :
absorbs 𝕜 s v
theorem
absorbs.union
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[add_comm_group E]
[module 𝕜 E]
{s u v : set E}
(hu : absorbs 𝕜 s u)
(hv : absorbs 𝕜 s v) :
@[simp]
theorem
absorbs_union
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[add_comm_group E]
[module 𝕜 E]
{s u v : set E} :
theorem
absorbent.subset
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[add_comm_group E]
[module 𝕜 E]
{A B : set E}
(hA : absorbent 𝕜 A)
(hAB : A ⊆ B) :
absorbent 𝕜 B
theorem
absorbent_iff_forall_absorbs_singleton
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[add_comm_group E]
[module 𝕜 E]
{A : set E} :
theorem
absorbent.absorbs
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[add_comm_group E]
[module 𝕜 E]
{s : set E}
(hs : absorbent 𝕜 s)
{x : E} :
absorbs 𝕜 s {x}
theorem
balanced.smul
{𝕜 : Type u_2}
{E : Type u_4}
[normed_comm_ring 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
{A : set E}
(a : 𝕜)
(hA : balanced 𝕜 A) :
theorem
balanced.smul_mono
{𝕜 : Type u_2}
{𝕝 : Type u_3}
{E : Type u_4}
[normed_field 𝕜]
[normed_ring 𝕝]
[normed_space 𝕜 𝕝]
[add_comm_group E]
[module 𝕜 E]
[smul_with_zero 𝕝 E]
[is_scalar_tower 𝕜 𝕝 E]
{s : set E}
(hs : balanced 𝕝 s)
{a : 𝕝}
{b : 𝕜}
(h : ∥a∥ ≤ ∥b∥) :
Scalar multiplication (by possibly different types) of a balanced set is monotone.
theorem
balanced.absorbs_self
{𝕜 : Type u_2}
{E : Type u_4}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
{A : set E}
(hA : balanced 𝕜 A) :
absorbs 𝕜 A A
A balanced set absorbs itself.
theorem
balanced.subset_smul
{𝕜 : Type u_2}
{E : Type u_4}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
{A : set E}
{a : 𝕜}
(hA : balanced 𝕜 A)
(ha : 1 ≤ ∥a∥) :
theorem
balanced.smul_eq
{𝕜 : Type u_2}
{E : Type u_4}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
{A : set E}
{a : 𝕜}
(hA : balanced 𝕜 A)
(ha : ∥a∥ = 1) :
theorem
absorbs.inter
{𝕜 : Type u_2}
{E : Type u_4}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
{s t u : set E}
(hs : absorbs 𝕜 s u)
(ht : absorbs 𝕜 t u) :
@[simp]
theorem
absorbs_inter
{𝕜 : Type u_2}
{E : Type u_4}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
{s t u : set E} :
theorem
absorbent_univ
{𝕜 : Type u_2}
{E : Type u_4}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E] :
Topological vector space #
theorem
absorbent_nhds_zero
{𝕜 : Type u_2}
{E : Type u_4}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
{A : set E}
[topological_space E]
[has_continuous_smul 𝕜 E]
(hA : A ∈ 𝓝 0) :
absorbent 𝕜 A
Every neighbourhood of the origin is absorbent.
theorem
balanced_zero_union_interior
{𝕜 : Type u_2}
{E : Type u_4}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
{A : set E}
[topological_space E]
[has_continuous_smul 𝕜 E]
(hA : balanced 𝕜 A) :
The union of {0} with the interior of a balanced set is balanced.
theorem
balanced.interior
{𝕜 : Type u_2}
{E : Type u_4}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
{A : set E}
[topological_space E]
[has_continuous_smul 𝕜 E]
(hA : balanced 𝕜 A)
(h : 0 ∈ interior A) :
The interior of a balanced set is balanced if it contains the origin.
theorem
balanced.closure
{𝕜 : Type u_2}
{E : Type u_4}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
{A : set E}
[topological_space E]
[has_continuous_smul 𝕜 E]
(hA : balanced 𝕜 A) :
The closure of a balanced set is balanced.
theorem
absorbs_zero_iff
{𝕜 : Type u_2}
{E : Type u_4}
[nondiscrete_normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
{s : set E} :
theorem
absorbent.zero_mem
{𝕜 : Type u_2}
{E : Type u_4}
[nondiscrete_normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
{s : set E}
(hs : absorbent 𝕜 s) :
0 ∈ s
Seminorms #
structure
seminorm
(𝕜 : Type u_9)
(E : Type u_10)
[semi_normed_ring 𝕜]
[add_monoid E]
[has_scalar 𝕜 E] :
Type u_10
- to_fun : E → ℝ
- smul' : ∀ (a : 𝕜) (x : E), self.to_fun (a • x) = ∥a∥ * self.to_fun x
- triangle' : ∀ (x y : E), self.to_fun (x + y) ≤ self.to_fun x + self.to_fun y
A seminorm on a vector space over a normed field is a function to the reals that is positive semidefinite, positive homogeneous, and subadditive.
@[protected, instance]
def
seminorm.fun_like
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[add_monoid E]
[has_scalar 𝕜 E] :
Equations
- seminorm.fun_like = {coe := seminorm.to_fun _inst_3, coe_injective' := _}
@[protected, instance]
def
seminorm.has_coe_to_fun
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[add_monoid E]
[has_scalar 𝕜 E] :
has_coe_to_fun (seminorm 𝕜 E) (λ (_x : seminorm 𝕜 E), E → ℝ)
Helper instance for when there's too many metavariables to apply to_fun.to_coe_fn.
@[ext]
theorem
seminorm.ext
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[add_monoid E]
[has_scalar 𝕜 E]
{p q : seminorm 𝕜 E}
(h : ∀ (x : E), ⇑p x = ⇑q x) :
p = q
@[protected, instance]
def
seminorm.has_zero
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[add_monoid E]
[has_scalar 𝕜 E] :
@[simp]
theorem
seminorm.coe_zero
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[add_monoid E]
[has_scalar 𝕜 E] :
@[simp]
theorem
seminorm.zero_apply
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[add_monoid E]
[has_scalar 𝕜 E]
(x : E) :
@[protected, instance]
def
seminorm.inhabited
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[add_monoid E]
[has_scalar 𝕜 E] :
Equations
- seminorm.inhabited = {default := 0}
@[protected]
theorem
seminorm.smul
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[add_monoid E]
[has_scalar 𝕜 E]
(p : seminorm 𝕜 E)
(c : 𝕜)
(x : E) :
@[protected]
theorem
seminorm.triangle
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[add_monoid E]
[has_scalar 𝕜 E]
(p : seminorm 𝕜 E)
(x y : E) :
@[protected, instance]
def
seminorm.has_scalar
{R : Type u_1}
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[add_monoid E]
[has_scalar 𝕜 E]
[has_scalar R ℝ]
[has_scalar R ℝ≥0]
[is_scalar_tower R ℝ≥0 ℝ] :
has_scalar R (seminorm 𝕜 E)
Any action on ℝ which factors through ℝ≥0 applies to a seminorm.
theorem
seminorm.coe_smul
{R : Type u_1}
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[add_monoid E]
[has_scalar 𝕜 E]
[has_scalar R ℝ]
[has_scalar R ℝ≥0]
[is_scalar_tower R ℝ≥0 ℝ]
(r : R)
(p : seminorm 𝕜 E) :
@[simp]
theorem
seminorm.smul_apply
{R : Type u_1}
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[add_monoid E]
[has_scalar 𝕜 E]
[has_scalar R ℝ]
[has_scalar R ℝ≥0]
[is_scalar_tower R ℝ≥0 ℝ]
(r : R)
(p : seminorm 𝕜 E)
(x : E) :
@[protected, instance]
def
seminorm.has_add
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[add_monoid E]
[has_scalar 𝕜 E] :
theorem
seminorm.coe_add
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[add_monoid E]
[has_scalar 𝕜 E]
(p q : seminorm 𝕜 E) :
@[simp]
theorem
seminorm.add_apply
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[add_monoid E]
[has_scalar 𝕜 E]
(p q : seminorm 𝕜 E)
(x : E) :
@[protected, instance]
def
seminorm.add_monoid
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[add_monoid E]
[has_scalar 𝕜 E] :
add_monoid (seminorm 𝕜 E)
Equations
- seminorm.add_monoid = function.injective.add_monoid_smul coe_fn seminorm.add_monoid._proof_2 seminorm.add_monoid._proof_3 seminorm.coe_add seminorm.add_monoid._proof_4
@[protected, instance]
def
seminorm.ordered_cancel_add_comm_monoid
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[add_monoid E]
[has_scalar 𝕜 E] :
Equations
- seminorm.ordered_cancel_add_comm_monoid = {add := add_monoid.add seminorm.add_monoid, add_assoc := _, add_left_cancel := _, zero := add_monoid.zero seminorm.add_monoid, zero_add := _, add_zero := _, nsmul := has_scalar.smul seminorm.has_scalar, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, le := ordered_cancel_add_comm_monoid.le (function.injective.ordered_cancel_add_comm_monoid coe_fn seminorm.ordered_cancel_add_comm_monoid._proof_9 seminorm.ordered_cancel_add_comm_monoid._proof_10 seminorm.coe_add), lt := ordered_cancel_add_comm_monoid.lt (function.injective.ordered_cancel_add_comm_monoid coe_fn seminorm.ordered_cancel_add_comm_monoid._proof_9 seminorm.ordered_cancel_add_comm_monoid._proof_10 seminorm.coe_add), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, le_of_add_le_add_left := _}
@[protected, instance]
def
seminorm.mul_action
{R : Type u_1}
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[add_monoid E]
[has_scalar 𝕜 E]
[monoid R]
[mul_action R ℝ]
[has_scalar R ℝ≥0]
[is_scalar_tower R ℝ≥0 ℝ] :
mul_action R (seminorm 𝕜 E)
Equations
- seminorm.mul_action = function.injective.mul_action coe_fn seminorm.mul_action._proof_1 seminorm.mul_action._proof_2
def
seminorm.coe_fn_add_monoid_hom
(𝕜 : Type u_2)
(E : Type u_4)
[semi_normed_ring 𝕜]
[add_monoid E]
[has_scalar 𝕜 E] :
coe_fn as an add_monoid_hom. Helper definition for showing that seminorm 𝕜 E is
a module.
Equations
- seminorm.coe_fn_add_monoid_hom 𝕜 E = {to_fun := coe_fn seminorm.has_coe_to_fun, map_zero' := _, map_add' := _}
@[simp]
theorem
seminorm.coe_fn_add_monoid_hom_apply
(𝕜 : Type u_2)
(E : Type u_4)
[semi_normed_ring 𝕜]
[add_monoid E]
[has_scalar 𝕜 E]
(x : seminorm 𝕜 E)
(ᾰ : E) :
⇑(seminorm.coe_fn_add_monoid_hom 𝕜 E) x ᾰ = ⇑x ᾰ
theorem
seminorm.coe_fn_add_monoid_hom_injective
(𝕜 : Type u_2)
(E : Type u_4)
[semi_normed_ring 𝕜]
[add_monoid E]
[has_scalar 𝕜 E] :
@[protected, instance]
def
seminorm.distrib_mul_action
{R : Type u_1}
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[add_monoid E]
[has_scalar 𝕜 E]
[monoid R]
[distrib_mul_action R ℝ]
[has_scalar R ℝ≥0]
[is_scalar_tower R ℝ≥0 ℝ] :
distrib_mul_action R (seminorm 𝕜 E)
Equations
- seminorm.distrib_mul_action = function.injective.distrib_mul_action (seminorm.coe_fn_add_monoid_hom 𝕜 E) _ seminorm.distrib_mul_action._proof_1
@[protected, instance]
def
seminorm.module
{R : Type u_1}
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[add_monoid E]
[has_scalar 𝕜 E]
[semiring R]
[module R ℝ]
[has_scalar R ℝ≥0]
[is_scalar_tower R ℝ≥0 ℝ] :
Equations
- seminorm.module = function.injective.module R (seminorm.coe_fn_add_monoid_hom 𝕜 E) _ seminorm.module._proof_1
@[protected, instance]
noncomputable
def
seminorm.has_sup
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[add_monoid E]
[has_scalar 𝕜 E] :
@[simp]
theorem
seminorm.coe_sup
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[add_monoid E]
[has_scalar 𝕜 E]
(p q : seminorm 𝕜 E) :
@[protected, instance]
def
seminorm.partial_order
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[add_monoid E]
[has_scalar 𝕜 E] :
partial_order (seminorm 𝕜 E)
Equations
- seminorm.partial_order = partial_order.lift coe_fn seminorm.partial_order._proof_1
theorem
seminorm.le_def
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[add_monoid E]
[has_scalar 𝕜 E]
(p q : seminorm 𝕜 E) :
theorem
seminorm.lt_def
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[add_monoid E]
[has_scalar 𝕜 E]
(p q : seminorm 𝕜 E) :
@[protected, instance]
noncomputable
def
seminorm.semilattice_sup
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[add_monoid E]
[has_scalar 𝕜 E] :
semilattice_sup (seminorm 𝕜 E)
Equations
- seminorm.semilattice_sup = function.injective.semilattice_sup coe_fn seminorm.semilattice_sup._proof_1 seminorm.coe_sup
@[protected, simp]
theorem
seminorm.zero
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[add_monoid E]
[smul_with_zero 𝕜 E]
(p : seminorm 𝕜 E) :
def
seminorm.comp
{𝕜 : Type u_2}
{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.
theorem
seminorm.coe_comp
{𝕜 : Type u_2}
{E : Type u_4}
{F : Type u_5}
[semi_normed_ring 𝕜]
[add_comm_group E]
[add_comm_group F]
[module 𝕜 E]
[module 𝕜 F]
(p : seminorm 𝕜 F)
(f : E →ₗ[𝕜] F) :
@[simp]
theorem
seminorm.comp_apply
{𝕜 : Type u_2}
{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) :
@[simp]
theorem
seminorm.comp_id
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[add_comm_group E]
[module 𝕜 E]
(p : seminorm 𝕜 E) :
p.comp linear_map.id = p
@[simp]
theorem
seminorm.comp_zero
{𝕜 : Type u_2}
{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) :
@[simp]
theorem
seminorm.zero_comp
{𝕜 : Type u_2}
{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) :
theorem
seminorm.comp_comp
{𝕜 : Type u_2}
{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) :
theorem
seminorm.add_comp
{𝕜 : Type u_2}
{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) :
theorem
seminorm.comp_triangle
{𝕜 : Type u_2}
{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) :
theorem
seminorm.smul_comp
{R : Type u_1}
{𝕜 : Type u_2}
{E : Type u_4}
{F : Type u_5}
[semi_normed_ring 𝕜]
[add_comm_group E]
[add_comm_group F]
[module 𝕜 E]
[module 𝕜 F]
[has_scalar R ℝ]
[has_scalar R ℝ≥0]
[is_scalar_tower R ℝ≥0 ℝ]
(p : seminorm 𝕜 F)
(f : E →ₗ[𝕜] F)
(c : R) :
theorem
seminorm.comp_mono
{𝕜 : Type u_2}
{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) :
def
seminorm.pullback
{𝕜 : Type u_2}
{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) :
The composition as an add_monoid_hom.
@[simp]
theorem
seminorm.pullback_apply
{𝕜 : Type u_2}
{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
@[protected, simp]
theorem
seminorm.neg
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[add_comm_group E]
[module 𝕜 E]
[norm_one_class 𝕜]
(p : seminorm 𝕜 E)
(x : E) :
@[protected]
theorem
seminorm.sub_le
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[add_comm_group E]
[module 𝕜 E]
[norm_one_class 𝕜]
(p : seminorm 𝕜 E)
(x y : E) :
theorem
seminorm.nonneg
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[add_comm_group E]
[module 𝕜 E]
[norm_one_class 𝕜]
(p : seminorm 𝕜 E)
(x : E) :
theorem
seminorm.sub_rev
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[add_comm_group E]
[module 𝕜 E]
[norm_one_class 𝕜]
(p : seminorm 𝕜 E)
(x y : E) :
@[protected, instance]
def
seminorm.order_bot
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[add_comm_group E]
[module 𝕜 E]
[norm_one_class 𝕜] :
Equations
- seminorm.order_bot = {bot := 0, bot_le := _}
@[simp]
theorem
seminorm.coe_bot
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[add_comm_group E]
[module 𝕜 E]
[norm_one_class 𝕜] :
theorem
seminorm.bot_eq_zero
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[add_comm_group E]
[module 𝕜 E]
[norm_one_class 𝕜] :
theorem
seminorm.smul_le_smul
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[add_comm_group E]
[module 𝕜 E]
[norm_one_class 𝕜]
{p q : seminorm 𝕜 E}
{a b : ℝ≥0}
(hpq : p ≤ q)
(hab : a ≤ b) :
theorem
seminorm.finset_sup_apply
{𝕜 : Type u_2}
{E : Type u_4}
{ι : Type u_7}
[semi_normed_ring 𝕜]
[add_comm_group E]
[module 𝕜 E]
[norm_one_class 𝕜]
(p : ι → seminorm 𝕜 E)
(s : finset ι)
(x : E) :
theorem
seminorm.finset_sup_le_sum
{𝕜 : Type u_2}
{E : Type u_4}
{ι : Type u_7}
[semi_normed_ring 𝕜]
[add_comm_group E]
[module 𝕜 E]
[norm_one_class 𝕜]
(p : ι → seminorm 𝕜 E)
(s : finset ι) :
theorem
seminorm.comp_smul
{𝕜 : Type u_2}
{E : Type u_4}
{F : Type u_5}
[semi_normed_comm_ring 𝕜]
[add_comm_group E]
[add_comm_group F]
[module 𝕜 E]
[module 𝕜 F]
(p : seminorm 𝕜 F)
(f : E →ₗ[𝕜] F)
(c : 𝕜) :
theorem
seminorm.comp_smul_apply
{𝕜 : Type u_2}
{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) :
Seminorm ball #
def
seminorm.ball
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[add_comm_group E]
[has_scalar 𝕜 E]
(p : seminorm 𝕜 E)
(x : E)
(r : ℝ) :
set E
The ball of radius r at x with respect to seminorm p is the set of elements y with
p (y - x) <r`.
@[simp]
theorem
seminorm.mem_ball
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[add_comm_group E]
[has_scalar 𝕜 E]
(p : seminorm 𝕜 E)
{x y : E}
{r : ℝ} :
theorem
seminorm.mem_ball_zero
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[add_comm_group E]
[has_scalar 𝕜 E]
(p : seminorm 𝕜 E)
{y : E}
{r : ℝ} :
theorem
seminorm.ball_zero_eq
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[add_comm_group E]
[has_scalar 𝕜 E]
(p : seminorm 𝕜 E)
{r : ℝ} :
@[simp]
theorem
seminorm.ball_zero'
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[add_comm_group E]
[has_scalar 𝕜 E]
{r : ℝ}
(x : E)
(hr : 0 < r) :
theorem
seminorm.ball_smul
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[add_comm_group E]
[has_scalar 𝕜 E]
(p : seminorm 𝕜 E)
{c : ℝ≥0}
(hc : 0 < c)
(r : ℝ)
(x : E) :
theorem
seminorm.ball_sup
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[add_comm_group E]
[has_scalar 𝕜 E]
(p q : seminorm 𝕜 E)
(e : E)
(r : ℝ) :
theorem
seminorm.ball_finset_sup'
{𝕜 : Type u_2}
{E : Type u_4}
{ι : Type u_7}
[semi_normed_ring 𝕜]
[add_comm_group E]
[has_scalar 𝕜 E]
(p : ι → seminorm 𝕜 E)
(s : finset ι)
(H : s.nonempty)
(e : E)
(r : ℝ) :
theorem
seminorm.ball_mono
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[add_comm_group E]
[has_scalar 𝕜 E]
{x : E}
{p : seminorm 𝕜 E}
{r₁ r₂ : ℝ}
(h : r₁ ≤ r₂) :
theorem
seminorm.ball_antitone
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[add_comm_group E]
[has_scalar 𝕜 E]
{x : E}
{r : ℝ}
{p q : seminorm 𝕜 E}
(h : q ≤ p) :
theorem
seminorm.ball_add_ball_subset
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[add_comm_group E]
[has_scalar 𝕜 E]
(p : seminorm 𝕜 E)
(r₁ r₂ : ℝ)
(x₁ x₂ : E) :
theorem
seminorm.ball_comp
{𝕜 : Type u_2}
{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 : ℝ) :
@[simp]
theorem
seminorm.ball_bot
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[add_comm_group E]
[module 𝕜 E]
[norm_one_class 𝕜]
{r : ℝ}
(x : E)
(hr : 0 < r) :
theorem
seminorm.balanced_ball_zero
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[add_comm_group E]
[module 𝕜 E]
[norm_one_class 𝕜]
(p : seminorm 𝕜 E)
(r : ℝ) :
Seminorm-balls at the origin are balanced.
theorem
seminorm.ball_finset_sup_eq_Inter
{𝕜 : Type u_2}
{E : Type u_4}
{ι : Type u_7}
[semi_normed_ring 𝕜]
[add_comm_group E]
[module 𝕜 E]
[norm_one_class 𝕜]
(p : ι → seminorm 𝕜 E)
(s : finset ι)
(x : E)
{r : ℝ}
(hr : 0 < r) :
theorem
seminorm.ball_finset_sup
{𝕜 : Type u_2}
{E : Type u_4}
{ι : Type u_7}
[semi_normed_ring 𝕜]
[add_comm_group E]
[module 𝕜 E]
[norm_one_class 𝕜]
(p : ι → seminorm 𝕜 E)
(s : finset ι)
(x : E)
{r : ℝ}
(hr : 0 < r) :
theorem
seminorm.ball_smul_ball
{𝕜 : Type u_2}
{E : Type u_4}
[semi_normed_ring 𝕜]
[add_comm_group E]
[module 𝕜 E]
[norm_one_class 𝕜]
(p : seminorm 𝕜 E)
(r₁ r₂ : ℝ) :
@[protected]
theorem
seminorm.absorbent_ball_zero
{𝕜 : Type u_2}
{E : Type u_4}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
(p : seminorm 𝕜 E)
{r : ℝ}
(hr : 0 < r) :
Seminorm-balls at the origin are absorbent.
@[protected]
theorem
seminorm.absorbent_ball
{𝕜 : Type u_2}
{E : Type u_4}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
(p : seminorm 𝕜 E)
{r : ℝ}
{x : E}
(hpr : ⇑p x < r) :
Seminorm-balls containing the origin are absorbent.
theorem
seminorm.symmetric_ball_zero
{𝕜 : Type u_2}
{E : Type u_4}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
(p : seminorm 𝕜 E)
{x : E}
(r : ℝ)
(hx : x ∈ p.ball 0 r) :
@[simp]
theorem
seminorm.neg_ball
{𝕜 : Type u_2}
{E : Type u_4}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
(p : seminorm 𝕜 E)
(r : ℝ)
(x : E) :
@[simp]
theorem
seminorm.smul_ball_preimage
{𝕜 : Type u_2}
{E : Type u_4}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
(p : seminorm 𝕜 E)
(y : E)
(r : ℝ)
(a : 𝕜)
(ha : a ≠ 0) :
@[protected]
theorem
seminorm.convex_on
{𝕜 : Type u_2}
{E : Type u_4}
[normed_linear_ordered_field 𝕜]
[add_comm_group E]
[normed_space ℝ 𝕜]
[module 𝕜 E]
[has_scalar ℝ E]
[is_scalar_tower ℝ 𝕜 E]
(p : seminorm 𝕜 E) :
A seminorm is convex. Also see convex_on_norm.
theorem
seminorm.convex_ball
{𝕜 : Type u_2}
{E : Type u_4}
[normed_linear_ordered_field 𝕜]
[add_comm_group E]
[normed_space ℝ 𝕜]
[module 𝕜 E]
[module ℝ E]
[is_scalar_tower ℝ 𝕜 E]
(p : seminorm 𝕜 E)
(x : E)
(r : ℝ) :
Seminorm-balls are convex.
The norm as a seminorm #
def
norm_seminorm
(𝕜 : Type u_2)
(E : Type u_4)
[normed_field 𝕜]
[semi_normed_group E]
[normed_space 𝕜 E] :
seminorm 𝕜 E
The norm of a seminormed group as a seminorm.
Equations
- norm_seminorm 𝕜 E = {to_fun := norm semi_normed_group.to_has_norm, smul' := _, triangle' := _}
@[simp]
theorem
coe_norm_seminorm
(𝕜 : Type u_2)
(E : Type u_4)
[normed_field 𝕜]
[semi_normed_group E]
[normed_space 𝕜 E] :
⇑(norm_seminorm 𝕜 E) = norm
@[simp]
theorem
ball_norm_seminorm
(𝕜 : Type u_2)
(E : Type u_4)
[normed_field 𝕜]
[semi_normed_group E]
[normed_space 𝕜 E] :
(norm_seminorm 𝕜 E).ball = metric.ball
theorem
absorbent_ball_zero
{𝕜 : Type u_2}
{E : Type u_4}
[normed_field 𝕜]
[semi_normed_group E]
[normed_space 𝕜 E]
{r : ℝ}
(hr : 0 < r) :
absorbent 𝕜 (metric.ball 0 r)
Balls at the origin are absorbent.
theorem
absorbent_ball
{𝕜 : Type u_2}
{E : Type u_4}
[normed_field 𝕜]
[semi_normed_group E]
[normed_space 𝕜 E]
{r : ℝ}
{x : E}
(hx : ∥x∥ < r) :
absorbent 𝕜 (metric.ball x r)
Balls containing the origin are absorbent.
theorem
balanced_ball_zero
{𝕜 : Type u_2}
{E : Type u_4}
[normed_field 𝕜]
[semi_normed_group E]
[normed_space 𝕜 E]
{r : ℝ}
[norm_one_class 𝕜] :
balanced 𝕜 (metric.ball 0 r)
Balls at the origin are balanced.
Minkowksi functional #
The Minkowski functional. Given a set s in a real vector space, gauge s is the functional
which sends x : E to the smallest r : ℝ such that x is in s scaled by r.
theorem
absorbent.gauge_set_nonempty
{E : Type u_4}
[add_comm_group E]
[module ℝ E]
{s : set E}
{x : E}
(absorbs : absorbent ℝ s) :
If the given subset is absorbent then the set we take an infimum over in gauge is nonempty,
which is useful for proving many properties about the gauge.
@[simp]
The gauge evaluated at 0 is always zero (mathematically this requires 0 to be in the set s
but, the real infimum of the empty set in Lean being defined as 0, it holds unconditionally).
theorem
gauge_of_subset_zero
{E : Type u_4}
[add_comm_group E]
[module ℝ E]
{s : set E}
(h : s ⊆ 0) :
The gauge is always nonnegative.
theorem
gauge_le_one_of_mem
{E : Type u_4}
[add_comm_group E]
[module ℝ E]
{s : set E}
{x : E}
(hx : x ∈ s) :
theorem
balanced.star_convex
{E : Type u_4}
[add_comm_group E]
[module ℝ E]
{s : set E}
(hs : balanced ℝ s) :
star_convex ℝ 0 s
theorem
le_gauge_of_not_mem
{E : Type u_4}
[add_comm_group E]
[module ℝ E]
{s : set E}
{a : ℝ}
{x : E}
(hs₀ : star_convex ℝ 0 s)
(hs₂ : absorbs ℝ s {x})
(hx : x ∉ a • s) :
theorem
one_le_gauge_of_not_mem
{E : Type u_4}
[add_comm_group E]
[module ℝ E]
{s : set E}
{x : E}
(hs₁ : star_convex ℝ 0 s)
(hs₂ : absorbs ℝ s {x})
(hx : x ∉ s) :
theorem
gauge_smul_of_nonneg
{E : Type u_4}
[add_comm_group E]
[module ℝ E]
{α : Type u_9}
[linear_ordered_field α]
[mul_action_with_zero α ℝ]
[ordered_smul α ℝ]
[mul_action_with_zero α E]
[is_scalar_tower α ℝ (set E)]
{s : set E}
{r : α}
(hr : 0 ≤ r)
(x : E) :
theorem
gauge_smul
{E : Type u_4}
[add_comm_group E]
[module ℝ E]
{α : Type u_9}
[linear_ordered_field α]
[mul_action_with_zero α ℝ]
[ordered_smul α ℝ]
[module α E]
[is_scalar_tower α ℝ (set E)]
{s : set E}
(symmetric : ∀ (x : E), x ∈ s → -x ∈ s)
(r : α)
(x : E) :
In textbooks, this is the homogeneity of the Minkowksi functional.
theorem
gauge_smul_left_of_nonneg
{E : Type u_4}
[add_comm_group E]
[module ℝ E]
{α : Type u_9}
[linear_ordered_field α]
[mul_action_with_zero α ℝ]
[ordered_smul α ℝ]
[mul_action_with_zero α E]
[smul_comm_class α ℝ ℝ]
[is_scalar_tower α ℝ ℝ]
[is_scalar_tower α ℝ E]
{s : set E}
{a : α}
(ha : 0 ≤ a) :
theorem
gauge_smul_left
{E : Type u_4}
[add_comm_group E]
[module ℝ E]
{α : Type u_9}
[linear_ordered_field α]
[mul_action_with_zero α ℝ]
[ordered_smul α ℝ]
[module α E]
[smul_comm_class α ℝ ℝ]
[is_scalar_tower α ℝ ℝ]
[is_scalar_tower α ℝ E]
{s : set E}
(symmetric : ∀ (x : E), x ∈ s → -x ∈ s)
(a : α) :
theorem
interior_subset_gauge_lt_one
{E : Type u_4}
[add_comm_group E]
[module ℝ E]
[topological_space E]
[has_continuous_smul ℝ E]
(s : set E) :
theorem
gauge_lt_one_eq_self_of_open
{E : Type u_4}
[add_comm_group E]
[module ℝ E]
{s : set E}
[topological_space E]
[has_continuous_smul ℝ E]
(hs₁ : convex ℝ s)
(hs₀ : 0 ∈ s)
(hs₂ : is_open s) :
theorem
gauge_lt_one_of_mem_of_open
{E : Type u_4}
[add_comm_group E]
[module ℝ E]
{s : set E}
[topological_space E]
[has_continuous_smul ℝ E]
(hs₁ : convex ℝ s)
(hs₀ : 0 ∈ s)
(hs₂ : is_open s)
{x : E}
(hx : x ∈ s) :
theorem
gauge_lt_of_mem_smul
{E : Type u_4}
[add_comm_group E]
[module ℝ E]
{s : set E}
[topological_space E]
[has_continuous_smul ℝ E]
(x : E)
(ε : ℝ)
(hε : 0 < ε)
(hs₀ : 0 ∈ s)
(hs₁ : convex ℝ s)
(hs₂ : is_open s)
(hx : x ∈ ε • s) :
theorem
gauge_seminorm_lt_one_of_open
{E : Type u_4}
[add_comm_group E]
[module ℝ E]
{s : set E}
{hs₀ : ∀ (x : E), x ∈ s → -x ∈ s}
{hs₁ : convex ℝ s}
{hs₂ : absorbent ℝ s}
[topological_space E]
[has_continuous_smul ℝ E]
(hs : is_open s)
{x : E}
(hx : x ∈ s) :
⇑(gauge_seminorm hs₀ hs₁ hs₂) x < 1
theorem
seminorm.gauge_seminorm_ball
{E : Type u_4}
[add_comm_group E]
[module ℝ E]
(p : seminorm ℝ E) :
gauge_seminorm _ _ _ = p
theorem
gauge_unit_ball
{E : Type u_4}
[semi_normed_group E]
[normed_space ℝ E]
(x : E) :
gauge (metric.ball 0 1) x = ∥x∥
theorem
smul_unit_ball
{E : Type u_4}
[semi_normed_group E]
[normed_space ℝ E]
{r : ℝ}
(hr : 0 < r) :
r • metric.ball 0 1 = metric.ball 0 r
theorem
gauge_ball
{E : Type u_4}
[semi_normed_group E]
[normed_space ℝ E]
{r : ℝ}
(hr : 0 < r)
(x : E) :
theorem
mul_gauge_le_norm
{E : Type u_4}
[semi_normed_group E]
[normed_space ℝ E]
{s : set E}
{r : ℝ}
{x : E}
(hs : metric.ball 0 r ⊆ s) :
Topology induced by a family of seminorms #
def
seminorm.seminorm_basis_zero
{𝕜 : Type u_2}
{E : Type u_4}
{ι : Type u_7}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
(p : ι → seminorm 𝕜 E) :
A filter basis for the neighborhood filter of 0.
theorem
seminorm.seminorm_basis_zero_iff
{𝕜 : Type u_2}
{E : Type u_4}
{ι : Type u_7}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
(p : ι → seminorm 𝕜 E)
(U : set E) :
theorem
seminorm.seminorm_basis_zero_mem
{𝕜 : Type u_2}
{E : Type u_4}
{ι : Type u_7}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
(p : ι → seminorm 𝕜 E)
(i : finset ι)
{r : ℝ}
(hr : 0 < r) :
(i.sup p).ball 0 r ∈ seminorm.seminorm_basis_zero p
theorem
seminorm.seminorm_basis_zero_singleton_mem
{𝕜 : Type u_2}
{E : Type u_4}
{ι : Type u_7}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
(p : ι → seminorm 𝕜 E)
(i : ι)
{r : ℝ}
(hr : 0 < r) :
(p i).ball 0 r ∈ seminorm.seminorm_basis_zero p
theorem
seminorm.seminorm_basis_zero_nonempty
{𝕜 : Type u_2}
{E : Type u_4}
{ι : Type u_7}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
(p : ι → seminorm 𝕜 E)
[nonempty ι] :
theorem
seminorm.seminorm_basis_zero_intersect
{𝕜 : Type u_2}
{E : Type u_4}
{ι : Type u_7}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
(p : ι → seminorm 𝕜 E)
(U V : set E)
(hU : U ∈ seminorm.seminorm_basis_zero p)
(hV : V ∈ seminorm.seminorm_basis_zero p) :
∃ (z : set E) (H : z ∈ seminorm.seminorm_basis_zero p), z ⊆ U ∩ V
theorem
seminorm.seminorm_basis_zero_zero
{𝕜 : Type u_2}
{E : Type u_4}
{ι : Type u_7}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
(p : ι → seminorm 𝕜 E)
(U : set E)
(hU : U ∈ seminorm.seminorm_basis_zero p) :
0 ∈ U
theorem
seminorm.seminorm_basis_zero_add
{𝕜 : Type u_2}
{E : Type u_4}
{ι : Type u_7}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
(p : ι → seminorm 𝕜 E)
(U : set E)
(hU : U ∈ seminorm.seminorm_basis_zero p) :
∃ (V : set E) (H : V ∈ seminorm.seminorm_basis_zero p), V + V ⊆ U
theorem
seminorm.seminorm_basis_zero_neg
{𝕜 : Type u_2}
{E : Type u_4}
{ι : Type u_7}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
(p : ι → seminorm 𝕜 E)
(U : set E)
(hU' : U ∈ seminorm.seminorm_basis_zero p) :
def
seminorm.seminorm_add_group_filter_basis
{𝕜 : Type u_2}
{E : Type u_4}
{ι : Type u_7}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
[nonempty ι]
(p : ι → seminorm 𝕜 E) :
The add_group_filter_basis induced by the filter basis seminorm_basis_zero.
Equations
theorem
seminorm.seminorm_basis_zero_smul_right
{𝕜 : Type u_2}
{E : Type u_4}
{ι : Type u_7}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
(p : ι → seminorm 𝕜 E)
(v : E)
(U : set E)
(hU : U ∈ seminorm.seminorm_basis_zero p) :
theorem
seminorm.seminorm_basis_zero_smul
{𝕜 : Type u_2}
{E : Type u_4}
{ι : Type u_7}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
[nonempty ι]
(p : ι → seminorm 𝕜 E)
(U : set E)
(hU : U ∈ seminorm.seminorm_basis_zero p) :
theorem
seminorm.seminorm_basis_zero_smul_left
{𝕜 : Type u_2}
{E : Type u_4}
{ι : Type u_7}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
[nonempty ι]
(p : ι → seminorm 𝕜 E)
(x : 𝕜)
(U : set E)
(hU : U ∈ seminorm.seminorm_basis_zero p) :
def
seminorm.seminorm_module_filter_basis
{𝕜 : Type u_2}
{E : Type u_4}
{ι : Type u_7}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
[nonempty ι]
(p : ι → seminorm 𝕜 E) :
The module_filter_basis induced by the filter basis seminorm_basis_zero.
Equations
def
seminorm.is_bounded
{𝕜 : Type u_2}
{E : Type u_4}
{F : Type u_5}
{ι : Type u_7}
{ι' : Type u_8}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
[add_comm_group F]
[module 𝕜 F]
(p : ι → seminorm 𝕜 E)
(q : ι' → seminorm 𝕜 F)
(f : E →ₗ[𝕜] F) :
Prop
The proposition that a linear map is bounded between spaces with families of seminorms.
theorem
seminorm.is_bounded_const
{𝕜 : Type u_2}
{E : Type u_4}
{F : Type u_5}
{ι : Type u_7}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
[add_comm_group F]
[module 𝕜 F]
(ι' : Type u_1)
[nonempty ι']
{p : ι → seminorm 𝕜 E}
{q : seminorm 𝕜 F}
(f : E →ₗ[𝕜] F) :
theorem
seminorm.const_is_bounded
{𝕜 : Type u_2}
{E : Type u_4}
{F : Type u_5}
{ι' : Type u_8}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
[add_comm_group F]
[module 𝕜 F]
(ι : Type u_1)
[nonempty ι]
{p : seminorm 𝕜 E}
{q : ι' → seminorm 𝕜 F}
(f : E →ₗ[𝕜] F) :
theorem
seminorm.is_bounded_sup
{𝕜 : Type u_2}
{E : Type u_4}
{F : Type u_5}
{ι : Type u_7}
{ι' : Type u_8}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
[add_comm_group F]
[module 𝕜 F]
{p : ι → seminorm 𝕜 E}
{q : ι' → seminorm 𝕜 F}
{f : E →ₗ[𝕜] F}
(hf : seminorm.is_bounded p q f)
(s' : finset ι') :
@[class]
structure
seminorm.with_seminorms
{𝕜 : Type u_2}
{E : Type u_4}
{ι : Type u_7}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
[nonempty ι]
(p : ι → seminorm 𝕜 E)
[t : topological_space E] :
Prop
- topology_eq_with_seminorms : t = (seminorm.seminorm_module_filter_basis p).topology
The proposition that the topology of E is induced by a family of seminorms p.
Instances
theorem
seminorm.with_seminorms_eq
{𝕜 : Type u_2}
{E : Type u_4}
{ι : Type u_7}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
[nonempty ι]
(p : ι → seminorm 𝕜 E)
[t : topological_space E]
[seminorm.with_seminorms p] :
@[protected, instance]
def
seminorm.norm_with_seminorms
(𝕜 : Type u_1)
(E : Type u_2)
[normed_field 𝕜]
[semi_normed_group E]
[normed_space 𝕜 E] :
seminorm.with_seminorms (λ (_x : fin 1), norm_seminorm 𝕜 E)
The topology of a normed_space 𝕜 E is induced by the seminorm norm_seminorm 𝕜 E.
theorem
seminorm.continuous_from_bounded
{𝕜 : Type u_2}
{E : Type u_4}
{F : Type u_5}
{ι : Type u_7}
{ι' : Type u_8}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
[add_comm_group F]
[module 𝕜 F]
[nonempty ι]
[nonempty ι']
(p : ι → seminorm 𝕜 E)
(q : ι' → seminorm 𝕜 F)
[uniform_space E]
[uniform_add_group E]
[seminorm.with_seminorms p]
[uniform_space F]
[uniform_add_group F]
[seminorm.with_seminorms q]
(f : E →ₗ[𝕜] F)
(hf : seminorm.is_bounded p q f) :
theorem
seminorm.cont_with_seminorms_normed_space
{𝕜 : Type u_2}
{E : Type u_4}
{ι : Type u_7}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
[nonempty ι]
(F : Type u_1)
[semi_normed_group F]
[normed_space 𝕜 F]
[uniform_space E]
[uniform_add_group E]
(p : ι → seminorm 𝕜 E)
[seminorm.with_seminorms p]
(f : E →ₗ[𝕜] F)
(hf : ∃ (s : finset ι) (C : ℝ≥0), C ≠ 0 ∧ (norm_seminorm 𝕜 F).comp f ≤ C • s.sup p) :
theorem
seminorm.cont_normed_space_to_with_seminorms
{𝕜 : Type u_2}
{F : Type u_5}
{ι : Type u_7}
[normed_field 𝕜]
[add_comm_group F]
[module 𝕜 F]
[nonempty ι]
(E : Type u_1)
[semi_normed_group E]
[normed_space 𝕜 E]
[uniform_space F]
[uniform_add_group F]
(q : ι → seminorm 𝕜 F)
[seminorm.with_seminorms q]
(f : E →ₗ[𝕜] F)
(hf : ∀ (i : ι), ∃ (C : ℝ≥0), C ≠ 0 ∧ (q i).comp f ≤ C • norm_seminorm 𝕜 E) :