Pointwise operations on the weak dual #
The addition and the scalar actions on WeakDual 𝕜 E are those of E →L[𝕜] 𝕜, so they are
computed pointwise. Registering IsAddApply and IsSMulApply makes the generic simp lemmas
add_apply and smul_apply available on WeakDual 𝕜 E, so that pointwise computations, such
as convex combinations of functionals, need not pass through WeakDual.toStrongDual or unfold
the type synonym.
It also records that, for ordered E and 𝕜, the functionals that are nonnegative on
nonnegative elements form a weak-* closed set, WeakDual.isClosed_setOf_map_nonneg.
instance
WeakDual.instIsAddApply
{𝕜 : Type u_1}
{E : Type u_2}
[CommSemiring 𝕜]
[TopologicalSpace 𝕜]
[ContinuousAdd 𝕜]
[ContinuousConstSMul 𝕜 𝕜]
[AddCommMonoid E]
[Module 𝕜 E]
[TopologicalSpace E]
:
IsAddApply (WeakDual 𝕜 E)
instance
WeakDual.instIsSMulApply
{𝕜 : Type u_1}
{E : Type u_2}
[CommSemiring 𝕜]
[TopologicalSpace 𝕜]
[ContinuousAdd 𝕜]
[ContinuousConstSMul 𝕜 𝕜]
[AddCommMonoid E]
[Module 𝕜 E]
[TopologicalSpace E]
(M : Type u_3)
[Monoid M]
[DistribMulAction M 𝕜]
[SMulCommClass 𝕜 M 𝕜]
[ContinuousConstSMul M 𝕜]
:
IsSMulApply M (WeakDual 𝕜 E)
theorem
WeakDual.isClosed_setOf_map_nonneg
{𝕜 : Type u_1}
{E : Type u_2}
[CommSemiring 𝕜]
[TopologicalSpace 𝕜]
[ContinuousAdd 𝕜]
[ContinuousConstSMul 𝕜 𝕜]
[AddCommMonoid E]
[Module 𝕜 E]
[TopologicalSpace E]
[Preorder 𝕜]
[ClosedIciTopology 𝕜]
[LE E]
:
The functionals that are nonnegative on nonnegative elements form a weak-* closed set.