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 #
LinearMap.toSeminorm
: turn a linear formf : E āā[š] š
into a seminormfun x => āf xā
.LinearMap.toSeminormFamily
: turn a bilinear formB : E āā[š] F āā[š] š
into a mapF ā Seminorm š E
.
Main statements #
LinearMap.hasBasis_weakBilin
: the seminorm balls ofB.toSeminormFamily
form a neighborhood basis of0
in the weak topology.LinearMap.toSeminormFamily.withSeminorms
: the topology of a weak space is induced by the family of seminormsB.toSeminormFamily
.WeakBilin.locallyConvexSpace
: a space endowed with a weak topology is locally convex.
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
- f.toSeminorm = (normSeminorm š š).comp f
Instances For
theorem
LinearMap.coe_toSeminorm
{š : Type u_1}
{E : Type u_2}
[NormedField š]
[AddCommGroup E]
[Module š E]
{f : E āā[š] š}
:
@[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
- B.toSeminormFamily y = (B.flip y).toSeminorm
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 āā[š] š)
:
theorem
LinearMap.mem_span_iff_continuous
{ι : Type u_4}
{š : Type u_5}
{E : Type u_6}
[NontriviallyNormedField š]
[AddCommGroup E]
[Module š E]
{f : ι ā E āā[š] š}
(Ļ : E āā[š] š)
:
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 āā[š] š}
: