---

Step * of Lemma Cauchy-Schwarz-equality

∀[n:ℕ]. ∀[x,y:ℝ^n].  ((r0 < ||y||) ⇒ (|x⋅y| = (||x|| * ||y||)) ⇒ req-vec(n;x;(x⋅y/||y||^2)*y))
BY
{ (Auto
   THEN (Assert r0 < ||y||^2 BY
               (BLemma `rnexp-positive` THEN Auto))
   THEN Auto
   THEN (Assert ¬(|x⋅y| < (||x|| * ||y||)) BY
               Auto)
   THEN (RWO "Cauchy-Schwarz-not-strict" (-1) THENA Auto)) }

1
1. n : ℕ
2. x : ℝ^n
3. y : ℝ^n
4. r0 < ||y||
5. |x⋅y| = (||x|| * ||y||)
6. r0 < ||y||^2
7. ∀i,j:ℕn.  (((x j) * (y i)) = ((x i) * (y j)))
⊢ req-vec(n;x;(x⋅y/||y||^2)*y)

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[x,y:\mBbbR{}\^{}n].    ((r0  <  ||y||)  {}\mRightarrow{}  (|x\mcdot{}y|  =  (||x||  *  ||y||))  {}\mRightarrow{}  req-vec(n;x;(x\mcdot{}y/||y||\^{}2)*y))


By

---

Latex:
(Auto
  THEN  (Assert  r0  <  ||y||\^{}2  BY
                          (BLemma  `rnexp-positive`  THEN  Auto))
  THEN  Auto
  THEN  (Assert  \mneg{}(|x\mcdot{}y|  <  (||x||  *  ||y||))  BY
                          Auto)
  THEN  (RWO  "Cauchy-Schwarz-not-strict"  (-1)  THENA  Auto))

---

Home Index