Nuprl Lemma : bounded-expectation
∀p:FinProbSpace. ∀f:ℕ ⟶ ℕ. ∀X:n:ℕ ⟶ RandomVariable(p;f[n]). ∀B:ℚ.
(nullset(p;(X[n]⟶∞ as n⟶∞))) supposing
((∀n:ℕ. (0 ≤ X[n] ∧ E(f[n];X[n]) < B)) and
0 < B and
(∀n:ℕ. ∀i:ℕn. X[i] ≤ X[n]) and
(∀n:ℕ. ∀i:ℕn. f[i] < f[n]))
Proof
Definitions occuring in Statement :
rv-unbounded: (X[n]⟶∞ as n⟶∞),
nullset: nullset(p;S),
rv-le: X ≤ Y,
expectation: E(n;F),
rv-const: a,
random-variable: RandomVariable(p;n),
finite-prob-space: FinProbSpace,
qless: r < s,
rationals: ℚ,
int_seg: {i..j-},
nat: ℕ,
less_than: a < b,
uimplies: b supposing a,
so_apply: x[s],
all: ∀x:A. B[x],
and: P ∧ Q,
function: x:A ⟶ B[x],
natural_number: $n
Definitions unfolded in proof :
all: ∀x:A. B[x],
uimplies: b supposing a,
member: t ∈ T,
uall: ∀[x:A]. B[x],
so_apply: x[s],
nat: ℕ,
int_seg: {i..j-},
lelt: i ≤ j < k,
and: P ∧ Q,
le: A ≤ B,
less_than: a < b,
squash: ↓T,
ge: i ≥ j ,
decidable: Dec(P),
or: P ∨ Q,
not: ¬A,
implies: P ⇒ Q,
satisfiable_int_formula: satisfiable_int_formula(fmla),
exists: ∃x:A. B[x],
false: False,
prop: ℙ,
subtype_rel: A ⊆r B,
guard: {T},
uiff: uiff(P;Q),
qdiv: (r/s),
iff: P ⇐⇒ Q,
true: True,
rev_implies: P ⇐ Q,
cand: A c∧ B,
random-variable: RandomVariable(p;n),
finite-prob-space: FinProbSpace,
so_lambda: λ2x.t[x],
less_than': less_than'(a;b),
p-outcome: Outcome,
pi1: fst(t),
pi2: snd(t),
sq_type: SQType(T),
p-open: p-open(p),
p-measure-le: measure(C) ≤ q,
rv-le: X ≤ Y,
rv-const: a,
rv-qle: A ≤ B,
istype: istype(T),
bool: 𝔹,
unit: Unit,
it: ⋅,
btrue: tt,
ifthenelse: if b then t else f fi ,
bfalse: ff,
p-open-member: s ∈ C,
nullset: nullset(p;S),
sq_stable: SqStable(P),
rv-unbounded: (X[n]⟶∞ as n⟶∞)
Lemmas referenced :
member-less_than,
int_seg_properties,
nat_properties,
decidable__le,
full-omega-unsat,
intformand_wf,
intformnot_wf,
intformle_wf,
itermConstant_wf,
itermVar_wf,
istype-int,
int_formula_prop_and_lemma,
int_formula_prop_not_lemma,
int_formula_prop_le_lemma,
int_term_value_constant_lemma,
int_term_value_var_lemma,
int_formula_prop_wf,
istype-le,
istype-nat,
rv-le_witness,
subtype_rel-random-variable,
le_weakening2,
qless_witness,
int-subtype-rationals,
rv-const_wf,
expectation_wf,
rv-le_wf,
qless_wf,
int_seg_wf,
istype-less_than,
rationals_wf,
random-variable_wf,
finite-prob-space_wf,
qless_transitivity_2_qorder,
qle_weakening_eq_qorder,
qless_irreflexivity,
qmul_preserves_qless,
qdiv_wf,
qinv-positive,
qmul_wf,
squash_wf,
true_wf,
qmul_comm_qrng,
qinv_wf,
iff_weakening_uiff,
assert_wf,
qeq_wf2,
equal-wf-T-base,
assert-qeq,
istype-assert,
subtype_rel_self,
iff_weakening_equal,
qmul_zero_qrng,
qmul_assoc_qrng,
qmul_one_qrng,
Markov-inequality,
rv-qle_wf,
equal_wf,
qmul_com,
istype-universe,
not_wf,
qmul-qdiv-cancel2,
qmul_ident,
qdiv-qdiv,
qless_transitivity_1_qorder,
p-open_wf,
p-measure-le_wf,
p-outcome_wf,
qle_wf,
length_wf,
subtype_rel_dep_function,
nat_wf,
int_seg_subtype_nat,
istype-false,
p-open-member_wf,
decidable__exists_int_seg,
less_than_wf,
int_seg_subtype,
decidable__cand,
decidable__lt,
decidable__qle,
decidable_wf,
intformless_wf,
int_formula_prop_less_lemma,
subtype_base_sq,
int_subtype_base,
set_subtype_base,
lelt_wf,
subtype_rel_function,
decidable__equal_int,
intformeq_wf,
int_formula_prop_eq_lemma,
ge_wf,
le_witness_for_triv,
istype-void,
subtract-1-ge-0,
itermSubtract_wf,
int_term_value_subtract_lemma,
subtract_wf,
int_seg_inc,
qle_reflexivity,
expectation-monotone-in-first,
expectation-monotone,
le_weakening,
q_le_wf,
bool_wf,
bnot_wf,
qle-int,
uiff_transitivity2,
eqtt_to_assert,
assert-q_le-eq,
iff_transitivity,
eqff_to_assert,
assert_of_bnot,
qle_transitivity_qorder,
add_nat_wf,
add-is-int-iff,
itermAdd_wf,
int_term_value_add_lemma,
false_wf,
sq_stable_from_decidable,
decidable__qless,
rv-unbounded_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation_alt,
isect_memberFormation_alt,
cut,
introduction,
sqequalRule,
sqequalHypSubstitution,
lambdaEquality_alt,
dependent_functionElimination,
thin,
hypothesisEquality,
extract_by_obid,
isectElimination,
applyEquality,
dependent_set_memberEquality_alt,
setElimination,
rename,
hypothesis,
productElimination,
imageElimination,
natural_numberEquality,
unionElimination,
independent_isectElimination,
approximateComputation,
independent_functionElimination,
dependent_pairFormation_alt,
int_eqEquality,
Error :memTop,
independent_pairFormation,
universeIsType,
voidElimination,
because_Cache,
functionIsTypeImplies,
inhabitedIsType,
closedConclusion,
independent_pairEquality,
functionIsType,
productIsType,
equalityIstype,
promote_hyp,
equalityTransitivity,
equalitySymmetry,
baseClosed,
imageMemberEquality,
instantiate,
universeEquality,
hyp_replacement,
sqequalBase,
functionEquality,
productEquality,
isect_memberEquality_alt,
functionExtensionality,
cumulativity,
intEquality,
dependent_pairEquality_alt,
applyLambdaEquality,
intWeakElimination,
equalityElimination,
addEquality,
pointwiseFunctionality,
baseApply,
setIsType
Latex:
\mforall{}p:FinProbSpace. \mforall{}f:\mBbbN{} {}\mrightarrow{} \mBbbN{}. \mforall{}X:n:\mBbbN{} {}\mrightarrow{} RandomVariable(p;f[n]). \mforall{}B:\mBbbQ{}.
(nullset(p;(X[n]{}\mrightarrow{}\minfty{} as n{}\mrightarrow{}\minfty{}))) supposing
((\mforall{}n:\mBbbN{}. (0 \mleq{} X[n] \mwedge{} E(f[n];X[n]) < B)) and
0 < B and
(\mforall{}n:\mBbbN{}. \mforall{}i:\mBbbN{}n. X[i] \mleq{} X[n]) and
(\mforall{}n:\mBbbN{}. \mforall{}i:\mBbbN{}n. f[i] < f[n]))
Date html generated:
2020_05_20-AM-09_31_52
Last ObjectModification:
2020_01_01-AM-11_22_52
Theory : randomness
Home
Index