Module Main

# Probability This file provides basic notions of probability theory. See `measure.v` for the type `probability T R` (a measure that sums to 1). `{RV P >-> T'}` ~ random variable: a measurable function to the `measurableType T'` from the measured space characterized by the probability `P` `distribution P X` ~ measure image of the probability measure `P` by the random variable `X : {RV P -> T'}` ~ `P` has type `probability T R` with `T` of type `measurableType`. ~ Declared as an instance of probability measure. `'E_P[X]` ~ expectation of the real measurable function X `covariance X Y` ~ covariance between real random variable X and Y `'V_P[X]` ~ variance of the real random variable `X` `'M_ X` ~ moment generating function of the random variable `X` `{dmfun T >-> R}` ~ type of discrete real-valued measurable functions `{dRV P >-> R}` ~ real-valued discrete random variable `dRV_dom X` ~ domain of the discrete random variable `X` `dRV_enum X` ~ bijection between the domain and the range of `X` `pmf X r` ~ ``fine (P (X @^-1` [set r]))`` `cdf X r` ~ cumulative distribution function of `X` ~ ``:= distribution P X `]-oo, r]`` `enum_prob X k` ~ probability of the kth value in the range of `X` `bernoulli_pmf p` ~ Bernoulli pmf with parameter `p : R` `bernoulli p` ~ Bernoulli probability measure when `0 <= p <= 1` and `\d_false` otherwise `binomial_pmf n p` ~ binomial pmf with parameters `n : nat` and `p : R` `binomial_prob n p` ~ binomial probability measure when `0 <= p <= 1` and `\d_0%N` otherwise `bin_prob n k p` ~ $\binom{n}{k}p^k (1-p)^{(n-k)}$ ~ Computes a binomial distribution term for $k$ successes in $n$ trials with success rate $p$ `uniform_pdf a b` ~ uniform pdf over the interval $[a,b]$ `uniform_prob a b ab` ~ uniform probability over the interval $[a,b]$ where `ab0` a proof that `0 < b - a` `normal_peak s` ~ `(sqrtr (s ^+ 2 * pi *+ 2))^-1` `normal_fun m s x` ~ `expR (- (x - m) ^+ 2 / (s ^+ 2 *+ 2))` `normal_pdf m s` ~ pdf of the normal distribution with mean `m` and standard deviation `s` ~ Using normal_peak and normal_pdf. `normal_prob m s` ~ normal probability measure

# Measure Theory NB: See CONTRIBUTING.md for an introduction to HB concepts and commands. This files provides a formalization of the basics of measure theory. This includes the formalization of mathematical structures and of measures, as well as standard theorems such as the Measure Extension theorem that builds a measure given a function defined over a semiring of sets, the intermediate outer measure being $\inf_F\{ \sum_{k=0}^\infty \mu(F_k) | X \subseteq \bigcup_k F_k\}.$ References: - R. Affeldt, C. Cohen. Measure construction by extension in dependent type theory with application to integration. JAR 2023 - Daniel Li. Intégration et applications. 2016 - Achim Klenke. Probability Theory. 2014 ## Mathematical structures `semiRingOfSetsType d` ~ the type of semirings of sets ~ The carrier is a set of sets A_i such that "measurable A_i" holds. ~ `measurable A` is printed as `d.-measurable A` where d is a "display parameter" whose purpose is to distinguish different `measurable` predicates in the same context. ~ The HB class is `SemiRingOfSets`. `ringOfSetsType d` ~ the type of rings of sets ~ The HB class is `RingOfSets`. `sigmaRingType d` ~ the type of sigma-rings (of sets) ~ The HB class is `SigmaRing`. `algebraOfSetsType d` ~ the type of algebras of sets ~ The HB class is `AlgebraOfsets`. `measurableType` ~ the type of sigma-algebras ~ The HB class is `Measurable`.