---

Step * of Lemma q-Cauchy-Schwarz

∀[n:ℕ]. ∀[x,y:ℕn + 1 ⟶ ℚ].
  ((Σ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]))
BY
{ (Auto THEN QMul ⌜2⌝ 0⋅ THEN Auto) }

1
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])

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[x,y:\mBbbN{}n  +  1  {}\mrightarrow{}  \mBbbQ{}].
    ((\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]))


By

---

Latex:
(Auto  THEN  QMul  \mkleeneopen{}2\mkleeneclose{}  0\mcdot{}  THEN  Auto)

---

Home Index