---

Step * 1 1 of Lemma q-Cauchy-Schwarz

.....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]))
BY
{ ((RWW "qsum_product" 0 THENA Auto) THEN RWW "qsum-linearity1<" 0 THEN Auto)⋅ }

1
1. n : ℕ
2. x : ℕn + 1 ⟶ ℚ
3. y : ℕn + 1 ⟶ ℚ
⊢ Σ0 ≤ i < n. Σ0 ≤ i1 < n. 2 * (x[i] * y[i]) * x[i1] * y[i1] ≤ (Σ0 ≤ i < n. Σ0 ≤ i1 < n. (x[i] * x[i]) * y[i1] * y[i1]
+ Σ0 ≤ i < n. Σ0 ≤ i1 < n. (y[i] * y[i]) * x[i1] * x[i1])

---

Latex:

---

Latex:
.....assertion..... 
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{}  ((\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]))


By

---

Latex:
((RWW  "qsum\_product"  0  THENA  Auto)  THEN  RWW  "qsum-linearity1<"  0  THEN  Auto)\mcdot{}

---

Home Index