---

Step * 1 of Lemma q-Cauchy-Schwarz


1. n : ℕ
2. x : ℕn + 1 ⟶ ℚ
3. y : ℕn + 1 ⟶ ℚ
⊢ (2 * Σ0 ≤ i < n. x[i] * y[i] * Σ0 ≤ i < n. x[i] * y[i]) ≤ (2 * Σ0 ≤ i < n. x[i] * x[i] * Σ0 ≤ i < n. y[i] * y[i])
BY
{ Assert ⌜(2 * Σ0 ≤ i < n. 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]))⌝⋅ }

1
.....assertion..... 
1. n : ℕ
2. x : ℕn + 1 ⟶ ℚ
3. y : ℕn + 1 ⟶ ℚ
⊢ (2 * Σ0 ≤ i < n. 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]))

2
1. n : ℕ
2. x : ℕn + 1 ⟶ ℚ
3. y : ℕn + 1 ⟶ ℚ
4. (2 * Σ0 ≤ i < n. 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]))
⊢ (2 * Σ0 ≤ i < n. x[i] * y[i] * Σ0 ≤ i < n. x[i] * y[i]) ≤ (2 * Σ0 ≤ i < n. x[i] * x[i] * Σ0 ≤ i < n. y[i] * y[i])

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  x  :  \mBbbN{}n  +  1  {}\mrightarrow{}  \mBbbQ{}
3.  y  :  \mBbbN{}n  +  1  {}\mrightarrow{}  \mBbbQ{}
\mvdash{}  (2  *  \mSigma{}0  \mleq{}  i  <  n.  x[i]  *  y[i]  *  \mSigma{}0  \mleq{}  i  <  n.  x[i]  *  y[i])  \mleq{}  (2
*  \mSigma{}0  \mleq{}  i  <  n.  x[i]  *  x[i]
*  \mSigma{}0  \mleq{}  i  <  n.  y[i]  *  y[i])


By

---

Latex:
Assert  \mkleeneopen{}(2  *  \mSigma{}0  \mleq{}  i  <  n.  x[i]  *  y[i]  *  \mSigma{}0  \mleq{}  i  <  n.  x[i]  *  y[i])  \mleq{}  ((\mSigma{}0  \mleq{}  i  <  n.  x[i]  *  x[i]
                *  \mSigma{}0  \mleq{}  i  <  n.  y[i]  *  y[i])
                +  (\mSigma{}0  \mleq{}  i  <  n.  y[i]  *  y[i]  *  \mSigma{}0  \mleq{}  i  <  n.  x[i]  *  x[i]))\mkleeneclose{}\mcdot{}

---

Home Index