Nuprl Definition : frequency
frequency(f;x) ~ (p/q) == ∀m,k:ℕ. ∃j:ℕ. (k < j c∧ |#{i<j|f i eq x}/j - p/q| < 1/m)
Definitions occuring in Statement :
seq-count: #{i<j|f i eq x},
ratio-dist: |a/b - p/q| < 1/m,
nat: ℕ,
less_than: a < b,
cand: A c∧ B,
all: ∀x:A. B[x],
exists: ∃x:A. B[x]
Definitions occuring in definition :
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
nat: ℕ,
cand: A c∧ B,
less_than: a < b,
ratio-dist: |a/b - p/q| < 1/m,
seq-count: #{i<j|f i eq x}
FDL editor aliases :
frequency
Latex:
frequency(f;x) \msim{} (p/q) == \mforall{}m,k:\mBbbN{}. \mexists{}j:\mBbbN{}. (k < j c\mwedge{} |\#\{i<j|f i eq x\}/j - p/q| < 1/m)
Date html generated:
2016_05_15-PM-04_44_00
Last ObjectModification:
2015_09_23-AM-07_50_01
Theory : general
Home
Index