Step
*
1
1
of Lemma
Cauchy-Schwarz1-strict-iff
1. n : ℕ
2. x : ℕn + 1 ⟶ ℝ
3. y : ℕn + 1 ⟶ ℝ
4. (r(2) * Σ{x[i] * y[i] | 0≤i≤n} * Σ{x[i] * y[i] | 0≤i≤n}) < ((Σ{x[i] * x[i] | 0≤i≤n} * Σ{y[i] * y[i] | 0≤i≤n})
+ (Σ{y[i] * y[i] | 0≤i≤n} * Σ{x[i] * x[i] | 0≤i≤n}))
⊢ ∃i,j:ℕn + 1. x[j] * y[i] ≠ x[i] * y[j]
BY
{ ((RWW "rsum_product" (-1) THENA Auto)
THEN RWW "rsum_linearity2<" (-1)
THEN Auto
THEN RWW "rsum_linearity1<" (-1)
THEN Auto) }
1
1. n : ℕ
2. x : ℕn + 1 ⟶ ℝ
3. y : ℕn + 1 ⟶ ℝ
4. Σ{Σ{r(2) * (x[i] * y[i]) * x[i1] * y[i1] | 0≤i1≤n} | 0≤i≤n} < Σ{Σ{((x[i] * x[i]) * y[i1] * y[i1])
+ ((y[i] * y[i]) * x[i1] * x[i1]) | 0≤i1≤n} | 0≤i≤n}
⊢ ∃i,j:ℕn + 1. x[j] * y[i] ≠ x[i] * y[j]
Latex:
Latex:
1. n : \mBbbN{}
2. x : \mBbbN{}n + 1 {}\mrightarrow{} \mBbbR{}
3. y : \mBbbN{}n + 1 {}\mrightarrow{} \mBbbR{}
4. (r(2) * \mSigma{}\{x[i] * y[i] | 0\mleq{}i\mleq{}n\} * \mSigma{}\{x[i] * y[i] | 0\mleq{}i\mleq{}n\}) < ((\mSigma{}\{x[i] * x[i] | 0\mleq{}i\mleq{}n\}
* \mSigma{}\{y[i] * y[i] | 0\mleq{}i\mleq{}n\})
+ (\mSigma{}\{y[i] * y[i] | 0\mleq{}i\mleq{}n\} * \mSigma{}\{x[i] * x[i] | 0\mleq{}i\mleq{}n\}))
\mvdash{} \mexists{}i,j:\mBbbN{}n + 1. x[j] * y[i] \mneq{} x[i] * y[j]
By
Latex:
((RWW "rsum\_product" (-1) THENA Auto)
THEN RWW "rsum\_linearity2<" (-1)
THEN Auto
THEN RWW "rsum\_linearity1<" (-1)
THEN Auto)
Home
Index