Monotone continuous functionals determine a closed order

Let E be a locally convex real topological vector space with a partial order compatible with its module structure, whose positive cone {x | 0 ≤ x} is closed. Farkas' lemma (ProperCone.hyperplane_separation_point) separates a point outside this cone from the cone by a continuous linear functional that is nonnegative on it, that is, by a monotone one. Consequently x ≤ y exactly when f x ≤ f y for every monotone continuous linear functional f, and such functionals separate the points of E. When E is moreover finite-dimensional, evaluation at the monotone functionals is an injective linear map, hence a closed embedding, so convergence in E is detected by the monotone functionals.

This reduces statements about vectors with nonnegative coordinates in an ordered space to statements about nonnegative real numbers, one monotone functional at a time.

Main results

• TauCeti.le_iff_forall_monotone_dual_le: x ≤ y if and only if f x ≤ f y for every monotone continuous linear functional f.
• TauCeti.eq_of_forall_monotone_dual_eq: monotone continuous linear functionals separate points.
• TauCeti.tendsto_iff_forall_monotone_dual: in finite dimension, f → c if and only if φ ∘ f → φ c for every monotone continuous linear functional φ.

theorem TauCeti.le_iff_forall_monotone_dual_le {E : Type u_1} [TopologicalSpace E] [AddCommGroup E] [IsTopologicalAddGroup E] [Module ℝ E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] [PartialOrder E] [IsOrderedAddMonoid E] [PosSMulMono ℝ E] [OrderClosedTopology E] {x y : E} : x ≤ y ↔ ∀ (f : StrongDual ℝ E), Monotone ⇑f → f x ≤ f y

Closed orders are determined by monotone functionals. In a locally convex real ordered vector space with closed positive cone, x ≤ y if and only if f x ≤ f y for every monotone continuous linear functional f.

theorem TauCeti.eq_of_forall_monotone_dual_eq {E : Type u_1} [TopologicalSpace E] [AddCommGroup E] [IsTopologicalAddGroup E] [Module ℝ E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] [PartialOrder E] [IsOrderedAddMonoid E] [PosSMulMono ℝ E] [OrderClosedTopology E] {x y : E} (h : ∀ (f : StrongDual ℝ E), Monotone ⇑f → f x = f y) : x = y

Monotone functionals separate points. In a locally convex real ordered vector space with closed positive cone, two vectors on which every monotone continuous linear functional agrees are equal.

theorem TauCeti.tendsto_iff_forall_monotone_dual {E : Type u_1} [TopologicalSpace E] [AddCommGroup E] [IsTopologicalAddGroup E] [Module ℝ E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] [PartialOrder E] [IsOrderedAddMonoid E] [PosSMulMono ℝ E] [OrderClosedTopology E] [FiniteDimensional ℝ E] {α : Type u_2} {l : Filter α} {f : α → E} {c : E} : Filter.Tendsto f l (nhds c) ↔ ∀ (φ : StrongDual ℝ E), Monotone ⇑φ → Filter.Tendsto (fun (a : α) => φ (f a)) l (nhds (φ c))

Monotone functionals detect convergence in finite dimension. In a finite-dimensional locally convex real ordered vector space with closed positive cone, f tends to c along l if and only if φ ∘ f tends to φ c for every monotone continuous linear functional φ.