---

Step * 2 1 1 of Lemma unit-ball-to-unit-cube


1. n : ℕ+
2. λi.r0 ∈ ℝ^n
3. max-metric(n) ≤ rn-metric(n)
4. rn-metric(n) ≤ r(n)*max-metric(n)
5. ∀p:{p:ℝ^n| r0 < mdist(max-metric(n);p;λi.r0)} . ((||p||/mdist(max-metric(n);p;λi.r0))*p ∈ ℝ^n)
6. m : ℕ+
7. p : ℝ^n
8. r0 < mdist(max-metric(n);p;λi.r0)
9. mdist(max-metric(n);p;λi.r0) ≤ (r(4)/r(m))
10. r0 < mdist(max-metric(n);λi.r0;p)
11. r0 < ||p||
12. (||p||/mdist(max-metric(n);p;λi.r0)) ∈ ℝ
13. v : ℝ
14. mdist(max-metric(n);p;λi.r0) = v ∈ ℝ
15. r0 < v
16. r0 < mdist(max-metric(n);λi.r0;p)
⊢ (|(||p||/v)| * mdist(rn-metric(n);p;λi.r0)) ≤ (r(4 * n * n)/r(m))
BY
{ (RWO "rabs-of-nonneg" 0 THENA Auto) }

1
.....rewrite subgoal..... 
1. n : ℕ+
2. λi.r0 ∈ ℝ^n
3. max-metric(n) ≤ rn-metric(n)
4. rn-metric(n) ≤ r(n)*max-metric(n)
5. ∀p:{p:ℝ^n| r0 < mdist(max-metric(n);p;λi.r0)} . ((||p||/mdist(max-metric(n);p;λi.r0))*p ∈ ℝ^n)
6. m : ℕ+
7. p : ℝ^n
8. r0 < mdist(max-metric(n);p;λi.r0)
9. mdist(max-metric(n);p;λi.r0) ≤ (r(4)/r(m))
10. r0 < mdist(max-metric(n);λi.r0;p)
11. r0 < ||p||
12. (||p||/mdist(max-metric(n);p;λi.r0)) ∈ ℝ
13. v : ℝ
14. mdist(max-metric(n);p;λi.r0) = v ∈ ℝ
15. r0 < v
16. r0 < mdist(max-metric(n);λi.r0;p)
⊢ r0 ≤ (||p||/v)

2
1. n : ℕ+
2. λi.r0 ∈ ℝ^n
3. max-metric(n) ≤ rn-metric(n)
4. rn-metric(n) ≤ r(n)*max-metric(n)
5. ∀p:{p:ℝ^n| r0 < mdist(max-metric(n);p;λi.r0)} . ((||p||/mdist(max-metric(n);p;λi.r0))*p ∈ ℝ^n)
6. m : ℕ+
7. p : ℝ^n
8. r0 < mdist(max-metric(n);p;λi.r0)
9. mdist(max-metric(n);p;λi.r0) ≤ (r(4)/r(m))
10. r0 < mdist(max-metric(n);λi.r0;p)
11. r0 < ||p||
12. (||p||/mdist(max-metric(n);p;λi.r0)) ∈ ℝ
13. v : ℝ
14. mdist(max-metric(n);p;λi.r0) = v ∈ ℝ
15. r0 < v
16. r0 < mdist(max-metric(n);λi.r0;p)
⊢ ((||p||/v) * mdist(rn-metric(n);p;λi.r0)) ≤ (r(4 * n * n)/r(m))

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  \mlambda{}i.r0  \mmember{}  \mBbbR{}\^{}n
3.  max-metric(n)  \mleq{}  rn-metric(n)
4.  rn-metric(n)  \mleq{}  r(n)*max-metric(n)
5.  \mforall{}p:\{p:\mBbbR{}\^{}n|  r0  <  mdist(max-metric(n);p;\mlambda{}i.r0)\}  .  ((||p||/mdist(max-metric(n);p;\mlambda{}i.r0))*p  \mmember{}  \mBbbR{}\^{}n)
6.  m  :  \mBbbN{}\msupplus{}
7.  p  :  \mBbbR{}\^{}n
8.  r0  <  mdist(max-metric(n);p;\mlambda{}i.r0)
9.  mdist(max-metric(n);p;\mlambda{}i.r0)  \mleq{}  (r(4)/r(m))
10.  r0  <  mdist(max-metric(n);\mlambda{}i.r0;p)
11.  r0  <  ||p||
12.  (||p||/mdist(max-metric(n);p;\mlambda{}i.r0))  \mmember{}  \mBbbR{}
13.  v  :  \mBbbR{}
14.  mdist(max-metric(n);p;\mlambda{}i.r0)  =  v
15.  r0  <  v
16.  r0  <  mdist(max-metric(n);\mlambda{}i.r0;p)
\mvdash{}  (|(||p||/v)|  *  mdist(rn-metric(n);p;\mlambda{}i.r0))  \mleq{}  (r(4  *  n  *  n)/r(m))


By

---

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

---

Home Index