---

Step * 1 1 1 2 of Lemma approx-ball-to-ball_wf


1. n : ℕ
2. k : ℕ+
3. s : ℕn ⟶ {-k..k + 1-}
4. Σ((s i) * (s i) | i < n) ≤ (k * k)
5. Σ{r(s i) * r(s i) | 0≤i≤n - 1} ≤ r(k * k)
6. Σ{(r(s i)/r(k)) * (r(s i)/r(k)) | 0≤i≤n - 1} = Σ{(r1/r(k * k)) * r(s i) * r(s i) | 0≤i≤n - 1}
⊢ Σ{(r(s i)/r(k)) * (r(s i)/r(k)) | 0≤i≤n - 1} ≤ r1
BY
{ ((RWO "-1" 0 THENA Auto)
   THEN (RWO "rsum_linearity2" 0 THENA Auto)
   THEN MoveToConcl (-2)
   THEN (GenConclTerm ⌜Σ{r(s i) * r(s i) | 0≤i≤n - 1}⌝⋅ THENA Auto)) }

1
1. n : ℕ
2. k : ℕ+
3. s : ℕn ⟶ {-k..k + 1-}
4. Σ((s i) * (s i) | i < n) ≤ (k * k)
5. Σ{(r(s i)/r(k)) * (r(s i)/r(k)) | 0≤i≤n - 1} = Σ{(r1/r(k * k)) * r(s i) * r(s i) | 0≤i≤n - 1}
6. v : ℝ
7. Σ{r(s i) * r(s i) | 0≤i≤n - 1} = v ∈ ℝ
⊢ (v ≤ r(k * k)) ⇒ (((r1/r(k * k)) * v) ≤ r1)

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  k  :  \mBbbN{}\msupplus{}
3.  s  :  \mBbbN{}n  {}\mrightarrow{}  \{-k..k  +  1\msupminus{}\}
4.  \mSigma{}((s  i)  *  (s  i)  |  i  <  n)  \mleq{}  (k  *  k)
5.  \mSigma{}\{r(s  i)  *  r(s  i)  |  0\mleq{}i\mleq{}n  -  1\}  \mleq{}  r(k  *  k)
6.  \mSigma{}\{(r(s  i)/r(k))  *  (r(s  i)/r(k))  |  0\mleq{}i\mleq{}n  -  1\}  =  \mSigma{}\{(r1/r(k  *  k))  *  r(s  i)  *  r(s  i)  |  0\mleq{}i\mleq{}n  -  1\}
\mvdash{}  \mSigma{}\{(r(s  i)/r(k))  *  (r(s  i)/r(k))  |  0\mleq{}i\mleq{}n  -  1\}  \mleq{}  r1


By

---

Latex:
((RWO  "-1"  0  THENA  Auto)
  THEN  (RWO  "rsum\_linearity2"  0  THENA  Auto)
  THEN  MoveToConcl  (-2)
  THEN  (GenConclTerm  \mkleeneopen{}\mSigma{}\{r(s  i)  *  r(s  i)  |  0\mleq{}i\mleq{}n  -  1\}\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index