Distributions

Distributions.ae Probability distribution producers paired with quantile-bound postulates. Refinement-language predicates (fracBelow, fracAbove, sampleMean, ...) and their monotonicity axioms (widenBelow, widenAbove, ...) live in Statistics. Each producer is `native` (numpy under the hood). Its return refinement is a *postulate* asserting the true distributional quantiles. For finite samples these are expected-value claims; we treat them as trusted facts since the FFI is on the user's honor. Constants are CDF-inverse evaluations (z-scores, ln(1-p), etc.) hardcoded. ─── Normal distribution N(mu, sigma) ────────────────────────────────── z-scores: 1.282 (90%), 1.645 (95%), 2.33 (99%).
Imports
open Array; open Math; open Statistics;
Table of Contents

Functions

normalSample

def normalSample (mu: Float) (sigma: {s : Float | s > 0.0}) (n: {m : Int | m > 0}) : {xs : Array Float | Array.size xs > 0 && (fracBelow xs (mu + 2.33 * sigma) >= 0.99 && (fracBelow xs (mu + 1.645 * sigma) >= 0.95 && (fracBelow xs (mu + 1.282 * sigma) >= 0.9 && (fracBelow xs mu >= 0.5 && (fracAbove xs (mu - 1.282 * sigma) >= 0.9 && (fracAbove xs (mu - 1.645 * sigma) >= 0.95 && fracAbove xs (mu - 2.33 * sigma) >= 0.99))))))}

standardNormalSample

def standardNormalSample (n: {m : Int | m > 0}) : {xs : Array Float | Array.size xs > 0 && (fracBelow xs 2.33 >= 0.99 && (fracBelow xs 1.645 >= 0.95 && (fracBelow xs 1.282 >= 0.9 && (fracBelow xs 0.0 >= 0.5 && (fracAbove xs 0.0 >= 0.5 && (fracAbove xs (0.0 - 1.282) >= 0.9 && fracAbove xs (0.0 - 2.33) >= 0.99))))))}

uniformSample

def uniformSample (a: Float) (b: {bb : Float | bb > a}) (n: {m : Int | m > 0}) : {xs : Array Float | Array.size xs > 0 && (fracAbove xs a >= 1.0 && (fracBelow xs b >= 1.0 && (fracBelow xs (a + 0.99 * (b - a)) >= 0.99 && (fracBelow xs (a + 0.95 * (b - a)) >= 0.95 && (fracBelow xs (a + 0.5 * (b - a)) >= 0.5 && fracBelow xs (a + 0.1 * (b - a)) >= 0.1)))))}

exponentialSample

def exponentialSample (lam: {l : Float | l > 0.0}) (n: {m : Int | m > 0}) : {xs : Array Float | Array.size xs > 0 && (fracAbove xs 0.0 >= 1.0 && (fracBelow xs (4.6052 / lam) >= 0.99 && (fracBelow xs (2.9957 / lam) >= 0.95 && (fracBelow xs (2.3026 / lam) >= 0.9 && fracBelow xs (0.6931 / lam) >= 0.5))))}

betaSample

def betaSample (alpha: {a : Float | a > 0.0}) (beta: {b : Float | b > 0.0}) (n: {m : Int | m > 0}) : {xs : Array Float | Array.size xs > 0 && (fracAbove xs 0.0 >= 1.0 && (fracBelow xs 1.0 >= 1.0 && sampleMean xs == alpha / (alpha + beta)))}

gammaSample

def gammaSample (k: {kk : Float | kk > 0.0}) (theta: {th : Float | th > 0.0}) (n: {m : Int | m > 0}) : {xs : Array Float | Array.size xs > 0 && (fracAbove xs 0.0 >= 1.0 && (sampleMean xs == k * theta && sampleVar xs == k * (theta * theta)))}

chiSquaredSample

def chiSquaredSample (k: {kk : Int | kk > 0}) (n: {m : Int | m > 0}) : {xs : Array Float | Array.size xs > 0 && fracAbove xs 0.0 >= 1.0}

bernoulliSample

def bernoulliSample (p: {pp : Float | pp >= 0.0 && pp <= 1.0}) (n: {m : Int | m > 0}) : {xs : Array Float | Array.size xs > 0 && (fracBelow xs 0.5 >= 1.0 - p && (fracAbove xs 0.5 >= p && (fracBelow xs 1.5 >= 1.0 && fracAbove xs (0.0 - 0.5) >= 1.0)))}

binomialSample

def binomialSample (trials: {t : Int | t > 0}) (p: {pp : Float | pp >= 0.0 && pp <= 1.0}) (n: {m : Int | m > 0}) : {xs : Array Float | Array.size xs > 0 && fracAbove xs (0.0 - 0.5) >= 1.0}

poissonSample

def poissonSample (lam: {l : Float | l > 0.0}) (n: {m : Int | m > 0}) : {xs : Array Float | Array.size xs > 0 && (fracAbove xs (0.0 - 0.5) >= 1.0 && sampleMean xs == lam)}