analysis.locally_convex.with_seminorms

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

p.basis_sets = ⋃ (s : finset ι) (r : ℝ) (hr : 0 < r), {(s.sup p).ball 0 r}

source

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

source

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

(i.sup p).ball 0 r ∈ p.basis_sets

source

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

source

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 ι] :

p.basis_sets.nonempty

source

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

source

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

source

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

source

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

source

@[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 ι] :

add_group_filter_basis E

The add_group_filter_basis induced by the filter basis seminorm_basis_zero.

Equations

p.add_group_filter_basis = add_group_filter_basis_of_comm p.basis_sets _ _ _ _ _

source

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

source

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

source

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

source

@[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 ι] :

module_filter_basis 𝕜 E

The module_filter_basis induced by the filter basis seminorm_basis_zero.

Equations

p.module_filter_basis = {to_add_group_filter_basis := p.add_group_filter_basis _inst_4, smul' := _, smul_left' := _, smul_right' := _}

source

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 ι) :

add_group_filter_basis.to_filter_basis.filter = ⨅ (i : ι), filter.comap ⇑(p i) (nhds 0)

source

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

seminorm.is_bounded p q f = ∀ (i : ι'), ∃ (s : finset ι) (C : nnreal), C ≠ 0 ∧ (q i).comp f ≤ C • s.sup p

source

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

source

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

source

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

source

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

topology_eq_with_seminorms : t = p.module_filter_basis.topology

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

source

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

t = p.module_filter_basis.topology

source

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

source

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

with_seminorms p

source

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

with_seminorms p

source

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)

source

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.

source

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

source

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

source

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

continuous ⇑f

source

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

continuous ⇑f

source

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

continuous ⇑f

source

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

locally_convex_space ℝ E

source

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

locally_convex_space ℝ E

Not an instance since 𝕜 can't be inferred. See normed_space.to_locally_convex_space for a slightly weaker instance version.

source

@[protected, instance]

def normed_space.to_locally_convex_space {E : Type u_2} [seminormed_add_comm_group E] [normed_space ℝ E] :

locally_convex_space ℝ E

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

source

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

q.comp f = λ (i : ι), (q i).comp f

source

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

source

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)

source

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

with_seminorms (q.comp f)

source

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

with_seminorms (q.comp f)

mathlib documentation

Topology induced by a family of seminorms #

Main definitions #

Main statements #

TODO #

Tags #