---

Step * of Lemma expectation-rv-disjoint

∀[p:FinProbSpace]. ∀[n:ℕ]. ∀[X,Y:RandomVariable(p;n)].
  E(n;X * Y) = (E(n;X) * E(n;Y)) ∈ ℚ supposing rv-disjoint(p;n;X;Y)
BY
{ ((InductionOnNat THEN Auto) THEN RecUnfold `expectation` 0 THEN Reduce 0 THEN Try ((SplitOnConclITE THEN Auto'))) }

1
1. p : FinProbSpace
2. n : ℤ
3. X : RandomVariable(p;0)
4. Y : RandomVariable(p;0)
5. rv-disjoint(p;0;X;Y)
⊢ (X * Y null) = ((X null) * (Y null)) ∈ ℚ

2
.....falsecase..... 
1. p : FinProbSpace
2. n : ℤ
3. 0 < n
4. ∀[X,Y:RandomVariable(p;n - 1)].  E(n - 1;X * Y) = (E(n - 1;X) * E(n - 1;Y)) ∈ ℚ supposing rv-disjoint(p;n - 1;X;Y)
5. X : RandomVariable(p;n)
6. Y : RandomVariable(p;n)
7. rv-disjoint(p;n;X;Y)
8. ¬(n = 0 ∈ ℤ)
⊢ weighted-sum(p;λx.E(n - 1;rv-shift(x;X * Y)))
= (weighted-sum(p;λx.E(n - 1;rv-shift(x;X))) * weighted-sum(p;λx.E(n - 1;rv-shift(x;Y))))
∈ ℚ

---

Latex:


\mforall{}[p:FinProbSpace].  \mforall{}[n:\mBbbN{}].  \mforall{}[X,Y:RandomVariable(p;n)].
    E(n;X  *  Y)  =  (E(n;X)  *  E(n;Y))  supposing  rv-disjoint(p;n;X;Y)


By

((InductionOnNat  THEN  Auto)
  THEN  RecUnfold  `expectation`  0
  THEN  Reduce  0
  THEN  Try  ((SplitOnConclITE  THEN  Auto')))

---

Home Index