Nuprl Definition : rv-identically-distributed
rv-identically-distributed(p;n.f[n];i.X[i]) ==
∀n,m:ℕ.
((E(f[n];X[n]) = E(f[m];X[m]) ∈ ℚ)
∧ (E(f[n];(x.x * x) o X[n]) = E(f[m];(x.x * x) o X[m]) ∈ ℚ)
∧ (E(f[n];(x.(x * x) * x) o X[n]) = E(f[m];(x.(x * x) * x) o X[m]) ∈ ℚ)
∧ (E(f[n];(x.(x * x) * x * x) o X[n]) = E(f[m];(x.(x * x) * x * x) o X[m]) ∈ ℚ))
Definitions occuring in Statement :
rv-compose: (x.F[x]) o X,
expectation: E(n;F),
qmul: r * s,
rationals: ℚ,
nat: ℕ,
all: ∀x:A. B[x],
and: P ∧ Q,
equal: s = t ∈ T
FDL editor aliases :
rv-identically-distributed
Latex:
rv-identically-distributed(p;n.f[n];i.X[i]) ==
\mforall{}n,m:\mBbbN{}.
((E(f[n];X[n]) = E(f[m];X[m]))
\mwedge{} (E(f[n];(x.x * x) o X[n]) = E(f[m];(x.x * x) o X[m]))
\mwedge{} (E(f[n];(x.(x * x) * x) o X[n]) = E(f[m];(x.(x * x) * x) o X[m]))
\mwedge{} (E(f[n];(x.(x * x) * x * x) o X[n]) = E(f[m];(x.(x * x) * x * x) o X[m])))
Date html generated:
2016_05_15-PM-11_51_17
Last ObjectModification:
2008_02_27-PM-05_49_57
Theory : randomness
Home
Index