Nuprl Lemma : Markov-inequality
∀[p:FinProbSpace]. ∀[n:ℕ]. ∀[X:RandomVariable(p;n)]. ∀[e:ℚ]. E(n;e ≤ X) ≤ (E(n;X)/e) supposing 0 < e supposing 0 ≤ X
Proof
Definitions occuring in Statement :
rv-le: X ≤ Y,
expectation: E(n;F),
rv-const: a,
rv-qle: A ≤ B,
random-variable: RandomVariable(p;n),
finite-prob-space: FinProbSpace,
qle: r ≤ s,
qless: r < s,
qdiv: (r/s),
rationals: ℚ,
nat: ℕ,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
natural_number: $n
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
not: ¬A,
implies: P ⇒ Q,
guard: {T},
subtype_rel: A ⊆r B,
false: False,
prop: ℙ,
squash: ↓T,
true: True,
iff: P ⇐⇒ Q,
and: P ∧ Q,
rev_implies: P ⇐ Q,
qdiv: (r/s),
uiff: uiff(P;Q),
rv-scale: q*X,
rv-const: a,
rv-qle: A ≤ B,
rv-le: X ≤ Y,
all: ∀x:A. B[x],
nat: ℕ,
random-variable: RandomVariable(p;n),
p-outcome: Outcome,
rev_uimplies: rev_uimplies(P;Q),
bool: 𝔹,
unit: Unit,
it: ⋅,
btrue: tt,
ifthenelse: if b then t else f fi ,
bfalse: ff
Lemmas referenced :
qle_witness,
expectation_wf,
rv-qle_wf,
rv-const_wf,
qdiv_wf,
qless_transitivity_2_qorder,
int-subtype-rationals,
qle_weakening_eq_qorder,
qless_irreflexivity,
equal-wf-T-base,
rationals_wf,
qless_wf,
rv-le_wf,
random-variable_wf,
nat_wf,
finite-prob-space_wf,
equal_wf,
squash_wf,
true_wf,
expectation-rv-scale,
iff_weakening_equal,
expectation-monotone,
rv-scale_wf,
qle_wf,
assert-qeq,
assert_wf,
qeq_wf2,
not_wf,
qmul_wf,
qinv_wf,
qmul_assoc_qrng,
qmul_one_qrng,
qmul_comm_qrng,
qinv-positive,
int_seg_wf,
p-outcome_wf,
q_le_wf,
bool_wf,
qmul_preserves_qle,
bnot_wf,
uiff_transitivity2,
eqtt_to_assert,
assert-q_le-eq,
uiff_transitivity,
eqff_to_assert,
assert_of_bnot,
qmul_ac_1_qrng,
qmul-qdiv-cancel,
qmul_zero_qrng
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
hypothesis,
because_Cache,
independent_isectElimination,
lambdaFormation,
natural_numberEquality,
applyEquality,
sqequalRule,
voidElimination,
baseClosed,
independent_functionElimination,
isect_memberEquality,
equalityTransitivity,
equalitySymmetry,
lambdaEquality,
imageElimination,
universeEquality,
imageMemberEquality,
productElimination,
hyp_replacement,
applyLambdaEquality,
addLevel,
impliesFunctionality,
dependent_functionElimination,
functionEquality,
setElimination,
rename,
functionExtensionality,
unionElimination,
equalityElimination
Latex:
\mforall{}[p:FinProbSpace]. \mforall{}[n:\mBbbN{}]. \mforall{}[X:RandomVariable(p;n)].
\mforall{}[e:\mBbbQ{}]. E(n;e \mleq{} X) \mleq{} (E(n;X)/e) supposing 0 < e supposing 0 \mleq{} X
Date html generated:
2018_05_22-AM-00_35_59
Last ObjectModification:
2017_07_26-PM-07_00_21
Theory : randomness
Home
Index