mathlib documentation

analysis.locally_convex.with_seminorms

Topology induced by a family of seminorms #

Main definitions #

Main statements #

TODO #

Show that for any locally convex space there exist seminorms that induce the topology.

Tags #

seminorm, locally convex

@[reducible]
def seminorm_family (π•œ : Type u_1) (E : Type u_2) (ΞΉ : Type u_5) [normed_field π•œ] [add_comm_group E] [module π•œ E] :
Type (max u_5 u_2)

An abbreviation for indexed families of seminorms. This is mainly to allow for dot-notation.

def seminorm_family.basis_sets {π•œ : Type u_1} {E : Type u_2} {ΞΉ : Type u_5} [normed_field π•œ] [add_comm_group E] [module π•œ E] (p : seminorm_family π•œ E ΞΉ) :
set (set E)

The sets of a filter basis for the neighborhood filter of 0.

Equations
theorem seminorm_family.basis_sets_iff {π•œ : Type u_1} {E : Type u_2} {ΞΉ : Type u_5} [normed_field π•œ] [add_comm_group E] [module π•œ E] (p : seminorm_family π•œ E ΞΉ) {U : set E} :
U ∈ p.basis_sets ↔ βˆƒ (i : finset ΞΉ) (r : ℝ) (hr : 0 < r), U = (i.sup p).ball 0 r
theorem seminorm_family.basis_sets_mem {π•œ : Type u_1} {E : Type u_2} {ΞΉ : Type u_5} [normed_field π•œ] [add_comm_group E] [module π•œ E] (p : seminorm_family π•œ E ΞΉ) (i : finset ΞΉ) {r : ℝ} (hr : 0 < r) :
theorem seminorm_family.basis_sets_singleton_mem {π•œ : Type u_1} {E : Type u_2} {ΞΉ : Type u_5} [normed_field π•œ] [add_comm_group E] [module π•œ E] (p : seminorm_family π•œ E ΞΉ) (i : ΞΉ) {r : ℝ} (hr : 0 < r) :
(p i).ball 0 r ∈ p.basis_sets
theorem seminorm_family.basis_sets_nonempty {π•œ : Type u_1} {E : Type u_2} {ΞΉ : Type u_5} [normed_field π•œ] [add_comm_group E] [module π•œ E] (p : seminorm_family π•œ E ΞΉ) [nonempty ΞΉ] :
theorem seminorm_family.basis_sets_intersect {π•œ : Type u_1} {E : Type u_2} {ΞΉ : Type u_5} [normed_field π•œ] [add_comm_group E] [module π•œ E] (p : seminorm_family π•œ E ΞΉ) (U V : set E) (hU : U ∈ p.basis_sets) (hV : V ∈ p.basis_sets) :
βˆƒ (z : set E) (H : z ∈ p.basis_sets), z βŠ† U ∩ V
theorem seminorm_family.basis_sets_zero {π•œ : Type u_1} {E : Type u_2} {ΞΉ : Type u_5} [normed_field π•œ] [add_comm_group E] [module π•œ E] (p : seminorm_family π•œ E ΞΉ) (U : set E) (hU : U ∈ p.basis_sets) :
0 ∈ U
theorem seminorm_family.basis_sets_add {π•œ : Type u_1} {E : Type u_2} {ΞΉ : Type u_5} [normed_field π•œ] [add_comm_group E] [module π•œ E] (p : seminorm_family π•œ E ΞΉ) (U : set E) (hU : U ∈ p.basis_sets) :
βˆƒ (V : set E) (H : V ∈ p.basis_sets), V + V βŠ† U
theorem seminorm_family.basis_sets_neg {π•œ : Type u_1} {E : Type u_2} {ΞΉ : Type u_5} [normed_field π•œ] [add_comm_group E] [module π•œ E] (p : seminorm_family π•œ E ΞΉ) (U : set E) (hU' : U ∈ p.basis_sets) :
βˆƒ (V : set E) (H : V ∈ p.basis_sets), V βŠ† (Ξ» (x : E), -x) ⁻¹' U
@[protected]
def seminorm_family.add_group_filter_basis {π•œ : Type u_1} {E : Type u_2} {ΞΉ : Type u_5} [normed_field π•œ] [add_comm_group E] [module π•œ E] (p : seminorm_family π•œ E ΞΉ) [nonempty ΞΉ] :

The add_group_filter_basis induced by the filter basis seminorm_basis_zero.

Equations
theorem seminorm_family.basis_sets_smul_right {π•œ : Type u_1} {E : Type u_2} {ΞΉ : Type u_5} [normed_field π•œ] [add_comm_group E] [module π•œ E] (p : seminorm_family π•œ E ΞΉ) (v : E) (U : set E) (hU : U ∈ p.basis_sets) :
βˆ€αΆ  (x : π•œ) in nhds 0, x β€’ v ∈ U
theorem seminorm_family.basis_sets_smul {π•œ : Type u_1} {E : Type u_2} {ΞΉ : Type u_5} [normed_field π•œ] [add_comm_group E] [module π•œ E] (p : seminorm_family π•œ E ΞΉ) [nonempty ΞΉ] (U : set E) (hU : U ∈ p.basis_sets) :
βˆƒ (V : set π•œ) (H : V ∈ nhds 0) (W : set E) (H : W ∈ add_group_filter_basis.to_filter_basis.sets), V β€’ W βŠ† U
theorem seminorm_family.basis_sets_smul_left {π•œ : Type u_1} {E : Type u_2} {ΞΉ : Type u_5} [normed_field π•œ] [add_comm_group E] [module π•œ E] (p : seminorm_family π•œ E ΞΉ) [nonempty ΞΉ] (x : π•œ) (U : set E) (hU : U ∈ p.basis_sets) :
βˆƒ (V : set E) (H : V ∈ add_group_filter_basis.to_filter_basis.sets), V βŠ† (Ξ» (y : E), x β€’ y) ⁻¹' U
@[protected]
def seminorm_family.module_filter_basis {π•œ : Type u_1} {E : Type u_2} {ΞΉ : Type u_5} [normed_field π•œ] [add_comm_group E] [module π•œ E] (p : seminorm_family π•œ E ΞΉ) [nonempty ΞΉ] :

The module_filter_basis induced by the filter basis seminorm_basis_zero.

Equations
theorem seminorm_family.filter_eq_infi {π•œ : Type u_1} {E : Type u_2} {ΞΉ : Type u_5} [normed_field π•œ] [add_comm_group E] [module π•œ E] [nonempty ΞΉ] (p : seminorm_family π•œ E ΞΉ) :
def seminorm.is_bounded {π•œ : Type u_1} {E : Type u_2} {F : Type u_3} {ΞΉ : Type u_5} {ΞΉ' : Type u_6} [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.

Equations
theorem seminorm.is_bounded_const {π•œ : Type u_1} {E : Type u_2} {F : Type u_3} {ΞΉ : Type u_5} [normed_field π•œ] [add_comm_group E] [module π•œ E] [add_comm_group F] [module π•œ F] (ΞΉ' : Type u_4) [nonempty ΞΉ'] {p : ΞΉ β†’ seminorm π•œ E} {q : seminorm π•œ F} (f : E β†’β‚—[π•œ] F) :
seminorm.is_bounded p (Ξ» (_x : ΞΉ'), q) f ↔ βˆƒ (s : finset ΞΉ) (C : nnreal), C β‰  0 ∧ q.comp f ≀ C β€’ s.sup p
theorem seminorm.const_is_bounded {π•œ : Type u_1} {E : Type u_2} {F : Type u_3} {ΞΉ' : Type u_6} [normed_field π•œ] [add_comm_group E] [module π•œ E] [add_comm_group F] [module π•œ F] (ΞΉ : Type u_4) [nonempty ΞΉ] {p : seminorm π•œ E} {q : ΞΉ' β†’ seminorm π•œ F} (f : E β†’β‚—[π•œ] F) :
seminorm.is_bounded (Ξ» (_x : ΞΉ), p) q f ↔ βˆ€ (i : ΞΉ'), βˆƒ (C : nnreal), C β‰  0 ∧ (q i).comp f ≀ C β€’ p
theorem seminorm.is_bounded_sup {π•œ : Type u_1} {E : Type u_2} {F : Type u_3} {ΞΉ : Type u_5} {ΞΉ' : Type u_6} [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 ΞΉ') :
βˆƒ (C : nnreal) (s : finset ΞΉ), 0 < C ∧ (s'.sup q).comp f ≀ C β€’ s.sup p
structure with_seminorms {π•œ : Type u_1} {E : Type u_2} {ΞΉ : Type u_5} [normed_field π•œ] [add_comm_group E] [module π•œ E] [nonempty ΞΉ] (p : seminorm_family π•œ E ΞΉ) [t : topological_space E] :
Prop

The proposition that the topology of E is induced by a family of seminorms p.

theorem seminorm_family.with_seminorms_eq {π•œ : Type u_1} {E : Type u_2} {ΞΉ : Type u_5} [normed_field π•œ] [add_comm_group E] [module π•œ E] [nonempty ΞΉ] {p : seminorm_family π•œ E ΞΉ} [t : topological_space E] (hp : with_seminorms p) :
theorem with_seminorms.has_basis {π•œ : Type u_1} {E : Type u_2} {ΞΉ : Type u_5} [normed_field π•œ] [add_comm_group E] [module π•œ E] [nonempty ΞΉ] [topological_space E] {p : seminorm_family π•œ E ΞΉ} (hp : with_seminorms p) :
(nhds 0).has_basis (λ (s : set E), s ∈ p.basis_sets) id
theorem seminorm_family.with_seminorms_of_nhds {π•œ : Type u_1} {E : Type u_2} {ΞΉ : Type u_5} [normed_field π•œ] [add_comm_group E] [module π•œ E] [topological_space E] [topological_add_group E] [nonempty ΞΉ] (p : seminorm_family π•œ E ΞΉ) (h : nhds 0 = add_group_filter_basis.to_filter_basis.filter) :
theorem seminorm_family.with_seminorms_of_has_basis {π•œ : Type u_1} {E : Type u_2} {ΞΉ : Type u_5} [normed_field π•œ] [add_comm_group E] [module π•œ E] [topological_space E] [topological_add_group E] [nonempty ΞΉ] (p : seminorm_family π•œ E ΞΉ) (h : (nhds 0).has_basis (Ξ» (s : set E), s ∈ p.basis_sets) id) :
theorem seminorm_family.with_seminorms_iff_nhds_eq_infi {π•œ : Type u_1} {E : Type u_2} {ΞΉ : Type u_5} [normed_field π•œ] [add_comm_group E] [module π•œ E] [topological_space E] [topological_add_group E] [nonempty ΞΉ] (p : seminorm_family π•œ E ΞΉ) :
with_seminorms p ↔ nhds 0 = β¨… (i : ΞΉ), filter.comap ⇑(p i) (nhds 0)
theorem norm_with_seminorms (π•œ : Type u_1) (E : Type u_2) [normed_field π•œ] [seminormed_add_comm_group E] [normed_space π•œ E] :
with_seminorms (Ξ» (_x : fin 1), norm_seminorm π•œ E)

The topology of a normed_space π•œ E is induced by the seminorm norm_seminorm π•œ E.

theorem with_seminorms.is_vonN_bounded_iff_finset_seminorm_bounded {π•œ : Type u_1} {E : Type u_2} {ΞΉ : Type u_5} [nontrivially_normed_field π•œ] [add_comm_group E] [module π•œ E] [nonempty ΞΉ] {p : seminorm_family π•œ E ΞΉ} [topological_space E] {s : set E} (hp : with_seminorms p) :
bornology.is_vonN_bounded π•œ s ↔ βˆ€ (I : finset ΞΉ), βˆƒ (r : ℝ) (hr : 0 < r), βˆ€ (x : E), x ∈ s β†’ ⇑(I.sup p) x < r
theorem bornology.is_vonN_bounded_iff_seminorm_bounded {π•œ : Type u_1} {E : Type u_2} {ΞΉ : Type u_5} [nontrivially_normed_field π•œ] [add_comm_group E] [module π•œ E] [nonempty ΞΉ] {p : seminorm_family π•œ E ΞΉ} [topological_space E] {s : set E} (hp : with_seminorms p) :
bornology.is_vonN_bounded π•œ s ↔ βˆ€ (i : ΞΉ), βˆƒ (r : ℝ) (hr : 0 < r), βˆ€ (x : E), x ∈ s β†’ ⇑(p i) x < r
theorem seminorm.continuous_from_bounded {π•œ : Type u_1} {E : Type u_2} {F : Type u_3} {ΞΉ : Type u_5} {ΞΉ' : Type u_6} [normed_field π•œ] [add_comm_group E] [module π•œ E] [add_comm_group F] [module π•œ F] [nonempty ΞΉ] [nonempty ΞΉ'] {p : seminorm_family π•œ E ΞΉ} {q : seminorm_family π•œ F ΞΉ'} [uniform_space E] [uniform_add_group E] (hp : with_seminorms p) [uniform_space F] [uniform_add_group F] (hq : with_seminorms q) (f : E β†’β‚—[π•œ] F) (hf : seminorm.is_bounded p q f) :
theorem seminorm.cont_with_seminorms_normed_space {π•œ : Type u_1} {E : Type u_2} {ΞΉ : Type u_5} [normed_field π•œ] [add_comm_group E] [module π•œ E] [nonempty ΞΉ] (F : Type u_3) [seminormed_add_comm_group F] [normed_space π•œ F] [uniform_space E] [uniform_add_group E] {p : ΞΉ β†’ seminorm π•œ E} (hp : with_seminorms p) (f : E β†’β‚—[π•œ] F) (hf : βˆƒ (s : finset ΞΉ) (C : nnreal), C β‰  0 ∧ (norm_seminorm π•œ F).comp f ≀ C β€’ s.sup p) :
theorem seminorm.cont_normed_space_to_with_seminorms {π•œ : Type u_1} {F : Type u_3} {ΞΉ : Type u_5} [normed_field π•œ] [add_comm_group F] [module π•œ F] [nonempty ΞΉ] (E : Type u_2) [seminormed_add_comm_group E] [normed_space π•œ E] [uniform_space F] [uniform_add_group F] {q : ΞΉ β†’ seminorm π•œ F} (hq : with_seminorms q) (f : E β†’β‚—[π•œ] F) (hf : βˆ€ (i : ΞΉ), βˆƒ (C : nnreal), C β‰  0 ∧ (q i).comp f ≀ C β€’ norm_seminorm π•œ E) :
theorem seminorm_family.to_locally_convex_space {π•œ : Type u_1} {E : Type u_2} {ΞΉ : Type u_5} [nonempty ΞΉ] [normed_field π•œ] [normed_space ℝ π•œ] [add_comm_group E] [module π•œ E] [module ℝ E] [is_scalar_tower ℝ π•œ E] [topological_space E] [topological_add_group E] {p : seminorm_family π•œ E ΞΉ} (hp : with_seminorms p) :
theorem normed_space.to_locally_convex_space' (π•œ : Type u_1) {E : Type u_2} [normed_field π•œ] [normed_space ℝ π•œ] [seminormed_add_comm_group E] [normed_space π•œ E] [module ℝ E] [is_scalar_tower ℝ π•œ E] :

Not an instance since π•œ can't be inferred. See normed_space.to_locally_convex_space for a slightly weaker instance version.

@[protected, instance]

See normed_space.to_locally_convex_space' for a slightly stronger version which is not an instance.

def seminorm_family.comp {π•œ : Type u_1} {E : Type u_2} {F : Type u_3} {ΞΉ : Type u_5} [normed_field π•œ] [add_comm_group F] [module π•œ F] [add_comm_group E] [module π•œ E] (q : seminorm_family π•œ F ΞΉ) (f : E β†’β‚—[π•œ] F) :
seminorm_family π•œ E ΞΉ

The family of seminorms obtained by composing each seminorm by a linear map.

Equations
theorem seminorm_family.comp_apply {π•œ : Type u_1} {E : Type u_2} {F : Type u_3} {ΞΉ : Type u_5} [normed_field π•œ] [add_comm_group F] [module π•œ F] [add_comm_group E] [module π•œ E] (q : seminorm_family π•œ F ΞΉ) (i : ΞΉ) (f : E β†’β‚—[π•œ] F) :
q.comp f i = (q i).comp f
theorem seminorm_family.finset_sup_comp {π•œ : Type u_1} {E : Type u_2} {F : Type u_3} {ΞΉ : Type u_5} [normed_field π•œ] [add_comm_group F] [module π•œ F] [add_comm_group E] [module π•œ E] (q : seminorm_family π•œ F ΞΉ) (s : finset ΞΉ) (f : E β†’β‚—[π•œ] F) :
(s.sup q).comp f = s.sup (q.comp f)
theorem linear_map.with_seminorms_induced {π•œ : Type u_1} {E : Type u_2} {F : Type u_3} {ΞΉ : Type u_5} [normed_field π•œ] [add_comm_group F] [module π•œ F] [add_comm_group E] [module π•œ E] [topological_space F] [topological_add_group F] [hΞΉ : nonempty ΞΉ] {q : seminorm_family π•œ F ΞΉ} (hq : with_seminorms q) (f : E β†’β‚—[π•œ] F) :
theorem inducing.with_seminorms {π•œ : Type u_1} {E : Type u_2} {F : Type u_3} {ΞΉ : Type u_5} [normed_field π•œ] [add_comm_group F] [module π•œ F] [add_comm_group E] [module π•œ E] [topological_space F] [topological_add_group F] [hΞΉ : nonempty ΞΉ] {q : seminorm_family π•œ F ΞΉ} (hq : with_seminorms q) [topological_space E] {f : E β†’β‚—[π•œ] F} (hf : inducing ⇑f) :