Distributions
Imports
open Array;
open Math;
open Random;
open Statistics;
Types
Functions
def sample_next (d : SampleDraw) : Rng
def normal_sample (1 g : Rng) (mu : Float) (sigma : Float | sigma > 0.0) (n : Int | n > 0) : SampleDraw
def normal_value (mu : Float) (sigma : Float | sigma > 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)
)
)
)
)
)
}
def standard_normal_sample (1 g : Rng) (n : Int | n > 0) : SampleDraw
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))
)
)
)
)
}
def exponential_sample (1 g : Rng) (lam : Float | lam > 0.0) (n : Int | n > 0) : SampleDraw
def exponential_value (lam : Float | lam > 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))
)
)
}
def beta_sample (1 g : Rng) (alpha : Float | alpha > 0.0) (beta : Float | beta > 0.0) (n : Int | n > 0) : SampleDraw
def beta_value (alpha : Float | alpha > 0.0) (beta : Float | beta > 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)))
}
def gamma_sample (1 g : Rng) (k : Float | k > 0.0) (theta : Float | theta > 0.0) (n : Int | n > 0) : SampleDraw
def gamma_value (k : Float | k > 0.0) (theta : Float | theta > 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)))
}
def chi_squared_sample (1 g : Rng) (k : Int | k > 0) (n : Int | n > 0) : SampleDraw
def chi_squared_value (d : SampleDraw) : {xs : Array Float | Array.size xs > 0 && fracAbove xs 0.0 ≥ 1.0}
def bernoulli_sample (1 g : Rng) (p : Float | p ≥ 0.0 && p ≤ 1.0) (n : Int | n > 0) : SampleDraw
def bernoulli_value (p : Float | p ≥ 0.0 && p ≤ 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)))
}
def binomial_sample (1 g : Rng) (trials : Int | trials > 0) (p : Float | p ≥ 0.0 && p ≤ 1.0) (n : Int | n > 0) : SampleDraw
def binomial_value (d : SampleDraw) : {xs : Array Float | Array.size xs > 0 && fracAbove xs (0.0 - 0.5) ≥ 1.0}
def poisson_sample (1 g : Rng) (lam : Float | lam > 0.0) (n : Int | n > 0) : SampleDraw
def poisson_value (lam : Float | lam > 0.0) (d : SampleDraw) : {xs : Array Float | Array.size xs > 0 && (fracAbove xs (0.0 - 0.5) ≥ 1.0 && sampleMean xs = lam)}