Ordered innerproduct spaces

Stream: Is there code for X?

[Apurva Nakade]

Is there a some structure that gives an "OrderedInnerProductSpace". I need the following lemma to hold:

import Mathlib.Analysis.InnerProductSpace.Adjoint

variable {V : Type _} [NormedOrderedAddGroup V] [InnerProductSpace ℝ V] [CompleteSpace V]

example (u v w : V) (hu : 0 ≤ u) (hvw : v ≤ w) : ⟪u, v⟫_ℝ ≤ ⟪u, w⟫_ℝ := by sorry

[Yaël Dillies]

We don't have anything like that, no. What's your application?

[Apurva Nakade]

Linear programming. It's usually stated for Rn But I was wondering if it's generalizable for inner product spaces.

See the weak duality proof here for example: https://en.m.wikipedia.org/wiki/Dual_linear_program#The_duality_theorems

[Apurva Nakade]

This is the relevant step:

$$x^Tc ≤ x^T(A^Ty)$$

since $A^Ty ≥ c$ by the dual constraints, and $x ≥ 0$.