---

Step * 1 of Lemma ws-lower-bound


1. p : {p:ℚ List| (Σ0 ≤ i < ||p||. p[i] = 1 ∈ ℚ) ∧ (∀q∈p.0 ≤ q)} 
2. F : ℕ||p|| ─→ ℚ
3. q : ℚ
4. ∀x:ℕ||p||. (q ≤ (F x))
5. weighted-sum(p;λs.q) ≤ weighted-sum(p;F)
⊢ q ≤ weighted-sum(p;F)
BY
{ (NthHypEq (-1)
   THEN EqCD
   THEN Auto
   THEN Try ((Fold `finite-prob-space` 1 THEN Complete (Auto)))
   THEN Try ((Unfold `p-outcome` 0 THEN Auto))) }

1
.....subterm..... T:t
1:n
1. p : {p:ℚ List| (Σ0 ≤ i < ||p||. p[i] = 1 ∈ ℚ) ∧ (∀q∈p.0 ≤ q)} 
2. F : ℕ||p|| ─→ ℚ
3. q : ℚ
4. ∀x:ℕ||p||. (q ≤ (F x))
5. weighted-sum(p;λs.q) ≤ weighted-sum(p;F)
⊢ q = weighted-sum(p;λs.q) ∈ ℚ

---

Latex:



1.  p  :  \{p:\mBbbQ{}  List|  (\mSigma{}0  \mleq{}  i  <  ||p||.  p[i]  =  1)  \mwedge{}  (\mforall{}q\mmember{}p.0  \mleq{}  q)\} 
2.  F  :  \mBbbN{}||p||  {}\mrightarrow{}  \mBbbQ{}
3.  q  :  \mBbbQ{}
4.  \mforall{}x:\mBbbN{}||p||.  (q  \mleq{}  (F  x))
5.  weighted-sum(p;\mlambda{}s.q)  \mleq{}  weighted-sum(p;F)
\mvdash{}  q  \mleq{}  weighted-sum(p;F)


By

(NthHypEq  (-1)
  THEN  EqCD
  THEN  Auto
  THEN  Try  ((Fold  `finite-prob-space`  1  THEN  Complete  (Auto)))
  THEN  Try  ((Unfold  `p-outcome`  0  THEN  Auto)))

---

Home Index