---

Step * 1 1 of Lemma ws-lower-bound

.....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) ∈ ℚ
BY
{ (Symmetry
   THEN BLemma `ws-constant` 
   THEN Auto
   THEN Try ((Fold `finite-prob-space` 1 THEN Complete (Auto)))
   THEN Reduce 0
   THEN Auto) }

---

Latex:


.....subterm.....  T:t
1:n
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  =  weighted-sum(p;\mlambda{}s.q)


By

(Symmetry
  THEN  BLemma  `ws-constant` 
  THEN  Auto
  THEN  Try  ((Fold  `finite-prob-space`  1  THEN  Complete  (Auto)))
  THEN  Reduce  0
  THEN  Auto)

---

Home Index