---

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


1. n : ℕ
2. k : ℕ+
3. p : B(n)
4. ¬(n = 0 ∈ ℤ)
⊢ ∃q:unit-ball-approx(n;k * 8 * n). (d(p;approx-ball-to-ball(k * 8 * n;q)) ≤ (r1/r(k)))
BY
{ ((GenConcl ⌜n = m ∈ ℕ+⌝⋅ THENA Auto)
   THEN Eliminate ⌜n⌝⋅
   THEN ThinVar `n'
   THEN RenameVar `n' 1
   THEN Thin (-1)
   THEN D -1
   THEN (Assert ∀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)))) BY
               ((D 0 THENA Auto) THEN InstLemma `rational-inner-approx-int` [⌜p i⌝;⌜k * 2 * n⌝]⋅ THEN Auto))
   THEN (Skolemize (-1) `f' THENA Auto)
   THEN (D 0 With ⌜f⌝  THENW (Try (MemTypeCD) THEN Auto))) }

1
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))))
⊢ f ∈ ℕn ⟶ {-(k * 8 * n)..(k * 8 * n) + 1-}

2
.....set predicate..... 
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))))
⊢ Σ((f i) * (f i) | i < n) ≤ ((k * 8 * n) * k * 8 * n)

3
1. n : ℕ+
2. k : ℕ+
3. p : ℝ^n
4. [%1] : ||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))))
⊢ d(p;approx-ball-to-ball(k * 8 * n;f)) ≤ (r1/r(k))

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  k  :  \mBbbN{}\msupplus{}
3.  p  :  B(n)
4.  \mneg{}(n  =  0)
\mvdash{}  \mexists{}q:unit-ball-approx(n;k  *  8  *  n).  (d(p;approx-ball-to-ball(k  *  8  *  n;q))  \mleq{}  (r1/r(k)))


By

---

Latex:
((GenConcl  \mkleeneopen{}n  =  m\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Eliminate  \mkleeneopen{}n\mkleeneclose{}\mcdot{}
  THEN  ThinVar  `n'
  THEN  RenameVar  `n'  1
  THEN  Thin  (-1)
  THEN  D  -1
  THEN  (Assert  \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))))  BY
                          ((D  0  THENA  Auto)
                            THEN  InstLemma  `rational-inner-approx-int`  [\mkleeneopen{}p  i\mkleeneclose{};\mkleeneopen{}k  *  2  *  n\mkleeneclose{}]\mcdot{}
                            THEN  Auto))
  THEN  (Skolemize  (-1)  `f'  THENA  Auto)
  THEN  (D  0  With  \mkleeneopen{}f\mkleeneclose{}    THENW  (Try  (MemTypeCD)  THEN  Auto)))

---

Home Index