---

Step * of Lemma expectation-qsum

∀[k:ℕ]. ∀[p:FinProbSpace]. ∀[n:ℕ]. ∀[X:ℕk ─→ RandomVariable(p;n)].
  (E(n;λs.Σ0 ≤ i < k. X i s) = Σ0 ≤ i < k. E(n;X i) ∈ ℚ)
BY
{ (InductionOnNat THEN Auto) }

1
1. k : ℤ
2. p : FinProbSpace
3. n : ℕ
4. X : ℕ0 ─→ RandomVariable(p;n)
⊢ E(n;λs.Σ0 ≤ i < 0. X i s) = Σ0 ≤ i < 0. E(n;X i) ∈ ℚ

2
1. k : ℤ
2. 0 < k
3. ∀[p:FinProbSpace]. ∀[n:ℕ]. ∀[X:ℕk - 1 ─→ RandomVariable(p;n)].
     (E(n;λs.Σ0 ≤ i < k - 1. X i s) = Σ0 ≤ i < k - 1. E(n;X i) ∈ ℚ)
4. p : FinProbSpace
5. n : ℕ
6. X : ℕk ─→ RandomVariable(p;n)
⊢ E(n;λs.Σ0 ≤ i < k. X i s) = Σ0 ≤ i < k. E(n;X i) ∈ ℚ

---

Latex:


\mforall{}[k:\mBbbN{}].  \mforall{}[p:FinProbSpace].  \mforall{}[n:\mBbbN{}].  \mforall{}[X:\mBbbN{}k  {}\mrightarrow{}  RandomVariable(p;n)].
    (E(n;\mlambda{}s.\mSigma{}0  \mleq{}  i  <  k.  X  i  s)  =  \mSigma{}0  \mleq{}  i  <  k.  E(n;X  i))


By

(InductionOnNat  THEN  Auto)

---

Home Index