Step
*
2
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:ℝ^n. (r0 < ||p|| ⇐⇒ r0 < mdist(max-metric(n);λi.r0;p))
⊢ ∃g:ℝ^n ⟶ ℝ^n
((∀p:ℝ^n. (req-vec(n;p;λi.r0) ⇒ g p ≡ λi.r0))
∧ (∀p:{p:ℝ^n| r0 < mdist(max-metric(n);λi.r0;p)} . g p ≡ (λp.(||p||/mdist(max-metric(n);p;λi.r0))*p) p)
∧ (g ∈ {p:ℝ^n| ||p|| ≤ r1} ⟶ {q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1} )
∧ g:FUN(ℝ^n;ℝ^n)
∧ (∀x,y:{p:ℝ^n| ||p|| ≤ r1} . (mdist(max-metric(n);g x;g y) ≤ (r((2 * n) + 1) * mdist(rn-metric(n);x;y)))))
BY
{ ((Assert ∀p:{p:ℝ^n| r0 < mdist(max-metric(n);p;λi.r0)} . ((||p||/mdist(max-metric(n);p;λi.r0))*p ∈ ℝ^n) BY
((D 0 THENA Auto) THEN D -1 THEN RepeatFor 2 (MemCD) THEN Try (OrRight) THEN Auto))
THEN (InstLemma `remove-singularity-max-mfun` [⌜ℝ^n⌝;⌜rn-metric(n)⌝;⌜n⌝;⌜λp.(||p||/mdist(max-metric(n);p;λi.r0))*p⌝;
⌜λi.r0⌝]⋅
THENA (Auto THEN Reduce 0 THEN D 0 With ⌜r(4 * n * n)⌝ THEN Auto)
)
) }
1
1. n : ℕ+
2. λi.r0 ∈ ℝ^n
3. max-metric(n) ≤ rn-metric(n)
4. rn-metric(n) ≤ r(n)*max-metric(n)
5. ∀p:ℝ^n. (r0 < ||p|| ⇐⇒ r0 < mdist(max-metric(n);λi.r0;p))
6. ∀p:{p:ℝ^n| r0 < mdist(max-metric(n);p;λi.r0)} . ((||p||/mdist(max-metric(n);p;λi.r0))*p ∈ ℝ^n)
7. m : ℕ+
8. p : {p:ℝ^n| r0 < mdist(max-metric(n);p;λi.r0)}
9. mdist(max-metric(n);p;λi.r0) ≤ (r(4)/r(m))
⊢ mdist(rn-metric(n);(||p||/mdist(max-metric(n);p;λi.r0))*p;λi.r0) ≤ (r(4 * n * n)/r(m))
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:ℝ^n. (r0 < ||p|| ⇐⇒ r0 < mdist(max-metric(n);λi.r0;p))
6. ∀p:{p:ℝ^n| r0 < mdist(max-metric(n);p;λi.r0)} . ((||p||/mdist(max-metric(n);p;λi.r0))*p ∈ ℝ^n)
7. ∃g:ℝ^n ⟶ ℝ^n
(((∀p:ℝ^n. (req-vec(n;p;λi.r0) ⇒ g p ≡ λi.r0))
∧ (∀p:{p:ℝ^n| r0 < mdist(max-metric(n);p;λi.r0)} . g p ≡ (λp.(||p||/mdist(max-metric(n);p;λi.r0))*p) p))
∧ (λp.(||p||/mdist(max-metric(n);p;λi.r0))*p:FUN({p:ℝ^n| r0 < mdist(max-metric(n);p;λi.r0)} ;ℝ^n) ⇒ g:FUN(ℝ^n;ℝ^n))\000C)
⊢ ∃g:ℝ^n ⟶ ℝ^n
((∀p:ℝ^n. (req-vec(n;p;λi.r0) ⇒ g p ≡ λi.r0))
∧ (∀p:{p:ℝ^n| r0 < mdist(max-metric(n);λi.r0;p)} . g p ≡ (λp.(||p||/mdist(max-metric(n);p;λi.r0))*p) p)
∧ (g ∈ {p:ℝ^n| ||p|| ≤ r1} ⟶ {q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1} )
∧ g:FUN(ℝ^n;ℝ^n)
∧ (∀x,y:{p:ℝ^n| ||p|| ≤ r1} . (mdist(max-metric(n);g x;g y) ≤ (r((2 * n) + 1) * mdist(rn-metric(n);x;y)))))
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:\mBbbR{}\^{}n. (r0 < ||p|| \mLeftarrow{}{}\mRightarrow{} r0 < mdist(max-metric(n);\mlambda{}i.r0;p))
\mvdash{} \mexists{}g:\mBbbR{}\^{}n {}\mrightarrow{} \mBbbR{}\^{}n
((\mforall{}p:\mBbbR{}\^{}n. (req-vec(n;p;\mlambda{}i.r0) {}\mRightarrow{} g p \mequiv{} \mlambda{}i.r0))
\mwedge{} (\mforall{}p:\{p:\mBbbR{}\^{}n| r0 < mdist(max-metric(n);\mlambda{}i.r0;p)\}
g p \mequiv{} (\mlambda{}p.(||p||/mdist(max-metric(n);p;\mlambda{}i.r0))*p) p)
\mwedge{} (g \mmember{} \{p:\mBbbR{}\^{}n| ||p|| \mleq{} r1\} {}\mrightarrow{} \{q:\mBbbR{}\^{}n| mdist(max-metric(n);\mlambda{}i.r0;q) \mleq{} r1\} )
\mwedge{} g:FUN(\mBbbR{}\^{}n;\mBbbR{}\^{}n)
\mwedge{} (\mforall{}x,y:\{p:\mBbbR{}\^{}n| ||p|| \mleq{} r1\} .
(mdist(max-metric(n);g x;g y) \mleq{} (r((2 * n) + 1) * mdist(rn-metric(n);x;y)))))
By
Latex:
((Assert \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) BY
((D 0 THENA Auto) THEN D -1 THEN RepeatFor 2 (MemCD) THEN Try (OrRight) THEN Auto))
THEN (InstLemma `remove-singularity-max-mfun` [\mkleeneopen{}\mBbbR{}\^{}n\mkleeneclose{};\mkleeneopen{}rn-metric(n)\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};
\mkleeneopen{}\mlambda{}p.(||p||/mdist(max-metric(n);p;\mlambda{}i.r0))*p\mkleeneclose{};\mkleeneopen{}\mlambda{}i.r0\mkleeneclose{}]\mcdot{}
THENA (Auto THEN Reduce 0 THEN D 0 With \mkleeneopen{}r(4 * n * n)\mkleeneclose{} THEN Auto)
)
)
Home
Index