Certified finite partition and expectation enclosure

Input a finite nonempty set $\mathsf{X}$ with an explicit enumeration $(x_1,\dots ,x_m)$ listing each element exactly once, functions $w:\mathsf{X}\to (0,\mathrm{\infty })$ and $f:\mathsf{X}\to \mathbb{R}$, and, for each $x\in \mathsf{X}$, rational numbers $a_x\le b_x$ and $c_x\le d_x$ such that $w(x)\in W_x:=[a_x,b_x]$ and $f(x)\in F_x:=[c_x,d_x]$. Here a closed rational input interval $[a,b]$ means $a,b\in \mathbb{Q}$ and $a\le b$; its endpoints need not be dyadic, so before conversion it is distinct from the finite-dyadic real interval defined in def-intervals-rectangles-and-complex-balls. Choose a finite dyadic format $\mathbb{F}$ as in def-dyadic-floating-point-format-and-directed-rounding, with its directed roundings. The interval assertions are certified input premises; this procedure does not derive them from energies or evaluate an exponential or logarithm.

For $i=1,\dots ,m$ in increasing order, convert $W_{x_i}$ and then $F_{x_i}$ by rounding each lower rational endpoint down and each upper rational endpoint up into $\mathbb{F}$; denote the converted intervals by ${\widehat{W}}_i$ and ${\widehat{F}}_i$. If any conversion overflows, return unresolved-overflow and no finite enclosure claim. Initialize ${\mathcal{Z}}_0={\mathcal{N}}_0=[0,0]$. For $i=1,\dots ,m$ in increasing order, compute the following three operations in the displayed order:

${\mathcal{P}}_i={\widehat{W}}_i{\widehat{F}}_i,{\mathcal{Z}}_i={\mathcal{Z}}_{i-1}+{\widehat{W}}_i,{\mathcal{N}}_i={\mathcal{N}}_{i-1}+{\mathcal{P}}_i\mathrm{.}$

These recurrences fix the finite expression DAG: both sums are accumulated from left to right in the supplied enumeration, with rounding after each displayed operation and no reassociation. On completing the loop, set $\mathcal{Z}={\mathcal{Z}}_m$ and $\mathcal{N}={\mathcal{N}}_m$.

Every addition and multiplication uses the outward-rounded interval operations; division is used only for a denominator interval excluding zero. If any operation returns a non-finite status, return unresolved-operation and no finite enclosure claim. Otherwise return the finite intervals $\mathcal{Z}$ and $\mathcal{N}$. If the lower endpoint of $\mathcal{Z}$ is strictly positive, also return the outward interval quotient $\mathcal{E}=\mathcal{N}\mathrm{/}\mathcal{Z}$; if that endpoint is nonpositive, return unresolved-denominator and no normalized-expectation enclosure.

This is finite enumeration and can require exponentially many operations in the model size. It certifies arithmetic from supplied weight intervals; it does not certify how those intervals were obtained.

Dyadic floating-point format and directed rounding

Real intervals, complex rectangles and ball enclosures

Outward-rounded interval, rectangle and ball operations

Directed dyadic rounding encloses with explicit underflow and overflow bounds

Finite real interval operations enclose their exact values