Step
*
of Lemma
rsum-triangle-inequality2
∀[n,m:ℤ]. ∀[x,y:{n..m + 1-} ⟶ ℝ].  ((Σ{|y[i]| | n≤i≤m} - Σ{|x[i]| | n≤i≤m}) ≤ Σ{|x[i] + y[i]| | n≤i≤m})
BY
{ (Auto THEN RWO "rsum-triangle-inequality1" 0 THEN Auto THEN nRNorm 0 THEN Auto) }
Latex:
Latex:
\mforall{}[n,m:\mBbbZ{}].  \mforall{}[x,y:\{n..m  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}].
    ((\mSigma{}\{|y[i]|  |  n\mleq{}i\mleq{}m\}  -  \mSigma{}\{|x[i]|  |  n\mleq{}i\mleq{}m\})  \mleq{}  \mSigma{}\{|x[i]  +  y[i]|  |  n\mleq{}i\mleq{}m\})
By
Latex:
(Auto  THEN  RWO  "rsum-triangle-inequality1"  0  THEN  Auto  THEN  nRNorm  0  THEN  Auto)
Home
Index