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