Documentation

Mathlib.Analysis.LocallyConvex.WeakDual

Weak Dual in Topological Vector Spaces #

We prove that the weak topology induced by a bilinear form B : E →ₗ[š•œ] F →ₗ[š•œ] š•œ is locally convex and we explicitly give a neighborhood basis in terms of the family of seminorms fun x => ‖B x y‖ for y : F.

Main definitions #

Main statements #

References #

Tags #

weak dual, seminorm

def LinearMap.toSeminorm {š•œ : Type u_1} {E : Type u_2} [NormedField š•œ] [AddCommGroup E] [Module š•œ E] (f : E →ₗ[š•œ] š•œ) :
Seminorm š•œ E

Construct a seminorm from a linear form f : E →ₗ[š•œ] š•œ over a normed field š•œ by fun x => ‖f x‖

Equations
Instances For
    theorem LinearMap.coe_toSeminorm {š•œ : Type u_1} {E : Type u_2} [NormedField š•œ] [AddCommGroup E] [Module š•œ E] {f : E →ₗ[š•œ] š•œ} :
    ⇑f.toSeminorm = fun (x : E) => ‖f x‖
    @[simp]
    theorem LinearMap.toSeminorm_apply {š•œ : Type u_1} {E : Type u_2} [NormedField š•œ] [AddCommGroup E] [Module š•œ E] {f : E →ₗ[š•œ] š•œ} {x : E} :
    theorem LinearMap.toSeminorm_ball_zero {š•œ : Type u_1} {E : Type u_2} [NormedField š•œ] [AddCommGroup E] [Module š•œ E] {f : E →ₗ[š•œ] š•œ} {r : ā„} :
    theorem LinearMap.toSeminorm_comp {š•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField š•œ] [AddCommGroup E] [Module š•œ E] [AddCommGroup F] [Module š•œ F] (f : F →ₗ[š•œ] š•œ) (g : E →ₗ[š•œ] F) :
    def LinearMap.toSeminormFamily {š•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField š•œ] [AddCommGroup E] [Module š•œ E] [AddCommGroup F] [Module š•œ F] (B : E →ₗ[š•œ] F →ₗ[š•œ] š•œ) :
    SeminormFamily š•œ E F

    Construct a family of seminorms from a bilinear form.

    Equations
    Instances For
      @[simp]
      theorem LinearMap.toSeminormFamily_apply {š•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField š•œ] [AddCommGroup E] [Module š•œ E] [AddCommGroup F] [Module š•œ F] {B : E →ₗ[š•œ] F →ₗ[š•œ] š•œ} {x : E} {y : F} :
      theorem LinearMap.mem_span_iff_continuous_of_finite {ι : Type u_4} {š•œ : Type u_5} {E : Type u_6} [Finite ι] [Field š•œ] [tš•œ : TopologicalSpace š•œ] [IsTopologicalRing š•œ] [AddCommGroup E] [Module š•œ E] [T0Space š•œ] {f : ι → E →ₗ[š•œ] š•œ} (φ : E →ₗ[š•œ] š•œ) :
      φ ∈ Submodule.span š•œ (Set.range f) ↔ Continuous ⇑φ
      theorem LinearMap.mem_span_iff_continuous {ι : Type u_4} {š•œ : Type u_5} {E : Type u_6} [NontriviallyNormedField š•œ] [AddCommGroup E] [Module š•œ E] {f : ι → E →ₗ[š•œ] š•œ} (φ : E →ₗ[š•œ] š•œ) :
      φ ∈ Submodule.span š•œ (Set.range f) ↔ Continuous ⇑φ
      theorem LinearMap.mem_span_iff_bound {ι : Type u_4} {š•œ : Type u_5} {E : Type u_6} [NontriviallyNormedField š•œ] [AddCommGroup E] [Module š•œ E] {f : ι → E →ₗ[š•œ] š•œ} (φ : E →ₗ[š•œ] š•œ) :
      φ ∈ Submodule.span š•œ (Set.range f) ↔ ∃ (s : Finset ι) (c : NNReal), φ.toSeminorm ≤ c • s.sup fun (i : ι) => (f i).toSeminorm
      theorem LinearMap.weakBilin_withSeminorms {š•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField š•œ] [AddCommGroup E] [Module š•œ E] [AddCommGroup F] [Module š•œ F] (B : E →ₗ[š•œ] F →ₗ[š•œ] š•œ) :
      theorem LinearMap.hasBasis_weakBilin {š•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField š•œ] [AddCommGroup E] [Module š•œ E] [AddCommGroup F] [Module š•œ F] (B : E →ₗ[š•œ] F →ₗ[š•œ] š•œ) :
      instance WeakBilin.locallyConvexSpace {š•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField š•œ] [AddCommGroup E] [Module š•œ E] [AddCommGroup F] [Module š•œ F] [NormedSpace ā„ š•œ] [Module ā„ E] [IsScalarTower ā„ š•œ E] {B : E →ₗ[š•œ] F →ₗ[š•œ] š•œ} :