Skip to content

Commit eae4ba7

Browse files
yoshihiro503yoshihiro503
authored
chore: 📝 Rocqdoc deflist sample (#2047)
1 parent 1024276 commit eae4ba7

1 file changed

Lines changed: 48 additions & 26 deletions

File tree

‎theories/probability_theory/random_variable.v‎

Lines changed: 48 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -19,32 +19,54 @@ From mathcomp Require Import lebesgue_measure lebesgue_integral hoelder.
1919
(* of `Lfun P n` hypotheses instead of the `integrable` predicate from *)
2020
(* `lebesgue_integral.v`. *)
2121
(* *)
22-
(* ``` *)
23-
(* {RV P >-> T'} == random variable: a measurable function to the *)
24-
(* measurableType T' from the measured space *)
25-
(* characterized by the probability P *)
26-
(* distribution P X == measure image of the probability measure P by the *)
27-
(* random variable X : {RV P -> T'} *)
28-
(* P as type probability T R with T of type *)
29-
(* measurableType. *)
30-
(* Declared as an instance of probability measure. *)
31-
(* 'E_P[X] == expectation of the real measurable function X *)
32-
(* covariance X Y == covariance between real random variable X and Y *)
33-
(* 'V_P[X] == variance of the real random variable X *)
34-
(* 'M_P X == moment generating function of the random variable X *)
35-
(* with sample space corresponding to the probability *)
36-
(* measure P *)
37-
(* {dmfun T >-> R} == type of discrete real-valued measurable functions *)
38-
(* {dRV P >-> R} == real-valued discrete random variable *)
39-
(* dRV_dom X == domain of the discrete random variable X *)
40-
(* dRV_enum X == bijection between the domain and the range of X *)
41-
(* pmf X r := fine (P (X @^-1` [set r])) *)
42-
(* cdf X r == cumulative distribution function of X *)
43-
(* := distribution P X `]-oo, r] *)
44-
(* ccdf X r == complementary cumulative distribution function of X *)
45-
(* := distribution P X `]r, +oo[ *)
46-
(* enum_prob X k == probability of the kth value in the range of X *)
47-
(* ``` *)
22+
(* `{RV P >-> T'}` *)
23+
(* ~ random variable: a measurable function to the `measurableType T'` *)
24+
(* from the measured space characterized by the probability `P` *)
25+
(* *)
26+
(* `distribution P X` *)
27+
(* ~ measure image of the probability measure `P` by the random variable *)
28+
(* `X : {RV P -> T'}` *)
29+
(* ~ `P` has type `probability T R` with `T` of type `measurableType`. *)
30+
(* ~ Declared as an instance of probability measure. *)
31+
(* *)
32+
(* `'E_P[X]` *)
33+
(* ~ expectation of the real measurable function `X` *)
34+
(* *)
35+
(* `covariance X Y` *)
36+
(* ~ covariance between real random variable `X` and `Y` *)
37+
(* *)
38+
(* `'V_P[X]` *)
39+
(* ~ variance of the real random variable `X` *)
40+
(* *)
41+
(* `'M_P X` *)
42+
(* ~ moment generating function of the random variable `X` with sample *)
43+
(* space corresponding to the probability measure `P` *)
44+
(* *)
45+
(* `{dmfun T >-> R}` *)
46+
(* ~ type of discrete real-valued measurable functions *)
47+
(* *)
48+
(* `{dRV P >-> R}` *)
49+
(* ~ real-valued discrete random variable *)
50+
(* *)
51+
(* `dRV_dom X` *)
52+
(* ~ domain of the discrete random variable `X` *)
53+
(* *)
54+
(* `dRV_enum X` *)
55+
(* ~ bijection between the domain and the range of `X` *)
56+
(* *)
57+
(* `pmf X r` *)
58+
(* ~ ``fine (P (X @^-1` [set r]))`` *)
59+
(* *)
60+
(* `cdf X r` *)
61+
(* ~ cumulative distribution function of `X` *)
62+
(* ~ ``:= distribution P X `]-oo, r]`` *)
63+
(* *)
64+
(* `ccdf X r` *)
65+
(* ~ complementary cumulative distribution function of `X` *)
66+
(* ~ := ``distribution P X `]r, +oo[`` *)
67+
(* *)
68+
(* `enum_prob X k` *)
69+
(* ~ probability of the kth value in the range of `X` *)
4870
(* *)
4971
(* *)
5072
(******************************************************************************)

0 commit comments

Comments
 (0)