Nuprl Lemma : expectation-imax-list
∀[p:FinProbSpace]. ∀[n:ℕ]. ∀[k:ℕ+]. ∀[X:ℕk ─→ (ℕn ─→ Outcome) ─→ ℕ].
(E(n;λs.imax-list(map(λi.(X i s);upto(k)))) ≤ Σ0 ≤ i < k. E(n;X i))
Proof
Definitions occuring in Statement :
expectation: E(n;F),
p-outcome: Outcome,
finite-prob-space: FinProbSpace,
upto: upto(n),
imax-list: imax-list(L),
map: map(f;as),
nat_plus: ℕ+,
int_seg: {i..j-},
nat: ℕ,
uall: ∀[x:A]. B[x],
apply: f a,
lambda: λx.A[x],
function: x:A ─→ B[x],
natural_number: $n
Lemmas :
expectation-monotone,
imax-list_wf,
map_wf,
int_seg_wf,
nat_wf,
upto_wf,
less_than_wf,
squash_wf,
true_wf,
map_length_nat,
iff_weakening_equal,
length_upto,
nat_plus_subtype_nat,
p-outcome_wf,
subtype_rel_dep_function,
length_wf,
rationals_wf,
int-subtype-rationals,
Error :qsum_wf,
subtype_rel_set,
le_wf,
length-map,
Error :qsum-int,
Error :qle-int,
imax-list-lb,
l_all_iff,
l_member_wf,
exists_wf,
member_map,
all_wf,
Error :summand-qle-sum,
zero-le-nat,
Error :qle_wf,
expectation_wf,
expectation-qsum,
random-variable_wf
\mforall{}[p:FinProbSpace]. \mforall{}[n:\mBbbN{}]. \mforall{}[k:\mBbbN{}\msupplus{}]. \mforall{}[X:\mBbbN{}k {}\mrightarrow{} (\mBbbN{}n {}\mrightarrow{} Outcome) {}\mrightarrow{} \mBbbN{}].
(E(n;\mlambda{}s.imax-list(map(\mlambda{}i.(X i s);upto(k)))) \mleq{} \mSigma{}0 \mleq{} i < k. E(n;X i))
Date html generated:
2015_07_17-AM-07_59_50
Last ObjectModification:
2015_02_03-PM-09_45_03
Home
Index