---

Step * of Lemma approx-ball-to-ball_wf

∀[n:ℕ]. ∀[k:ℕ+]. ∀[p:unit-ball-approx(n;k)].  (approx-ball-to-ball(k;p) ∈ B(n))
BY
{ (Auto
   THEN (Assert approx-ball-to-ball(k;p) ∈ ℝ^n BY
               ProveWfLemma)
   THEN D -2
   THEN MemTypeCD
   THEN Auto
   THEN (InstLemma `square-rleq-1-iff` [⌜||approx-ball-to-ball(k;p)||⌝]⋅ THENA Auto)
   THEN (RWO "rabs-of-nonneg" (-1) THENA Auto)
   THEN (RWO "real-vec-norm-squared" (-1) THENA Auto)
   THEN BackThruSomeHyp
   THEN RepUR ``dot-product approx-ball-to-ball`` 0
   THEN RepeatFor 2 (Thin (-1))) }

1
1. n : ℕ
2. k : ℕ+
3. p : ℕn ⟶ {-k..k + 1-}
4. Σ((p i) * (p i) | i < n) ≤ (k * k)
⊢ Σ{(r(p i))/k * (r(p i))/k | 0≤i≤n - 1} ≤ r1

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[k:\mBbbN{}\msupplus{}].  \mforall{}[p:unit-ball-approx(n;k)].    (approx-ball-to-ball(k;p)  \mmember{}  B(n))


By

---

Latex:
(Auto
  THEN  (Assert  approx-ball-to-ball(k;p)  \mmember{}  \mBbbR{}\^{}n  BY
                          ProveWfLemma)
  THEN  D  -2
  THEN  MemTypeCD
  THEN  Auto
  THEN  (InstLemma  `square-rleq-1-iff`  [\mkleeneopen{}||approx-ball-to-ball(k;p)||\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "rabs-of-nonneg"  (-1)  THENA  Auto)
  THEN  (RWO  "real-vec-norm-squared"  (-1)  THENA  Auto)
  THEN  BackThruSomeHyp
  THEN  RepUR  ``dot-product  approx-ball-to-ball``  0
  THEN  RepeatFor  2  (Thin  (-1)))

---

Home Index