Documentation

Let \(\mathcal{I}\) be a bag with indices, let \(c\) be an upper bound on the number of times a single item may occur in (mathcal{I}), and let \(\varepsilon\) be a function mapping indices to real numbers that satisfies:

1. \(0 < \varepsilon(j) < 1\), for all \(1 \leq j\),
2. \(\prod_{0 \leq i \leq j} \varepsilon(i)^c > \varepsilon(k)\), for all \(1 \leq j < k\)

Note that such a function exists:

begin{lemma} label{lem:condition_2} Let \(\delta \in (0,1)\) and \(d \geq c+1\). The function \(\varepsilon(i) = \delta^{d^i}\) satisfies condition 2. end{lemma}

begin{proof} By transitivity it suffices to argue this for \(k=j+1\):

begin{align*} &qquad prod_{0 leq i leq j} varepsilon(i)^c > varepsilon(j+1) \ equiv &qquad prod_{0 leq i leq j} (delta^{d^i})^c > delta^{d^{j+1}}\ equiv &qquad prod_{0 leq i leq j} delta^{cd^i} > delta^{d^{j+1}} \ equiv &qquad delta^{sum_{0 leq i leq j} cd^i} > delta^{d^{j+1}} & text{using } delta in (0,1)\ equiv &qquad sum_{0 leq i leq j} cd^i < d^{j+1} \ equiv &qquad csum_{0 leq i leq j} d^i < d^{j+1} \ end{align*}

We prove this by induction.

For the base case \(j=0\): we have \(0 < 1\), which is trivially true.

For the step case we have the induction hypothesis \(c\sum_{0 \leq i \leq j} d^i < d^{j+1}\), and we have to prove that \(c\sum_{0 \leq i \leq j+1} d^i < d^{j+2}\):

begin{align*} csum_{0 leq i leq j+1} d^i &= cd^{j+1} + csum_{0 leq i leq j} d^i \ &< cd^{j+1} + d^{j+1} & text{using IH} \ &= (c+1)d^{j+1} & text{using that } c+1 leq d \ &leq dd^{j+1} \ &=d^{j+2} end{align*} This completes the proof. end{proof}

An EpsFold now represents the term

\[ \prod_{i \in \mathcal{I}} \varepsilon(i) \]

for some bag \(\mathcal{I}\).

Let \(\mathcal{J}\) be some sub-bag of \(\mathcal{I}\). Note that condition 2 implies that:

\(\prod_{i \in \mathcal{J}} \varepsilon(i) > \varepsilon(k)\), for all \(1 \leq j < k\)

This means that when comparing two EpsFolds, say \(e_1\) and \(e_2\), representing bags \(\mathcal{I}_1\) and \(\mathcal{I}_2\), respectively. It suffices to compare the largest index (j in mathcal{I}_1setminusmathcal{I}_2) with the largest index (k in mathcal{I}_2setminusmathcal{I}_1). We have that

\(e_1 > e_2\) if and only if \(j < k\).

Creates the term \(\varepsilon(i)\)

Constructs an epsfold from a list of elements

Evaluate an eps-fold using the choice of eps from the lemma above, i.e. \(\varepsilon(i) = \delta^{d^i}\) >>> evalEps 2 (1/2) $ mkEpsFold [1] 0.25 >>> evalEps 2 (1/2) $ mkEpsFold [2] 6.25e-2 >>> evalEps 2 (1/2) $ mkEpsFold [1,2] 1.5625e-2

Test if the epsfold has no pertubation at all (i.e. if it is \(\Pi_{\emptyset}\)

Gets the factors

computes a base d that can be used as:

\( \varepsilon(i) = \varepsilon^{d^i} \)

A term 'Term c es' represents a term:

\[ c \Pi_{i \in es} \varepsilon(i) \]

for a constant c and an arbitrarily small value \(\varepsilon\), parameterized by i.

Creates a singleton term

Lens to access the constant c in the term.

Represents a Sum of terms, i.e. given a sequence of terms Term \(c_i\) \(I_i\) s where \(c_i\) is a constant and \(I_i\) is a set of indices, a Symbolic represents an expression of the form:

\[ \sum c_i \Pi_{j in I_i} \varepsilon(j) \]

The terms are represented in order of decreasing significance.

The main idea in this type is that, if symbolic values contains \(\varepsilon(i)\) terms we can always order them. That is, two Symbolic terms will be equal only if:

• they contain *only* a constant term (that is equal)
• they contain the exact same \(\varepsilon\)-fold.

Creates a constant symbolic value

Creates a symbolic vlaue with a single indexed term. If you just need a constant (i.e. non-indexed), use constant

given the value c and the index i, creates the perturbed value \(c + \varepsilon(i)\)

Produces a list of terms, in decreasing order of significance

Computing the Sign of an expression. (Nothing represents zero)

Drops all the epsilon terms

Number type representing

Helper to construct sosRationals