---

Step * of Lemma ws-lower-bound

∀[p:FinProbSpace]. ∀[F:Outcome ⟶ ℚ]. ∀[q:ℚ].  q ≤ weighted-sum(p;F) supposing ∀x:Outcome. (q ≤ (F x))
BY
{ (Unfolds ``finite-prob-space p-outcome`` 0
   THEN Auto
   THEN ((InstLemma `ws-monotone` [⌜p⌝; ⌜λs.q⌝; ⌜F⌝])⋅ THENA Auto)
   THEN Reduce 0
   THEN Try (((DVar `p' THEN Unhide) THEN Auto THEN RWO "l_all_iff" 3 THEN Complete (Auto)))) }

1
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)

---

Latex:

---

Latex:
\mforall{}[p:FinProbSpace].  \mforall{}[F:Outcome  {}\mrightarrow{}  \mBbbQ{}].  \mforall{}[q:\mBbbQ{}].
    q  \mleq{}  weighted-sum(p;F)  supposing  \mforall{}x:Outcome.  (q  \mleq{}  (F  x))


By

---

Latex:
(Unfolds  ``finite-prob-space  p-outcome``  0
  THEN  Auto
  THEN  ((InstLemma  `ws-monotone`  [\mkleeneopen{}p\mkleeneclose{};  \mkleeneopen{}\mlambda{}s.q\mkleeneclose{};  \mkleeneopen{}F\mkleeneclose{}])\mcdot{}  THENA  Auto)
  THEN  Reduce  0
  THEN  Try  (((DVar  `p'  THEN  Unhide)  THEN  Auto  THEN  RWO  "l\_all\_iff"  3  THEN  Complete  (Auto))))

---

Home Index