PhyslibAlpha.Mathematics.Order.PositiveDual.BidualLattice

Let $E$ be an ordered real vector space and $E \to_p \mathbb{R}$ be the set of positive linear functionals on $E$. For two elements $x, y$ in the bidual $\text{Bidual } E$ and a positive linear functional $\phi \in E \to_p \mathbb{R}$, this set consists of all real values $x(\phi_1) + y(\phi_2)$ where $\phi_1$ and $\phi_2$ are positive linear functionals such that $\phi_1 + \phi_2 = \phi$. Mathematically, this is the set $\{ x(\phi_1) + y(\phi_2) \mid \phi_1, \phi_2 \in E \to_p \mathbb{R}, \phi_1 + \phi_2 = \phi \}$.

Let $E$ be an ordered real vector space. For any two elements $x, y$ in the bidual $\text{Bidual } E$ and any positive linear functional $\phi \in E \to_p \mathbb{R}$, the set of values $$\{ x(\phi_1) + y(\phi_2) \mid \phi_1, \phi_2 \in E \to_p \mathbb{R}, \phi_1 + \phi_2 = \phi \}$$ is non-empty.

Let $E$ be an ordered real vector space. Let $x, y \in \text{Bidual } E$ be elements of the bidual and $f, g \in E$ be elements of $E$. Suppose that for every positive linear functional $\phi \in E \to_p \mathbb{R}$, the inequalities $|x(\phi)| \leq \phi(f)$ and $|y(\phi)| \leq \phi(g)$ hold. Then for any positive linear functionals $\phi, \phi_1, \phi_2$ such that $\phi = \phi_1 + \phi_2$, it follows that $$x(\phi_1) + y(\phi_2) \leq \phi(f + g).$$

Let $E$ be an ordered real vector space. For any elements $x, y$ in the bidual $\text{Bidual } E$ and any positive linear functional $\phi: E \to \mathbb{R}$, the set of values $$\{ x(\phi_1) + y(\phi_2) \mid \phi_1, \phi_2 \in E \to_p \mathbb{R}, \phi_1 + \phi_2 = \phi \}$$ is bounded above in $\mathbb{R}$.

Let $E$ be an ordered real vector space, and let $E \to_p \mathbb{R}$ denote the set of positive linear functionals on $E$. For two elements $x, y$ in the bidual $\text{Bidual } E$ and a positive linear functional $\phi \in E \to_p \mathbb{R}$, this function returns the supremum of the set of values $x(\phi_1) + y(\phi_2)$ obtained by splitting $\phi$ into two positive linear functionals $\phi_1$ and $\phi_2$. Mathematically, it is defined as: $$\text{dsupFun}(x, y, \phi) = \sup \{ x(\phi_1) + y(\phi_2) \mid \phi_1, \phi_2 \in E \to_p \mathbb{R}, \phi_1 + \phi_2 = \phi \}$$ This value represents the "best split" of the functional $\phi$ between the bidual elements $x$ and $y$, which corresponds to the Riesz–Kantorovich formula for the supremum in the bidual.

Let $E$ be an ordered real vector space. For any elements $x, y$ in the bidual $\text{Bidual } E$ and any positive linear functionals $\phi, \phi_1, \phi_2 \in E \to_p \mathbb{R}$, if $\phi_1 + \phi_2 = \phi$, then $$x(\phi_1) + y(\phi_2) \leq \text{dsupFun}(x, y, \phi)$$ where $\text{dsupFun}(x, y, \phi) = \sup \{ x(\psi_1) + y(\psi_2) \mid \psi_1, \psi_2 \in E \to_p \mathbb{R}, \psi_1 + \psi_2 = \phi \}$.

Let $E$ be an ordered real vector space. Let $x, y \in \text{Bidual } E$ be elements of the bidual, $\phi \in E \to_p \mathbb{R}$ be a positive linear functional, and $r \in \mathbb{R}$. If for all positive linear functionals $\phi_1, \phi_2 \in E \to_p \mathbb{R}$ such that $\phi_1 + \phi_2 = \phi$, it holds that $x(\phi_1) + y(\phi_2) \le r$, then $\text{dsupFun}(x, y, \phi) \le r$, where $\text{dsupFun}(x, y, \phi) = \sup \{ x(\phi_1) + y(\phi_2) \mid \phi_1, \phi_2 \in E \to_p \mathbb{R}, \phi_1 + \phi_2 = \phi \}$.

Let $E$ be an ordered real vector space and $E \to_p \mathbb{R}$ denote the set of positive linear functionals on $E$. For any two elements $x, y$ in the bidual $\text{Bidual } E$ and any positive linear functionals $\phi, \psi \in E \to_p \mathbb{R}$, let the "best split" value be defined as $\text{dsupFun}(x, y, \omega) = \sup \{ x(\omega_1) + y(\omega_2) \mid \omega_1, \omega_2 \in E \to_p \mathbb{R}, \omega_1 + \omega_2 = \omega \}$. Then the following inequality holds: $$\text{dsupFun}(x, y, \phi) + \text{dsupFun}(x, y, \psi) \leq \text{dsupFun}(x, y, \phi + \psi)$$

Let $E$ be an ordered real vector space, and let $E \to_p \mathbb{R}$ denote the set of positive linear functionals on $E$. Let $\text{Bidual } E$ be the bidual of $E$, consisting of functions $x: (E \to_p \mathbb{R}) \to \mathbb{R}$ that are additive, positively homogeneous, and dominated by some element of $E$. For any two elements $x, y \in \text{Bidual } E$ and a positive linear functional $\phi \in E \to_p \mathbb{R}$, let the "best split" value (representing the Riesz–Kantorovich formula for the supremum) be defined as: $$\text{dsupFun}(x, y, \phi) = \sup \{ x(\phi_1) + y(\phi_2) \mid \phi_1, \phi_2 \in E \to_p \mathbb{R}, \phi_1 + \phi_2 = \phi \}$$ Then, for any $x, y \in \text{Bidual } E$ and any positive linear functionals $\phi, \psi \in E \to_p \mathbb{R}$, the best split value is additive with respect to the functionals: $$\text{dsupFun}(x, y, \phi + \psi) = \text{dsupFun}(x, y, \phi) + \text{dsupFun}(x, y, \psi)$$

Let $E$ be an ordered real vector space and let $E \to_p \mathbb{R}$ denote the set of positive linear functionals on $E$. For any two elements $x, y$ in the bidual $\text{Bidual } E$, the "best split" value of the zero functional, defined as $\text{dsupFun}(x, y, 0) = \sup \{ x(\phi_1) + y(\phi_2) \mid \phi_1, \phi_2 \in E \to_p \mathbb{R}, \phi_1 + \phi_2 = 0 \}$, is equal to $0$.

Let $E$ be an ordered real vector space. For any elements $x, y$ in the bidual of $E$, any non-negative real number $c \in \mathbb{R}_{\ge 0}$, and any positive linear functional $\phi \in E \to_p \mathbb{R}$, the "best split" function $\text{dsupFun}$ satisfies: $$\text{dsupFun}(x, y, c \cdot \phi) = c \cdot \text{dsupFun}(x, y, \phi)$$ where $\text{dsupFun}(x, y, \phi) = \sup \{ x(\phi_1) + y(\phi_2) \mid \phi_1, \phi_2 \in E \to_p \mathbb{R}, \phi_1 + \phi_2 = \phi \}$.

Let $E$ be an ordered real vector space and $\text{Bidual } E$ be its bidual space consisting of additive, positively homogeneous, and dominated functions on the set of positive linear functionals $E \to_p \mathbb{R}$. For any two elements $x, y \in \text{Bidual } E$, this definition constructs their least upper bound (supremum), denoted as $x \vee y$, which is itself an element of $\text{Bidual } E$. For a positive linear functional $\phi \in E \to_p \mathbb{R}$, its value is determined by the Riesz–Kantorovich formula: $$(x \vee y)(\phi) = \sup \{ x(\phi_1) + y(\phi_2) \mid \phi_1, \phi_2 \in E \to_p \mathbb{R}, \phi_1 + \phi_2 = \phi \}$$ The definition ensures that this supremum satisfies the required properties of the bidual (additivity, positive homogeneity, and domination) to be a valid element of $\text{Bidual } E$.

Let $E$ be an ordered real vector space and $\text{Bidual } E$ be its bidual space. For any elements $x, y \in \text{Bidual } E$ and any positive linear functional $\phi \in E \to_p \mathbb{R}$, the value of the supremum $x \vee y$ at $\phi$ is given by the Riesz–Kantorovich formula: $$(x \vee y)(\phi) = \sup \{ x(\phi_1) + y(\phi_2) \mid \phi_1, \phi_2 \in E \to_p \mathbb{R}, \phi_1 + \phi_2 = \phi \}$$

Let $E$ be an ordered real vector space and $\text{Bidual } E$ be its bidual space, consisting of additive, positively homogeneous, and dominated functions on the set of positive linear functionals $E \to_p \mathbb{R}$. For any two elements $x, y \in \text{Bidual } E$, let $x \vee y$ (denoted in the formal statement as `dsup hE x y`) be the function defined by the Riesz–Kantorovich formula: $$(x \vee y)(\phi) = \sup \{ x(\phi_1) + y(\phi_2) \mid \phi_1, \phi_2 \in E \to_p \mathbb{R}, \phi_1 + \phi_2 = \phi \}$$ for each positive linear functional $\phi$. Then $x \vee y$ is the least upper bound of the set $\{x, y\}$ with respect to the pointwise partial order on $\text{Bidual } E$.

Let $E$ be an ordered real vector space such that its positive linear functionals form a lattice. The bidual space $\text{Bidual } E$ is equipped with a lattice structure where the partial order is defined pointwise. For any two elements $x, y \in \text{Bidual } E$, their supremum $x \vee y$ is defined by the Riesz–Kantorovich formula: $$(x \vee y)(\phi) = \sup \{ x(\phi_1) + y(\phi_2) \mid \phi_1, \phi_2 \in E \to_p \mathbb{R}, \phi_1 + \phi_2 = \phi \}$$ for every positive linear functional $\phi$. The infimum $x \wedge y$ is defined via the supremum and negation as $x \wedge y = -((-x) \vee (-y))$.