---

Step * 1 of Lemma expectation-qsum


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) ∈ ℚ
BY
{ (RepUR ``qsum rng_sum mon_itop`` 0
   THEN RecUnfold `itop` 0
   THEN SplitOnConclITE
   THEN Auto'
   THEN BLemma `expectation-constant`
   THEN Auto
   THEN Reduce 0
   THEN Auto)⋅ }

---

Latex:



1.  k  :  \mBbbZ{}
2.  p  :  FinProbSpace
3.  n  :  \mBbbN{}
4.  X  :  \mBbbN{}0  {}\mrightarrow{}  RandomVariable(p;n)
\mvdash{}  E(n;\mlambda{}s.\mSigma{}0  \mleq{}  i  <  0.  X  i  s)  =  \mSigma{}0  \mleq{}  i  <  0.  E(n;X  i)


By

(RepUR  ``qsum  rng\_sum  mon\_itop``  0
  THEN  RecUnfold  `itop`  0
  THEN  SplitOnConclITE
  THEN  Auto'
  THEN  BLemma  `expectation-constant`
  THEN  Auto
  THEN  Reduce  0
  THEN  Auto)\mcdot{}

---

Home Index