Module infotheo.toy_examples.expected_value_variance_ordn
Require realType_ext.From mathcomp Require Import all_ssreflect ssralg ssrnum lra ring.
From mathcomp Require Import reals.
Require Import realType_ext ssralg_ext fdist proba.
Set Implicit Arguments.
Set SsrOldRewriteGoalsOrder.
Unset Strict Implicit.
Import Prenex Implicits.
Local Open Scope reals_ext_scope.
Local Open Scope tuple_ext_scope.
Local Open Scope ring_scope.
Import GRing.Theory Num.Theory Order.Theory.
From mathcomp Require Import normedtype.
Import numFieldNormedType.Exports.
Section expected_value_variance_ordn.
Variable R : realType.
Definition
ord1
{n} := lift ord0 (@ord0 n).ord1 : all_equal_to (ord0 : 'I_1) ord1 is not universe polymorphic Arguments ord1 x ord1 is opaque Expands to: Constant mathcomp.boot.fintype.ord1 Declared in library mathcomp.boot.fintype, line 2260, characters 6-10
Definition
ord2
{n} := lift ord0 (@ord1 n).ord2 not a defined object.
Lemma ord0E n : 0%nat = @ord0 n
Proof.
done. Qed.
Proof.
done. Qed.
Proof.
done. Qed.
Definition
pmf
: {ffun 'I_3 -> R} :=pmf not a defined object.
finfun [fun x => 0 with ord0 |-> 1/2, ord1 |-> 1/3, ord2 |-> 1/6].
Lemma pmf_ge0 : [forall a : 'I_3, 0 <= pmf a].
Lemma pmf01 : [forall a, 0 <= pmf a] && (\sum_(a in 'I_3) pmf a == 1).
Proof.
Local Open Scope fdist_scope.
Local Open Scope proba_scope.
Definition
P
: {fdist 'I_3} := FDist.mk pmf01.P not a defined object.
Definition
X
: {RV P -> R} := (fun i => i.+1%:R).X not a defined object.
Lemma expected : `E X = 5/3.
Proof.
Lemma variance : `V X = 5/9.
Proof.
End expected_value_variance_ordn.