Statistics

─── Uninterpreted refinement-language symbols ───────────────────────── These live in the refinement language so Z3 can reason about them as abstract symbols. Runtime providers below tie concrete values back to them via refined return types. Fraction of xs strictly below threshold t.
Imports
open Array;
Table of Contents

Functions

widenBelow

Monotonicity below: t1 <= t2 ⇒ fracBelow xs t1 <= fracBelow xs t2.
def widenBelow (1 xs : (Array Float) | Array.size xs > 0) (t1 : Float) (t2 : Float | t2 ≥ t1) : {r : (Array Float) | Array.size r > 0 && fracBelow r t2 ≥ fracBelow xs t1}

widenAbove

Monotonicity above: t1 <= t2 ⇒ fracAbove xs t1 >= fracAbove xs t2.
def widenAbove (1 xs : (Array Float) | Array.size xs > 0) (t1 : Float) (t2 : Float | t2 ≤ t1) : {r : (Array Float) | Array.size r > 0 && fracAbove r t2 ≥ fracAbove xs t1}

belowComplement

Complement at a non-atomic point: fracBelow + fracAbove = 1.
def belowComplement (1 xs : (Array Float) | Array.size xs > 0) (t : Float) : {r : (Array Float) | Array.size r > 0 && fracBelow r t = 1.0 - fracAbove xs t}

betweenFromBelow

Between bound: fracBetween lo hi >= fracBelow hi - fracBelow lo (slack covers atoms).
def betweenFromBelow (1 xs : (Array Float) | Array.size xs > 0) (lo : Float) (hi : Float | hi ≥ lo) : {r : (Array Float) | Array.size r > 0 && fracBetween r lo hi ≥ fracBelow xs hi - fracBelow xs lo}

mean

Returns the mean (average) of a non-empty list of numbers.
def mean (borrow xs : (Array Float) | Array.size xs > 0) : {m : Float | m = sampleMean xs}

median

Returns the median (middle value) of a non-empty list of numbers.
def median (borrow xs : (Array Float) | Array.size xs > 0) : Float

std

Returns the sample standard deviation of a non-empty list of numbers.
def std (borrow xs : (Array Float) | Array.size xs > 0) : {s : Float | s = sampleStd xs}

var

Returns the sample variance of a non-empty list of numbers.
def var (borrow xs : (Array Float) | Array.size xs > 0) : {v : Float | v = sampleVar xs}

min

Returns the minimum value in a non-empty list of numbers.
def min (borrow xs : (Array Float) | Array.size xs > 0) : {m : Float | m = sampleMin xs}

max

Returns the maximum value in a non-empty list of numbers.
def max (borrow xs : (Array Float) | Array.size xs > 0) : {m : Float | m = sampleMax xs}

sum

Returns the sum of a non-empty list of numbers.
def sum (borrow xs : (Array Float) | Array.size xs > 0) : Float

quantile

Returns the quantile of a non-empty list of numbers.
def quantile (borrow xs : (Array Float) | Array.size xs > 0) (q : Float) : Float

prod

Returns the product of a non-empty list of numbers.
def prod (borrow xs : (Array Float) | Array.size xs > 0) : Float

cumsum

Returns the cumulative sum of a non-empty list of numbers.
def cumsum (borrow xs : (Array Float) | Array.size xs > 0) : (Array Float)

cumprod

Returns the cumulative product of a non-empty list of numbers.
def cumprod (borrow xs : (Array Float) | Array.size xs > 0) : (Array Float)

quartiles

Returns the 1st (Q1), 2nd (median), and 3rd (Q3) quartiles of a non-empty list of numbers.
def quartiles (borrow xs : (Array Float) | Array.size xs > 0) : (Array Float)

unique

Returns the unique values in a non-empty list.
def unique (borrow xs : (Array Float) | Array.size xs > 0) : (Array Float)

argmax

Returns the index of the maximum value in a non-empty list of numbers.
def argmax (borrow xs : (Array Float) | Array.size xs > 0) : Float

argmin

Returns the index of the minimum value in a non-empty list of numbers.
def argmin (borrow xs : (Array Float) | Array.size xs > 0) : Float

percentile

Returns the percentile of a non-empty list of numbers.
def percentile (borrow xs : (Array Float) | Array.size xs > 0) (p : Float) : Float

corrcoef

Returns the correlation coefficient of two non-empty lists of equal length.
def corrcoef (borrow xs : (Array Float) | Array.size xs > 0) (borrow ys : (Array Float) | Array.size ys = Array.size xs) : Float

cov

Returns the covariance of two non-empty lists of equal length.
def cov (borrow xs : (Array Float) | Array.size xs > 0) (borrow ys : (Array Float) | Array.size ys = Array.size xs) : Float

proportionBelow

Proportion of values strictly below a threshold.
def proportionBelow (borrow xs : (Array Float) | Array.size xs > 0) (t : Float) : {f : Float | f = fracBelow xs t && 0.0 ≤ f && f ≤ 1.0}

proportionAbove

Proportion of values strictly above a threshold.
def proportionAbove (borrow xs : (Array Float) | Array.size xs > 0) (t : Float) : {f : Float | f = fracAbove xs t && 0.0 ≤ f && f ≤ 1.0}

proportionBetween

Proportion of values strictly inside the open interval (lo, hi).
def proportionBetween (borrow xs : (Array Float) | Array.size xs > 0) (lo : Float) (hi : Float | hi ≥ lo) : {f : Float | f = fracBetween xs lo hi && 0.0 ≤ f && f ≤ 1.0}

Uninterpreted

Functions declared as def f ... = uninterpreted: only their signature is known to the verifier; they have no body.

fracBelow

uninterpreted
Fraction of xs strictly below threshold t.
def fracBelow : (xs : (Array Float)) → (t : Float) → Float

fracAbove

uninterpreted
Fraction of xs strictly above threshold t.
def fracAbove : (xs : (Array Float)) → (t : Float) → Float

fracBetween

uninterpreted
Fraction of xs in the open interval (lo, hi).
def fracBetween : (xs : (Array Float)) → (lo : Float) → (hi : Float) → Float

sampleMean

uninterpreted
Sample summary statistics as abstract symbols.
def sampleMean : (xs : (Array Float)) → Float

sampleVar

uninterpreted
def sampleVar : (xs : (Array Float)) → Float

sampleStd

uninterpreted
def sampleStd : (xs : (Array Float)) → Float

sampleMin

uninterpreted
def sampleMin : (xs : (Array Float)) → Float

sampleMax

uninterpreted
def sampleMax : (xs : (Array Float)) → Float