### Nuprl Lemma : expectation-rv-sample

`∀[p:FinProbSpace]. ∀[n:ℕ]. ∀[i:ℕn]. ∀[X:Outcome ─→ ℚ].  (E(n;X@i) = weighted-sum(p;X) ∈ ℚ)`

Proof

Definitions occuring in Statement :  expectation: `E(n;F)` rv-sample: `X@i` weighted-sum: `weighted-sum(p;F)` p-outcome: `Outcome` finite-prob-space: `FinProbSpace` int_seg: `{i..j-}` nat: `ℕ` uall: `∀[x:A]. B[x]` function: `x:A ─→ B[x]` natural_number: `\$n` equal: `s = t ∈ T` rationals: `ℚ`
Lemmas :  nat_properties less_than_transitivity1 less_than_irreflexivity ge_wf less_than_wf p-outcome_wf rationals_wf int_seg_wf decidable__le subtract_wf false_wf not-ge-2 less-iff-le condition-implies-le minus-one-mul zero-add minus-add minus-minus add-associates add-swap add-commutes add_functionality_wrt_le add-zero le-add-cancel nat_wf finite-prob-space_wf equal-wf-base int_subtype_base assert_wf bnot_wf not_wf uiff_transitivity eqtt_to_assert assert_of_eq_int iff_transitivity iff_weakening_uiff eqff_to_assert assert_of_bnot decidable__equal_int le_weakening2 rv-sample_wf rv-shift_wf le_wf not-le-2 expectation-constant true_wf squash_wf weighted-sum_wf2 subtype_base_sq equal_wf expectation_wf ws-constant length_wf lelt_wf le-add-cancel-alt decidable__lt minus-zero sq_stable__le not-equal-2 equal-wf-T-base bool_wf eq_int_wf
\mforall{}[p:FinProbSpace].  \mforall{}[n:\mBbbN{}].  \mforall{}[i:\mBbbN{}n].  \mforall{}[X:Outcome  {}\mrightarrow{}  \mBbbQ{}].    (E(n;X@i)  =  weighted-sum(p;X))

Date html generated: 2015_07_17-AM-07_59_03
Last ObjectModification: 2015_07_16-AM-09_52_18

Home Index