Distributions

Distributions.ae — linear batch samplers (issue #441 follow-up). Each producer draws a batch from a linear ``Rng`` (``libraries/Random.ae``), returning an opaque ``SampleDraw`` paired with the successor generator. Project the array through the distribution-specific ``*_value`` function (where the quantile-bound refinements live), then bind ``sample_next`` to continue the chain. Batch draws never use ``numpy.random`` or other global RNG state. Refinement-language predicates (fracBelow, fracAbove, sampleMean, ...) and their monotonicity axioms (widenBelow, widenAbove, ...) live in Statistics. Opaque batch draw: a sample array paired with the successor generator.
Imports
open Array; open Math; open Random; open Statistics;
Table of Contents

Types

SampleDraw

(type)
Opaque batch draw: a sample array paired with the successor generator.
type SampleDraw

Functions

sample_next

def sample_next (d: SampleDraw) : Rng

normal_sample

def normal_sample (g: Rng) (mu: Float) (sigma: {s : Float | s > 0.0}) (n: {m : Int | m > 0}) : SampleDraw

normal_value

def normal_value (mu: Float) (sigma: {s : Float | s > 0.0}) (d: SampleDraw) : {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))))))}

standard_normal_sample

def standard_normal_sample (g: Rng) (n: {m : Int | m > 0}) : SampleDraw

standard_normal_value

def standard_normal_value (d: SampleDraw) : {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))))))}

uniform_sample

def uniform_sample (g: Rng) (a: Float) (b: {bb : Float | bb > a}) (n: {m : Int | m > 0}) : SampleDraw

uniform_value

def uniform_value (a: Float) (b: {bb : Float | bb > a}) (d: SampleDraw) : {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)))))}

exponential_sample

def exponential_sample (g: Rng) (lam: {l : Float | l > 0.0}) (n: {m : Int | m > 0}) : SampleDraw

exponential_value

def exponential_value (lam: {l : Float | l > 0.0}) (d: SampleDraw) : {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))))}

beta_sample

def beta_sample (g: Rng) (alpha: {a : Float | a > 0.0}) (beta: {b : Float | b > 0.0}) (n: {m : Int | m > 0}) : SampleDraw

beta_value

def beta_value (alpha: {a : Float | a > 0.0}) (beta: {b : Float | b > 0.0}) (d: SampleDraw) : {xs : Array Float | Array.size xs > 0 && (fracAbove xs 0.0 ≥ 1.0 && (fracBelow xs 1.0 ≥ 1.0 && sampleMean xs = alpha / (alpha + beta)))}

gamma_sample

def gamma_sample (g: Rng) (k: {kk : Float | kk > 0.0}) (theta: {th : Float | th > 0.0}) (n: {m : Int | m > 0}) : SampleDraw

gamma_value

def gamma_value (k: {kk : Float | kk > 0.0}) (theta: {th : Float | th > 0.0}) (d: SampleDraw) : {xs : Array Float | Array.size xs > 0 && (fracAbove xs 0.0 ≥ 1.0 && (sampleMean xs = k * theta && sampleVar xs = k * (theta * theta)))}

chi_squared_sample

def chi_squared_sample (g: Rng) (k: {kk : Int | kk > 0}) (n: {m : Int | m > 0}) : SampleDraw

chi_squared_value

def chi_squared_value (d: SampleDraw) : {xs : Array Float | Array.size xs > 0 && fracAbove xs 0.0 ≥ 1.0}

bernoulli_sample

def bernoulli_sample (g: Rng) (p: {pp : Float | pp ≥ 0.0 && pp ≤ 1.0}) (n: {m : Int | m > 0}) : SampleDraw

bernoulli_value

def bernoulli_value (p: {pp : Float | pp ≥ 0.0 && pp ≤ 1.0}) (d: SampleDraw) : {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)))}

binomial_sample

def binomial_sample (g: Rng) (trials: {t : Int | t > 0}) (p: {pp : Float | pp ≥ 0.0 && pp ≤ 1.0}) (n: {m : Int | m > 0}) : SampleDraw

binomial_value

def binomial_value (d: SampleDraw) : {xs : Array Float | Array.size xs > 0 && fracAbove xs (0.0 - 0.5) ≥ 1.0}

poisson_sample

def poisson_sample (g: Rng) (lam: {l : Float | l > 0.0}) (n: {m : Int | m > 0}) : SampleDraw

poisson_value

def poisson_value (lam: {l : Float | l > 0.0}) (d: SampleDraw) : {xs : Array Float | Array.size xs > 0 && (fracAbove xs (0.0 - 0.5) ≥ 1.0 && sampleMean xs = lam)}