---

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


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))
13. |(r(f i)/r(N))^2| ≤ |p i^2|
⊢ r((f i) * (f i)) ≤ (r(N * N) * (p i) * (p i))
BY
{ (RWO  "rabs-of-nonneg" (-1) THENA Auto) }

1
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))
13. (r(f i)/r(N))^2 ≤ p i^2
⊢ r((f i) * (f i)) ≤ (r(N * N) * (p i) * (p i))

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  k  :  \mBbbN{}\msupplus{}
3.  p  :  \mBbbR{}\^{}n
4.  ||p||  \mleq{}  r1
5.  f  :  i:\mBbbN{}n  {}\mrightarrow{}  \mBbbZ{}
6.  N  :  \mBbbN{}\msupplus{}
7.  (k  *  8  *  n)  =  N
8.  i  :  \mBbbZ{}
9.  0  \mleq{}  i
10.  i  \mleq{}  (n  -  1)
11.  |(r(f  i)/r(N))|  \mleq{}  |p  i|
12.  |(p  i)  -  (r(f  i)/r(N))|  \mleq{}  (r(2)/r(k  *  2  *  n))
13.  |(r(f  i)/r(N))\^{}2|  \mleq{}  |p  i\^{}2|
\mvdash{}  r((f  i)  *  (f  i))  \mleq{}  (r(N  *  N)  *  (p  i)  *  (p  i))


By

---

Latex:
(RWO    "rabs-of-nonneg"  (-1)  THENA  Auto)

---

Home Index