---

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


1. n : ℕ
2. k : ℕ+
3. p : ℕn ⟶ {-k..k + 1-}
4. Σ((p i) * (p i) | i < n) ≤ (k * k)
⊢ Σ{(r(p i))/k * (r(p i))/k | 0≤i≤n - 1} ≤ r1
BY
{ (RenameVar `s' (-2) THEN (RWO "int-rdiv-req" 0 THENA Auto)) }

1
1. n : ℕ
2. k : ℕ+
3. s : ℕn ⟶ {-k..k + 1-}
4. Σ((s i) * (s i) | i < n) ≤ (k * k)
⊢ Σ{(r(s i)/r(k)) * (r(s i)/r(k)) | 0≤i≤n - 1} ≤ r1

---

Latex:

---

Latex:

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


By

---

Latex:
(RenameVar  `s'  (-2)  THEN  (RWO  "int-rdiv-req"  0  THENA  Auto))

---

Home Index