---

Step * 2 2 1 of Lemma real-unit-ball-totally-bounded1


1. n : ℕ+
2. k : ℕ+
3. p : ℝ^n
4. ||p|| ≤ r1
5. ∀i:ℕn. ∃z:ℤ. ((|(r(z)/r(k * 8 * n))| ≤ |p i|) ∧ (|(p i) - (r(z)/r(k * 8 * n))| ≤ (r(2)/r(k * 2 * n))))
6. f : i:ℕn ⟶ ℤ
7. ∀i:ℕn. ((|(r(f i)/r(k * 8 * n))| ≤ |p i|) ∧ (|(p i) - (r(f i)/r(k * 8 * n))| ≤ (r(2)/r(k * 2 * n))))
⊢ Σ{r((f i) * (f i)) | 0≤i≤n - 1} ≤ r((k * 8 * n) * k * 8 * n)
BY
{ ((MoveToConcl (-1) THEN (GenConcl ⌜(k * 8 * n) = N ∈ ℕ+⌝⋅ THENA Auto))
   THEN Thin 5
   THEN (D 0 THENA Auto)
   THEN (Assert Σ{r((f i) * (f i)) | 0≤i≤n - 1} ≤ Σ{r(N * N) * (p i) * (p i) | 0≤i≤n - 1} BY
               ((BLemma `rsum_functionality_wrt_rleq` THEN Auto)
                THEN D 0
                THEN Auto
                THEN (D -4 With ⌜i⌝  THENA Auto)
                THEN D -1))) }

1
.....aux..... 
1. n : ℕ+
2. k : ℕ+
3. p : ℝ^n
4. ||p|| ≤ r1
5. f : i:ℕn ⟶ ℤ
6. N : ℕ+
7. (k * 8 * n) = N ∈ ℕ+
8. i : ℤ
9. 0 ≤ i
10. i ≤ (n - 1)
11. |(r(f i)/r(N))| ≤ |p i|
12. |(p i) - (r(f i)/r(N))| ≤ (r(2)/r(k * 2 * n))
⊢ r((f i) * (f i)) ≤ (r(N * N) * (p i) * (p i))

2
1. n : ℕ+
2. k : ℕ+
3. p : ℝ^n
4. ||p|| ≤ r1
5. f : i:ℕn ⟶ ℤ
6. N : ℕ+
7. (k * 8 * n) = N ∈ ℕ+
8. ∀i:ℕn. ((|(r(f i)/r(N))| ≤ |p i|) ∧ (|(p i) - (r(f i)/r(N))| ≤ (r(2)/r(k * 2 * n))))
9. Σ{r((f i) * (f i)) | 0≤i≤n - 1} ≤ Σ{r(N * N) * (p i) * (p i) | 0≤i≤n - 1}
⊢ Σ{r((f i) * (f i)) | 0≤i≤n - 1} ≤ r(N * N)

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  k  :  \mBbbN{}\msupplus{}
3.  p  :  \mBbbR{}\^{}n
4.  ||p||  \mleq{}  r1
5.  \mforall{}i:\mBbbN{}n
          \mexists{}z:\mBbbZ{}.  ((|(r(z)/r(k  *  8  *  n))|  \mleq{}  |p  i|)  \mwedge{}  (|(p  i)  -  (r(z)/r(k  *  8  *  n))|  \mleq{}  (r(2)/r(k  *  2  *  n))))
6.  f  :  i:\mBbbN{}n  {}\mrightarrow{}  \mBbbZ{}
7.  \mforall{}i:\mBbbN{}n
          ((|(r(f  i)/r(k  *  8  *  n))|  \mleq{}  |p  i|)  \mwedge{}  (|(p  i)  -  (r(f  i)/r(k  *  8  *  n))|  \mleq{}  (r(2)/r(k  *  2  *  n))))
\mvdash{}  \mSigma{}\{r((f  i)  *  (f  i))  |  0\mleq{}i\mleq{}n  -  1\}  \mleq{}  r((k  *  8  *  n)  *  k  *  8  *  n)


By

---

Latex:
((MoveToConcl  (-1)  THEN  (GenConcl  \mkleeneopen{}(k  *  8  *  n)  =  N\mkleeneclose{}\mcdot{}  THENA  Auto))
  THEN  Thin  5
  THEN  (D  0  THENA  Auto)
  THEN  (Assert  \mSigma{}\{r((f  i)  *  (f  i))  |  0\mleq{}i\mleq{}n  -  1\}  \mleq{}  \mSigma{}\{r(N  *  N)  *  (p  i)  *  (p  i)  |  0\mleq{}i\mleq{}n  -  1\}  BY
                          ((BLemma  `rsum\_functionality\_wrt\_rleq`  THEN  Auto)
                            THEN  D  0
                            THEN  Auto
                            THEN  (D  -4  With  \mkleeneopen{}i\mkleeneclose{}    THENA  Auto)
                            THEN  D  -1)))

---

Home Index