Nuprl Definition : p-open-measure-one
measure(C) = 1 == ∀m:ℕ+. ∃n:ℕ. ((1 - (1/m)) ≤ E(n;λs.(C <n, s>)))
Definitions occuring in Statement :
expectation: E(n;F),
qle: r ≤ s,
qsub: r - s,
qdiv: (r/s),
nat_plus: ℕ+,
nat: ℕ,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
apply: f a,
lambda: λx.A[x],
pair: <a, b>,
natural_number: $n
FDL editor aliases :
p-open-measure-one
Latex:
measure(C) = 1 == \mforall{}m:\mBbbN{}\msupplus{}. \mexists{}n:\mBbbN{}. ((1 - (1/m)) \mleq{} E(n;\mlambda{}s.(C <n, s>)))
Date html generated:
2016_05_15-PM-11_49_04
Last ObjectModification:
2008_02_27-PM-05_49_31
Theory : randomness
Home
Index