From 0b33610dd515c9fd8c01f2c41d78c60994ac6258 Mon Sep 17 00:00:00 2001 From: Yoshihiro Imai Date: Wed, 16 Sep 2026 16:50:20 +0900 Subject: [PATCH] chore: :memo: Links in deflist in Rocqnavi comments --- theories/probability_theory/random_variable.v | 28 +++++++++---------- 1 file changed, 14 insertions(+), 14 deletions(-) diff --git a/theories/probability_theory/random_variable.v b/theories/probability_theory/random_variable.v index 9d975b517c..c3de66847e 100644 --- a/theories/probability_theory/random_variable.v +++ b/theories/probability_theory/random_variable.v @@ -19,53 +19,53 @@ From mathcomp Require Import lebesgue_measure lebesgue_integral hoelder. (* of `Lfun P n` hypotheses instead of the `integrable` predicate from *) (* `lebesgue_integral.v`. *) (* *) -(* `{RV P >-> T'}` *) +(* [`{RV P >-> T'}`](#31c5002a151d32a5908113f99aedfaa1) *) (* : random variable: a measurable function to the `measurableType T'` *) (* from the measured space characterized by the probability `P` *) (* *) -(* `distribution P X` *) +(* [`distribution P X`](#distribution) *) (* : 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]` *) +(* [`'E_P[X]`](#69ec4e730a589c79df0349357bb8311f) *) (* : expectation of the real measurable function `X` *) (* *) -(* `covariance X Y` *) +(* [`covariance X Y`](#covariance) *) (* : covariance between real random variable `X` and `Y` *) (* *) -(* `'V_P[X]` *) +(* [`'V_P[X]`](#de9eec9fd477bbbff8d31b0d161e82f0) *) (* : variance of the real random variable `X` *) (* *) -(* `'M_P X` *) +(* [`'M_P X`](#:::'''M_'_x_x) *) (* : moment generating function of the random variable `X` with sample *) (* space corresponding to the probability measure `P` *) (* *) -(* `{dmfun T >-> R}` *) +(* [`{dmfun T >-> R}`](#b17f6ab1cd771e519085733c5b2ec6bc) *) (* : type of discrete real-valued measurable functions *) (* *) -(* `{dRV P >-> R}` *) +(* [`{dRV P >-> R}`](#b5a1ea6c8f3277fde90807f8c5935ab3) *) (* : real-valued discrete random variable *) (* *) -(* `dRV_dom X` *) +(* [`dRV_dom X`](#dRV_dom) *) (* : domain of the discrete random variable `X` *) (* *) -(* `dRV_enum X` *) +(* [`dRV_enum X`](#dRV_enum) *) (* : bijection between the domain and the range of `X` *) (* *) -(* `pmf X r` *) +(* [`pmf X r`](#pmf) *) (* : ``fine (P (X @^-1` [set r]))`` *) (* *) -(* `cdf X r` *) +(* [`cdf X r`](#cdf) *) (* : cumulative distribution function of `X` *) (* : ``:= distribution P X `]-oo, r]`` *) (* *) -(* `ccdf X r` *) +(* [`ccdf X r`](#ccdf) *) (* : complementary cumulative distribution function of `X` *) (* : := ``distribution P X `]r, +oo[`` *) (* *) -(* `enum_prob X k` *) +(* [`enum_prob X k`](#enum_prob) *) (* : probability of the kth value in the range of `X` *) (* *) (* *)