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),
nat: ℕ,
all: ∀x:A. B[x],
and: P ∧ Q,
equal: s = t ∈ T,
qmul: r * s,
rationals: ℚ
Definitions :
all: ∀x:A. B[x],
nat: ℕ,
and: P ∧ Q,
equal: s = t ∈ T,
rationals: ℚ,
expectation: E(n;F),
rv-compose: (x.F[x]) o X,
qmul: r * s
FDL editor aliases :
rv-identically-distributed
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:
2015_07_17-AM-08_01_58
Last ObjectModification:
2008_02_27-PM-05_49_57
Home
Index