:: Extended Real Valued Double Sequence and Its Convergence :: by Noboru Endou :: :: Received July 1, 2015 :: Copyright (c) 2015 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, SUBSET_1, FUNCT_1, RELAT_1, XBOOLE_0, ARYTM_3, ARYTM_1, XXREAL_0, CARD_1, NAT_1, ZFMISC_1, VALUED_0, ORDINAL2, SEQ_2, ORDINAL1, COMPLEX1, XCMPLX_0, XXREAL_2, MESFUNC9, DBLSEQ_1, FUNCOP_1, REAL_1, DBLSEQ_2, DBLSEQ_3, SUPINF_1, SUPINF_2, MESFUNC5, SERIES_1, PARTFUN1, CARD_3, RINFSUP1, QC_LANG1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, BINOP_1, XREAL_0, XXREAL_3, XCMPLX_0, COMPLEX1, PARTFUN1, FUNCT_1, XXREAL_0, RELSET_1, FUNCT_2, FUNCOP_1, NAT_1, XXREAL_2, SUPINF_1, VALUED_0, SUPINF_2, SEQ_2, EXTREAL1, MESFUNC1, MESFUNC5, RINFSUP2, MESFUNC9, DBLSEQ_1, DBLSEQ_2; constructors TOPMETR, NAT_D, MESFUNC9, SEQ_2, COMSEQ_2, DBLSEQ_1, MESFUNC5, SUPINF_1, EXTREAL1, MESFUNC1, RINFSUP2, DBLSEQ_2; registrations ORDINAL1, XXREAL_0, XREAL_0, XBOOLE_0, NUMBERS, XCMPLX_0, SUBSET_1, MEMBERED, VALUED_0, RELSET_1, FUNCT_2, NAT_1, RELAT_1, XXREAL_3, COMPLEX1, RINFSUP2; requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM; equalities BINOP_1, XXREAL_3; theorems TARSKI, XREAL_0, NAT_1, FUNCT_1, XXREAL_0, ZFMISC_1, XREAL_1, FUNCT_2, RELAT_1, MESFUNC9, ORDINAL1, XXREAL_2, SEQM_3, SEQ_2, FUNCOP_1, DBLSEQ_1, EXTREAL1, XXREAL_3, SUPINF_2, MEASURE6, MESFUNC5, XBOOLE_0, FUNCT_3, VALUED_0, MESFUNC1, RINFSUP2, BINOP_1, DBLSEQ_2, MESFUN10; schemes FUNCT_2, DBLSEQ_2, NAT_1, BINOP_1; begin :: Preliminaries Lm1: for X be set, x be object holds (X-->0.).x = 0 proof let X be set, x be object; set M = X-->0.; per cases; suppose x in dom M; then x in X; hence (X-->0.).x = 0 by FUNCOP_1:7; end; suppose not x in dom M; then M.x = 0 by FUNCT_1:def 2; hence (X-->0.).x = 0; end; end; registration let X be non empty set; cluster nonnegative nonpositive for Function of X,REAL; existence proof reconsider M = X --> 0 as Function of X,REAL by FUNCOP_1:45,XREAL_0:def 1; take M; A1:M is Function of X,ExtREAL by FUNCOP_1:45,XXREAL_0:def 1; for x be object holds 0 <= M.x; hence M is nonnegative by A1,SUPINF_2:51; for x be object holds M.x <= 0 by Lm1; hence M is nonpositive by A1,MESFUNC5:8; end; end; registration let X be non empty set; cluster without-infty without+infty nonnegative nonpositive for Function of X,ExtREAL; existence proof reconsider M = X --> 0. as Function of X,ExtREAL; take M; for x be object holds -infty < M.x; hence M is without-infty by MESFUNC5:def 5; for x be object holds M.x < +infty by Lm1; hence M is without+infty by MESFUNC5:def 6; for x be object holds 0 <= M.x; hence M is nonnegative by SUPINF_2:51; for x be object holds M.x <= 0 by Lm1; hence M is nonpositive by MESFUNC5:8; end; end; Lm2: for X be non empty set holds X --> 0. is without-infty Function of X,ExtREAL & X --> 0. is without+infty Function of X,ExtREAL proof let X be non empty set; reconsider P = X --> 0. as Function of X,ExtREAL; for x be object holds -infty < P.x; hence X --> 0. is without-infty Function of X,ExtREAL by MESFUNC5:def 5; reconsider M = X --> 0. as Function of X,ExtREAL; for x be object holds M.x < +infty by Lm1; hence X --> 0. is without+infty Function of X,ExtREAL by MESFUNC5:def 6; end; registration let X be non empty set; cluster nonnegative -> without-infty for Function of X,ExtREAL; correctness proof now let f be nonnegative Function of X,ExtREAL; for x be object holds f.x > -infty by SUPINF_2:51; hence f is without-infty by MESFUNC5:def 5; end; hence thesis; end; cluster nonpositive -> without+infty for Function of X,ExtREAL; correctness proof now let f be nonpositive Function of X,ExtREAL; for x be object holds f.x < +infty by MESFUNC5:8; hence f is without+infty by MESFUNC5:def 6; end; hence thesis; end; cluster without-infty for without+infty Function of X,ExtREAL; existence proof reconsider f = X --> 0. as without+infty Function of X,ExtREAL by Lm2; take f; thus f is without-infty by Lm2; end; end; definition let X be non empty set, f be Function of X,ExtREAL; redefine func -f -> Function of X,ExtREAL; correctness proof dom (-f) = dom f by MESFUNC1:def 7; then A1:dom (-f) = X by FUNCT_2:def 1; now let x be object; assume x in X; then reconsider x1=x as Element of X; (-f).x = -(f.x1) by A1,MESFUNC1:def 7; hence (-f).x in ExtREAL; end; hence -f is Function of X,ExtREAL by A1,FUNCT_2:3; end; end; registration let X be non empty set, f be without-infty Function of X,ExtREAL; cluster -f -> without+infty; correctness proof now let x be object; per cases; suppose A1: x in dom(-f); then reconsider x1=x as Element of X; (-f).x = -(f.x1) by A1,MESFUNC1:def 7; hence (-f).x < +infty by XXREAL_3:5,38,MESFUNC5:def 5; end; suppose not x in dom(-f); hence (-f).x < +infty by FUNCT_1:def 2; end; end; hence -f is without+infty by MESFUNC5:def 6; end; end; registration let X be non empty set, f be without+infty Function of X,ExtREAL; cluster -f -> without-infty; correctness proof now let x be object; per cases; suppose A1: x in dom(-f); then reconsider x1=x as Element of X; (-f).x = -(f.x1) by A1,MESFUNC1:def 7; hence (-f).x > -infty by XXREAL_3:6,38,MESFUNC5:def 6; end; suppose not x in dom(-f); hence (-f).x > -infty by FUNCT_1:def 2; end; end; hence -f is without-infty by MESFUNC5:def 5; end; end; registration let X be non empty set, f be nonnegative Function of X,ExtREAL; cluster -f -> nonpositive; correctness proof now let x be object; per cases; suppose A1: x in dom(-f); then reconsider x1=x as Element of X; A2: (-f).x = -(f.x1) by A1,MESFUNC1:def 7; f.x1 >= 0 by SUPINF_2:51; hence (-f).x <= 0 by A2; end; suppose not x in dom(-f); hence (-f).x <= 0 by FUNCT_1:def 2; end; end; hence -f is nonpositive by MESFUNC5:8; end; end; registration let X be non empty set, f be nonpositive Function of X,ExtREAL; cluster -f -> nonnegative; correctness proof now let x be object; per cases; suppose A1: x in dom(-f); then reconsider x1=x as Element of X; A2: (-f).x = -(f.x1) by A1,MESFUNC1:def 7; f.x1 <= 0 by MESFUNC5:8; hence (-f).x >= 0 by A2; end; suppose not x in dom(-f); hence (-f).x >= 0 by FUNCT_1:def 2; end; end; hence -f is nonnegative by SUPINF_2:51; end; end; registration let A,B be non empty set; let f be without-infty Function of [:A,B:],ExtREAL; cluster f@ -> without-infty; correctness proof now let x be object; per cases; suppose x in dom(f@); then consider b,a be object such that A1: b in B & a in A & x = [b,a] by ZFMISC_1:def 2; reconsider a as Element of A by A1; reconsider b as Element of B by A1; f.(a,b) > -infty by MESFUNC5:def 5; then f@.(b,a) > -infty by DBLSEQ_2:def 2; hence (f@).x > -infty by A1; end; suppose not x in dom(f@); hence (f@).x > -infty by FUNCT_1:def 2; end; end; hence thesis by MESFUNC5:def 5; end; end; registration let A,B be non empty set; let f be without+infty Function of [:A,B:],ExtREAL; cluster f@ -> without+infty; correctness proof now let x be object; per cases; suppose x in dom(f@); then consider b,a be object such that A1: b in B & a in A & x = [b,a] by ZFMISC_1:def 2; reconsider a as Element of A by A1; reconsider b as Element of B by A1; f.(a,b) < +infty by MESFUNC5:def 6; then f@.(b,a) < +infty by DBLSEQ_2:def 2; hence (f@).x < +infty by A1; end; suppose not x in dom(f@); hence (f@).x < +infty by FUNCT_1:def 2; end; end; hence thesis by MESFUNC5:def 6; end; end; registration let A,B be non empty set; let f be nonnegative Function of [:A,B:],ExtREAL; cluster f@ -> nonnegative; correctness proof now let x be object; assume x in dom(f@); then consider b,a be object such that A1: b in B & a in A & x = [b,a] by ZFMISC_1:def 2; reconsider a as Element of A by A1; reconsider b as Element of B by A1; f.(a,b) >= 0 by SUPINF_2:51; then f@.(b,a) >= 0 by DBLSEQ_2:def 2; hence (f@).x >= 0 by A1; end; hence thesis by SUPINF_2:52; end; end; registration let A,B be non empty set; let f be nonpositive Function of [:A,B:],ExtREAL; cluster f@ -> nonpositive; correctness proof now let x be object; per cases; suppose not x in dom(f@); hence (f@).x <= 0. by FUNCT_1:def 2; end; suppose x in dom(f@); then consider b,a be object such that A1: b in B & a in A & x = [b,a] by ZFMISC_1:def 2; reconsider a as Element of A by A1; reconsider b as Element of B by A1; f.(a,b) <= 0 by MESFUNC5:8; then f@.(b,a) <= 0 by DBLSEQ_2:def 2; hence (f@).x <= 0. by A1; end; end; hence f@ is nonpositive by MESFUNC5:8; end; end; theorem Th1: for seq be ExtREAL_sequence holds Partial_Sums(-seq) = -(Partial_Sums seq) proof let seq be ExtREAL_sequence; A1:dom(-seq) = NAT & dom(-(Partial_Sums seq)) = NAT by FUNCT_2:def 1; defpred Q[Nat] means ( -(Partial_Sums seq) ).$1 = -((Partial_Sums seq).$1); A3:Q[0] by A1,MESFUNC1:def 7; A4:for n be Nat st Q[n] holds Q[n+1] by A1,MESFUNC1:def 7; A5:for n be Nat holds Q[n] from NAT_1:sch 2(A3,A4); defpred P[Nat] means (Partial_Sums -(seq)).$1 = (-(Partial_Sums seq)).$1; (Partial_Sums -(seq)).0 = (-seq).0 by MESFUNC9:def 1; then A6:(Partial_Sums -(seq)).0 = -(seq.0) by A1,MESFUNC1:def 7; (Partial_Sums seq).0 = seq.0 by MESFUNC9:def 1; then A7:P[0] by A1,A6,MESFUNC1:def 7; A8:for n be Nat st P[n] holds P[n+1] proof let n be Nat; assume A9: P[n]; (Partial_Sums -(seq)).(n+1) = (-(Partial_Sums seq)).n + (-seq).(n+1) by A9,MESFUNC9:def 1 .= ( -(Partial_Sums seq) ).n + (-(seq.(n+1))) by A1,MESFUNC1:def 7 .= -( (Partial_Sums seq).n ) - (seq.(n+1)) by A5 .= -( (Partial_Sums seq).n + seq.(n+1) ) by XXREAL_3:25 .= -( (Partial_Sums seq).(n+1) ) by MESFUNC9:def 1; hence P[n+1] by A1,MESFUNC1:def 7; end; for n be Nat holds P[n] from NAT_1:sch 2(A7,A8); then for n be Element of NAT holds (Partial_Sums -(seq)).n = (-(Partial_Sums seq)).n; hence thesis by FUNCT_2:def 8; end; theorem Th2: for X be non empty set, f be PartFunc of X,ExtREAL holds -(-f) = f proof let X be non empty set, f be PartFunc of X,ExtREAL; A1:dom f = dom (-f) by MESFUNC1:def 7; then A2:dom f = dom (-(-f)) by MESFUNC1:def 7; now let x be object; assume A3: x in dom f; then (-f).x = -(f.x) by A1,MESFUNC1:def 7; then (-(-f)).x = -(-(f.x)) by A2,A3,MESFUNC1:def 7; hence (-(-f)).x = f.x; end; hence thesis by A2,FUNCT_1:2; end; theorem for X,Y be non empty set, f be Function of [:X,Y:], ExtREAL holds (-f)@ = -(f@) proof let X,Y be non empty set, f be Function of [:X,Y:],ExtREAL; now let z be Element of [:Y,X:]; consider y,x be object such that A1: y in Y & x in X & z = [y,x] by ZFMISC_1:def 2; A2: dom (-f) = [:X,Y:] & dom(-(f@)) = [:Y,X:] by FUNCT_2:def 1; reconsider y as Element of Y by A1; reconsider x as Element of X by A1; reconsider z1 = [x,y] as Element of [:X,Y:] by ZFMISC_1:87; (-f)@.z = (-f)@.(y,x) by A1; then (-f)@.z = (-f).(x,y) by DBLSEQ_2:def 2; then (-f)@.z = -(f.z1) by A2,MESFUNC1:def 7; then (-f)@.z = -(f.(x,y)); then (-f)@.z = -(f@.(y,x)) by DBLSEQ_2:def 2; hence (-f)@.z = (-(f@)).z by A1,A2,MESFUNC1:def 7; end; hence thesis by FUNCT_2:def 8; end; registration let seq be nonnegative ExtREAL_sequence; cluster Partial_Sums seq -> nonnegative; correctness by MESFUNC9:16; end; registration let seq be nonpositive ExtREAL_sequence; cluster Partial_Sums seq -> nonpositive; correctness proof set f = -seq; Partial_Sums f is nonnegative; then -(Partial_Sums seq) is nonnegative by Th1; then --(Partial_Sums seq) is nonpositive; hence Partial_Sums seq is nonpositive by Th2; end; end; theorem Th4: for seq be nonnegative ExtREAL_sequence, m be Nat holds seq.m <= (Partial_Sums seq).m proof let seq be nonnegative ExtREAL_sequence, m be Nat; defpred P[Nat] means seq.$1 <= (Partial_Sums seq).$1; A1:P[0] by MESFUNC9:def 1; A2:for k be Nat st P[k] holds P[k+1] proof let k be Nat; assume P[k]; (Partial_Sums seq).(k+1) = (Partial_Sums seq).k + seq.(k+1) by MESFUNC9:def 1; hence P[k+1] by XXREAL_3:39,SUPINF_2:51; end; for k be Nat holds P[k] from NAT_1:sch 2(A1,A2); hence seq.m <= Partial_Sums(seq).m; end; theorem for seq be nonpositive ExtREAL_sequence, m be Nat holds seq.m >= (Partial_Sums seq).m proof let seq be nonpositive ExtREAL_sequence, m be Nat; reconsider f = -seq as nonnegative ExtREAL_sequence; A1:dom f = NAT & dom seq = NAT & dom (-f) = NAT & dom (Partial_Sums seq) = NAT & dom (-(Partial_Sums seq)) = NAT & dom (-(-(Partial_Sums seq))) = NAT by FUNCT_2:def 1; A2:m in NAT by ORDINAL1:def 12; f.m <= (Partial_Sums f).m by Th4; then f.m <= (-(Partial_Sums seq)).m by Th1; then -((-seq).m) >= -(-(Partial_Sums seq)).m by XXREAL_3:38; then (-(-seq)).m >= -(-(Partial_Sums seq)).m by A1,A2,MESFUNC1:def 7; then seq.m >= -(-(Partial_Sums seq)).m by Th2; then seq.m >= -(-(Partial_Sums seq).m) by A1,A2,MESFUNC1:def 7; hence thesis; end; theorem for X be non empty set, f be without-infty without+infty Function of X,ExtREAL holds f is Function of X,REAL proof let X be non empty set, f be without-infty without+infty Function of X,ExtREAL; A1:dom f = X by FUNCT_2:def 1; now let x be object; assume x in X; then f.x in ExtREAL & f.x > -infty & f.x < +infty by FUNCT_2:5,MESFUNC5:def 5,def 6; hence f.x in REAL by XXREAL_0:14; end; hence thesis by A1,FUNCT_2:3; end; definition let X be non empty set; let f1,f2 be without-infty Function of X,ExtREAL; redefine func f1+f2 -> without-infty Function of X,ExtREAL; correctness proof A1:dom f1 = X & dom f2 = X by FUNCT_2:def 1; {-infty} misses rng f1 & {-infty} misses rng f2 by ZFMISC_1:50,MESFUNC5:def 3; then f1"{-infty} = {} & f2"{-infty} = {} by RELAT_1:138; then (dom f1 /\ dom f2) \ ((f1"{-infty} /\ f2"{+infty}) \/ (f1"{+infty} /\ f2"{-infty})) = X by A1; then A2:dom(f1+f2) = X by MESFUNC1:def 3; now assume -infty in rng(f1+f2); then consider x be object such that A3: x in dom(f1+f2) & (f1+f2).x = -infty by FUNCT_1:def 3; reconsider x as Element of X by A3; (f1+f2).x = f1.x + f2.x by A3,MESFUNC1:def 3; then f1.x = -infty or f2.x = -infty by A3,XXREAL_3:17; hence contradiction by MESFUNC5:def 5; end; hence thesis by A2,FUNCT_2:def 1,MESFUNC5:def 3; end; end; definition let X be non empty set; let f1,f2 be without+infty Function of X,ExtREAL; redefine func f1+f2 -> without+infty Function of X,ExtREAL; correctness proof A1:dom f1 = X & dom f2 = X by FUNCT_2:def 1; {+infty} misses rng f1 & {+infty} misses rng f2 by ZFMISC_1:50,MESFUNC5:def 4; then f1"{+infty} = {} & f2"{+infty} = {} by RELAT_1:138; then (dom f1 /\ dom f2) \ ((f1"{-infty} /\ f2"{+infty}) \/ (f1"{+infty} /\ f2"{-infty})) = X by A1; then A2:dom(f1+f2) = X by MESFUNC1:def 3; now assume +infty in rng(f1+f2); then consider x be object such that A3: x in dom(f1+f2) & (f1+f2).x = +infty by FUNCT_1:def 3; reconsider x as Element of X by A3; (f1+f2).x = f1.x + f2.x by A3,MESFUNC1:def 3; then f1.x = +infty or f2.x = +infty by A3,XXREAL_3:16; hence contradiction by MESFUNC5:def 6; end; hence thesis by A2,FUNCT_2:def 1,MESFUNC5:def 4; end; end; definition let X be non empty set; let f1 be without-infty Function of X,ExtREAL; let f2 be without+infty Function of X,ExtREAL; redefine func f1-f2 -> without-infty Function of X,ExtREAL; correctness proof A1:dom f1 = X & dom f2 = X by FUNCT_2:def 1; {-infty} misses rng f1 & {+infty} misses rng f2 by ZFMISC_1:50,MESFUNC5:def 3,def 4; then f1"{-infty} = {} & f2"{+infty} = {} by RELAT_1:138; then (dom f1 /\ dom f2) \ ((f1"{+infty} /\ f2"{+infty}) \/ (f1"{-infty} /\ f2"{-infty})) = X by A1; then A2:dom(f1-f2) = X by MESFUNC1:def 4; now assume -infty in rng(f1-f2); then consider x be object such that A3: x in dom(f1-f2) & (f1-f2).x = -infty by FUNCT_1:def 3; reconsider x as Element of X by A3; (f1-f2).x = f1.x - f2.x by A3,MESFUNC1:def 4; then f1.x = -infty or f2.x = +infty by A3,XXREAL_3:19; hence contradiction by MESFUNC5:def 5,def 6; end; hence thesis by A2,FUNCT_2:def 1,MESFUNC5:def 3; end; end; definition let X be non empty set; let f1 be without+infty Function of X,ExtREAL; let f2 be without-infty Function of X,ExtREAL; redefine func f1-f2 -> without+infty Function of X,ExtREAL; correctness proof A1:dom f1 = X & dom f2 = X by FUNCT_2:def 1; {-infty} misses rng f2 & {+infty} misses rng f1 by ZFMISC_1:50,MESFUNC5:def 3,def 4; then f2"{-infty} = {} & f1"{+infty} = {} by RELAT_1:138; then (dom f1 /\ dom f2) \ ((f1"{+infty} /\ f2"{+infty}) \/ (f1"{-infty} /\ f2"{-infty})) = X by A1; then A2:dom(f1-f2) = X by MESFUNC1:def 4; now assume +infty in rng(f1-f2); then consider x be object such that A3: x in dom(f1-f2) & (f1-f2).x = +infty by FUNCT_1:def 3; reconsider x as Element of X by A3; (f1-f2).x = f1.x - f2.x by A3,MESFUNC1:def 4; then f2.x = -infty or f1.x = +infty by A3,XXREAL_3:18; hence contradiction by MESFUNC5:def 5,def 6; end; hence thesis by A2,FUNCT_2:def 1,MESFUNC5:def 4; end; end; theorem Th7: for X be non empty set, x be Element of X, f1,f2 be Function of X,ExtREAL holds ( f1 is without-infty & f2 is without-infty implies (f1+f2).x = f1.x + f2.x ) & ( f1 is without+infty & f2 is without+infty implies (f1+f2).x = f1.x + f2.x ) & ( f1 is without-infty & f2 is without+infty implies (f1-f2).x = f1.x - f2.x ) & ( f1 is without+infty & f2 is without-infty implies (f1-f2).x = f1.x - f2.x ) proof let X be non empty set, x be Element of X, f1,f2 be Function of X,ExtREAL; hereby assume f1 is without-infty & f2 is without-infty; then reconsider F1=f1,F2=f2 as without-infty Function of X,ExtREAL; dom (F1+F2) = X by FUNCT_2:def 1; hence (f1+f2).x = f1.x + f2.x by MESFUNC1:def 3; end; hereby assume f1 is without+infty & f2 is without+infty; then reconsider F1=f1,F2=f2 as without+infty Function of X,ExtREAL; dom (F1+F2) = X by FUNCT_2:def 1; hence (f1+f2).x = f1.x + f2.x by MESFUNC1:def 3; end; hereby assume A1: f1 is without-infty & f2 is without+infty; then reconsider F1=f1 as without-infty Function of X,ExtREAL; reconsider F2=f2 as without+infty Function of X,ExtREAL by A1; dom (F1-F2) = X by FUNCT_2:def 1; hence (f1-f2).x = f1.x - f2.x by MESFUNC1:def 4; end; hereby assume A1: f1 is without+infty & f2 is without-infty; then reconsider F1=f1 as without+infty Function of X,ExtREAL; reconsider F2=f2 as without-infty Function of X,ExtREAL by A1; dom (F1-F2) = X by FUNCT_2:def 1; hence (f1-f2).x = f1.x - f2.x by MESFUNC1:def 4; end; end; Lm3: for X be non empty set, f1,f2 be without-infty Function of X,ExtREAL holds f1 + f2 = f1 - (-f2) proof let X be non empty set, f1,f2 be without-infty Function of X,ExtREAL; now let x be Element of X; dom (-f2) = X by FUNCT_2:def 1; then (-f2).x = -(f2.x) by MESFUNC1:def 7; then (f1-(-f2)).x = f1.x - -(f2.x) by Th7; hence (f1+f2).x = (f1-(-f2)).x by Th7; end; hence thesis by FUNCT_2:def 8; end; Lm4: for X be non empty set, f1,f2 be without+infty Function of X,ExtREAL holds f1 + f2 = f1 - (-f2) proof let X be non empty set, f1,f2 be without+infty Function of X,ExtREAL; now let x be Element of X; dom (-f2) = X by FUNCT_2:def 1; then (-f2).x = -(f2.x) by MESFUNC1:def 7; then (f1-(-f2)).x = f1.x - -(f2.x) by Th7; hence (f1+f2).x = (f1-(-f2)).x by Th7; end; hence thesis by FUNCT_2:def 8; end; Lm5: for X be non empty set, f1 be without-infty Function of X,ExtREAL, f2 be without+infty Function of X,ExtREAL holds f1 - f2 = f1 + (-f2) & f2 - f1 = f2 + (-f1) proof let X be non empty set, f1 be without-infty Function of X,ExtREAL, f2 be without+infty Function of X,ExtREAL; now let x be Element of X; dom (-f2) = X by FUNCT_2:def 1; then (-f2).x = -(f2.x) by MESFUNC1:def 7; then (f1+(-f2)).x = f1.x - f2.x by Th7; hence (f1-f2).x = (f1+(-f2)).x by Th7; end; hence f1-f2 = f1+(-f2) by FUNCT_2:def 8; now let x be Element of X; dom (-f1) = X by FUNCT_2:def 1; then (-f1).x = -(f1.x) by MESFUNC1:def 7; then (f2+(-f1)).x = f2.x - f1.x by Th7; hence (f2-f1).x = (f2+(-f1)).x by Th7; end; hence f2-f1 = f2+(-f1) by FUNCT_2:def 8; end; theorem Th8: for X be non empty set, f1,f2 be without-infty Function of X,ExtREAL holds f1 + f2 = f1 - (-f2) & -(f1 + f2) = -f1 - f2 proof let X be non empty set, f1,f2 be without-infty Function of X,ExtREAL; thus f1 + f2 = f1 - (-f2) by Lm3; A1:dom(-f1) = X by FUNCT_2:def 1; A2:dom(-f2) = X by FUNCT_2:def 1; A3:dom(-(f1+f2)) = X by FUNCT_2:def 1; now let x be Element of X; (-(f1+f2)).x = -((f1+f2).x) by A3,MESFUNC1:def 7 .= -(f1.x + f2.x) by Th7 .= -(f1.x) - (f2.x) by XXREAL_3:25 .= (-f1).x + -(f2.x) by A1,MESFUNC1:def 7 .= (-f1).x + (-f2).x by A2,MESFUNC1:def 7 .= ((-f1) + (-f2)).x by Th7; hence (-(f1+f2)).x = (-f1-f2).x by Lm5; end; hence thesis by FUNCT_2:def 8; end; theorem Th9: for X be non empty set, f1,f2 be without+infty Function of X,ExtREAL holds f1 + f2 = f1 - (-f2) & -(f1 + f2) = -f1 - f2 proof let X be non empty set, f1,f2 be without+infty Function of X,ExtREAL; thus f1 + f2 = f1 - (-f2) by Lm4; A1:dom(-f1) = X by FUNCT_2:def 1; A2:dom(-f2) = X by FUNCT_2:def 1; A3:dom(-(f1+f2)) = X by FUNCT_2:def 1; now let x be Element of X; (-(f1+f2)).x = -((f1+f2).x) by A3,MESFUNC1:def 7 .= -(f1.x + f2.x) by Th7 .= -(f1.x) - (f2.x) by XXREAL_3:25 .= (-f1).x + -(f2.x) by A1,MESFUNC1:def 7 .= (-f1).x + (-f2).x by A2,MESFUNC1:def 7 .= ((-f1) + (-f2)).x by Th7; hence (-(f1+f2)).x = (-f1-f2).x by Lm5; end; hence thesis by FUNCT_2:def 8; end; theorem Th10: for X be non empty set, f1 be without-infty Function of X,ExtREAL, f2 be without+infty Function of X,ExtREAL holds f1 - f2 = f1 + (-f2) & f2 - f1 = f2 + (-f1) & -(f1 - f2) = -f1 + f2 & -(f2 - f1) = -f2 + f1 proof let X be non empty set, f1 be without-infty Function of X,ExtREAL, f2 be without+infty Function of X,ExtREAL; thus A1: f1 - f2 = f1 + (-f2) & f2 - f1 = f2 + (-f1) by Lm5; thus -(f1 - f2) = (-f1) -(-f2) by A1,Th8 .= (-f1) + (-(-f2)) by Lm5 .= -f1 + f2 by Th2; thus -(f2 - f1) = (-f2) -(-f1) by A1,Th9 .= (-f2) + (-(-f1)) by Lm5 .= -f2 + f1 by Th2; end; definition let f be Function of [:NAT,NAT:],ExtREAL, n,m be Nat; redefine func f.(n,m) -> Element of ExtREAL; coherence proof reconsider n,m as Element of NAT by ORDINAL1:def 12; f.(n,m) in ExtREAL; hence thesis; end; end; theorem Th11: for f1,f2 be without-infty Function of [:NAT,NAT:],ExtREAL, n,m be Nat holds (f1+f2).(n,m) = f1.(n,m) + f2.(n,m) proof let f1,f2 be without-infty Function of [:NAT,NAT:],ExtREAL, n,m be Nat; A1:n in NAT & m in NAT by ORDINAL1:def 12; then reconsider z = [n,m] as Element of [:NAT,NAT:] by ZFMISC_1:87; [n,m] in [:NAT,NAT:] by A1,ZFMISC_1:87; hence thesis by Th7; end; theorem for f1,f2 be without+infty Function of [:NAT,NAT:],ExtREAL, n,m be Nat holds (f1+f2).(n,m) = f1.(n,m) + f2.(n,m) proof let f1,f2 be without+infty Function of [:NAT,NAT:],ExtREAL, n,m be Nat; A1:n in NAT & m in NAT by ORDINAL1:def 12; then reconsider z = [n,m] as Element of [:NAT,NAT:] by ZFMISC_1:87; [n,m] in [:NAT,NAT:] by A1,ZFMISC_1:87; hence thesis by Th7; end; theorem for f1 be without-infty Function of [:NAT,NAT:],ExtREAL, f2 be without+infty Function of [:NAT,NAT:],ExtREAL, n,m be Nat holds (f1-f2).(n,m) = f1.(n,m) - f2.(n,m) & (f2-f1).(n,m) = f2.(n,m) - f1.(n,m) proof let f1 be without-infty Function of [:NAT,NAT:],ExtREAL, f2 be without+infty Function of [:NAT,NAT:],ExtREAL, n,m be Nat; A1:n in NAT & m in NAT by ORDINAL1:def 12; then reconsider z = [n,m] as Element of [:NAT,NAT:] by ZFMISC_1:87; [n,m] in [:NAT,NAT:] by A1,ZFMISC_1:87; hence thesis by Th7; end; theorem for X,Y be non empty set, f1,f2 be without-infty Function of [:X,Y:],ExtREAL holds (f1+f2)@ = f1@ + f2@ proof let X,Y be non empty set, f1,f2 be without-infty Function of [:X,Y:],ExtREAL; now let z be Element of [:Y,X:]; consider y,x be object such that A1: y in Y & x in X & z = [y,x] by ZFMISC_1:def 2; reconsider y as Element of Y by A1; reconsider x as Element of X by A1; reconsider z1 = [x,y] as Element of [:X,Y:] by ZFMISC_1:87; (f1+f2)@.z = (f1+f2)@.(y,x) by A1; then (f1+f2)@.z = (f1+f2).(x,y) by DBLSEQ_2:def 2; then A2: (f1+f2)@.z = f1.z1 + f2.z1 by Th7; f1.z1 = f1.(x,y) & f2.z1 = f2.(x,y); then f1.z1 = f1@.(y,x) & f2.z1 = f2@.(y,x) by DBLSEQ_2:def 2; hence (f1+f2)@.z =(f1@ + f2@).z by A1,A2,Th7; end; hence thesis by FUNCT_2:def 8; end; theorem for X,Y be non empty set, f1,f2 be without+infty Function of [:X,Y:],ExtREAL holds (f1+f2)@ = f1@ + f2@ proof let X,Y be non empty set, f1,f2 be without+infty Function of [:X,Y:],ExtREAL; now let z be Element of [:Y,X:]; consider y,x be object such that A1: y in Y & x in X & z = [y,x] by ZFMISC_1:def 2; reconsider y as Element of Y by A1; reconsider x as Element of X by A1; reconsider z1 = [x,y] as Element of [:X,Y:] by ZFMISC_1:87; (f1+f2)@.z = (f1+f2)@.(y,x) by A1; then (f1+f2)@.z = (f1+f2).(x,y) by DBLSEQ_2:def 2; then A2: (f1+f2)@.z = f1.z1 + f2.z1 by Th7; f1.z1 = f1.(x,y) & f2.z1 = f2.(x,y); then f1.z1 = f1@.(y,x) & f2.z1 = f2@.(y,x) by DBLSEQ_2:def 2; hence (f1+f2)@.z =(f1@ + f2@).z by A1,A2,Th7; end; hence thesis by FUNCT_2:def 8; end; theorem for X,Y be non empty set, f1 be without-infty Function of [:X,Y:],ExtREAL, f2 be without+infty Function of [:X,Y:],ExtREAL holds (f1-f2)@ = f1@ - f2@ & (f2-f1)@ = f2@ - f1@ proof let X,Y be non empty set, f1 be without-infty Function of [:X,Y:],ExtREAL, f2 be without+infty Function of [:X,Y:],ExtREAL; now let z be Element of [:Y,X:]; consider y,x be object such that A1: y in Y & x in X & z = [y,x] by ZFMISC_1:def 2; reconsider y as Element of Y by A1; reconsider x as Element of X by A1; reconsider z1 = [x,y] as Element of [:X,Y:] by ZFMISC_1:87; (f1-f2)@.z = (f1-f2)@.(y,x) by A1; then (f1-f2)@.z = (f1-f2).(x,y) by DBLSEQ_2:def 2; then A2: (f1-f2)@.z = f1.z1 - f2.z1 by Th7; f1.z1 = f1.(x,y) & f2.z1 = f2.(x,y); then f1.z1 = f1@.(y,x) & f2.z1 = f2@.(y,x) by DBLSEQ_2:def 2; hence (f1-f2)@.z =(f1@ - f2@).z by A1,A2,Th7; end; hence (f1-f2)@ = f1@ - f2@ by FUNCT_2:def 8; now let z be Element of [:Y,X:]; consider y,x be object such that A1: y in Y & x in X & z = [y,x] by ZFMISC_1:def 2; reconsider y as Element of Y by A1; reconsider x as Element of X by A1; reconsider z1 = [x,y] as Element of [:X,Y:] by ZFMISC_1:87; (f2-f1)@.z = (f2-f1)@.(y,x) by A1; then (f2-f1)@.z = (f2-f1).(x,y) by DBLSEQ_2:def 2; then A2: (f2-f1)@.z = f2.z1 - f1.z1 by Th7; f1.z1 = f1.(x,y) & f2.z1 = f2.(x,y); then f1.z1 = f1@.(y,x) & f2.z1 = f2@.(y,x) by DBLSEQ_2:def 2; hence (f2-f1)@.z =(f2@ - f1@).z by A1,A2,Th7; end; hence (f2-f1)@ = f2@ - f1@ by FUNCT_2:def 8; end; registration cluster convergent_to_+infty -> convergent for ExtREAL_sequence; correctness by MESFUNC5:def 11; cluster convergent_to_-infty -> convergent for ExtREAL_sequence; correctness by MESFUNC5:def 11; cluster convergent_to_finite_number -> convergent for ExtREAL_sequence; correctness by MESFUNC5:def 11; end; registration cluster convergent for ExtREAL_sequence; existence proof reconsider z = 0 as Element of ExtREAL by XXREAL_0:def 1; reconsider M = NAT --> z as ExtREAL_sequence; take M; for n be Nat holds M.n = 0 by Lm1; then M is convergent_to_finite_number by MESFUNC5:52; hence M is convergent; end; cluster convergent for without-infty ExtREAL_sequence; existence proof reconsider z = 0 as Element of ExtREAL by XXREAL_0:def 1; reconsider M = NAT --> z as ExtREAL_sequence; reconsider M as without-infty ExtREAL_sequence by Lm2; take M; for n be Nat holds M.n = 0 by Lm1; then M is convergent_to_finite_number by MESFUNC5:52; hence M is convergent; end; cluster convergent for without+infty ExtREAL_sequence; existence proof reconsider z = 0 as Element of ExtREAL by XXREAL_0:def 1; reconsider M = NAT --> z as ExtREAL_sequence; reconsider M as without+infty ExtREAL_sequence by Lm2; take M; for n be Nat holds M.n = 0 by Lm1; then M is convergent_to_finite_number by MESFUNC5:52; hence M is convergent; end; end; Lm6: for seq be convergent ExtREAL_sequence holds (seq is convergent_to_finite_number implies -seq is convergent_to_finite_number) & (seq is convergent_to_+infty implies -seq is convergent_to_-infty) & (seq is convergent_to_-infty implies -seq is convergent_to_+infty) & -seq is convergent & lim (-seq) = - lim seq proof let seq be convergent ExtREAL_sequence; P0:now assume seq is convergent_to_finite_number; then consider g be Real such that A1: lim seq = g & for p be Real st 0
= -(seq.m) by A8,XXREAL_3:38; then
A9: --g >= -(seq.m) by XXREAL_3:def 3;
m in NAT by ORDINAL1:def 12; then
m in dom(-seq) by FUNCT_2:def 1;
hence (-seq).m <= g by A9,MESFUNC1:def 7;
end;
end;
hence -seq is convergent_to_-infty by MESFUNC5:def 10;
hence -seq is convergent;
lim(-seq) = -infty & lim seq = +infty by A6,A10,MESFUNC9:7,MESFUNC5:def 10;
hence lim (-seq) = - lim seq by XXREAL_3:6;
end;
thus seq is convergent_to_+infty
implies -seq is convergent_to_-infty by P1;
P2:now assume A11: seq is convergent_to_-infty;
A15:now let g be Real;
assume A12: g > 0;
reconsider p = -g as ExtReal;
consider n be Nat such that
A13: for m be Nat st n <= m holds seq.m <= p by A11,A12,MESFUNC5:def 10;
take n;
hereby let m be Nat;
assume n<=m; then
-(seq.m) >= -p by A13,XXREAL_3:38; then
A14: -(seq.m) >= --g by XXREAL_3:def 3;
m in NAT by ORDINAL1:def 12; then
m in dom(-seq) by FUNCT_2:def 1;
hence (-seq).m >= g by A14,MESFUNC1:def 7;
end;
end;
hence -seq is convergent_to_+infty by MESFUNC5:def 9;
hence -seq is convergent;
lim(-seq) = +infty & lim seq = -infty by A11,A15,MESFUNC9:7,MESFUNC5:def 9;
hence lim (-seq) = - lim seq by XXREAL_3:5;
end;
thus seq is convergent_to_-infty
implies -seq is convergent_to_+infty by P2;
thus thesis by P0,P1,P2,MESFUNC5:def 11;
end;
theorem Th17:
for seq be convergent ExtREAL_sequence holds
(seq is convergent_to_finite_number iff -seq is convergent_to_finite_number)
& (seq is convergent_to_+infty iff -seq is convergent_to_-infty)
& (seq is convergent_to_-infty iff -seq is convergent_to_+infty)
& -seq is convergent & lim (-seq) = - lim seq
proof
let seq be convergent ExtREAL_sequence;
now assume -seq is convergent_to_finite_number; then
-(-seq) is convergent_to_finite_number by Lm6;
hence seq is convergent_to_finite_number by Th2;
end;
hence seq is convergent_to_finite_number
iff -seq is convergent_to_finite_number by Lm6;
now assume -seq is convergent_to_-infty; then
-(-seq) is convergent_to_+infty by Lm6;
hence seq is convergent_to_+infty by Th2;
end;
hence seq is convergent_to_+infty iff -seq is convergent_to_-infty by Lm6;
now assume -seq is convergent_to_+infty; then
-(-seq) is convergent_to_-infty by Lm6;
hence seq is convergent_to_-infty by Th2;
end;
hence seq is convergent_to_-infty iff -seq is convergent_to_+infty by Lm6;
thus -seq is convergent & lim (-seq) = - lim seq by Lm6;
end;
theorem Th18:
for seq1,seq2 be without-infty ExtREAL_sequence
st seq1 is convergent_to_+infty & seq2 is convergent_to_+infty
holds seq1 + seq2 is convergent_to_+infty & seq1 + seq2 is convergent
& lim(seq1+seq2) = +infty
proof
let seq1,seq2 be without-infty ExtREAL_sequence;
assume A1: seq1 is convergent_to_+infty & seq2 is convergent_to_+infty;
now let g be Real;
assume A2: 0 < g; then
consider n1 be Nat such that
A3: for m be Nat st n1<=m holds g/2<=seq1.m by A1,MESFUNC5:def 9;
consider n2 be Nat such that
A4: for m be Nat st n2<=m holds g/2<=seq2.m by A1,A2,MESFUNC5:def 9;
reconsider N1=n1, N2=n2 as Element of NAT by ORDINAL1:def 12;
reconsider n = max(N1,N2) as Nat;
A5: n1<=n & n2<=n by XXREAL_0:25;
now let m be Nat;
assume n<=m; then
n1<=m & n2<=m by A5,XXREAL_0:2; then
g/2 <= seq1.m & g/2 <= seq2.m by A3,A4; then
A6: g/2 + g/2 <= seq1.m + seq2.m by XXREAL_3:36;
m is Element of NAT by ORDINAL1:def 12;
hence g<=(seq1+seq2).m by A6,Th7;
end;
hence ex n be Nat st for m be Nat st n<=m holds g <= (seq1+seq2).m;
end;
hence
A7: seq1+seq2 is convergent_to_+infty by MESFUNC5:def 9;
hence seq1+seq2 is convergent;
thus lim(seq1+seq2) = +infty by A7,MESFUNC5:def 12;
end;
theorem Th19:
for seq1,seq2 be without-infty ExtREAL_sequence
st seq1 is convergent_to_+infty & seq2 is convergent_to_finite_number
holds seq1 + seq2 is convergent_to_+infty & seq1 + seq2 is convergent
& lim(seq1+seq2)=+infty
proof
let seq1,seq2 be without-infty ExtREAL_sequence;
assume
A1: seq1 is convergent_to_+infty & seq2 is convergent_to_finite_number; then
consider S2 be Real such that
A2: for g be Real st 0 =N & m>=N holds
|. Eseq.(n,m) - (p qua ExtReal) .| < e;
attr Eseq is P-convergent_to_+infty means
for g be Real st 0 < g
ex N be Nat st
for n,m be Nat st n>=N & m>=N holds
g <= Eseq.(n,m);
attr Eseq is P-convergent_to_-infty means
for g be Real st g < 0
ex N be Nat st
for n,m be Nat st n>=N & m>=N holds
Eseq.(n,m) <= g;
end;
definition let f be Function of [:NAT,NAT:],ExtREAL;
attr f is convergent_in_cod1_to_+infty means
for m be Element of NAT holds ProjMap2(f,m) is convergent_to_+infty;
attr f is convergent_in_cod1_to_-infty means
for m be Element of NAT holds ProjMap2(f,m) is convergent_to_-infty;
attr f is convergent_in_cod1_to_finite means
for m be Element of NAT holds
ProjMap2(f,m) is convergent_to_finite_number;
attr f is convergent_in_cod1 means
for m be Element of NAT holds ProjMap2(f,m) is convergent;
attr f is convergent_in_cod2_to_+infty means
for m be Element of NAT holds ProjMap1(f,m) is convergent_to_+infty;
attr f is convergent_in_cod2_to_-infty means
for m be Element of NAT holds ProjMap1(f,m) is convergent_to_-infty;
attr f is convergent_in_cod2_to_finite means
for m be Element of NAT holds
ProjMap1(f,m) is convergent_to_finite_number;
attr f is convergent_in_cod2 means
for m be Element of NAT holds ProjMap1(f,m) is convergent;
end;
theorem
for f be Function of [:NAT,NAT:],ExtREAL holds
( f is convergent_in_cod1_to_+infty or f is convergent_in_cod1_to_-infty
or f is convergent_in_cod1_to_finite
implies f is convergent_in_cod1 )
& ( f is convergent_in_cod2_to_+infty or f is convergent_in_cod2_to_-infty
or f is convergent_in_cod2_to_finite
implies f is convergent_in_cod2 )
proof
let f be Function of [:NAT,NAT:],ExtREAL;
hereby assume
A1: f is convergent_in_cod1_to_+infty or f is convergent_in_cod1_to_-infty or
f is convergent_in_cod1_to_finite;
per cases by A1;
suppose A2: f is convergent_in_cod1_to_+infty;
now let m be Element of NAT;
ProjMap2(f,m) is convergent_to_+infty by A2;
hence ProjMap2(f,m) is convergent;
end;
hence f is convergent_in_cod1;
end;
suppose A3: f is convergent_in_cod1_to_-infty;
now let m be Element of NAT;
ProjMap2(f,m) is convergent_to_-infty by A3;
hence ProjMap2(f,m) is convergent;
end;
hence f is convergent_in_cod1;
end;
suppose A4: f is convergent_in_cod1_to_finite;
now let m be Element of NAT;
ProjMap2(f,m) is convergent_to_finite_number by A4;
hence ProjMap2(f,m) is convergent;
end;
hence f is convergent_in_cod1;
end;
end;
assume
A5: f is convergent_in_cod2_to_+infty or f is convergent_in_cod2_to_-infty or
f is convergent_in_cod2_to_finite;
per cases by A5;
suppose A6: f is convergent_in_cod2_to_+infty;
now let m be Element of NAT;
ProjMap1(f,m) is convergent_to_+infty by A6;
hence ProjMap1(f,m) is convergent;
end;
hence f is convergent_in_cod2;
end;
suppose A7: f is convergent_in_cod2_to_-infty;
now let m be Element of NAT;
ProjMap1(f,m) is convergent_to_-infty by A7;
hence ProjMap1(f,m) is convergent;
end;
hence f is convergent_in_cod2;
end;
suppose A8: f is convergent_in_cod2_to_finite;
now let m be Element of NAT;
ProjMap1(f,m) is convergent_to_finite_number by A8;
hence ProjMap1(f,m) is convergent;
end;
hence f is convergent_in_cod2;
end;
end;
theorem Th32:
for X,Y,Z be non empty set, F be Function of [:X,Y:],Z, x be Element of X
holds ProjMap1(F,x) = ProjMap2(F@,x)
proof
let X,Y,Z be non empty set;
let F be Function of [:X,Y:],Z;
let x be Element of X;
now let y be Element of Y;
ProjMap1(F,x).y = F.(x,y) by MESFUNC9:def 6
.= F@.(y,x) by DBLSEQ_2:def 2;
hence ProjMap1(F,x).y = ProjMap2(F@,x).y by MESFUNC9:def 7;
end;
hence ProjMap1(F,x) = ProjMap2(F@,x) by FUNCT_2:def 8;
end;
theorem Th33:
for X,Y,Z be non empty set, F be Function of [:X,Y:],Z, y be Element of Y
holds ProjMap2(F,y) = ProjMap1(F@,y)
proof
let X,Y,Z be non empty set;
let F be Function of [:X,Y:],Z;
let y be Element of Y;
now let x be Element of X;
ProjMap2(F,y).x = F.(x,y) by MESFUNC9:def 7
.= F@.(y,x) by DBLSEQ_2:def 2;
hence ProjMap2(F,y).x = ProjMap1(F@,y).x by MESFUNC9:def 6;
end;
hence ProjMap2(F,y) = ProjMap1(F@,y) by FUNCT_2:def 8;
end;
theorem Th34:
for X,Y be non empty set, F be Function of [:X,Y:],ExtREAL, x be Element of X
holds ProjMap1(-F,x) = -ProjMap1(F,x)
proof
let X,Y be non empty set, F be Function of [:X,Y:],ExtREAL,
x be Element of X;
now let y be Element of Y;
[x,y] in [:X,Y:] by ZFMISC_1:87; then
A1: [x,y] in dom(-F) by FUNCT_2:def 1;
A2: dom(-ProjMap1(F,x)) = Y by FUNCT_2:def 1;
ProjMap1(-F,x).y = (-F).(x,y) by MESFUNC9:def 6; then
ProjMap1(-F,x).y = -(F.(x,y)) by A1,MESFUNC1:def 7; then
ProjMap1(-F,x).y = -(ProjMap1(F,x).y) by MESFUNC9:def 6;
hence ProjMap1(-F,x).y = (-ProjMap1(F,x)).y by A2,MESFUNC1:def 7;
end;
hence ProjMap1(-F,x) = -ProjMap1(F,x) by FUNCT_2:def 8;
end;
theorem Th35:
for X,Y be non empty set, F be Function of [:X,Y:],ExtREAL, y be Element of Y
holds ProjMap2(-F,y) = -ProjMap2(F,y)
proof
let X,Y be non empty set, F be Function of [:X,Y:],ExtREAL,
y be Element of Y;
now let x be Element of X;
[x,y] in [:X,Y:] by ZFMISC_1:87; then
A1: [x,y] in dom(-F) by FUNCT_2:def 1;
A2: dom(-ProjMap2(F,y)) = X by FUNCT_2:def 1;
ProjMap2(-F,y).x = (-F).(x,y) by MESFUNC9:def 7; then
ProjMap2(-F,y).x = -(F.(x,y)) by A1,MESFUNC1:def 7; then
ProjMap2(-F,y).x = -(ProjMap2(F,y).x) by MESFUNC9:def 7;
hence ProjMap2(-F,y).x = (-ProjMap2(F,y)).x by A2,MESFUNC1:def 7;
end;
hence ProjMap2(-F,y) = -ProjMap2(F,y) by FUNCT_2:def 8;
end;
theorem Th36:
for f be Function of [:NAT,NAT:],ExtREAL holds
(f is convergent_in_cod1_to_+infty
iff f@ is convergent_in_cod2_to_+infty)
& (f is convergent_in_cod2_to_+infty
iff f@ is convergent_in_cod1_to_+infty)
& (f is convergent_in_cod1_to_-infty
iff f@ is convergent_in_cod2_to_-infty)
& (f is convergent_in_cod2_to_-infty
iff f@ is convergent_in_cod1_to_-infty)
& (f is convergent_in_cod1_to_finite
iff f@ is convergent_in_cod2_to_finite)
& (f is convergent_in_cod2_to_finite
iff f@ is convergent_in_cod1_to_finite)
proof
let f be Function of [:NAT,NAT:],ExtREAL;
now hereby assume
A1: f is convergent_in_cod1_to_+infty;
now let m be Element of NAT;
ProjMap2(f,m) = ProjMap1(f@,m) by Th33;
hence ProjMap1(f@,m) is convergent_to_+infty by A1;
end;
hence f@ is convergent_in_cod2_to_+infty;
end;
assume A2: f@ is convergent_in_cod2_to_+infty;
now let m be Element of NAT;
ProjMap2(f,m) = ProjMap1(f@,m) by Th33;
hence ProjMap2(f,m) is convergent_to_+infty by A2;
end;
hence f is convergent_in_cod1_to_+infty;
end;
hence
f is convergent_in_cod1_to_+infty iff f@ is convergent_in_cod2_to_+infty;
now hereby assume
A3: f is convergent_in_cod2_to_+infty;
now let m be Element of NAT;
ProjMap1(f,m) = ProjMap2(f@,m) by Th32;
hence ProjMap2(f@,m) is convergent_to_+infty by A3;
end;
hence f@ is convergent_in_cod1_to_+infty;
end;
assume A4: f@ is convergent_in_cod1_to_+infty;
now let m be Element of NAT;
ProjMap1(f,m) = ProjMap2(f@,m) by Th32;
hence ProjMap1(f,m) is convergent_to_+infty by A4;
end;
hence f is convergent_in_cod2_to_+infty;
end;
hence
f is convergent_in_cod2_to_+infty iff f@ is convergent_in_cod1_to_+infty;
now hereby assume
A5: f is convergent_in_cod1_to_-infty;
now let m be Element of NAT;
ProjMap2(f,m) = ProjMap1(f@,m) by Th33;
hence ProjMap1(f@,m) is convergent_to_-infty by A5;
end;
hence f@ is convergent_in_cod2_to_-infty;
end;
assume A6: f@ is convergent_in_cod2_to_-infty;
now let m be Element of NAT;
ProjMap2(f,m) = ProjMap1(f@,m) by Th33;
hence ProjMap2(f,m) is convergent_to_-infty by A6;
end;
hence f is convergent_in_cod1_to_-infty;
end;
hence
f is convergent_in_cod1_to_-infty iff f@ is convergent_in_cod2_to_-infty;
now hereby assume
A7: f is convergent_in_cod2_to_-infty;
now let m be Element of NAT;
ProjMap1(f,m) = ProjMap2(f@,m) by Th32;
hence ProjMap2(f@,m) is convergent_to_-infty by A7;
end;
hence f@ is convergent_in_cod1_to_-infty;
end;
assume A8: f@ is convergent_in_cod1_to_-infty;
now let m be Element of NAT;
ProjMap1(f,m) = ProjMap2(f@,m) by Th32;
hence ProjMap1(f,m) is convergent_to_-infty by A8;
end;
hence f is convergent_in_cod2_to_-infty;
end;
hence
f is convergent_in_cod2_to_-infty iff f@ is convergent_in_cod1_to_-infty;
now hereby assume
A9: f is convergent_in_cod1_to_finite;
now let m be Element of NAT;
ProjMap2(f,m) = ProjMap1(f@,m) by Th33;
hence ProjMap1(f@,m) is convergent_to_finite_number by A9;
end;
hence f@ is convergent_in_cod2_to_finite;
end;
assume A10: f@ is convergent_in_cod2_to_finite;
now let m be Element of NAT;
ProjMap2(f,m) = ProjMap1(f@,m) by Th33;
hence ProjMap2(f,m) is convergent_to_finite_number by A10;
end;
hence f is convergent_in_cod1_to_finite;
end;
hence
f is convergent_in_cod1_to_finite iff f@ is convergent_in_cod2_to_finite;
now hereby assume
A11: f is convergent_in_cod2_to_finite;
now let m be Element of NAT;
ProjMap1(f,m) = ProjMap2(f@,m) by Th32;
hence ProjMap2(f@,m) is convergent_to_finite_number by A11;
end;
hence f@ is convergent_in_cod1_to_finite;
end;
assume A12: f@ is convergent_in_cod1_to_finite;
now let m be Element of NAT;
ProjMap1(f,m) = ProjMap2(f@,m) by Th32;
hence ProjMap1(f,m) is convergent_to_finite_number by A12;
end;
hence f is convergent_in_cod2_to_finite;
end;
hence
f is convergent_in_cod2_to_finite iff f@ is convergent_in_cod1_to_finite;
end;
theorem
for f be Function of [:NAT,NAT:],ExtREAL holds
(f is convergent_in_cod1_to_+infty
iff -f is convergent_in_cod1_to_-infty)
& (f is convergent_in_cod1_to_-infty
iff -f is convergent_in_cod1_to_+infty)
& (f is convergent_in_cod1_to_finite
iff -f is convergent_in_cod1_to_finite)
& (f is convergent_in_cod2_to_+infty
iff -f is convergent_in_cod2_to_-infty)
& (f is convergent_in_cod2_to_-infty
iff -f is convergent_in_cod2_to_+infty)
& (f is convergent_in_cod2_to_finite
iff -f is convergent_in_cod2_to_finite)
proof
let f be Function of [:NAT,NAT:],ExtREAL;
now hereby assume
A1: f is convergent_in_cod1_to_+infty;
now let m be Element of NAT;
A2: ProjMap2(f,m) is convergent_to_+infty by A1;
-ProjMap2(f,m) = ProjMap2(-f,m) by Th35;
hence ProjMap2(-f,m) is convergent_to_-infty by A2,Th17;
end;
hence -f is convergent_in_cod1_to_-infty;
end;
assume A3: -f is convergent_in_cod1_to_-infty;
now let m be Element of NAT;
-ProjMap2(f,m) = ProjMap2(-f,m) by Th35; then
-ProjMap2(f,m) is convergent_to_-infty by A3; then
-(-ProjMap2(f,m)) is convergent_to_+infty by Th17;
hence ProjMap2(f,m) is convergent_to_+infty by Th2;
end;
hence f is convergent_in_cod1_to_+infty;
end;
hence
f is convergent_in_cod1_to_+infty iff -f is convergent_in_cod1_to_-infty;
now hereby assume
A1: f is convergent_in_cod1_to_-infty;
now let m be Element of NAT;
A2: ProjMap2(f,m) is convergent_to_-infty by A1;
-ProjMap2(f,m) = ProjMap2(-f,m) by Th35;
hence ProjMap2(-f,m) is convergent_to_+infty by A2,Th17;
end;
hence -f is convergent_in_cod1_to_+infty;
end;
assume A3: -f is convergent_in_cod1_to_+infty;
now let m be Element of NAT;
-ProjMap2(f,m) = ProjMap2(-f,m) by Th35; then
-ProjMap2(f,m) is convergent_to_+infty by A3; then
-(-ProjMap2(f,m)) is convergent_to_-infty by Th17;
hence ProjMap2(f,m) is convergent_to_-infty by Th2;
end;
hence f is convergent_in_cod1_to_-infty;
end;
hence
f is convergent_in_cod1_to_-infty iff -f is convergent_in_cod1_to_+infty;
now hereby assume
A1: f is convergent_in_cod1_to_finite;
now let m be Element of NAT;
A2: ProjMap2(f,m) is convergent_to_finite_number by A1;
-ProjMap2(f,m) = ProjMap2(-f,m) by Th35;
hence ProjMap2(-f,m) is convergent_to_finite_number by A2,Th17;
end;
hence -f is convergent_in_cod1_to_finite;
end;
assume A3: -f is convergent_in_cod1_to_finite;
now let m be Element of NAT;
-ProjMap2(f,m) = ProjMap2(-f,m) by Th35; then
-ProjMap2(f,m) is convergent_to_finite_number by A3; then
-(-ProjMap2(f,m)) is convergent_to_finite_number by Th17;
hence ProjMap2(f,m) is convergent_to_finite_number by Th2;
end;
hence f is convergent_in_cod1_to_finite;
end;
hence
f is convergent_in_cod1_to_finite iff -f is convergent_in_cod1_to_finite;
now hereby assume
A1: f is convergent_in_cod2_to_+infty;
now let m be Element of NAT;
A2: ProjMap1(f,m) is convergent_to_+infty by A1;
-ProjMap1(f,m) = ProjMap1(-f,m) by Th34;
hence ProjMap1(-f,m) is convergent_to_-infty by A2,Th17;
end;
hence -f is convergent_in_cod2_to_-infty;
end;
assume A3: -f is convergent_in_cod2_to_-infty;
now let m be Element of NAT;
-ProjMap1(f,m) = ProjMap1(-f,m) by Th34; then
-ProjMap1(f,m) is convergent_to_-infty by A3; then
-(-ProjMap1(f,m)) is convergent_to_+infty by Th17;
hence ProjMap1(f,m) is convergent_to_+infty by Th2;
end;
hence f is convergent_in_cod2_to_+infty;
end;
hence
f is convergent_in_cod2_to_+infty iff -f is convergent_in_cod2_to_-infty;
now hereby assume
A1: f is convergent_in_cod2_to_-infty;
now let m be Element of NAT;
A2: ProjMap1(f,m) is convergent_to_-infty by A1;
-ProjMap1(f,m) = ProjMap1(-f,m) by Th34;
hence ProjMap1(-f,m) is convergent_to_+infty by A2,Th17;
end;
hence -f is convergent_in_cod2_to_+infty;
end;
assume A3: -f is convergent_in_cod2_to_+infty;
now let m be Element of NAT;
-ProjMap1(f,m) = ProjMap1(-f,m) by Th34; then
-ProjMap1(f,m) is convergent_to_+infty by A3; then
-(-ProjMap1(f,m)) is convergent_to_-infty by Th17;
hence ProjMap1(f,m) is convergent_to_-infty by Th2;
end;
hence f is convergent_in_cod2_to_-infty;
end;
hence
f is convergent_in_cod2_to_-infty iff -f is convergent_in_cod2_to_+infty;
now hereby assume
A1: f is convergent_in_cod2_to_finite;
now let m be Element of NAT;
A2: ProjMap1(f,m) is convergent_to_finite_number by A1;
-ProjMap1(f,m) = ProjMap1(-f,m) by Th34;
hence ProjMap1(-f,m) is convergent_to_finite_number by A2,Th17;
end;
hence -f is convergent_in_cod2_to_finite;
end;
assume A3: -f is convergent_in_cod2_to_finite;
now let m be Element of NAT;
-ProjMap1(f,m) = ProjMap1(-f,m) by Th34; then
-ProjMap1(f,m) is convergent_to_finite_number by A3; then
-(-ProjMap1(f,m)) is convergent_to_finite_number by Th17;
hence ProjMap1(f,m) is convergent_to_finite_number by Th2;
end;
hence f is convergent_in_cod2_to_finite;
end;
hence
f is convergent_in_cod2_to_finite iff -f is convergent_in_cod2_to_finite;
end;
definition let f be Function of [:NAT,NAT:],ExtREAL;
func lim_in_cod1 f -> ExtREAL_sequence means :D1DEF5:
for m be Element of NAT holds it.m = lim ProjMap2(f,m);
existence
proof
defpred P[Element of NAT,set] means $2 = lim ProjMap2(f,$1);
A1:for m be Element of NAT ex n be Element of ExtREAL st P[m,n];
consider IT be Function of NAT,ExtREAL such that
A2: for m be Element of NAT holds P[m,IT.m] from FUNCT_2:sch 3(A1);
take IT;
thus thesis by A2;
end;
uniqueness
proof
let f1,f2 be Function of NAT,ExtREAL;
assume that
A3: for m be Element of NAT holds f1.m = lim ProjMap2(f,m) and
A4: for m be Element of NAT holds f2.m = lim ProjMap2(f,m);
now let m be Element of NAT;
thus f1.m = lim ProjMap2(f,m) by A3 .= f2.m by A4;
end;
hence f1 = f2 by FUNCT_2:63;
end;
func lim_in_cod2 f -> ExtREAL_sequence means :D1DEF6:
for n be Element of NAT holds it.n = lim ProjMap1(f,n);
existence
proof
defpred P[Element of NAT,set] means $2 = lim ProjMap1(f,$1);
A1:for m be Element of NAT holds ex n be Element of ExtREAL st P[m,n];
consider IT be Function of NAT,ExtREAL such that
A2: for m be Element of NAT holds P[m,IT.m] from FUNCT_2:sch 3(A1);
take IT;
thus thesis by A2;
end;
uniqueness
proof
let f1,f2 be Function of NAT,ExtREAL;
assume that
A3: for n be Element of NAT holds f1.n = lim ProjMap1(f,n) and
A4: for n be Element of NAT holds f2.n = lim ProjMap1(f,n);
now let n be Element of NAT;
thus f1.n = lim ProjMap1(f,n) by A3 .= f2.n by A4;
end;
hence f1 = f2 by FUNCT_2:63;
end;
end;
theorem Th38:
for f be Function of [:NAT,NAT:],ExtREAL holds
lim_in_cod1 f = lim_in_cod2 (f@) & lim_in_cod2 f = lim_in_cod1 (f@)
proof
let f be Function of [:NAT,NAT:],ExtREAL;
now let n be Element of NAT;
(lim_in_cod1 f).n = lim ProjMap2(f,n) by D1DEF5
.= lim ProjMap1(f@,n) by Th33;
hence (lim_in_cod1 f).n = (lim_in_cod2 (f@)).n by D1DEF6;
end;
hence lim_in_cod1 f = lim_in_cod2 (f@) by FUNCT_2:def 8;
now let n be Element of NAT;
(lim_in_cod2 f).n = lim ProjMap1(f,n) by D1DEF6
.= lim ProjMap2(f@,n) by Th32;
hence (lim_in_cod2 f).n = (lim_in_cod1 (f@)).n by D1DEF5;
end;
hence lim_in_cod2 f = lim_in_cod1 (f@) by FUNCT_2:def 8;
end;
registration
let X,Y be non empty set, F be without+infty Function of [:X,Y:],ExtREAL,
x be Element of X;
cluster ProjMap1(F,x) -> without+infty;
correctness
proof
now let y be object;
per cases;
suppose not y in dom (ProjMap1(F,x));
hence (ProjMap1(F,x)).y < +infty by FUNCT_1:def 2;
end;
suppose y in dom (ProjMap1(F,x)); then
reconsider y1=y as Element of Y;
(ProjMap1(F,x)).y = F.(x,y1) by MESFUNC9:def 6;
hence (ProjMap1(F,x)).y < +infty by MESFUNC5:def 6;
end;
end;
hence thesis by MESFUNC5:def 6;
end;
end;
registration
let X,Y be non empty set, F be without+infty Function of [:X,Y:],ExtREAL,
y be Element of Y;
cluster ProjMap2(F,y) -> without+infty;
correctness
proof
now let x be object;
per cases;
suppose not x in dom (ProjMap2(F,y));
hence (ProjMap2(F,y)).x < +infty by FUNCT_1:def 2;
end;
suppose x in dom (ProjMap2(F,y)); then
reconsider x1=x as Element of X;
(ProjMap2(F,y)).x = F.(x1,y) by MESFUNC9:def 7;
hence (ProjMap2(F,y)).x < +infty by MESFUNC5:def 6;
end;
end;
hence thesis by MESFUNC5:def 6;
end;
end;
registration
let X,Y be non empty set, F be without-infty Function of [:X,Y:],ExtREAL,
x be Element of X;
cluster ProjMap1(F,x) -> without-infty;
correctness
proof
now let y be object;
per cases;
suppose not y in dom (ProjMap1(F,x));
hence -infty < (ProjMap1(F,x)).y by FUNCT_1:def 2;
end;
suppose y in dom (ProjMap1(F,x)); then
reconsider y1=y as Element of Y;
(ProjMap1(F,x)).y = F.(x,y1) by MESFUNC9:def 6;
hence -infty < (ProjMap1(F,x)).y by MESFUNC5:def 5;
end;
end;
hence thesis by MESFUNC5:def 5;
end;
end;
registration
let X,Y be non empty set, F be without-infty Function of [:X,Y:],ExtREAL,
y be Element of Y;
cluster ProjMap2(F,y) -> without-infty;
correctness
proof
now let x be object;
per cases;
suppose not x in dom (ProjMap2(F,y));
hence -infty < (ProjMap2(F,y)).x by FUNCT_1:def 2;
end;
suppose x in dom (ProjMap2(F,y)); then
reconsider x1=x as Element of X;
(ProjMap2(F,y)).x = F.(x1,y) by MESFUNC9:def 7;
hence -infty < (ProjMap2(F,y)).x by MESFUNC5:def 5;
end;
end;
hence thesis by MESFUNC5:def 5;
end;
end;
definition
let f be Function of [:NAT,NAT:],ExtREAL;
func Partial_Sums_in_cod2 f -> Function of [:NAT,NAT:],ExtREAL means :DefCSM:
for n,m be Nat holds
it.(n,0) = f.(n,0) & it.(n,m+1) = it.(n,m) + f.(n,m+1);
existence
proof
deffunc F0(Element of NAT) = f.($1,0);
consider f0 be Function of NAT,ExtREAL such that
A1: for n be Element of NAT holds f0.n = F0(n) from FUNCT_2:sch 4;
deffunc F(Element of ExtREAL,Nat,Nat) = $1 + f.($2,$3+1);
consider IT be Function of [:NAT,NAT:],ExtREAL such that
A2: for a be Element of NAT holds
IT.(a,0) = f0.a &
for n be Nat holds IT.(a,n+1) = F(IT.(a,n),a,n)
from DBLSEQ_2:sch 1;
take IT;
hereby let n,m be Nat;
A3: n in NAT & m in NAT by ORDINAL1:def 12; then
IT.(n,0) = f0.n by A2;
hence IT.(n,0) = f.(n,0) & IT.(n,m+1) = IT.(n,m) + f.(n,m+1) by A1,A2,A3;
end;
end;
uniqueness
proof
let f1,f2 be Function of [:NAT,NAT:],ExtREAL;
assume that
A1: for n,m be natural number holds
f1.(n,0) = f.(n,0) & f1.(n,m+1) = f1.(n,m) + f.(n,m+1) and
A2: for n,m be natural number holds
f2.(n,0) = f.(n,0) & f2.(n,m+1) = f2.(n,m) + f.(n,m+1);
A3:dom f1 = [:NAT,NAT:] & dom f2 = [:NAT,NAT:] by FUNCT_2:def 1;
for n,m be object st n in NAT & m in NAT holds f1.(n,m) = f2.(n,m)
proof
let n,m be object;
assume n in NAT & m in NAT; then
reconsider n1 = n, m1 = m as Element of NAT;
defpred P[Nat] means f1.(n1,$1) = f2.(n1,$1);
f1.(n1,0) = f.(n1,0) by A1; then
A4: P[0] by A2;
A5: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A6: P[k];
f1.(n1,k+1) = f1.(n1,k) + f.(n1,k+1) by A1;
hence f1.(n1,k+1) = f2.(n1,k+1) by A2,A6;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A4,A5); then
P[m1];
hence f1.(n,m) = f2.(n,m);
end;
hence thesis by A3,FUNCT_3:6;
end;
end;
definition
let f be Function of [:NAT,NAT:],ExtREAL;
func Partial_Sums_in_cod1 f -> Function of [:NAT,NAT:],ExtREAL means :DefRSM:
for n,m be Nat holds
it.(0,m) = f.(0,m) & it.(n+1,m) = it.(n,m) + f.(n+1,m);
existence
proof
deffunc F0(Element of NAT) = f.(0,$1);
consider f0 be Function of NAT,ExtREAL such that
A1: for n be Element of NAT holds f0.n = F0(n) from FUNCT_2:sch 4;
deffunc F(Element of ExtREAL, Nat, Nat) = $1 + f.($3+1,$2);
consider IT be Function of [:NAT,NAT:],ExtREAL such that
A2: for a be Element of NAT holds
IT.(0,a) = f0.a &
for n be Nat holds IT.(n+1,a) = F(IT.(n,a),a,n)
from DBLSEQ_2:sch 3;
take IT;
hereby let n,m be Nat;
A3: n in NAT & m in NAT by ORDINAL1:def 12; then
IT.(0,m) = f0.m by A2;
hence IT.(0,m) = f.(0,m) & IT.(n+1,m) = IT.(n,m) + f.(n+1,m) by A1,A2,A3;
end;
end;
uniqueness
proof
let f1,f2 be Function of [:NAT,NAT:],ExtREAL;
assume that
A1: for n,m be natural number holds
f1.(0,m) = f.(0,m) & f1.(n+1,m) = f1.(n,m) + f.(n+1,m) and
A2: for n,m be natural number holds
f2.(0,m) = f.(0,m) & f2.(n+1,m) = f2.(n,m) + f.(n+1,m);
A3:dom f1 = [:NAT,NAT:] & dom f2 = [:NAT,NAT:] by FUNCT_2:def 1;
for n,m be object st n in NAT & m in NAT holds f1.(n,m) = f2.(n,m)
proof
let n,m be object;
assume n in NAT & m in NAT; then
reconsider n1 = n, m1 = m as Element of NAT;
defpred P[Nat] means f1.($1,m1) = f2.($1,m1);
f1.(0,m1) = f.(0,m1) by A1; then
A4: P[0] by A2;
A5: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A6: P[k];
f1.(k+1,m1) = f1.(k,m1) + f.(k+1,m1) by A1;
hence f1.(k+1,m1) = f2.(k+1,m1) by A2,A6;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A4,A5); then
P[n1];
hence f1.(n,m) = f2.(n,m);
end;
hence thesis by A3,FUNCT_3:6;
end;
end;
registration
let f be without-infty Function of [:NAT,NAT:],ExtREAL;
cluster Partial_Sums_in_cod2 f -> without-infty;
correctness
proof
for x be object holds -infty < (Partial_Sums_in_cod2 f).x
proof
let x be object;
per cases;
suppose x in dom (Partial_Sums_in_cod2 f); then
consider n,m be object such that
A1: n in NAT & m in NAT & x = [n,m] by ZFMISC_1:def 2;
reconsider n,m as Element of NAT by A1;
defpred P[Nat] means (Partial_Sums_in_cod2 f).(n,$1) > -infty;
(Partial_Sums_in_cod2 f).(n,0) = f.(n,0) by DefCSM; then
A2: P[0] by MESFUNC5:def 5;
A3: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A4: P[k];
A5: f.(n,k+1) > -infty by MESFUNC5:def 5;
(Partial_Sums_in_cod2 f).(n,k+1)
= (Partial_Sums_in_cod2 f).(n,k) + f.(n,k+1) by DefCSM;
hence P[k+1] by A4,A5,XXREAL_3:17,XXREAL_0:6;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A2,A3); then
P[m];
hence -infty < (Partial_Sums_in_cod2 f).x by A1;
end;
suppose not x in dom (Partial_Sums_in_cod2 f);
hence -infty < (Partial_Sums_in_cod2 f).x by FUNCT_1:def 2;
end;
end;
hence (Partial_Sums_in_cod2 f) is without-infty by MESFUNC5:def 5;
end;
end;
registration
let f be without+infty Function of [:NAT,NAT:],ExtREAL;
cluster Partial_Sums_in_cod2 f -> without+infty;
correctness
proof
for x be object holds +infty > (Partial_Sums_in_cod2 f).x
proof
let x be object;
per cases;
suppose x in dom (Partial_Sums_in_cod2 f); then
consider n,m be object such that
A1: n in NAT & m in NAT & x = [n,m] by ZFMISC_1:def 2;
reconsider n,m as Element of NAT by A1;
defpred P[Nat] means (Partial_Sums_in_cod2 f).(n,$1) < +infty;
(Partial_Sums_in_cod2 f).(n,0) = f.(n,0) by DefCSM; then
A2: P[0] by MESFUNC5:def 6;
A3: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A4: P[k];
A5: f.(n,k+1) < +infty by MESFUNC5:def 6;
(Partial_Sums_in_cod2 f).(n,k+1)
= (Partial_Sums_in_cod2 f).(n,k) + f.(n,k+1) by DefCSM;
hence P[k+1] by A4,A5,XXREAL_3:16,XXREAL_0:4;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A2,A3); then
P[m];
hence +infty > (Partial_Sums_in_cod2 f).x by A1;
end;
suppose not x in dom (Partial_Sums_in_cod2 f);
hence +infty > (Partial_Sums_in_cod2 f).x by FUNCT_1:def 2;
end;
end;
hence (Partial_Sums_in_cod2 f) is without+infty by MESFUNC5:def 6;
end;
end;
registration
let f be nonnegative Function of [:NAT,NAT:],ExtREAL;
cluster Partial_Sums_in_cod2 f
-> nonnegative for Function of [:NAT,NAT:],ExtREAL;
correctness
proof
for z be object st z in dom (Partial_Sums_in_cod2 f)
holds 0. <= (Partial_Sums_in_cod2 f).z
proof
let z be object;
assume z in dom(Partial_Sums_in_cod2 f); then
consider n,m be object such that
A1: n in NAT & m in NAT & z = [n,m] by ZFMISC_1:def 2;
reconsider n,m as Element of NAT by A1;
defpred P[Nat] means (Partial_Sums_in_cod2 f).(n,$1) >= 0;
(Partial_Sums_in_cod2 f).(n,0) = f.(n,0) by DefCSM; then
A2: P[0] by SUPINF_2:51;
A3: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A4: P[k];
A5: f.(n,k+1) >= 0 by SUPINF_2:51;
(Partial_Sums_in_cod2 f).(n,k+1)
= (Partial_Sums_in_cod2 f).(n,k) + f.(n,k+1) by DefCSM;
hence (Partial_Sums_in_cod2 f).(n,k+1) >= 0 by A5,A4;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A2,A3); then
(Partial_Sums_in_cod2 f).(n,m) >= 0;
hence 0. <= (Partial_Sums_in_cod2 f).z by A1;
end;
hence thesis by SUPINF_2:52;
end;
end;
registration
let f be nonpositive Function of [:NAT,NAT:],ExtREAL;
cluster Partial_Sums_in_cod2 f
-> nonpositive for Function of [:NAT,NAT:],ExtREAL;
correctness
proof
for z be set st z in dom (Partial_Sums_in_cod2 f)
holds 0. >= (Partial_Sums_in_cod2 f).z
proof
let z be set;
assume z in dom(Partial_Sums_in_cod2 f); then
consider n,m be object such that
A1: n in NAT & m in NAT & z = [n,m] by ZFMISC_1:def 2;
reconsider n,m as Element of NAT by A1;
defpred P[Nat] means (Partial_Sums_in_cod2 f).(n,$1) <= 0;
(Partial_Sums_in_cod2 f).(n,0) = f.(n,0) by DefCSM; then
A2: P[0] by MESFUNC5:8;
A3: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A4: P[k];
A5: f.(n,k+1) <= 0 by MESFUNC5:8;
(Partial_Sums_in_cod2 f).(n,k+1)
= (Partial_Sums_in_cod2 f).(n,k) + f.(n,k+1) by DefCSM;
hence (Partial_Sums_in_cod2 f).(n,k+1) <= 0 by A5,A4;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A2,A3); then
(Partial_Sums_in_cod2 f).(n,m) <= 0;
hence 0. >= (Partial_Sums_in_cod2 f).z by A1;
end;
hence thesis by MESFUNC5:9;
end;
end;
registration
let f be without-infty Function of [:NAT,NAT:],ExtREAL;
cluster Partial_Sums_in_cod1 f -> without-infty;
correctness
proof
for x be object holds -infty < (Partial_Sums_in_cod1 f).x
proof
let x be object;
per cases;
suppose x in dom Partial_Sums_in_cod1 f; then
consider n,m be object such that
A1: n in NAT & m in NAT & x = [n,m] by ZFMISC_1:def 2;
reconsider n,m as Element of NAT by A1;
defpred P[Nat] means (Partial_Sums_in_cod1 f).($1,m) > -infty;
(Partial_Sums_in_cod1 f).(0,m) = f.(0,m) by DefRSM; then
A2: P[0] by MESFUNC5:def 5;
A3: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A4: P[k];
A5: f.(k+1,m) > -infty by MESFUNC5:def 5;
(Partial_Sums_in_cod1 f).(k+1,m)
= (Partial_Sums_in_cod1 f).(k,m) + f.(k+1,m) by DefRSM;
hence P[k+1] by A4,A5,XXREAL_3:17,XXREAL_0:6;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A2,A3); then
P[n];
hence -infty < (Partial_Sums_in_cod1 f).x by A1;
end;
suppose not x in dom (Partial_Sums_in_cod1 f);
hence -infty < (Partial_Sums_in_cod1 f).x by FUNCT_1:def 2;
end;
end;
hence Partial_Sums_in_cod1 f is without-infty by MESFUNC5:def 5;
end;
end;
registration
let f be without+infty Function of [:NAT,NAT:],ExtREAL;
cluster Partial_Sums_in_cod1 f -> without+infty;
correctness
proof
for x be object holds +infty > (Partial_Sums_in_cod1 f).x
proof
let x be object;
per cases;
suppose x in dom (Partial_Sums_in_cod1 f); then
consider n,m be object such that
A1: n in NAT & m in NAT & x = [n,m] by ZFMISC_1:def 2;
reconsider n,m as Element of NAT by A1;
defpred P[Nat] means (Partial_Sums_in_cod1 f).($1,m) < +infty;
(Partial_Sums_in_cod1 f).(0,m) = f.(0,m) by DefRSM; then
A2: P[0] by MESFUNC5:def 6;
A3: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A4: P[k];
A5: f.(k+1,m) < +infty by MESFUNC5:def 6;
(Partial_Sums_in_cod1 f).(k+1,m)
= (Partial_Sums_in_cod1 f).(k,m) + f.(k+1,m) by DefRSM;
hence P[k+1] by A4,A5,XXREAL_3:16,XXREAL_0:4;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A2,A3); then
P[n];
hence +infty > (Partial_Sums_in_cod1 f).x by A1;
end;
suppose not x in dom (Partial_Sums_in_cod1 f);
hence +infty > (Partial_Sums_in_cod1 f).x by FUNCT_1:def 2;
end;
end;
hence (Partial_Sums_in_cod1 f) is without+infty by MESFUNC5:def 6;
end;
end;
registration
let f be nonnegative Function of [:NAT,NAT:],ExtREAL;
cluster Partial_Sums_in_cod1 f
-> nonnegative for Function of [:NAT,NAT:],ExtREAL;
correctness
proof
for z be object st z in dom (Partial_Sums_in_cod1 f)
holds 0. <= (Partial_Sums_in_cod1 f).z
proof
let z be object;
assume z in dom(Partial_Sums_in_cod1 f); then
consider m,n be object such that
A1: m in NAT & n in NAT & z = [m,n] by ZFMISC_1:def 2;
reconsider n,m as Element of NAT by A1;
defpred P[Nat] means (Partial_Sums_in_cod1 f).($1,n) >= 0;
(Partial_Sums_in_cod1 f).(0,n) = f.(0,n) by DefRSM; then
A2: P[0] by SUPINF_2:51;
A3: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A4: P[k];
A5: f.(k+1,n) >= 0 by SUPINF_2:51;
(Partial_Sums_in_cod1 f).(k+1,n)
= (Partial_Sums_in_cod1 f).(k,n) + f.(k+1,n) by DefRSM;
hence (Partial_Sums_in_cod1 f).(k+1,n) >= 0 by A5,A4;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A2,A3); then
(Partial_Sums_in_cod1 f).(m,n) >= 0;
hence 0. <= (Partial_Sums_in_cod1 f).z by A1;
end;
hence thesis by SUPINF_2:52;
end;
end;
registration
let f be nonpositive Function of [:NAT,NAT:],ExtREAL;
cluster Partial_Sums_in_cod1 f
-> nonpositive for Function of [:NAT,NAT:],ExtREAL;
correctness
proof
for z be set st z in dom (Partial_Sums_in_cod1 f)
holds 0. >= (Partial_Sums_in_cod1 f).z
proof
let z be set;
assume z in dom(Partial_Sums_in_cod1 f); then
consider m,n be object such that
A1: m in NAT & n in NAT & z = [m,n] by ZFMISC_1:def 2;
reconsider n,m as Element of NAT by A1;
defpred P[Nat] means (Partial_Sums_in_cod1 f).($1,n) <= 0;
(Partial_Sums_in_cod1 f).(0,n) = f.(0,n) by DefRSM; then
A2: P[0] by MESFUNC5:8;
A3: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A4: P[k];
A5: f.(k+1,n) <= 0 by MESFUNC5:8;
(Partial_Sums_in_cod1 f).(k+1,n)
= (Partial_Sums_in_cod1 f).(k,n) + f.(k+1,n) by DefRSM;
hence (Partial_Sums_in_cod1 f).(k+1,n) <= 0 by A5,A4;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A2,A3); then
(Partial_Sums_in_cod1 f).(m,n) <= 0;
hence 0. >= (Partial_Sums_in_cod1 f).z by A1;
end;
hence thesis by MESFUNC5:9;
end;
end;
definition
let f be Function of [:NAT,NAT:],ExtREAL;
func Partial_Sums f -> Function of [:NAT,NAT:],ExtREAL
equals Partial_Sums_in_cod2( Partial_Sums_in_cod1 f );
correctness;
end;
theorem Th39:
for f be Function of [:NAT,NAT:],ExtREAL, n,m be Nat holds
(Partial_Sums_in_cod1 f).(n,m) = (Partial_Sums_in_cod2 f@).(m,n)
& (Partial_Sums_in_cod2 f).(n,m) = (Partial_Sums_in_cod1 f@).(m,n)
proof
let f be Function of [:NAT,NAT:],ExtREAL;
let n,m be Nat;
reconsider n1=n, m1=m as Element of NAT by ORDINAL1:def 12;
defpred P1[Nat] means
(Partial_Sums_in_cod1 f).($1,m) = (Partial_Sums_in_cod2 f@).(m,$1);
(Partial_Sums_in_cod1 f).(0,m) = f.(0,m) by DefRSM
.= (f@).(m1,0) by DBLSEQ_2:def 2; then
A2:P1[0] by DefCSM;
A3:for k be Nat st P1[k] holds P1[k+1]
proof
let k be Nat;
assume A4: P1[k];
(Partial_Sums_in_cod1 f).(k+1,m)
= (Partial_Sums_in_cod1 f).(k,m) + f.(k+1,m) by DefRSM
.= (Partial_Sums_in_cod2 f@).(m,k) + f@.(m1,k+1) by A4,DBLSEQ_2:def 2;
hence P1[k+1] by DefCSM;
end;
for k be Nat holds P1[k] from NAT_1:sch 2(A2,A3);
hence (Partial_Sums_in_cod1 f).(n,m) = (Partial_Sums_in_cod2 f@).(m,n);
defpred P2[Nat] means
(Partial_Sums_in_cod2 f).(n,$1) = (Partial_Sums_in_cod1 f@).($1,n);
(Partial_Sums_in_cod2 f).(n,0) = f.(n,0) by DefCSM
.= (f@).(0,n1) by DBLSEQ_2:def 2; then
A5:P2[0] by DefRSM;
A6:for k be Nat st P2[k] holds P2[k+1]
proof
let k be Nat;
assume A7: P2[k];
(Partial_Sums_in_cod2 f).(n,k+1)
= (Partial_Sums_in_cod2 f).(n,k) + f.(n,k+1) by DefCSM
.= (Partial_Sums_in_cod1 f@).(k,n) + f@.(k+1,n1) by A7,DBLSEQ_2:def 2;
hence P2[k+1] by DefRSM;
end;
for k be Nat holds P2[k] from NAT_1:sch 2(A5,A6);
hence (Partial_Sums_in_cod2 f).(n,m) = (Partial_Sums_in_cod1 f@).(m,n);
end;
theorem Th40:
for f be Function of [:NAT,NAT:],ExtREAL holds
(Partial_Sums_in_cod1 f)@ = Partial_Sums_in_cod2 f@
& (Partial_Sums_in_cod2 f)@ = Partial_Sums_in_cod1 f@
proof
let f be Function of [:NAT,NAT:],ExtREAL;
now let z be Element of [:NAT,NAT:];
consider n,m be object such that
A1: n in NAT & m in NAT & z = [n,m] by ZFMISC_1:def 2;
reconsider n,m as Element of NAT by A1;
(Partial_Sums_in_cod2 f@).z = (Partial_Sums_in_cod2 f@).(n,m) by A1
.= (Partial_Sums_in_cod1 f).(m,n) by Th39
.= (Partial_Sums_in_cod1 f)@.(n,m) by DBLSEQ_2:def 2;
hence (Partial_Sums_in_cod2 f@).z = (Partial_Sums_in_cod1 f)@.z by A1;
end;
hence (Partial_Sums_in_cod1 f)@ = Partial_Sums_in_cod2 f@ by FUNCT_2:def 8;
now let z be Element of [:NAT,NAT:];
consider n,m be object such that
A2: n in NAT & m in NAT & z = [n,m] by ZFMISC_1:def 2;
reconsider n,m as Element of NAT by A2;
(Partial_Sums_in_cod1 f@).z = (Partial_Sums_in_cod1 f@).(n,m) by A2
.= (Partial_Sums_in_cod2 f).(m,n) by Th39
.= (Partial_Sums_in_cod2 f)@.(n,m) by DBLSEQ_2:def 2;
hence (Partial_Sums_in_cod1 f@).z = (Partial_Sums_in_cod2 f)@.z by A2;
end;
hence (Partial_Sums_in_cod2 f)@ = Partial_Sums_in_cod1 f@ by FUNCT_2:def 8;
end;
theorem
for f be Function of [:NAT,NAT:],ExtREAL,
g be ext-real-valued Function, n be Nat
st (for k be Nat holds (Partial_Sums_in_cod1 f).(n,k) = g.k) holds
(for k be Nat holds (Partial_Sums f).(n,k) = (Partial_Sums g).k)
& (lim_in_cod2(Partial_Sums f)).n = Sum g
proof
let f be Function of [:NAT,NAT:],ExtREAL,
g be ext-real-valued Function, n be Nat;
assume A1: for k be Nat holds (Partial_Sums_in_cod1 f).(n,k) = g.k;
A4:now let k be Nat;
defpred P[Nat] means (Partial_Sums f).(n,$1) = (Partial_Sums g).$1;
(Partial_Sums f).(n,0) = (Partial_Sums_in_cod1 f).(n,0) by DefCSM
.= g.0 by A1; then
A2: P[0] by MESFUNC9:def 1;
A3: for m be Nat st P[m] holds P[m+1]
proof
let m be Nat;
assume A4: P[m];
(Partial_Sums f).(n,m+1)
= (Partial_Sums_in_cod2(Partial_Sums_in_cod1 f)).(n,m)
+ (Partial_Sums_in_cod1 f).(n,m+1) by DefCSM
.= (Partial_Sums g).m + g.(m+1) by A1,A4;
hence P[m+1] by MESFUNC9:def 1;
end;
for m be Nat holds P[m] from NAT_1:sch 2(A2,A3);
hence (Partial_Sums f).(n,k) = (Partial_Sums g).k;
end;
reconsider n1=n as Element of NAT by ORDINAL1:def 12;
now let k be Element of NAT;
ProjMap1(Partial_Sums f,n1).k = (Partial_Sums f).(n,k) by MESFUNC9:def 6;
hence ProjMap1(Partial_Sums f,n1).k = (Partial_Sums g).k by A4;
end; then
ProjMap1(Partial_Sums f,n1) = Partial_Sums g by FUNCT_2:def 8; then
(lim_in_cod2(Partial_Sums f)).n1 = lim (Partial_Sums g) by D1DEF6;
hence thesis by A4,MESFUNC9:def 3;
end;
theorem Th42:
for f be Function of [:NAT,NAT:],ExtREAL holds
Partial_Sums_in_cod2(-f) = -(Partial_Sums_in_cod2 f)
& Partial_Sums_in_cod1(-f) = -(Partial_Sums_in_cod1 f)
proof
let f be Function of [:NAT,NAT:],ExtREAL;
A1:dom(-(Partial_Sums_in_cod2 f)) = [:NAT,NAT:]
& dom(-(Partial_Sums_in_cod1 f)) = [:NAT,NAT:] by FUNCT_2:def 1;
A2:dom(-f) = [:NAT,NAT:] by FUNCT_2:def 1;
for z be Element of [:NAT,NAT:] holds
(-(Partial_Sums_in_cod2 f)).z = (Partial_Sums_in_cod2(-f)).z
proof
let z be Element of [:NAT,NAT:];
consider n,m be object such that
A3: n in NAT & m in NAT & z = [n,m] by ZFMISC_1:def 2;
reconsider n,m as Element of NAT by A3;
defpred P[Nat] means (Partial_Sums_in_cod2(-f)).(n,$1)
= -((Partial_Sums_in_cod2 f).(n,$1));
reconsider z0 = [n,0] as Element of [:NAT,NAT:] by ZFMISC_1:87;
A4: [n,0] in [:NAT,NAT:] by ZFMISC_1:87;
(Partial_Sums_in_cod2(-f)).(n,0)
= (-f).(n,0) by DefCSM
.= -(f.(n,0)) by A4,A2,MESFUNC1:def 7; then
A5: P[0] by DefCSM;
A6: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A7: P[k];
A8: [n,k+1] in [:NAT,NAT:] by ZFMISC_1:87;
thus (Partial_Sums_in_cod2 -f).(n,k+1)
= (Partial_Sums_in_cod2 -f).(n,k) + (-f).(n,k+1) by DefCSM
.= -((Partial_Sums_in_cod2 f).(n,k)) -(f.(n,k+1))
by A7,A8,A2,MESFUNC1:def 7
.= -((Partial_Sums_in_cod2 f).(n,k) + f.(n,k+1)) by XXREAL_3:25
.= -( (Partial_Sums_in_cod2 f).(n,k+1) ) by DefCSM;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A5,A6); then
(Partial_Sums_in_cod2(-f)).(n,m) = -((Partial_Sums_in_cod2 f).(n,m));
hence thesis by A3,A1,MESFUNC1:def 7;
end;
hence Partial_Sums_in_cod2(-f) = -(Partial_Sums_in_cod2 f) by FUNCT_2:def 8;
for z be Element of [:NAT,NAT:] holds
(-(Partial_Sums_in_cod1 f)).z = (Partial_Sums_in_cod1(-f)).z
proof
let z be Element of [:NAT,NAT:];
consider n,m be object such that
A3: n in NAT & m in NAT & z = [n,m] by ZFMISC_1:def 2;
reconsider n,m as Element of NAT by A3;
defpred P[Nat] means (Partial_Sums_in_cod1(-f)).($1,m)
= -((Partial_Sums_in_cod1 f).($1,m));
reconsider z0 = [0,m] as Element of [:NAT,NAT:] by ZFMISC_1:87;
A4: [0,m] in [:NAT,NAT:] by ZFMISC_1:87;
(Partial_Sums_in_cod1(-f)).(0,m)
= (-f).(0,m) by DefRSM
.= -(f.(0,m)) by A4,A2,MESFUNC1:def 7; then
A5: P[0] by DefRSM;
A6: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A7: P[k];
A8: [k+1,m] in [:NAT,NAT:] by ZFMISC_1:87;
thus (Partial_Sums_in_cod1 -f).(k+1,m)
= (Partial_Sums_in_cod1 -f).(k,m) + (-f).(k+1,m) by DefRSM
.= -((Partial_Sums_in_cod1 f).(k,m)) -(f.(k+1,m))
by A7,A8,A2,MESFUNC1:def 7
.= -((Partial_Sums_in_cod1 f).(k,m) + f.(k+1,m)) by XXREAL_3:25
.= -( (Partial_Sums_in_cod1 f).(k+1,m) ) by DefRSM;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A5,A6); then
(Partial_Sums_in_cod1(-f)).(n,m) = -((Partial_Sums_in_cod1 f).(n,m));
hence thesis by A3,A1,MESFUNC1:def 7;
end;
hence Partial_Sums_in_cod1(-f) = -(Partial_Sums_in_cod1 f) by FUNCT_2:def 8;
end;
theorem Th43:
for f be Function of [:NAT,NAT:],ExtREAL,
m,n be Element of NAT holds
(Partial_Sums_in_cod1 f).(m,n) = Partial_Sums(ProjMap2(f,n)).m &
(Partial_Sums_in_cod2 f).(m,n) = Partial_Sums(ProjMap1(f,m)).n
proof
let f be Function of [:NAT,NAT:],ExtREAL;
let m,n be Element of NAT;
defpred P[Nat] means
(Partial_Sums_in_cod1 f).($1,n) = Partial_Sums(ProjMap2(f,n)).$1;
Partial_Sums(ProjMap2(f,n)).0 = (ProjMap2(f,n)).0 by MESFUNC9:def 1
.= f.(0,n) by MESFUNC9:def 7; then
a1:P[0] by DefRSM;
a2:for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume P[k]; then
(Partial_Sums_in_cod1 f).(k+1,n)
= Partial_Sums(ProjMap2(f,n)).k + f.(k+1,n) by DefRSM
.= Partial_Sums(ProjMap2(f,n)).k + (ProjMap2(f,n)).(k+1)
by MESFUNC9:def 7;
hence P[k+1] by MESFUNC9:def 1;
end;
for k be Nat holds P[k] from NAT_1:sch 2(a1,a2);
hence (Partial_Sums_in_cod1 f).(m,n) = Partial_Sums(ProjMap2(f,n)).m;
defpred Q[Nat] means
(Partial_Sums_in_cod2 f).(m,$1) = Partial_Sums(ProjMap1(f,m)).$1;
Partial_Sums(ProjMap1(f,m)).0 = (ProjMap1(f,m)).0 by MESFUNC9:def 1
.= f.(m,0) by MESFUNC9:def 6; then
a3:Q[0] by DefCSM;
a4:for k be Nat st Q[k] holds Q[k+1]
proof
let k be Nat;
assume Q[k]; then
(Partial_Sums_in_cod2 f).(m,k+1)
= Partial_Sums(ProjMap1(f,m)).k + f.(m,k+1) by DefCSM
.= Partial_Sums(ProjMap1(f,m)).k + (ProjMap1(f,m)).(k+1)
by MESFUNC9:def 6;
hence Q[k+1] by MESFUNC9:def 1;
end;
for k be Nat holds Q[k] from NAT_1:sch 2(a3,a4);
hence thesis;
end;
theorem Th44:
for f1,f2 be without-infty Function of [:NAT,NAT:],ExtREAL holds
Partial_Sums_in_cod2(f1+f2)
= Partial_Sums_in_cod2 f1 + Partial_Sums_in_cod2 f2 &
Partial_Sums_in_cod1(f1+f2)
= Partial_Sums_in_cod1 f1 + Partial_Sums_in_cod1 f2
proof
let f1,f2 be without-infty Function of [:NAT,NAT:],ExtREAL;
set CS1 = Partial_Sums_in_cod2 f1;
set CS2 = Partial_Sums_in_cod2 f2;
set CS12 = Partial_Sums_in_cod2(f1+f2);
set RS1 = Partial_Sums_in_cod1 f1;
set RS2 = Partial_Sums_in_cod1 f2;
set RS12 = Partial_Sums_in_cod1(f1+f2);
now let n be Element of NAT, m be Element of NAT;
defpred C[Nat] means CS12.(n,$1) = CS1.(n,$1) + CS2.(n,$1);
CS12.(n,0) = (f1+f2).(n,0) by DefCSM
.= f1.(n,0) + f2.(n,0) by Th11
.= CS1.(n,0) + f2.(n,0) by DefCSM; then
a1: C[0] by DefCSM;
a2: for k be Nat st C[k] holds C[k+1]
proof
let k be Nat;
assume a3: C[k];
X1: CS1.(n,k) <> -infty & CS2.(n,k) <> -infty & f1.(n,k+1) <> -infty
& f2.(n,k+1) <> -infty & (f1+f2).(n,k+1) <> -infty
by MESFUNC5:def 5; then
X2: CS2.(n,k) + f2.(n,k+1) <> -infty by XXREAL_3:17;
CS12.(n,k+1) = CS12.(n,k) + (f1+f2).(n,k+1) by DefCSM
.= CS1.(n,k) + ( (f1+f2).(n,k+1) + CS2.(n,k) ) by a3,X1,XXREAL_3:29
.= CS1.(n,k) + ( f1.(n,k+1) + f2.(n,k+1) + CS2.(n,k) ) by Th11
.= CS1.(n,k) + ( f1.(n,k+1) + ( CS2.(n,k) + f2.(n,k+1) ) )
by X1,XXREAL_3:29
.= CS1.(n,k) + f1.(n,k+1) + ( CS2.(n,k) + f2.(n,k+1) )
by X1,X2,XXREAL_3:29
.= CS1.(n,k+1) + ( CS2.(n,k) + f2.(n,k+1) ) by DefCSM;
hence C[k+1] by DefCSM;
end;
for k be Nat holds C[k] from NAT_1:sch 2(a1,a2); then
C[m];
hence CS12.(n,m) = (CS1+CS2).(n,m) by Th11;
end;
hence CS12 = CS1 + CS2 by BINOP_1:2;
now let n,m be Element of NAT;
defpred R[Nat] means RS12.($1,m) = RS1.($1,m) + RS2.($1,m);
RS12.(0,m) = (f1+f2).(0,m) by DefRSM
.= f1.(0,m) + f2.(0,m) by Th11
.= RS1.(0,m) + f2.(0,m) by DefRSM; then
a4: R[0] by DefRSM;
a5: for k be Nat st R[k] holds R[k+1]
proof
let k be Nat;
assume a6: R[k];
X3: RS1.(k,m) <> -infty & RS2.(k,m) <> -infty & f1.(k+1,m) <> -infty
& f2.(k+1,m) <> -infty & (f1+f2).(k+1,m) <> -infty
by MESFUNC5:def 5; then
X4: RS2.(k,m) + f2.(k+1,m) <> -infty by XXREAL_3:17;
RS12.(k+1,m) = RS12.(k,m) + (f1+f2).(k+1,m) by DefRSM
.= RS1.(k,m) + ( (f1+f2).(k+1,m) + RS2.(k,m) ) by a6,X3,XXREAL_3:29
.= RS1.(k,m) + ( f1.(k+1,m) + f2.(k+1,m) + RS2.(k,m) ) by Th11
.= RS1.(k,m) + ( f1.(k+1,m) + ( RS2.(k,m) + f2.(k+1,m) ) )
by X3,XXREAL_3:29
.= RS1.(k,m) + f1.(k+1,m) + ( RS2.(k,m) + f2.(k+1,m) )
by X3,X4,XXREAL_3:29
.= RS1.(k+1,m) + (RS2.(k,m) + f2.(k+1,m)) by DefRSM;
hence R[k+1] by DefRSM;
end;
for k be Nat holds R[k] from NAT_1:sch 2(a4,a5); then
R[n];
hence RS12.(n,m) = (RS1+RS2).(n,m) by Th11;
end;
hence RS12 = RS1 + RS2 by BINOP_1:2;
end;
theorem Th45:
for f1,f2 be without+infty Function of [:NAT,NAT:],ExtREAL holds
Partial_Sums_in_cod2(f1+f2)
= Partial_Sums_in_cod2 f1 + Partial_Sums_in_cod2 f2 &
Partial_Sums_in_cod1(f1+f2)
= Partial_Sums_in_cod1 f1 + Partial_Sums_in_cod1 f2
proof
let f1,f2 be without+infty Function of [:NAT,NAT:],ExtREAL;
reconsider F1=-f1, F2=-f2 as without-infty Function of [:NAT,NAT:],ExtREAL;
F1+F2 = -f1 -f2 by Th10 .= -(f1+f2) by Th9; then
A1:-(F1+F2) = f1+f2 by Th2; then
Partial_Sums_in_cod2(f1+f2) = -(Partial_Sums_in_cod2(F1+F2)) by Th42
.= -(Partial_Sums_in_cod2 F1 + Partial_Sums_in_cod2 F2) by Th44
.= -( -(Partial_Sums_in_cod2 f1) + Partial_Sums_in_cod2 F2 ) by Th42
.= -( -(Partial_Sums_in_cod2 f1) + -(Partial_Sums_in_cod2 f2) ) by Th42
.= -(-(Partial_Sums_in_cod2 f1)) -(-(Partial_Sums_in_cod2 f2))
by Th8
.= Partial_Sums_in_cod2 f1 -(-(Partial_Sums_in_cod2 f2)) by Th2
.= Partial_Sums_in_cod2 f1 + (-(-(Partial_Sums_in_cod2 f2))) by Th10;
hence Partial_Sums_in_cod2(f1+f2)
= Partial_Sums_in_cod2 f1 + Partial_Sums_in_cod2 f2 by Th2;
Partial_Sums_in_cod1(f1+f2) = -(Partial_Sums_in_cod1(F1+F2)) by A1,Th42
.= -(Partial_Sums_in_cod1 F1 + Partial_Sums_in_cod1 F2) by Th44
.= -( -(Partial_Sums_in_cod1 f1) + Partial_Sums_in_cod1 F2 ) by Th42
.= -( -(Partial_Sums_in_cod1 f1) + -(Partial_Sums_in_cod1 f2) ) by Th42
.= -(-(Partial_Sums_in_cod1 f1)) -(-(Partial_Sums_in_cod1 f2))
by Th8
.= Partial_Sums_in_cod1 f1 -(-(Partial_Sums_in_cod1 f2)) by Th2
.= Partial_Sums_in_cod1 f1 + (-(-(Partial_Sums_in_cod1 f2))) by Th10;
hence thesis by Th2;
end;
theorem Th46:
for f1 be without-infty Function of [:NAT,NAT:],ExtREAL,
f2 be without+infty Function of [:NAT,NAT:],ExtREAL holds
Partial_Sums_in_cod2(f1-f2)
= Partial_Sums_in_cod2 f1 - Partial_Sums_in_cod2 f2 &
Partial_Sums_in_cod1(f1-f2)
= Partial_Sums_in_cod1 f1 - Partial_Sums_in_cod1 f2 &
Partial_Sums_in_cod2(f2-f1)
= Partial_Sums_in_cod2 f2 - Partial_Sums_in_cod2 f1 &
Partial_Sums_in_cod1(f2-f1)
= Partial_Sums_in_cod1 f2 - Partial_Sums_in_cod1 f1
proof
let f1 be without-infty Function of [:NAT,NAT:],ExtREAL,
f2 be without+infty Function of [:NAT,NAT:],ExtREAL;
Partial_Sums_in_cod2(f1-f2) = Partial_Sums_in_cod2(f1+(-f2)) by Th10
.= Partial_Sums_in_cod2 f1 + Partial_Sums_in_cod2 (-f2)
by Th44
.= Partial_Sums_in_cod2 f1 + -(Partial_Sums_in_cod2 f2) by Th42;
hence Partial_Sums_in_cod2(f1-f2)
= Partial_Sums_in_cod2 f1 - Partial_Sums_in_cod2 f2 by Th10;
Partial_Sums_in_cod1(f1-f2) = Partial_Sums_in_cod1(f1+(-f2)) by Th10
.= Partial_Sums_in_cod1 f1 + Partial_Sums_in_cod1 (-f2)
by Th44
.= Partial_Sums_in_cod1 f1 + -(Partial_Sums_in_cod1 f2) by Th42;
hence Partial_Sums_in_cod1(f1-f2)
= Partial_Sums_in_cod1 f1 - Partial_Sums_in_cod1 f2 by Th10;
Partial_Sums_in_cod2(f2-f1) = Partial_Sums_in_cod2(f2+(-f1)) by Th10
.= Partial_Sums_in_cod2 f2 + Partial_Sums_in_cod2 (-f1)
by Th45
.= Partial_Sums_in_cod2 f2 + -(Partial_Sums_in_cod2 f1) by Th42;
hence Partial_Sums_in_cod2(f2-f1)
= Partial_Sums_in_cod2 f2 - Partial_Sums_in_cod2 f1 by Th10;
Partial_Sums_in_cod1(f2-f1) = Partial_Sums_in_cod1(f2+(-f1)) by Th10
.= Partial_Sums_in_cod1 f2 + Partial_Sums_in_cod1 (-f1)
by Th45
.= Partial_Sums_in_cod1 f2 + -(Partial_Sums_in_cod1 f1) by Th42;
hence Partial_Sums_in_cod1(f2-f1)
= Partial_Sums_in_cod1 f2 - Partial_Sums_in_cod1 f1 by Th10;
end;
theorem Th47:
for f be without-infty Function of [:NAT,NAT:],ExtREAL,
n,m be Nat holds
(Partial_Sums f).(n+1,m)
= (Partial_Sums_in_cod2 f).(n+1,m) + (Partial_Sums f).(n,m) &
(Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)).(n,m+1)
= (Partial_Sums_in_cod1 f).(n,m+1)
+ (Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)).(n,m)
proof
let f be without-infty Function of [:NAT,NAT:],ExtREAL;
let n,m be Nat;
set RPS = Partial_Sums f;
set CPS = Partial_Sums_in_cod1(Partial_Sums_in_cod2 f);
set ROW = Partial_Sums_in_cod1 f;
set COL = Partial_Sums_in_cod2 f;
defpred P[Nat] means RPS.(n+1,$1) = COL.(n+1,$1) + RPS.(n,$1);
a1:RPS.(n,0) = ROW.(n,0) by DefCSM;
RPS.(n+1,0) = ROW.(n+1,0) by DefCSM
.= ROW.(n,0) + f.(n+1,0) by DefRSM; then
a3:P[0] by a1,DefCSM;
a4:for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A5: P[k];
a6: COL.(n+1,k+1) = COL.(n+1,k) + f.(n+1,k+1) by DefCSM;
X1: COL.(n+1,k) <> -infty & f.(n+1,k+1) <> -infty & RPS.(n,k) <> -infty
& ROW.(n,k+1) <> -infty & RPS.(n+1,k) <> -infty by MESFUNC5:def 5; then
X2: COL.(n+1,k) + f.(n+1,k+1) <> -infty by XXREAL_3:17;
RPS.(n,k+1) = RPS.(n,k) + ROW.(n,k+1) by DefCSM; then
COL.(n+1,k+1) + RPS.(n,k+1)
= COL.(n+1,k) + f.(n+1,k+1) + RPS.(n,k) + ROW.(n,k+1)
by a6,X1,X2,XXREAL_3:29
.= COL.(n+1,k) + RPS.(n,k) + f.(n+1,k+1) + ROW.(n,k+1)
by X1,XXREAL_3:29
.= RPS.(n+1,k) + ( f.(n+1,k+1) + ROW.(n,k+1) ) by A5,X1,XXREAL_3:29
.= RPS.(n+1,k) + ROW.(n+1,k+1) by DefRSM;
hence P[k+1] by DefCSM;
end;
for k be Nat holds P[k] from NAT_1:sch 2(a3,a4);
hence RPS.(n+1,m) = COL.(n+1,m) + RPS.(n,m);
defpred Q[Nat] means CPS.($1,m+1) = ROW.($1,m+1) + CPS.($1,m);
b1:CPS.(0,m) = COL.(0,m) by DefRSM;
CPS.(0,m+1) = COL.(0,m+1) by DefRSM
.= COL.(0,m) + f.(0,m+1) by DefCSM; then
b3:Q[0] by b1,DefRSM;
b4:for k be Nat st Q[k] holds Q[k+1]
proof
let k be Nat;
assume B5: Q[k];
b6: ROW.(k+1,m+1) = ROW.(k,m+1) + f.(k+1,m+1) by DefRSM;
X3: ROW.(k,m+1) <> -infty & f.(k+1,m+1) <> -infty & CPS.(k,m) <> -infty
& COL.(k+1,m) <> -infty & CPS.(k,m+1) <> -infty by MESFUNC5:def 5; then
X4: ROW.(k,m+1) + f.(k+1,m+1) <> -infty by XXREAL_3:17;
CPS.(k+1,m) = CPS.(k,m) + COL.(k+1,m) by DefRSM; then
ROW.(k+1,m+1) + CPS.(k+1,m)
= ROW.(k,m+1) + f.(k+1,m+1) + CPS.(k,m) + COL.(k+1,m)
by b6,X3,X4,XXREAL_3:29
.= ROW.(k,m+1) + CPS.(k,m) + f.(k+1,m+1) + COL.(k+1,m)
by X3,XXREAL_3:29
.= CPS.(k,m+1) + ( f.(k+1,m+1) + COL.(k+1,m) ) by B5,X3,XXREAL_3:29
.= CPS.(k,m+1) + COL.(k+1,m+1) by DefCSM;
hence Q[k+1] by DefRSM;
end;
for k be Nat holds Q[k] from NAT_1:sch 2(b3,b4);
hence thesis;
end;
theorem
for f be without+infty Function of [:NAT,NAT:],ExtREAL,
n,m be Nat holds
(Partial_Sums f).(n+1,m)
= (Partial_Sums_in_cod2 f).(n+1,m) + (Partial_Sums f).(n,m) &
(Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)).(n,m+1)
= (Partial_Sums_in_cod1 f).(n,m+1)
+ (Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)).(n,m)
proof
let f be without+infty Function of [:NAT,NAT:],ExtREAL;
let n,m be Nat;
reconsider g = -f as without-infty Function of [:NAT,NAT:],ExtREAL;
A2:dom(-(Partial_Sums_in_cod2(Partial_Sums_in_cod1 g))) = [:NAT,NAT:]
& dom(-(Partial_Sums_in_cod1(Partial_Sums_in_cod2 g))) = [:NAT,NAT:]
by FUNCT_2:def 1;
A4:dom(-(Partial_Sums_in_cod2 g)) = [:NAT,NAT:]
& dom(-(Partial_Sums_in_cod1 g)) = [:NAT,NAT:] by FUNCT_2:def 1;
A5:dom(-(Partial_Sums g)) = [:NAT,NAT:] by FUNCT_2:def 1;
n in NAT & m in NAT by ORDINAL1:def 12; then
A3:[n+1,m] in [:NAT,NAT:] & [n,m] in [:NAT,NAT:]
& [n,m+1] in [:NAT,NAT:] by ZFMISC_1:87;
A1:Partial_Sums f = Partial_Sums_in_cod2(Partial_Sums_in_cod1 (-(g))) by Th2
.= Partial_Sums_in_cod2(-(Partial_Sums_in_cod1 g)) by Th42
.= -(Partial_Sums g) by Th42;
thus (Partial_Sums f).(n+1,m)
= -( (Partial_Sums_in_cod2(Partial_Sums_in_cod1 g)).(n+1,m) )
by A1,A2,A3,MESFUNC1:def 7
.= -( (Partial_Sums_in_cod2 g).(n+1,m) + (Partial_Sums g).(n,m) ) by Th47
.= - (Partial_Sums_in_cod2 g).(n+1,m) - (Partial_Sums g).(n,m)
by XXREAL_3:25
.= (-(Partial_Sums_in_cod2 g)).(n+1,m) + -(Partial_Sums g).(n,m)
by A3,A4,MESFUNC1:def 7
.= (Partial_Sums_in_cod2(-g)).(n+1,m) + -(Partial_Sums g).(n,m) by Th42
.= (Partial_Sums_in_cod2 f).(n+1,m) + -(Partial_Sums g).(n,m) by Th2
.= (Partial_Sums_in_cod2 f).(n+1,m) + (Partial_Sums f).(n,m)
by A1,A3,A5,MESFUNC1:def 7;
thus (Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)).(n,m+1)
= (Partial_Sums_in_cod1( (Partial_Sums_in_cod2(-g)) )).(n,m+1) by Th2
.= (Partial_Sums_in_cod1( -(Partial_Sums_in_cod2 g) )).(n,m+1) by Th42
.= ( -(Partial_Sums_in_cod1(Partial_Sums_in_cod2 g)) ).(n,m+1) by Th42
.= -( (Partial_Sums_in_cod1(Partial_Sums_in_cod2 g)).(n,m+1) )
by A3,A2,MESFUNC1:def 7
.= -( (Partial_Sums_in_cod1 g).(n,m+1)
+(Partial_Sums_in_cod1(Partial_Sums_in_cod2 g)).(n,m) ) by Th47
.= -(Partial_Sums_in_cod1 g).(n,m+1)
-(Partial_Sums_in_cod1(Partial_Sums_in_cod2 g)).(n,m) by XXREAL_3:25
.= (-(Partial_Sums_in_cod1 g)).(n,m+1)
-(Partial_Sums_in_cod1(Partial_Sums_in_cod2 g)).(n,m)
by A4,A3,MESFUNC1:def 7
.= (-(Partial_Sums_in_cod1 g)).(n,m+1)
+ (-(Partial_Sums_in_cod1(Partial_Sums_in_cod2 g))).(n,m)
by A3,A2,MESFUNC1:def 7
.= (Partial_Sums_in_cod1(-g)).(n,m+1)
+ (-(Partial_Sums_in_cod1(Partial_Sums_in_cod2 g))).(n,m) by Th42
.= (Partial_Sums_in_cod1 f).(n,m+1)
+ (-(Partial_Sums_in_cod1(Partial_Sums_in_cod2 g))).(n,m) by Th2
.= (Partial_Sums_in_cod1 f).(n,m+1)
+ ((Partial_Sums_in_cod1-(Partial_Sums_in_cod2 g))).(n,m) by Th42
.= (Partial_Sums_in_cod1 f).(n,m+1)
+ ((Partial_Sums_in_cod1(Partial_Sums_in_cod2(-g)))).(n,m) by Th42
.= (Partial_Sums_in_cod1 f).(n,m+1)
+ ((Partial_Sums_in_cod1(Partial_Sums_in_cod2 f))).(n,m) by Th2;
end;
Lm7:
for f be without-infty Function of [:NAT,NAT:],ExtREAL, m,n be Nat holds
(Partial_Sums f).(m,n)
= (Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)).(m,n)
proof
let f be without-infty Function of [:NAT,NAT:],ExtREAL, m,n be Nat;
defpred P1[Nat] means
for m be Nat holds
(Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)).(m,$1)
= (Partial_Sums f).(m,$1);
defpred P2[Nat] means
(Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)).($1,0)
= (Partial_Sums f).($1,0);
Y3:(Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)).(0,0)
= (Partial_Sums_in_cod2 f).(0,0) by DefRSM
.= f.(0,0) by DefCSM;
(Partial_Sums f).(0,0) = (Partial_Sums_in_cod1(f)).(0,0) by DefCSM
.= f.(0,0) by DefRSM; then
Y1:P2[0] by Y3;
Y2:for i be Nat st P2[i] holds P2[i+1]
proof
let i be Nat;
assume Y3: P2[i];
Y4: (Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)).(i+1,0)
= (Partial_Sums_in_cod1(Partial_Sums_in_cod2(f))).(i,0)
+ (Partial_Sums_in_cod2(f)).(i+1,0) by DefRSM
.= (Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)).(i,0) + f.(i+1,0)
by DefCSM;
(Partial_Sums f).(i+1,0) = (Partial_Sums_in_cod1 f).(i+1,0) by DefCSM
.= (Partial_Sums_in_cod1 f).(i,0) + f.(i+1,0) by DefRSM
.= (Partial_Sums f).(i,0) + f.(i+1,0) by DefCSM;
hence P2[i+1] by Y3,Y4;
end;
for n be Nat holds P2[n] from NAT_1:sch 2(Y1,Y2); then
X1:P1[0];
X2:for j be Nat st P1[j] holds P1[j+1]
proof
let j be Nat;
assume Z3: P1[j];
for m be Nat holds
(Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)).(m,j+1)
= (Partial_Sums f).(m,j+1)
proof
let n be Nat;
defpred P3[Nat] means
(Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)).($1,j+1)
= (Partial_Sums f).($1,j+1);
Z4: (Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)).(0,j+1)
= (Partial_Sums_in_cod2 f).(0,j+1) by DefRSM
.= (Partial_Sums_in_cod2 f).(0,j) + f.(0,j+1) by DefCSM
.= (Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)).(0,j)
+ f.(0,j+1) by DefRSM;
(Partial_Sums f).(0,j+1)
= (Partial_Sums f).(0,j) + (Partial_Sums_in_cod1 f).(0,j+1) by DefCSM
.= (Partial_Sums f).(0,j) + f.(0,j+1) by DefRSM
.= (Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)).(0,j) + f.(0,j+1)
by Z3; then
Z1: P3[0] by Z4;
Z2: for i be Nat st P3[i] holds P3[i+1]
proof
let i be Nat;
assume P3[i];
W1: (Partial_Sums f).(i,j) <> -infty
& (Partial_Sums_in_cod1 f).(i,j+1) <> -infty
& (Partial_Sums_in_cod2 f).(i+1,j) <> -infty & f.(i+1,j+1) <> -infty
& (Partial_Sums_in_cod1 f).(i+1,j+1) <> -infty
& (Partial_Sums_in_cod2 f).(i+1,j) <> -infty by MESFUNC5:def 5; then
W2: (Partial_Sums f).(i,j) + (Partial_Sums_in_cod1 f).(i,j+1) <> -infty
by XXREAL_3:17;
Z6: (Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)).(i,j)
= (Partial_Sums f).(i,j) by Z3;
(Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)).(i+1,j+1)
= (Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)).(i,j+1)
+ (Partial_Sums_in_cod2 f).(i+1,j+1) by DefRSM
.= (Partial_Sums f).(i,j) + (Partial_Sums_in_cod1 f).(i,j+1)
+ (Partial_Sums_in_cod2 f).(i+1,j+1) by Z6,Th47
.= (Partial_Sums f).(i,j) + (Partial_Sums_in_cod1 f).(i,j+1)
+ ( (Partial_Sums_in_cod2 f).(i+1,j) + f.(i+1,j+1) ) by DefCSM
.= (Partial_Sums f).(i,j) + (Partial_Sums_in_cod1 f).(i,j+1)
+ f.(i+1,j+1) + (Partial_Sums_in_cod2 f).(i+1,j) by W1,W2,XXREAL_3:29
.= (Partial_Sums f).(i,j) + ( (Partial_Sums_in_cod1(f)).(i,j+1)
+ f.(i+1,j+1) ) + (Partial_Sums_in_cod2(f)).(i+1,j) by W1,XXREAL_3:29
.= (Partial_Sums f).(i,j) + (Partial_Sums_in_cod1 f).(i+1,j+1)
+ (Partial_Sums_in_cod2 f).(i+1,j) by DefRSM
.= (Partial_Sums f).(i,j) + (Partial_Sums_in_cod2 f).(i+1,j)
+ (Partial_Sums_in_cod1 f).(i+1,j+1) by W1,XXREAL_3:29
.= (Partial_Sums f).(i+1,j) + (Partial_Sums_in_cod1 f).(i+1,j+1)
by Th47;
hence thesis by DefCSM;
end;
for n be Nat holds P3[n] from NAT_1:sch 2(Z1,Z2);
hence thesis;
end;
hence P1[j+1];
end;
for m be Nat holds P1[m] from NAT_1:sch 2(X1,X2);
hence thesis;
end;
Lm8:
for f be without-infty Function of [:NAT,NAT:],ExtREAL holds
Partial_Sums f = Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)
proof
let f be without-infty Function of [:NAT,NAT:],ExtREAL;
now let x be Element of [:NAT,NAT:];
consider n,m be object such that
A1: n in NAT & m in NAT & x = [n,m] by ZFMISC_1:def 2;
reconsider n1=n,m1=m as Nat by A1;
(Partial_Sums f).(n1,m1)
= (Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)).(n1,m1) by Lm7;
hence (Partial_Sums f).x
= (Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)).x by A1;
end;
hence thesis by FUNCT_2:63;
end;
Lm9:
for f be without+infty Function of [:NAT,NAT:],ExtREAL holds
Partial_Sums f = Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)
proof
let f be without+infty Function of [:NAT,NAT:],ExtREAL;
reconsider g = -f as without-infty Function of [:NAT,NAT:],ExtREAL;
A1:Partial_Sums f = Partial_Sums (-g) by Th2
.= Partial_Sums_in_cod2(-(Partial_Sums_in_cod1 g)) by Th42
.= -(Partial_Sums g) by Th42;
Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)
= Partial_Sums_in_cod1(Partial_Sums_in_cod2 (-g)) by Th2
.= Partial_Sums_in_cod1(-(Partial_Sums_in_cod2 g)) by Th42
.= -(Partial_Sums_in_cod1(Partial_Sums_in_cod2 g)) by Th42;
hence thesis by A1,Lm8;
end;
theorem
for f be Function of [:NAT,NAT:],ExtREAL st
f is without-infty or f is without+infty holds
Partial_Sums f = Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)
by Lm8,Lm9;
theorem
for f1,f2 be without-infty Function of [:NAT,NAT:],ExtREAL holds
Partial_Sums(f1 + f2) = Partial_Sums f1 + Partial_Sums f2
proof
let f1,f2 be without-infty Function of [:NAT,NAT:],ExtREAL;
Partial_Sums(f1+f2)
= Partial_Sums_in_cod2(Partial_Sums_in_cod1 f1 +Partial_Sums_in_cod1 f2)
by Th44;
hence thesis by Th44;
end;
theorem
for f1,f2 be without+infty Function of [:NAT,NAT:],ExtREAL holds
Partial_Sums(f1 + f2) = Partial_Sums f1 + Partial_Sums f2
proof
let f1,f2 be without+infty Function of [:NAT,NAT:],ExtREAL;
Partial_Sums(f1+f2)
= Partial_Sums_in_cod2(Partial_Sums_in_cod1 f1 +Partial_Sums_in_cod1 f2)
by Th45;
hence thesis by Th45;
end;
theorem
for f1 be without-infty Function of [:NAT,NAT:],ExtREAL,
f2 be without+infty Function of [:NAT,NAT:],ExtREAL holds
Partial_Sums(f1 - f2) = Partial_Sums f1 - Partial_Sums f2
& Partial_Sums(f2 - f1) = Partial_Sums f2 - Partial_Sums f1
proof
let f1 be without-infty Function of [:NAT,NAT:],ExtREAL,
f2 be without+infty Function of [:NAT,NAT:],ExtREAL;
Partial_Sums(f1-f2)
= Partial_Sums_in_cod2(Partial_Sums_in_cod1 f1 - Partial_Sums_in_cod1 f2)
by Th46;
hence Partial_Sums(f1-f2) = Partial_Sums f1 - Partial_Sums f2 by Th46;
Partial_Sums(f2-f1)
= Partial_Sums_in_cod2(Partial_Sums_in_cod1 f2 - Partial_Sums_in_cod1 f1)
by Th46;
hence Partial_Sums(f2-f1) = Partial_Sums f2 - Partial_Sums f1 by Th46;
end;
theorem
for f be Function of [:NAT,NAT:],ExtREAL,
k be Element of NAT holds
ProjMap2(Partial_Sums_in_cod1 f,k) = Partial_Sums(ProjMap2(f,k)) &
ProjMap1(Partial_Sums_in_cod2 f,k) = Partial_Sums(ProjMap1(f,k))
proof
let f be Function of [:NAT,NAT:],ExtREAL, k be Element of NAT;
now let n be Element of NAT;
ProjMap2(Partial_Sums_in_cod1 f,k).n
= (Partial_Sums_in_cod1 f).(n,k) by MESFUNC9:def 7;
hence ProjMap2(Partial_Sums_in_cod1 f,k).n
= Partial_Sums(ProjMap2(f,k)).n by Th43;
end;
hence ProjMap2(Partial_Sums_in_cod1 f,k) = Partial_Sums(ProjMap2(f,k))
by FUNCT_2:def 8;
now let n be Element of NAT;
ProjMap1(Partial_Sums_in_cod2 f,k).n
= (Partial_Sums_in_cod2 f).(k,n) by MESFUNC9:def 6;
hence ProjMap1(Partial_Sums_in_cod2 f,k).n
= Partial_Sums(ProjMap1(f,k)).n by Th43;
end;
hence ProjMap1(Partial_Sums_in_cod2 f,k) = Partial_Sums(ProjMap1(f,k))
by FUNCT_2:def 8;
end;
theorem Th54:
for f be Function of [:NAT,NAT:],ExtREAL st
f is without-infty or f is without+infty holds
ProjMap1(Partial_Sums f,0) = ProjMap1(Partial_Sums_in_cod2 f,0)
& ProjMap2(Partial_Sums f,0) = ProjMap2(Partial_Sums_in_cod1 f,0)
proof
let f be Function of [:NAT,NAT:],ExtREAL;
assume A0: f is without-infty or f is without+infty;
A1:now let m be Element of NAT;
ProjMap1(Partial_Sums f,0).m
= (Partial_Sums f).(0,m) by MESFUNC9:def 6
.= (Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)).(0,m)
by A0,Lm8,Lm9
.= (Partial_Sums_in_cod2 f).(0,m) by DefRSM;
hence ProjMap1(Partial_Sums f,0).m
= ProjMap1(Partial_Sums_in_cod2 f,0).m by MESFUNC9:def 6;
end;
now let n be Element of NAT;
ProjMap2(Partial_Sums f,0).n
= (Partial_Sums f).(n,0) by MESFUNC9:def 7
.= (Partial_Sums_in_cod1 f).(n,0) by DefCSM;
hence ProjMap2(Partial_Sums f,0).n
= ProjMap2(Partial_Sums_in_cod1 f,0).n by MESFUNC9:def 7;
end;
hence thesis by A1,FUNCT_2:63;
end;
theorem
for C,D be non empty set,
F1,F2 be without-infty Function of [:C,D:],ExtREAL,
c be Element of C holds
ProjMap1(F1+F2,c) = ProjMap1(F1,c) + ProjMap1(F2,c)
proof
let C,D be non empty set;
let F1,F2 be without-infty Function of [:C,D:],ExtREAL;
let c be Element of C;
A2:dom ProjMap1(F1+F2,c) = D & dom ProjMap1(F1,c) = D & dom ProjMap1(F2,c) = D
by FUNCT_2:def 1;
{-infty} misses rng ProjMap1(F1,c) & {-infty} misses rng ProjMap1(F2,c)
by ZFMISC_1:50,MESFUNC5:def 3; then
ProjMap1(F1,c)"{-infty} = {} & ProjMap1(F2,c)"{-infty} = {}
by RELAT_1:138; then
dom ProjMap1(F1+F2,c) = (dom ProjMap1(F1,c) /\ dom ProjMap1(F2,c))
\ ((ProjMap1(F1,c)"{-infty} /\ ProjMap1(F2,c)"{+infty})
\/ (ProjMap1(F1,c)"{+infty} /\ ProjMap1(F2,c)"{-infty})) by A2; then
A5:dom ProjMap1(F1+F2,c) = dom (ProjMap1(F1,c) + ProjMap1(F2,c))
by MESFUNC1:def 3;
for d be object st d in dom ProjMap1(F1+F2,c) holds
ProjMap1(F1+F2,c).d = (ProjMap1(F1,c) + ProjMap1(F2,c)).d
proof
let d be object;
assume A3: d in dom ProjMap1(F1+F2,c); then
A4: ProjMap1(F1+F2,c).d = (F1+F2).(c,d) & ProjMap1(F1,c).d = F1.(c,d)
& ProjMap1(F2,c).d = F2.(c,d) by MESFUNC9:def 6;
reconsider d1=d as Element of D by A3;
[c,d] in [:C,D:] by A3,ZFMISC_1:def 2; then
ProjMap1(F1+F2,c).d = ProjMap1(F1,c).d + ProjMap1(F2,c).d by A4,Th7;
hence thesis by A3,A5,MESFUNC1:def 3;
end;
hence ProjMap1(F1+F2,c) = ProjMap1(F1,c) + ProjMap1(F2,c) by A5,FUNCT_1:2;
end;
theorem
for C,D be non empty set,
F1,F2 be without-infty Function of [:C,D:],ExtREAL,
d be Element of D holds
ProjMap2(F1+F2,d) = ProjMap2(F1,d) + ProjMap2(F2,d)
proof
let C,D be non empty set;
let F1,F2 be without-infty Function of [:C,D:],ExtREAL;
let d be Element of D;
A2:dom ProjMap2(F1+F2,d) = C & dom ProjMap2(F1,d) = C & dom ProjMap2(F2,d) = C
by FUNCT_2:def 1;
{-infty} misses rng ProjMap2(F1,d) & {-infty} misses rng ProjMap2(F2,d)
by ZFMISC_1:50,MESFUNC5:def 3; then
ProjMap2(F1,d)"{-infty} = {} & ProjMap2(F2,d)"{-infty} = {}
by RELAT_1:138; then
dom ProjMap2(F1+F2,d) = (dom ProjMap2(F1,d) /\ dom ProjMap2(F2,d))
\ ((ProjMap2(F1,d)"{-infty} /\ ProjMap2(F2,d)"{+infty})
\/ (ProjMap2(F1,d)"{+infty} /\ ProjMap2(F2,d)"{-infty})) by A2; then
A5:dom ProjMap2(F1+F2,d) = dom (ProjMap2(F1,d) + ProjMap2(F2,d))
by MESFUNC1:def 3;
for c be object st c in dom ProjMap2(F1+F2,d) holds
ProjMap2(F1+F2,d).c = (ProjMap2(F1,d) + ProjMap2(F2,d)).c
proof
let c be object;
assume A3: c in dom ProjMap2(F1+F2,d); then
A4: ProjMap2(F1+F2,d).c = (F1+F2).(c,d) & ProjMap2(F1,d).c = F1.(c,d)
& ProjMap2(F2,d).c = F2.(c,d) by MESFUNC9:def 7;
reconsider c1=c as Element of C by A3;
[c,d] in [:C,D:] by A3,ZFMISC_1:def 2; then
ProjMap2(F1+F2,d).c = ProjMap2(F1,d).c + ProjMap2(F2,d).c by A4,Th7;
hence thesis by A3,A5,MESFUNC1:def 3;
end;
hence ProjMap2(F1+F2,d) = ProjMap2(F1,d) + ProjMap2(F2,d) by A5,FUNCT_1:2;
end;
theorem
for C,D be non empty set,
F1,F2 be without+infty Function of [:C,D:],ExtREAL,
c be Element of C holds
ProjMap1(F1+F2,c) = ProjMap1(F1,c) + ProjMap1(F2,c)
proof
let C,D be non empty set;
let F1,F2 be without+infty Function of [:C,D:],ExtREAL;
let c be Element of C;
A2:dom ProjMap1(F1+F2,c) = D & dom ProjMap1(F1,c) = D & dom ProjMap1(F2,c) = D
by FUNCT_2:def 1;
{+infty} misses rng ProjMap1(F1,c) & {+infty} misses rng ProjMap1(F2,c)
by ZFMISC_1:50,MESFUNC5:def 4; then
ProjMap1(F1,c)"{+infty} = {} & ProjMap1(F2,c)"{+infty} = {}
by RELAT_1:138; then
dom ProjMap1(F1+F2,c) = (dom ProjMap1(F1,c) /\ dom ProjMap1(F2,c))
\ ((ProjMap1(F1,c)"{-infty} /\ ProjMap1(F2,c)"{+infty})
\/ (ProjMap1(F1,c)"{+infty} /\ ProjMap1(F2,c)"{-infty})) by A2; then
A5:dom ProjMap1(F1+F2,c) = dom (ProjMap1(F1,c) + ProjMap1(F2,c))
by MESFUNC1:def 3;
for d be object st d in dom ProjMap1(F1+F2,c) holds
ProjMap1(F1+F2,c).d = (ProjMap1(F1,c) + ProjMap1(F2,c)).d
proof
let d be object;
assume A3: d in dom ProjMap1(F1+F2,c); then
A4: ProjMap1(F1+F2,c).d = (F1+F2).(c,d) & ProjMap1(F1,c).d = F1.(c,d)
& ProjMap1(F2,c).d = F2.(c,d) by MESFUNC9:def 6;
reconsider d1=d as Element of D by A3;
[c,d] in [:C,D:] by A3,ZFMISC_1:def 2; then
ProjMap1(F1+F2,c).d = ProjMap1(F1,c).d + ProjMap1(F2,c).d by A4,Th7;
hence thesis by A3,A5,MESFUNC1:def 3;
end;
hence ProjMap1(F1+F2,c) = ProjMap1(F1,c) + ProjMap1(F2,c) by A5,FUNCT_1:2;
end;
theorem
for C,D be non empty set,
F1,F2 be without+infty Function of [:C,D:],ExtREAL,
d be Element of D holds
ProjMap2(F1+F2,d) = ProjMap2(F1,d) + ProjMap2(F2,d)
proof
let C,D be non empty set;
let F1,F2 be without+infty Function of [:C,D:],ExtREAL;
let d be Element of D;
A2:dom ProjMap2(F1+F2,d) = C & dom ProjMap2(F1,d) = C & dom ProjMap2(F2,d) = C
by FUNCT_2:def 1;
{+infty} misses rng ProjMap2(F1,d) & {+infty} misses rng ProjMap2(F2,d)
by ZFMISC_1:50,MESFUNC5:def 4; then
ProjMap2(F1,d)"{+infty} = {} & ProjMap2(F2,d)"{+infty} = {}
by RELAT_1:138; then
dom ProjMap2(F1+F2,d) = (dom ProjMap2(F1,d) /\ dom ProjMap2(F2,d))
\ ((ProjMap2(F1,d)"{-infty} /\ ProjMap2(F2,d)"{+infty})
\/ (ProjMap2(F1,d)"{+infty} /\ ProjMap2(F2,d)"{-infty})) by A2; then
A5:dom ProjMap2(F1+F2,d) = dom (ProjMap2(F1,d) + ProjMap2(F2,d))
by MESFUNC1:def 3;
for c be object st c in dom ProjMap2(F1+F2,d) holds
ProjMap2(F1+F2,d).c = (ProjMap2(F1,d) + ProjMap2(F2,d)).c
proof
let c be object;
assume A3: c in dom ProjMap2(F1+F2,d); then
A4: ProjMap2(F1+F2,d).c = (F1+F2).(c,d) & ProjMap2(F1,d).c = F1.(c,d)
& ProjMap2(F2,d).c = F2.(c,d) by MESFUNC9:def 7;
reconsider c1=c as Element of C by A3;
[c,d] in [:C,D:] by A3,ZFMISC_1:def 2; then
ProjMap2(F1+F2,d).c = ProjMap2(F1,d).c + ProjMap2(F2,d).c by A4,Th7;
hence thesis by A3,A5,MESFUNC1:def 3;
end;
hence ProjMap2(F1+F2,d) = ProjMap2(F1,d) + ProjMap2(F2,d) by A5,FUNCT_1:2;
end;
theorem
for C,D be non empty set,
F1 be without-infty Function of [:C,D:],ExtREAL,
F2 be without+infty Function of [:C,D:],ExtREAL,
c be Element of C holds
ProjMap1(F1-F2,c) = ProjMap1(F1,c) - ProjMap1(F2,c) &
ProjMap1(F2-F1,c) = ProjMap1(F2,c) - ProjMap1(F1,c)
proof
let C,D be non empty set;
let F1 be without-infty Function of [:C,D:],ExtREAL;
let F2 be without+infty Function of [:C,D:],ExtREAL;
let c be Element of C;
A2:dom ProjMap1(F1-F2,c) = D & dom ProjMap1(F2-F1,c) = D &
dom ProjMap1(F1,c) = D & dom ProjMap1(F2,c) = D by FUNCT_2:def 1;
{-infty} misses rng ProjMap1(F1,c) & {+infty} misses rng ProjMap1(F2,c)
by ZFMISC_1:50,MESFUNC5:def 3,def 4; then
B1:ProjMap1(F1,c)"{-infty} = {} & ProjMap1(F2,c)"{+infty} = {}
by RELAT_1:138; then
dom ProjMap1(F1-F2,c) = (dom ProjMap1(F1,c) /\ dom ProjMap1(F2,c))
\ ((ProjMap1(F1,c)"{-infty} /\ ProjMap1(F2,c)"{-infty})
\/ (ProjMap1(F1,c)"{+infty} /\ ProjMap1(F2,c)"{+infty})) by A2; then
A5:dom ProjMap1(F1-F2,c) = dom (ProjMap1(F1,c) - ProjMap1(F2,c))
by MESFUNC1:def 4;
dom ProjMap1(F2-F1,c) = (dom ProjMap1(F2,c) /\ dom ProjMap1(F1,c))
\ ((ProjMap1(F2,c)"{+infty} /\ ProjMap1(F1,c)"{+infty})
\/ (ProjMap1(F2,c)"{-infty} /\ ProjMap1(F1,c)"{-infty})) by A2,B1; then
A6:dom ProjMap1(F2-F1,c) = dom (ProjMap1(F2,c) - ProjMap1(F1,c))
by MESFUNC1:def 4;
for d be object st d in dom ProjMap1(F1-F2,c) holds
ProjMap1(F1-F2,c).d = (ProjMap1(F1,c) - ProjMap1(F2,c)).d
proof
let d be object;
assume A3: d in dom ProjMap1(F1-F2,c); then
A4: ProjMap1(F1-F2,c).d = (F1-F2).(c,d) & ProjMap1(F1,c).d = F1.(c,d)
& ProjMap1(F2,c).d = F2.(c,d) by MESFUNC9:def 6;
reconsider d1=d as Element of D by A3;
[c,d] in [:C,D:] by A3,ZFMISC_1:def 2; then
ProjMap1(F1-F2,c).d = ProjMap1(F1,c).d - ProjMap1(F2,c).d by A4,Th7;
hence thesis by A3,A5,MESFUNC1:def 4;
end;
hence ProjMap1(F1-F2,c) = ProjMap1(F1,c) - ProjMap1(F2,c) by A5,FUNCT_1:2;
for d be object st d in dom ProjMap1(F2-F1,c) holds
ProjMap1(F2-F1,c).d = (ProjMap1(F2,c) - ProjMap1(F1,c)).d
proof
let d be object;
assume A3: d in dom ProjMap1(F2-F1,c); then
A4: ProjMap1(F2-F1,c).d = (F2-F1).(c,d) & ProjMap1(F1,c).d = F1.(c,d)
& ProjMap1(F2,c).d = F2.(c,d) by MESFUNC9:def 6;
reconsider d1=d as Element of D by A3;
[c,d] in [:C,D:] by A3,ZFMISC_1:def 2; then
ProjMap1(F2-F1,c).d = ProjMap1(F2,c).d - ProjMap1(F1,c).d by A4,Th7;
hence thesis by A3,A6,MESFUNC1:def 4;
end;
hence ProjMap1(F2-F1,c) = ProjMap1(F2,c) - ProjMap1(F1,c) by A6,FUNCT_1:2;
end;
theorem
for C,D be non empty set,
F1 be without-infty Function of [:C,D:],ExtREAL,
F2 be without+infty Function of [:C,D:],ExtREAL,
d be Element of D holds
ProjMap2(F1-F2,d) = ProjMap2(F1,d) - ProjMap2(F2,d) &
ProjMap2(F2-F1,d) = ProjMap2(F2,d) - ProjMap2(F1,d)
proof
let C,D be non empty set;
let F1 be without-infty Function of [:C,D:],ExtREAL;
let F2 be without+infty Function of [:C,D:],ExtREAL;
let d be Element of D;
A2:dom ProjMap2(F1-F2,d) = C & dom ProjMap2(F2-F1,d) = C &
dom ProjMap2(F1,d) = C & dom ProjMap2(F2,d) = C by FUNCT_2:def 1;
{-infty} misses rng ProjMap2(F1,d) & {+infty} misses rng ProjMap2(F2,d)
by ZFMISC_1:50,MESFUNC5:def 3,def 4; then
B1:ProjMap2(F1,d)"{-infty} = {} & ProjMap2(F2,d)"{+infty} = {}
by RELAT_1:138; then
dom ProjMap2(F1-F2,d) = (dom ProjMap2(F1,d) /\ dom ProjMap2(F2,d))
\ ((ProjMap2(F1,d)"{-infty} /\ ProjMap2(F2,d)"{-infty})
\/ (ProjMap2(F1,d)"{+infty} /\ ProjMap2(F2,d)"{+infty})) by A2; then
A5:dom ProjMap2(F1-F2,d) = dom (ProjMap2(F1,d) - ProjMap2(F2,d))
by MESFUNC1:def 4;
dom ProjMap2(F2-F1,d) = (dom ProjMap2(F2,d) /\ dom ProjMap2(F1,d))
\ ((ProjMap2(F2,d)"{+infty} /\ ProjMap2(F1,d)"{+infty})
\/ (ProjMap2(F2,d)"{-infty} /\ ProjMap2(F1,d)"{-infty})) by A2,B1; then
A6:dom ProjMap2(F2-F1,d) = dom (ProjMap2(F2,d) - ProjMap2(F1,d))
by MESFUNC1:def 4;
for c be object st c in dom ProjMap2(F1-F2,d) holds
ProjMap2(F1-F2,d).c = (ProjMap2(F1,d) - ProjMap2(F2,d)).c
proof
let c be object;
assume A3: c in dom ProjMap2(F1-F2,d); then
A4: ProjMap2(F1-F2,d).c = (F1-F2).(c,d) & ProjMap2(F1,d).c = F1.(c,d)
& ProjMap2(F2,d).c = F2.(c,d) by MESFUNC9:def 7;
reconsider c1=c as Element of C by A3;
[c,d] in [:C,D:] by A3,ZFMISC_1:def 2; then
ProjMap2(F1-F2,d).c = ProjMap2(F1,d).c - ProjMap2(F2,d).c by A4,Th7;
hence thesis by A3,A5,MESFUNC1:def 4;
end;
hence ProjMap2(F1-F2,d) = ProjMap2(F1,d) - ProjMap2(F2,d) by A5,FUNCT_1:2;
for c be object st c in dom ProjMap2(F2-F1,d) holds
ProjMap2(F2-F1,d).c = (ProjMap2(F2,d) - ProjMap2(F1,d)).c
proof
let c be object;
assume A3: c in dom ProjMap2(F2-F1,d); then
A4: ProjMap2(F2-F1,d).c = (F2-F1).(c,d) & ProjMap2(F1,d).c = F1.(c,d)
& ProjMap2(F2,d).c = F2.(c,d) by MESFUNC9:def 7;
reconsider c1=c as Element of C by A3;
[c,d] in [:C,D:] by A3,ZFMISC_1:def 2; then
ProjMap2(F2-F1,d).c = ProjMap2(F2,d).c - ProjMap2(F1,d).c by A4,Th7;
hence thesis by A3,A6,MESFUNC1:def 4;
end;
hence ProjMap2(F2-F1,d) = ProjMap2(F2,d) - ProjMap2(F1,d) by A6,FUNCT_1:2;
end;
begin :: Nonnegative extended real valued double sequences
theorem
for seq be nonnegative ExtREAL_sequence
st not Partial_Sums seq is convergent_to_+infty
holds for n be Nat holds seq.n is Real
proof
let seq be nonnegative ExtREAL_sequence;
assume A2:not Partial_Sums seq is convergent_to_+infty;
given N be Nat such that
A3: not seq.N is Real;
not seq.N in REAL by A3; then
A4:seq.N = +infty or seq.N = -infty by XXREAL_0:14;
A6:Partial_Sums seq is non-decreasing by MESFUNC9:16;
now let g be Real;
assume 0 < g;
take N;
hereby let m be Nat;
assume A7: N<=m;
per cases;
suppose N = 0; then
(Partial_Sums seq).N = seq.N by MESFUNC9:def 1; then
A9: g <= (Partial_Sums seq).N by A4,SUPINF_2:51,XXREAL_0:3;
(Partial_Sums seq).N <= (Partial_Sums seq).m
by A7,MESFUNC9:16,RINFSUP2:7;
hence g <= (Partial_Sums seq).m by A9,XXREAL_0:2;
end;
suppose N <> 0; then
consider N1 be Nat such that
A11: N = N1 + 1 by NAT_1:6;
A12: (Partial_Sums seq).N1 >= 0 by SUPINF_2:51;
(Partial_Sums seq).N
= (Partial_Sums seq).N1 + seq.N by A11,MESFUNC9:def 1
.= +infty by A4,SUPINF_2:51,XXREAL_0:4,A12,XXREAL_3:39; then
(Partial_Sums seq).m = +infty by A6,A7,RINFSUP2:7,XXREAL_0:4;
hence g <= (Partial_Sums seq).m by XXREAL_0:3;
end;
end;
end;
hence contradiction by A2,MESFUNC5:def 9;
end;
theorem Th62:
for seq be nonnegative ExtREAL_sequence st seq is non-decreasing holds
seq is convergent_to_+infty or seq is convergent_to_finite_number
proof
let seq be nonnegative ExtREAL_sequence;
assume A1: seq is non-decreasing;
now assume seq is convergent_to_-infty; then
consider N be Nat such that
A4: for n be Nat st N<=n holds seq.n <= -1 by MESFUNC5:def 10;
seq.N <= -1 & seq.N >= 0 by SUPINF_2:51,A4;
hence contradiction;
end;
hence thesis by A1,RINFSUP2:37,MESFUNC5:def 11;
end;
Lm10:
for f be Function of [:NAT,NAT:],ExtREAL, n be Element of NAT
st f is nonnegative
holds ProjMap1(f,n) is nonnegative & ProjMap2(f,n) is nonnegative
proof
let f be Function of [:NAT,NAT:],ExtREAL, n be Element of NAT;
assume A1: f is nonnegative;
now let m be object;
assume m in dom(ProjMap1(f,n)); then
reconsider m1=m as Element of NAT;
(ProjMap1(f,n)).m1 = f.(n,m1) by MESFUNC9:def 6;
hence (ProjMap1(f,n)).m >= 0 by A1,SUPINF_2:51;
end;
hence ProjMap1(f,n) is nonnegative by SUPINF_2:52;
now let m be object;
assume m in dom(ProjMap2(f,n)); then
reconsider m1=m as Element of NAT;
(ProjMap2(f,n)).m1 = f.(m1,n) by MESFUNC9:def 7;
hence (ProjMap2(f,n)).m >= 0 by A1,SUPINF_2:51;
end;
hence ProjMap2(f,n) is nonnegative by SUPINF_2:52;
end;
registration
let f be nonnegative Function of [:NAT,NAT:],ExtREAL, n be Element of NAT;
cluster ProjMap1(f,n) -> nonnegative;
correctness by Lm10;
cluster ProjMap2(f,n) -> nonnegative;
correctness by Lm10;
end;
theorem Th63:
for f be nonnegative Function of [:NAT,NAT:],ExtREAL, m be Element of NAT
holds ProjMap1(Partial_Sums_in_cod2 f,m) is non-decreasing
proof
let f be nonnegative Function of [:NAT,NAT:],ExtREAL,
m be Element of NAT;
set PS = ProjMap1(Partial_Sums_in_cod2 f,m);
for n,j be Nat st j <= n holds PS.j <= PS.n
proof
let n,j be Nat;
defpred Q[Nat] means PS.j <= PS.$1;
A6: for k be Nat holds PS.k <= PS.(k+1)
proof
let k be Nat;
reconsider k1=k as Element of NAT by ORDINAL1:def 12;
PS.(k+1) = (Partial_Sums_in_cod2 f).(m,k+1) by MESFUNC9:def 6
.= (Partial_Sums_in_cod2 f).(m,k1) + f.(m,k+1) by DefCSM
.= PS.k + f.(m,k+1) by MESFUNC9:def 6;
hence thesis by SUPINF_2:51,XXREAL_3:39;
end;
A8: for k be Nat st k >= j & (for l be Nat st l >= j & l < k holds Q[l])
holds Q[k]
proof
let k be Nat;
assume that
A9: k >= j and
A10: for l be Nat st l >= j & l < k holds Q[l];
now assume k > j; then
A11: k >= j + 1 by NAT_1:13;
per cases by A11,XXREAL_0:1;
suppose k = j + 1;
hence thesis by A6;
end;
suppose
A12: k > j + 1;
then reconsider l = k-1 as Element of NAT by NAT_1:20;
k < k+1 by NAT_1:13; then
A13: k > l by XREAL_1:19;
k = l+1; then
A14: PS.l <= PS.k by A6;
PS.j <= PS.l by A10,A13,A12,XREAL_1:19;
hence thesis by A14,XXREAL_0:2;
end;
end;
hence thesis by A9,XXREAL_0:1;
end;
A15: for k be Nat st k >= j holds Q[k] from NAT_1:sch 9(A8);
assume j <= n;
hence thesis by A15;
end;
hence thesis by RINFSUP2:7;
end;
theorem Th64:
for f be nonnegative Function of [:NAT,NAT:],ExtREAL, n be Element of NAT
holds ProjMap2(Partial_Sums_in_cod1 f,n) is non-decreasing
proof
let f be nonnegative without-infty Function of [:NAT,NAT:],ExtREAL,
n be Element of NAT;
A1:ProjMap1(Partial_Sums_in_cod2 f@,n) is non-decreasing by Th63;
Partial_Sums_in_cod2 f@ = (Partial_Sums_in_cod1 f)@ by Th40;
hence ProjMap2(Partial_Sums_in_cod1 f,n) is non-decreasing by A1,Th33;
end;
registration
let f be nonnegative Function of [:NAT,NAT:],ExtREAL,
m be Element of NAT;
cluster ProjMap1(Partial_Sums_in_cod2 f,m) -> non-decreasing;
correctness by Th63;
cluster ProjMap2(Partial_Sums_in_cod1 f,m) -> non-decreasing;
correctness by Th64;
end;
theorem Th65:
for f be nonnegative Function of [:NAT,NAT:],ExtREAL holds
( f is convergent_in_cod1 implies lim_in_cod1 f is nonnegative )
& ( f is convergent_in_cod2 implies lim_in_cod2 f is nonnegative )
proof
let f be nonnegative Function of [:NAT,NAT:],ExtREAL;
hereby assume A2:f is convergent_in_cod1;
now let n be object;
assume n in dom(lim_in_cod1 f); then
reconsider n1=n as Element of NAT;
A4: (lim_in_cod1 f).n = lim ProjMap2(f,n1) by D1DEF5;
for k be Nat holds 0 <= ProjMap2(f,n1).k by SUPINF_2:51;
hence (lim_in_cod1 f).n >= 0 by A2,A4,MESFUNC9:10;
end;
hence lim_in_cod1 f is nonnegative by SUPINF_2:52;
end;
assume A2:f is convergent_in_cod2;
now let n be object;
assume n in dom(lim_in_cod2 f); then
reconsider n1=n as Element of NAT;
A4: (lim_in_cod2 f).n = lim ProjMap1(f,n1) by D1DEF6;
for k be Nat holds 0 <= ProjMap1(f,n1).k by SUPINF_2:51;
hence (lim_in_cod2 f).n >= 0 by A2,A4,MESFUNC9:10;
end;
hence thesis by SUPINF_2:52;
end;
theorem
for f be nonnegative Function of [:NAT,NAT:],ExtREAL
holds Partial_Sums_in_cod1 f is convergent_in_cod1
& Partial_Sums_in_cod2 f is convergent_in_cod2 by RINFSUP2:37;
theorem
for f be nonnegative Function of [:NAT,NAT:],ExtREAL,
m be Element of NAT
st not ProjMap2(Partial_Sums_in_cod1 f,m) is convergent_to_+infty
holds for n be Nat holds f.(n,m) is Real
proof
let f be nonnegative Function of [:NAT,NAT:],ExtREAL;
let m be Element of NAT;
assume
A2:not ProjMap2(Partial_Sums_in_cod1 f,m) is convergent_to_+infty;
given N be Nat such that
A3: not f.(N,m) is Real;
not f.(N,m) in REAL by A3; then
A4:f.(N,m) = +infty or f.(N,m) = -infty by XXREAL_0:14;
reconsider N1=N as Element of NAT by ORDINAL1:def 12;
now let g be Real;
assume 0 < g;
take N;
hereby let k be Nat;
assume A7: N<=k;
per cases;
suppose A8: N = 0;
ProjMap2(Partial_Sums_in_cod1 f,m).N
= (Partial_Sums_in_cod1 f).(N1,m) by MESFUNC9:def 7
.= f.(N,m) by A8,DefRSM; then
A9: g <= ProjMap2(Partial_Sums_in_cod1 f,m).N
by A4,SUPINF_2:51,XXREAL_0:3;
ProjMap2(Partial_Sums_in_cod1 f,m).N
<= ProjMap2(Partial_Sums_in_cod1 f,m).k by A7,RINFSUP2:7;
hence g <= ProjMap2(Partial_Sums_in_cod1 f,m).k by A9,XXREAL_0:2;
end;
suppose N <> 0; then
consider N2 be Nat such that
A11: N = N2 + 1 by NAT_1:6;
reconsider N3=N2 as Element of NAT by ORDINAL1:def 12;
A12: (Partial_Sums_in_cod1 f).(N3,m) >= 0 by SUPINF_2:51;
ProjMap2(Partial_Sums_in_cod1 f,m).N1
= (Partial_Sums_in_cod1 f).(N1,m) by MESFUNC9:def 7
.= (Partial_Sums_in_cod1 f).(N2,m) + f.(N1,m) by A11,DefRSM; then
ProjMap2(Partial_Sums_in_cod1 f,m).N1 = +infty
by A4,SUPINF_2:51,XXREAL_0:4,A12,XXREAL_3:39; then
ProjMap2(Partial_Sums_in_cod1 f,m).k = +infty
by XXREAL_0:4,A7,RINFSUP2:7;
hence g <= ProjMap2(Partial_Sums_in_cod1 f,m).k by XXREAL_0:3;
end;
end;
end;
hence contradiction by A2,MESFUNC5:def 9;
end;
theorem
for f be nonnegative Function of [:NAT,NAT:],ExtREAL,
m be Element of NAT
st not ProjMap1(Partial_Sums_in_cod2 f,m) is convergent_to_+infty
holds for n be Nat holds f.(m,n) is Real
proof
let f be nonnegative Function of [:NAT,NAT:],ExtREAL;
let m be Element of NAT;
assume
A2:not ProjMap1(Partial_Sums_in_cod2 f,m) is convergent_to_+infty;
given N be Nat such that
A3: not f.(m,N) is Real;
not f.(m,N) in REAL by A3; then
A4:f.(m,N) = +infty or f.(m,N) = -infty by XXREAL_0:14;
reconsider N1=N as Element of NAT by ORDINAL1:def 12;
now let g be Real;
assume 0 < g;
take N;
hereby let k be Nat;
assume A7: N<=k;
per cases;
suppose A8: N = 0;
ProjMap1(Partial_Sums_in_cod2 f,m).N
= (Partial_Sums_in_cod2 f).(m,N1) by MESFUNC9:def 6
.= f.(m,N) by A8,DefCSM; then
A9: g <= ProjMap1(Partial_Sums_in_cod2 f,m).N
by A4,SUPINF_2:51,XXREAL_0:3;
ProjMap1(Partial_Sums_in_cod2 f,m).N
<= ProjMap1(Partial_Sums_in_cod2 f,m).k by A7,RINFSUP2:7;
hence g <= ProjMap1(Partial_Sums_in_cod2 f,m).k by A9,XXREAL_0:2;
end;
suppose N <> 0; then
consider N2 be Nat such that
A11: N = N2 + 1 by NAT_1:6;
reconsider N3=N2 as Element of NAT by ORDINAL1:def 12;
A12: (Partial_Sums_in_cod2 f).(m,N3) >= 0 by SUPINF_2:51;
ProjMap1(Partial_Sums_in_cod2 f,m).N1
= (Partial_Sums_in_cod2 f).(m,N1) by MESFUNC9:def 6
.= (Partial_Sums_in_cod2 f).(m,N2) + f.(m,N1) by A11,DefCSM; then
ProjMap1(Partial_Sums_in_cod2 f,m).N1 = +infty
by A4,SUPINF_2:51,XXREAL_0:4,A12,XXREAL_3:39; then
ProjMap1(Partial_Sums_in_cod2 f,m).k = +infty
by XXREAL_0:4,A7,RINFSUP2:7;
hence g <= ProjMap1(Partial_Sums_in_cod2 f,m).k by XXREAL_0:3;
end;
end;
end;
hence contradiction by A2,MESFUNC5:def 9;
end;
theorem
for f be nonnegative Function of [:NAT,NAT:],ExtREAL, n,m be Nat
st (for i be Nat st i <= n holds f.(i,m) is Real)
holds (Partial_Sums_in_cod1 f).(n,m) < +infty
proof
let f be nonnegative Function of [:NAT,NAT:],ExtREAL, n,m be Nat;
assume
A2: for i be Nat st i<=n holds f.(i,m) is Real;
defpred P[Nat] means $1<=n implies
(Partial_Sums_in_cod1 f).($1,m) < +infty;
(Partial_Sums_in_cod1 f).(0,m) = f.(0,m) by DefRSM; then
(Partial_Sums_in_cod1 f).(0,m) is Real by A2; then
A4:P[0] by XXREAL_0:9,XREAL_0:def 1;
A5:for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A6: P[k];
now assume A7: k+1<=n; then
A8: f.(k+1,m) is Real & f.(k+1,m) >= 0 by A2,SUPINF_2:51;
(Partial_Sums_in_cod1 f).(k+1,m)
= (Partial_Sums_in_cod1 f).(k,m) + f.(k+1,m) by DefRSM;
hence (Partial_Sums_in_cod1 f).(k+1,m) < +infty
by A6,A7,A8,NAT_1:13,XXREAL_3:16,XXREAL_0:4;
end;
hence P[k+1];
end;
for k be Nat holds P[k] from NAT_1:sch 2(A4,A5);
hence thesis;
end;
theorem
for f be nonnegative Function of [:NAT,NAT:],ExtREAL, n,m be Nat
st (for i be Nat st i <= m holds f.(n,i) is Real)
holds (Partial_Sums_in_cod2 f).(n,m) < +infty
proof
let f be nonnegative Function of [:NAT,NAT:],ExtREAL, n,m be Nat;
assume
A2: for i be Nat st i<=m holds f.(n,i) is Real;
defpred P[Nat] means $1<=m implies
(Partial_Sums_in_cod2 f).(n,$1) < +infty;
(Partial_Sums_in_cod2 f).(n,0) = f.(n,0) by DefCSM; then
(Partial_Sums_in_cod2 f).(n,0) is Real by A2; then
A4:P[0] by XXREAL_0:9,XREAL_0:def 1;
A5:for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A6: P[k];
now assume A7: k+1<=m; then
A8: f.(n,k+1) is Real & f.(n,k+1) >= 0 by A2,SUPINF_2:51;
(Partial_Sums_in_cod2 f).(n,k+1)
= (Partial_Sums_in_cod2 f).(n,k) + f.(n,k+1) by DefCSM;
hence (Partial_Sums_in_cod2 f).(n,k+1) < +infty
by A6,A7,A8,NAT_1:13,XXREAL_3:16,XXREAL_0:4;
end;
hence P[k+1];
end;
for k be Nat holds P[k] from NAT_1:sch 2(A4,A5);
hence thesis;
end;
theorem
for f be without-infty Function of [:NAT,NAT:],ExtREAL holds
Partial_Sums f is convergent_in_cod1_to_-infty implies
ex m be Element of NAT st
ProjMap2(Partial_Sums_in_cod1 f,m) is convergent_to_-infty
proof
let f be without-infty Function of [:NAT,NAT:],ExtREAL;
assume
A1: Partial_Sums f is convergent_in_cod1_to_-infty;
A3:ProjMap2(Partial_Sums_in_cod2(Partial_Sums_in_cod1 f),0)
= ProjMap2(Partial_Sums f,0)
.= ProjMap2(Partial_Sums_in_cod1 f,0) by Th54;
assume for m be Element of NAT holds
not ProjMap2(Partial_Sums_in_cod1 f,m) is convergent_to_-infty;
hence contradiction by A1,A3;
end;
theorem Th72:
for f be nonnegative Function of [:NAT,NAT:],ExtREAL, m be Nat holds
(for k be Element of NAT st k<=m holds
not ProjMap1(Partial_Sums_in_cod2 f,k) is convergent_to_+infty)
iff
(for k be Element of NAT st k<=m holds
lim ProjMap1(Partial_Sums_in_cod2 f,k) < +infty)
proof
let f be nonnegative Function of [:NAT,NAT:],ExtREAL, m be Nat;
hereby assume
A1: for k be Element of NAT st k<=m holds
not ProjMap1(Partial_Sums_in_cod2 f,k) is convergent_to_+infty;
hereby let k be Element of NAT;
assume k<=m; then
not ProjMap1(Partial_Sums_in_cod2 f,k) is convergent_to_+infty
by A1; then
ProjMap1(Partial_Sums_in_cod2 f,k) is convergent_to_finite_number
by Th62; then
ex g be Real st
lim ProjMap1(Partial_Sums_in_cod2 f,k) = g
& for p be Real st 0 m or
not ProjMap1(Partial_Sums_in_cod2 f,k) is convergent_to_+infty;
defpred P[Nat] means $1 <= m implies
(Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2 f))).$1 <> +infty;
(Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2 f))).0
= (lim_in_cod2(Partial_Sums_in_cod2 f)).0 by MESFUNC9:def 1
.= lim ProjMap1(Partial_Sums_in_cod2 f,0) by D1DEF6; then
A5: P[0] by A3,Th72;
A6: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A7: P[k];
assume A8: k+1 <= m;
A10: (Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2 f))).(k+1)
= (Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2 f))).k
+ (lim_in_cod2(Partial_Sums_in_cod2 f)).(k+1) by MESFUNC9:def 1;
now assume (lim_in_cod2(Partial_Sums_in_cod2 f)).(k+1) = +infty; then
lim ProjMap1(Partial_Sums_in_cod2 f,k+1) = +infty by D1DEF6;
hence contradiction by A3,A8,Th72;
end;
hence (Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2 f))).(k+1)
<> +infty by A7,A8,NAT_1:13,A10,XXREAL_3:16;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A5,A6);
hence contradiction by A2;
end;
hence
ex k be Element of NAT st k <= m
& ProjMap1(Partial_Sums_in_cod2 f,k) is convergent_to_+infty;
end;
given k be Element of NAT such that
B1: k <= m
& ProjMap1(Partial_Sums_in_cod2 f,k) is convergent_to_+infty;
lim ProjMap1(Partial_Sums_in_cod2 f,k) = +infty by B1,MESFUNC9:7; then
B2:(lim_in_cod2(Partial_Sums_in_cod2 f)).k = +infty by D1DEF6;
B3:Partial_Sums_in_cod2 f is convergent_in_cod2 by RINFSUP2:37; then
(lim_in_cod2(Partial_Sums_in_cod2 f)) is nonnegative by Th65; then
B5:(Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2 f))).k
>= +infty by B2,Th4;
lim_in_cod2(Partial_Sums_in_cod2 f) is nonnegative by B3,Th65; then
(Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2 f))).k
<= (Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2 f))).m
by B1,RINFSUP2:7,MESFUNC9:16;
hence (Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2 f))).m = +infty
by B5,XXREAL_0:2,4;
end;
theorem
for f be nonnegative Function of [:NAT,NAT:],ExtREAL, m be Nat holds
(Partial_Sums(lim_in_cod1(Partial_Sums_in_cod1 f))).m = +infty
iff
ex k be Element of NAT
st k <= m & ProjMap2(Partial_Sums_in_cod1 f,k) is convergent_to_+infty
proof
let f be nonnegative Function of [:NAT,NAT:],ExtREAL, m be Nat;
hereby assume
A1: (Partial_Sums(lim_in_cod1(Partial_Sums_in_cod1 f))).m = +infty;
lim_in_cod1(Partial_Sums_in_cod1 f)
= lim_in_cod2((Partial_Sums_in_cod1 f)@) by Th38
.= lim_in_cod2(Partial_Sums_in_cod2 f@) by Th40; then
consider k be Element of NAT such that
A2: k <= m & ProjMap1(Partial_Sums_in_cod2 f@,k) is convergent_to_+infty
by A1,Th74;
ProjMap1(Partial_Sums_in_cod2 f@,k)
= ProjMap2((Partial_Sums_in_cod2 f@)@,k) by Th32
.= ProjMap2(Partial_Sums_in_cod1 (f@)@,k) by Th40
.= ProjMap2(Partial_Sums_in_cod1 f,k) by DBLSEQ_2:7;
hence ex k be Element of NAT
st k <= m & ProjMap2(Partial_Sums_in_cod1 f,k) is convergent_to_+infty
by A2;
end;
given k be Element of NAT such that
A3: k <= m & ProjMap2(Partial_Sums_in_cod1 f,k) is convergent_to_+infty;
A4:ProjMap2(Partial_Sums_in_cod1 f,k)
= ProjMap2(Partial_Sums_in_cod1 (f@)@,k) by DBLSEQ_2:7
.= ProjMap2((Partial_Sums_in_cod2 f@)@,k) by Th40
.= ProjMap1(Partial_Sums_in_cod2 f@,k) by Th32;
lim_in_cod1(Partial_Sums_in_cod1 f)
= lim_in_cod2((Partial_Sums_in_cod1 f)@) by Th38
.= lim_in_cod2(Partial_Sums_in_cod2 f@) by Th40;
hence (Partial_Sums(lim_in_cod1(Partial_Sums_in_cod1 f))).m = +infty
by A3,A4,Th74;
end;
theorem Th76:
for f be nonnegative Function of [:NAT,NAT:],ExtREAL, n,m be Nat holds
(Partial_Sums_in_cod1 f).(n,m) >= f.(n,m)
& (Partial_Sums_in_cod2 f).(n,m) >= f.(n,m)
proof
let f be nonnegative Function of [:NAT,NAT:],ExtREAL, n,m be Nat;
defpred P[Nat] means
$1 <= n implies (Partial_Sums_in_cod1 f).($1,m) >= f.($1,m);
A2:P[0] by DefRSM;
A5:for k be Nat st P[k] holds P[k+1]
proof
let k be Nat such that P[k];
assume k+1 <= n;
(Partial_Sums_in_cod1 f).(k+1,m)
= (Partial_Sums_in_cod1 f).(k,m) + f.(k+1,m) by DefRSM;
hence (Partial_Sums_in_cod1 f).(k+1,m) >= f.(k+1,m)
by SUPINF_2:51,XXREAL_3:39;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A2,A5);
hence (Partial_Sums_in_cod1 f).(n,m) >= f.(n,m);
defpred Q[Nat] means
$1 <= m implies (Partial_Sums_in_cod2 f).(n,$1) >= f.(n,$1);
A2:Q[0] by DefCSM;
A5:for k be Nat st Q[k] holds Q[k+1]
proof
let k be Nat such that Q[k];
assume k+1 <= m;
(Partial_Sums_in_cod2 f).(n,k+1)
= (Partial_Sums_in_cod2 f).(n,k) + f.(n,k+1) by DefCSM;
hence (Partial_Sums_in_cod2 f).(n,k+1) >= f.(n,k+1)
by SUPINF_2:51,XXREAL_3:39;
end;
for k be Nat holds Q[k] from NAT_1:sch 2(A2,A5);
hence (Partial_Sums_in_cod2 f).(n,m) >= f.(n,m);
end;
theorem Th77:
for f be nonnegative Function of [:NAT,NAT:],ExtREAL, m be Element of NAT
st (ex k be Element of NAT st k <= m
& ProjMap1(Partial_Sums_in_cod2 f,k) is convergent_to_+infty)
holds
ProjMap1(Partial_Sums_in_cod2(Partial_Sums_in_cod1 f),m)
is convergent_to_+infty
& lim(ProjMap1(Partial_Sums_in_cod2(Partial_Sums_in_cod1 f),m)) = +infty
proof
let f be nonnegative Function of [:NAT,NAT:],ExtREAL,
m be Element of NAT;
given k be Element of NAT such that
A2: k<=m & ProjMap1(Partial_Sums_in_cod2 f,k) is convergent_to_+infty;
A5: for g be Real st 0 < g
ex N be Nat st for n be Nat st N<=n holds
g <= ProjMap1(Partial_Sums_in_cod2(Partial_Sums_in_cod1 f),m).n
proof
let g be Real;
assume 0 = n+1; then
A17: k = n+1 by A16,XXREAL_0:1; then
A18: (Partial_Sums(lim_in_cod1 Partial_Sums_in_cod1 f)).k
= (Partial_Sums(lim_in_cod1 Partial_Sums_in_cod1 f)).n
+ (lim_in_cod1 Partial_Sums_in_cod1 f).(n+1) by MESFUNC9:def 1
.= lim ProjMap2(Partial_Sums_in_cod1(Partial_Sums_in_cod2 f),n1)
+ (lim_in_cod1 Partial_Sums_in_cod1 f).(n+1) by A15
.= lim ProjMap2(Partial_Sums f,n1)
+ (lim_in_cod1 Partial_Sums_in_cod1 f).(n+1) by Lm8
.= lim ProjMap2(Partial_Sums f,n1)
+ lim ProjMap2(Partial_Sums_in_cod1 f,k) by A17,D1DEF5;
consider Gn be Real such that
A19: lim ProjMap2(Partial_Sums f,n1) = Gn &
for p be Real st 0 = I1 & I >= I2 by XXREAL_0:25;
now let i be Nat;
reconsider i1 = i as Element of NAT by ORDINAL1:def 12;
assume I<=i; then
I1<=i & I2<=i by A27,XXREAL_0:2; then
|. ProjMap2(Partial_Sums f,n1).i - Gn .| < p/2
& |. ProjMap2(Partial_Sums_in_cod1 f,k).i - Gn1 .| < p/2
by A19,A20,A25,A26; then
A28: |. ProjMap2(Partial_Sums f,n1).i - Gn .|
+ |. ProjMap2(Partial_Sums_in_cod1 f,k).i - Gn1 .| < p/2+p/2
by XXREAL_3:64;
A29: ProjMap2(Partial_Sums f,k).i1
= (Partial_Sums f).(i,k) by MESFUNC9:def 7
.= (Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)).(i,k) by Lm8
.= (Partial_Sums_in_cod1 f).(i,k)
+ (Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)).(i,n)
by A17,Th47
.= (Partial_Sums f).(i,n) + (Partial_Sums_in_cod1 f).(i,k) by Lm8
.= ProjMap2(Partial_Sums f,n1).i1
+ (Partial_Sums_in_cod1 f).(i,k) by MESFUNC9:def 7
.= ProjMap2(Partial_Sums f,n1).i1
+ ProjMap2(Partial_Sums_in_cod1 f,k).i1 by MESFUNC9:def 7;
ProjMap2(Partial_Sums_in_cod1 f,k).i1 <> -infty by SUPINF_2:51; then
A30: ProjMap2(Partial_Sums_in_cod1 f,k).i1 - Gn1a <> -infty
by XXREAL_3:19; then
A31: (ProjMap2(Partial_Sums_in_cod1 f,k).i1 - Gn1a) + Gn1a <> -infty
by XXREAL_3:17;
ProjMap2(Partial_Sums f,n1).i1 >= 0 by SUPINF_2:51; then
A32: ProjMap2(Partial_Sums f,n1).i - Gna <> -infty by XXREAL_3:19;
ProjMap2(Partial_Sums f,n1).i
= ProjMap2(Partial_Sums f,n1).i - Gna + Gna
& ProjMap2(Partial_Sums_in_cod1 f,k).i
= ProjMap2(Partial_Sums_in_cod1 f,k).i - Gn1a + Gn1a
by XXREAL_3:22; then
ProjMap2(Partial_Sums f,k).i
= (ProjMap2(Partial_Sums f,n1).i - Gna)
+ (((ProjMap2(Partial_Sums_in_cod1 f,k).i - Gn1a) + Gn1a) + Gna)
by A29,A31,A32,XXREAL_3:29
.= (ProjMap2(Partial_Sums f,n1).i - Gna)
+ ( (ProjMap2(Partial_Sums_in_cod1 f,k).i - Gn1a) + (Gn1a + Gna) )
by XXREAL_3:29
.= (ProjMap2(Partial_Sums f,n1).i - Gna)
+ (ProjMap2(Partial_Sums_in_cod1 f,k).i - Gn1a) + (Gna + Gn1a)
by A30,A32,XXREAL_3:29; then
ProjMap2(Partial_Sums f,k).i - G
= (ProjMap2(Partial_Sums f,n1).i - Gna)
+ (ProjMap2(Partial_Sums_in_cod1 f,k).i - Gn1a)
by XXREAL_3:22; then
|. ProjMap2(Partial_Sums f,k).i - G .|
<= |. ProjMap2(Partial_Sums f,n1).i - Gna .|
+ |. ProjMap2(Partial_Sums_in_cod1 f,k).i - Gn1a .|
by EXTREAL1:24;
hence |. ProjMap2(Partial_Sums f,k).i - G .| < p by A28,XXREAL_0:2;
end;
hence thesis;
end;
hence (Partial_Sums(lim_in_cod1 Partial_Sums_in_cod1 f)).k
= lim ProjMap2(Partial_Sums_in_cod1(Partial_Sums_in_cod2 f),k)
by A18,A19,A20,A21,A22,MESFUNC5:def 12;
end;
end;
hence P[n+1];
end;
for n be Nat holds P[n] from NAT_1:sch 2(A13,A14);
hence thesis;
end;
theorem
for f be without-infty Function of [:NAT,NAT:],ExtREAL holds
Partial_Sums f is convergent_in_cod2_to_finite iff
Partial_Sums_in_cod2 f is convergent_in_cod2_to_finite
proof
let f be without-infty Function of [:NAT,NAT:],ExtREAL;
hereby assume Partial_Sums f is convergent_in_cod2_to_finite; then
(Partial_Sums_in_cod2(Partial_Sums_in_cod1 f))@
is convergent_in_cod1_to_finite by Th36; then
Partial_Sums_in_cod1(Partial_Sums_in_cod1 f)@
is convergent_in_cod1_to_finite by Th40; then
Partial_Sums_in_cod1(Partial_Sums_in_cod2 f@)
is convergent_in_cod1_to_finite by Th40; then
Partial_Sums (f@) is convergent_in_cod1_to_finite by Lm8; then
Partial_Sums_in_cod1 (f@) is convergent_in_cod1_to_finite
by Th79; then
(Partial_Sums_in_cod2 f)@ is convergent_in_cod1_to_finite by Th40;
hence Partial_Sums_in_cod2 f is convergent_in_cod2_to_finite by Th36;
end;
assume Partial_Sums_in_cod2 f is convergent_in_cod2_to_finite; then
(Partial_Sums_in_cod2 f)@ is convergent_in_cod1_to_finite by Th36; then
Partial_Sums_in_cod1 (f@) is convergent_in_cod1_to_finite by Th40; then
Partial_Sums (f@) is convergent_in_cod1_to_finite by Th79; then
Partial_Sums_in_cod1(Partial_Sums_in_cod2 f@)
is convergent_in_cod1_to_finite by Lm8; then
Partial_Sums_in_cod1(Partial_Sums_in_cod1 f)@
is convergent_in_cod1_to_finite by Th40; then
(Partial_Sums_in_cod2(Partial_Sums_in_cod1 f))@
is convergent_in_cod1_to_finite by Th40;
hence Partial_Sums f is convergent_in_cod2_to_finite by Th36;
end;
theorem
for f be nonnegative Function of [:NAT,NAT:],ExtREAL st
Partial_Sums f is convergent_in_cod2_to_finite
holds
for m be Element of NAT holds
(Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2 f))).m
= lim(ProjMap1(Partial_Sums_in_cod2(Partial_Sums_in_cod1 f),m))
proof
let f be nonnegative Function of [:NAT,NAT:],ExtREAL;
assume Partial_Sums f is convergent_in_cod2_to_finite; then
Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)
is convergent_in_cod2_to_finite by Lm8; then
(Partial_Sums_in_cod1(Partial_Sums_in_cod2 f))@
is convergent_in_cod1_to_finite by Th36; then
Partial_Sums_in_cod2(Partial_Sums_in_cod2 f)@
is convergent_in_cod1_to_finite by Th40; then
A1:Partial_Sums (f@) is convergent_in_cod1_to_finite by Th40;
hereby let m be Element of NAT;
lim_in_cod2(Partial_Sums_in_cod2 f)
= lim_in_cod1((Partial_Sums_in_cod2 f)@) by Th38
.= lim_in_cod1(Partial_Sums_in_cod1 (f@)) by Th40; then
(Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2 f))).m
= lim(ProjMap2(Partial_Sums_in_cod1(Partial_Sums_in_cod2 (f@)),m))
by A1,Th80
.= lim(ProjMap2(Partial_Sums_in_cod1(Partial_Sums_in_cod1 f)@,m)) by Th40
.= lim(ProjMap2((Partial_Sums_in_cod2(Partial_Sums_in_cod1 f))@,m))
by Th40;
hence (Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2 f))).m
= lim(ProjMap1(Partial_Sums_in_cod2(Partial_Sums_in_cod1 f),m)) by Th32;
end;
end;
:: Fatou's Lemma for Double Sequence
theorem Th83:
for f be nonnegative Function of [:NAT,NAT:],ExtREAL,
seq be ExtREAL_sequence st
(for m be Element of NAT holds seq.m = lim_inf ProjMap2(f,m))
holds Sum seq <= lim_inf lim_in_cod2(Partial_Sums_in_cod2 f)
proof
let f be nonnegative Function of [:NAT,NAT:],ExtREAL,
seq be ExtREAL_sequence;
assume
A1: for m be Element of NAT holds seq.m = lim_inf ProjMap2(f,m);
A2:for m be Element of NAT holds
for N,n be Element of NAT st n>=N holds
(inferior_realsequence ProjMap2(f,m)).N <= f.(n,m)
proof
let m be Element of NAT;
let N,n be Element of NAT;
assume n >= N; then
A4: (inferior_realsequence ProjMap2(f,m)).N
<= (inferior_realsequence ProjMap2(f,m)).n by RINFSUP2:7;
(inferior_realsequence ProjMap2(f,m)).n <= (ProjMap2(f,m)).n
by RINFSUP2:8; then
(inferior_realsequence ProjMap2(f,m)).n <= f.(n,m) by MESFUNC9:def 7;
hence (inferior_realsequence ProjMap2(f,m)).N <= f.(n,m)
by A4,XXREAL_0:2;
end;
deffunc F(Element of NAT) = inferior_realsequence ProjMap2(f,$1);
deffunc G(Element of NAT,Element of NAT)
= (inferior_realsequence ProjMap2(f,$2)).$1;
consider g be Function of [:NAT,NAT:],ExtREAL such that
A5: for n be Element of NAT for m be Element of NAT holds
g.(n,m) = G(n,m) from BINOP_1:sch 4;
now let z be object;
per cases;
suppose z in dom g; then
consider n,m be object such that
D1: n in NAT & m in NAT & z = [n,m] by ZFMISC_1:def 2;
reconsider n,m as Element of NAT by D1;
g.(n,m) = (inferior_realsequence ProjMap2(f,m)).n by A5; then
consider Y be non empty Subset of ExtREAL such that
D2: Y = {ProjMap2(f,m).k where k is Nat : n<=k}
& g.z = inf Y by D1,RINFSUP2:def 6;
for x be ExtReal st x in Y holds 0 <= x
proof
let x be ExtReal;
assume x in Y; then
ex k be Nat st x = ProjMap2(f,m).k & n <= k by D2;
hence 0 <= x by SUPINF_2:51;
end; then
0 is LowerBound of Y by XXREAL_2:def 2;
hence 0 <= g.z by D2,XXREAL_2:def 4;
end;
suppose not z in dom g;
hence 0 <= g.z by FUNCT_1:def 2;
end;
end; then
g is nonnegative by SUPINF_2:51; then
reconsider g as nonnegative without-infty Function of [:NAT,NAT:],ExtREAL;
A6:for m be Element of NAT holds
for N,n be Element of NAT st n>=N holds
(Partial_Sums_in_cod2 g).(N,m) <= (Partial_Sums_in_cod2 f).(n,m)
proof
let m be Element of NAT;
let N,n be Element of NAT;
assume A7: n >= N;
defpred P[Nat] means
(Partial_Sums_in_cod2 g).(N,$1) <= (Partial_Sums_in_cod2 f).(n,$1);
A8: (Partial_Sums_in_cod2 g).(N,0) = g.(N,0) by DefCSM
.= (inferior_realsequence ProjMap2(f,0)).N by A5;
(Partial_Sums_in_cod2 f).(n,0) = f.(n,0) by DefCSM; then
A9: P[0] by A2,A7,A8;
A10:for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
reconsider k1=k as Element of NAT by ORDINAL1:def 12;
assume A11: P[k];
g.(N,k1+1) = (inferior_realsequence ProjMap2(f,k1+1)).N by A5; then
A12: g.(N,k1+1) <= f.(n,k1+1) by A2,A7;
(Partial_Sums_in_cod2 g).(N,k+1)
= (Partial_Sums_in_cod2 g).(N,k) + g.(N,k1+1)
& (Partial_Sums_in_cod2 f).(n,k+1)
= (Partial_Sums_in_cod2 f).(n,k) + f.(n,k1+1) by DefCSM;
hence P[k+1] by A11,A12,XXREAL_3:36;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A9,A10);
hence thesis;
end;
A13:for m be Element of NAT holds
for N,n be Element of NAT st n>=N holds
(Partial_Sums_in_cod2 g).(N,m)
<= (inferior_realsequence(lim_in_cod2(Partial_Sums_in_cod2 f))).n
proof
let m be Element of NAT;
let N,n be Element of NAT;
assume A14: n>=N;
consider Y be non empty Subset of ExtREAL such that
A15: Y = {ProjMap2(Partial_Sums_in_cod2 f,m).k where k is Nat : n <= k}
& (inferior_realsequence(ProjMap2(Partial_Sums_in_cod2 f,m))).n = inf Y
by RINFSUP2:def 6;
for x be ExtReal st x in Y holds (Partial_Sums_in_cod2 g).(N,m) <= x
proof
let x be ExtReal;
assume x in Y; then
consider k be Nat such that
A17: x = ProjMap2(Partial_Sums_in_cod2 f,m).k & n<=k by A15;
reconsider k1=k as Element of NAT by ORDINAL1:def 12;
A18: N <= k1 by A14,A17,XXREAL_0:2;
x = (Partial_Sums_in_cod2 f).(k1,m) by A17,MESFUNC9:def 7;
hence (Partial_Sums_in_cod2 g).(N,m) <= x by A6,A18;
end; then
(Partial_Sums_in_cod2 g).(N,m) is LowerBound of Y by XXREAL_2:def 2; then
A19:(Partial_Sums_in_cod2 g).(N,m)
<= (inferior_realsequence(ProjMap2(Partial_Sums_in_cod2 f,m))).n
by A15,XXREAL_2:def 4;
consider Z be non empty Subset of ExtREAL such that
A20: Z = {(lim_in_cod2(Partial_Sums_in_cod2 f)).k where k is Nat : n <= k}
& (inferior_realsequence(lim_in_cod2(Partial_Sums_in_cod2 f))).n = inf Z
by RINFSUP2:def 6;
for z be ExtReal st z in Z ex y be ExtReal st y in Y & y <= z
proof
let z be ExtReal;
assume z in Z; then
consider j be Nat such that
A21: z = (lim_in_cod2(Partial_Sums_in_cod2 f)).j & n <= j by A20;
reconsider j1=j as Element of NAT by ORDINAL1:def 12;
z = lim ProjMap1(Partial_Sums_in_cod2 f,j1) by A21,D1DEF6; then
A23: z = sup ProjMap1(Partial_Sums_in_cod2 f,j1) by RINFSUP2:37;
set y = ProjMap2(Partial_Sums_in_cod2 f,m).j1;
take y;
y = (Partial_Sums_in_cod2 f).(j1,m) by MESFUNC9:def 7
.= ProjMap1(Partial_Sums_in_cod2 f,j1).m by MESFUNC9:def 6;
hence y in Y & y <= z by A15,A21,A23,RINFSUP2:23;
end; then
inf Y <= inf Z by XXREAL_2:64;
hence thesis by A15,A20,A19,XXREAL_0:2;
end;
defpred Q[Nat] means
for m be Element of NAT st m = $1 holds
(Partial_Sums seq).m = lim ProjMap2(Partial_Sums_in_cod2 g,m);
now let m be Element of NAT;
assume A24: m = 0; then
(Partial_Sums seq).m = seq.0 by MESFUNC9:def 1
.= lim_inf ProjMap2(f,0) by A1
.= sup inferior_realsequence ProjMap2(f,0) by RINFSUP2:def 9; then
A26:(Partial_Sums seq).m
= lim inferior_realsequence ProjMap2(f,0) by RINFSUP2:37;
now let n be Element of NAT;
ProjMap2(Partial_Sums_in_cod2 g,0).n
= (Partial_Sums_in_cod2 g).(n,0) by MESFUNC9:def 7
.= g.(n,0) by DefCSM
.= (inferior_realsequence ProjMap2(f,0)).n by A5;
hence (inferior_realsequence ProjMap2(f,0)).n
= ProjMap2(Partial_Sums_in_cod2 g,0).n;
end;
hence (Partial_Sums seq).m = lim ProjMap2(Partial_Sums_in_cod2 g,m)
by A24,A26,FUNCT_2:63;
end; then
A28:Q[0];
P1:for m be Element of NAT holds
ProjMap2(Partial_Sums_in_cod2 g,m) is convergent
proof
let m be Element of NAT;
for j,i be Nat st i<=j holds
ProjMap2(Partial_Sums_in_cod2 g,m).i
<= ProjMap2(Partial_Sums_in_cod2 g,m).j
proof
let j,i be Nat;
reconsider i1=i, j1=j as Element of NAT by ORDINAL1:def 12;
assume B2: i <= j;
B3: ProjMap2(Partial_Sums_in_cod2 g,m).i1 = (Partial_Sums_in_cod2 g).(i,m)
& ProjMap2(Partial_Sums_in_cod2 g,m).j1 = (Partial_Sums_in_cod2 g).(j,m)
by MESFUNC9:def 7;
defpred R[Nat] means
(Partial_Sums_in_cod2 g).(i,$1) <= (Partial_Sums_in_cod2 g).(j,$1);
B4: (Partial_Sums_in_cod2 g).(i,0) = g.(i,0) by DefCSM
.= (inferior_realsequence ProjMap2(f,0)).i1 by A5;
(Partial_Sums_in_cod2 g).(j,0) = g.(j,0) by DefCSM
.= (inferior_realsequence ProjMap2(f,0)).j1 by A5; then
B5: R[0] by B2,B4,RINFSUP2:7;
B6: for l be Nat st R[l] holds R[l+1]
proof
let l be Nat;
reconsider l1=l as Element of NAT by ORDINAL1:def 12;
assume B7: R[l];
g.(i,l+1) = (inferior_realsequence ProjMap2(f,l1+1)).i1
& g.(j,l+1) = (inferior_realsequence ProjMap2(f,l1+1)).j1 by A5; then
B8: g.(i,l+1) <= g.(j,l+1) by B2,RINFSUP2:7;
(Partial_Sums_in_cod2 g).(i,l+1)
= (Partial_Sums_in_cod2 g).(i,l) + g.(i,l+1)
& (Partial_Sums_in_cod2 g).(j,l+1)
= (Partial_Sums_in_cod2 g).(j,l) + g.(j,l+1) by DefCSM;
hence R[l+1] by B7,B8,XXREAL_3:36;
end;
for l be Nat holds R[l] from NAT_1:sch 2(B5,B6);
hence thesis by B3;
end; then
ProjMap2(Partial_Sums_in_cod2 g,m) is non-decreasing by RINFSUP2:7;
hence ProjMap2(Partial_Sums_in_cod2 g,m) is convergent by RINFSUP2:37;
end;
A29:for k be Nat st Q[k] holds Q[k+1]
proof
let k be Nat;
reconsider k1=k as Element of NAT by ORDINAL1:def 12;
assume A30: Q[k];
now let m be Element of NAT;
assume B00: m = k+1; then
B0: (Partial_Sums seq).m
= (Partial_Sums seq).k + seq.(k+1) by MESFUNC9:def 1
.= lim ProjMap2(Partial_Sums_in_cod2 g,k1) + seq.(k+1) by A30
.= lim ProjMap2(Partial_Sums_in_cod2 g,k1) + lim_inf ProjMap2(f,k+1)
by A1;
B1: lim_inf ProjMap2(f,k+1)
= sup inferior_realsequence ProjMap2(f,k1+1) by RINFSUP2:def 9
.= lim inferior_realsequence ProjMap2(f,k1+1) by RINFSUP2:37;
B9: ProjMap2(Partial_Sums_in_cod2 g,k1) is convergent by P1;
B10: inferior_realsequence ProjMap2(f,k1+1) is convergent
by RINFSUP2:37;
for n be object st n in dom(inferior_realsequence ProjMap2(f,k1+1))
holds 0. <= (inferior_realsequence ProjMap2(f,k1+1)).n
proof
let n be object;
assume n in dom(inferior_realsequence ProjMap2(f,k1+1)); then
g.(n,k1+1) = (inferior_realsequence ProjMap2(f,k1+1)).n by A5;
hence thesis by SUPINF_2:51;
end; then
C2: inferior_realsequence ProjMap2(f,k1+1) is nonnegative by SUPINF_2:52;
for i be Nat holds
ProjMap2(Partial_Sums_in_cod2 g,m).i
= ProjMap2(Partial_Sums_in_cod2 g,k1).i
+ (inferior_realsequence ProjMap2(f,k1+1)).i
proof
let i be Nat;
reconsider i1=i as Element of NAT by ORDINAL1:def 12;
ProjMap2(Partial_Sums_in_cod2 g,m).i1
= (Partial_Sums_in_cod2 g).(i,m) by MESFUNC9:def 7
.= (Partial_Sums_in_cod2 g).(i,k) + g.(i,k+1) by B00,DefCSM
.= ProjMap2(Partial_Sums_in_cod2 g,k1).i1 + g.(i,k+1) by MESFUNC9:def 7;
hence thesis by A5;
end;
hence (Partial_Sums seq).m = lim ProjMap2(Partial_Sums_in_cod2 g,m)
by B0,B1,B9,B10,C2,MESFUNC9:11;
end;
hence Q[k+1];
end;
A30: for k be Nat holds Q[k] from NAT_1:sch 2(A28,A29);
A31:
for m be Nat holds
(Partial_Sums seq).m <= lim_inf lim_in_cod2(Partial_Sums_in_cod2 f)
proof
let m be Nat;
reconsider m1=m as Element of NAT by ORDINAL1:def 12;
A32:for n be Nat holds
ProjMap2(Partial_Sums_in_cod2 g,m1).n
<= (inferior_realsequence(lim_in_cod2(Partial_Sums_in_cod2 f))).n
proof
let n be Nat;
reconsider n1=n as Element of NAT by ORDINAL1:def 12;
ProjMap2(Partial_Sums_in_cod2 g,m1).n1
= (Partial_Sums_in_cod2 g).(n,m) by MESFUNC9:def 7;
hence ProjMap2(Partial_Sums_in_cod2 g,m1).n
<= (inferior_realsequence(lim_in_cod2(Partial_Sums_in_cod2 f))).n
by A13;
end;
A33:ProjMap2(Partial_Sums_in_cod2 g,m1) is convergent by P1;
(inferior_realsequence(lim_in_cod2(Partial_Sums_in_cod2 f)))
is convergent by RINFSUP2:37; then
lim ProjMap2(Partial_Sums_in_cod2 g,m1)
<= lim (inferior_realsequence(lim_in_cod2(Partial_Sums_in_cod2 f)))
by A32,A33,RINFSUP2:38; then
(Partial_Sums seq).m
<= lim (inferior_realsequence(lim_in_cod2(Partial_Sums_in_cod2 f)))
by A30; then
(Partial_Sums seq).m
<= sup (inferior_realsequence(lim_in_cod2(Partial_Sums_in_cod2 f)))
by RINFSUP2:37;
hence thesis by RINFSUP2:def 9;
end;
for m be object st m in dom seq holds 0<=seq.m
proof
let m be object;
assume m in dom seq; then
reconsider m1=m as Element of NAT;
E1: seq.m = lim_inf ProjMap2(f,m1) by A1
.= sup inferior_realsequence ProjMap2(f,m1) by RINFSUP2:def 9;
for n be object st n in dom(inferior_realsequence ProjMap2(f,m1))
holds 0. <= (inferior_realsequence ProjMap2(f,m1)).n
proof
let n be object;
assume n in dom(inferior_realsequence ProjMap2(f,m1)); then
g.(n,m1) = (inferior_realsequence ProjMap2(f,m1)).n by A5;
hence thesis by SUPINF_2:51;
end; then
(inferior_realsequence ProjMap2(f,m1)).0 >= 0 by SUPINF_2:51,52;
hence thesis by E1,RINFSUP2:23;
end; then
seq is nonnegative by SUPINF_2:52; then
Partial_Sums seq is non-decreasing by MESFUNC9:16; then
lim (Partial_Sums seq) <= lim_inf lim_in_cod2(Partial_Sums_in_cod2 f)
by A31,MESFUNC9:9,RINFSUP2:37;
hence thesis by MESFUNC9:def 3;
end;
theorem
for f be nonnegative Function of [:NAT,NAT:],ExtREAL,
seq be ExtREAL_sequence st
(for m be Element of NAT holds seq.m = lim_inf ProjMap1(f,m))
holds Sum seq <= lim_inf lim_in_cod1(Partial_Sums_in_cod1 f)
proof
let f be nonnegative Function of [:NAT,NAT:],ExtREAL,
seq be ExtREAL_sequence;
assume A1: for m be Element of NAT holds seq.m = lim_inf ProjMap1(f,m);
now let m be Element of NAT;
ProjMap1(f,m) = ProjMap2(f@,m) by Th32;
hence seq.m = lim_inf ProjMap2(f@,m) by A1;
end; then
A2:Sum seq <= lim_inf lim_in_cod2(Partial_Sums_in_cod2 f@) by Th83;
lim_in_cod2(Partial_Sums_in_cod2 f@)
= lim_in_cod1((Partial_Sums_in_cod2 f@)@) by Th38
.= lim_in_cod1(Partial_Sums_in_cod1 (f@)@) by Th40;
hence Sum seq <= lim_inf lim_in_cod1(Partial_Sums_in_cod1 f)
by A2,DBLSEQ_2:7;
end;
theorem Th85:
for f be Function of [:NAT,NAT:],ExtREAL, seq be ExtREAL_sequence, n,m be Nat
holds
( (for i,j be Nat holds f.(i,j) <= seq.i) implies
(Partial_Sums_in_cod1 f).(n,m) <= (Partial_Sums seq).n )
& ( (for i,j be Nat holds f.(i,j) <= seq.j) implies
(Partial_Sums_in_cod2 f).(n,m) <= (Partial_Sums seq).m )
proof
let f be Function of [:NAT,NAT:],ExtREAL, seq be ExtREAL_sequence,
n,m be Nat;
hereby assume
A1: for i,j be Nat holds f.(i,j) <= seq.i;
defpred P[Nat] means
(Partial_Sums_in_cod1 f).($1,m) <= (Partial_Sums seq).$1;
A2: (Partial_Sums_in_cod1 f).(0,m) = f.(0,m) by DefRSM;
(Partial_Sums seq).0 = seq.0 by MESFUNC9:def 1; then
A3: P[0] by A1,A2;
A4: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A5: P[k];
A6: f.(k+1,m) <= seq.(k+1) by A1;
A7: (Partial_Sums_in_cod1 f).(k+1,m)
= (Partial_Sums_in_cod1 f).(k,m) + f.(k+1,m) by DefRSM;
(Partial_Sums seq).(k+1) = (Partial_Sums seq).k + seq.(k+1)
by MESFUNC9:def 1;
hence thesis by A5,A6,A7,XXREAL_3:36;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A3,A4);
hence (Partial_Sums_in_cod1 f).(n,m) <= (Partial_Sums seq).n;
end;
assume
A1: for i,j be Nat holds f.(i,j) <= seq.j;
defpred P[Nat] means
(Partial_Sums_in_cod2 f).(n,$1) <= (Partial_Sums seq).$1;
A2:(Partial_Sums_in_cod2 f).(n,0) = f.(n,0) by DefCSM;
(Partial_Sums seq).0 = seq.0 by MESFUNC9:def 1; then
A3:P[0] by A1,A2;
A4:for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A5: P[k];
A6: f.(n,k+1) <= seq.(k+1) by A1;
A7: (Partial_Sums_in_cod2 f).(n,k+1)
= (Partial_Sums_in_cod2 f).(n,k) + f.(n,k+1) by DefCSM;
(Partial_Sums seq).(k+1) = (Partial_Sums seq).k + seq.(k+1)
by MESFUNC9:def 1;
hence thesis by A5,A6,A7,XXREAL_3:36;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A3,A4);
hence thesis;
end;
theorem Th86:
for seq be ExtREAL_sequence, r be R_eal st
(for n be Nat holds seq.n <= r) holds lim_sup seq <= r
proof
let seq be ExtREAL_sequence, r be R_eal;
assume
A1: for n be Nat holds seq.n <= r;
deffunc F(Element of NAT) = r;
consider f be Function of NAT,ExtREAL such that
A2: for n be Element of NAT holds f.n = F(n) from FUNCT_2:sch 4;
A4:for n be Nat holds f.n = r
proof
let n be Nat;
n is Element of NAT by ORDINAL1:def 12;
hence f.n = r by A2;
end; then
A5:f is convergent & lim f = r by MESFUNC5:60;
for n be Nat holds seq.n <= f.n
proof
let n be Nat;
f.n = r by A4;
hence seq.n <= f.n by A1;
end; then
lim_sup seq <= lim_sup f by MESFUN10:3;
hence lim_sup seq <= r by A5,RINFSUP2:41;
end;
theorem Th87:
for seq be ExtREAL_sequence, r be R_eal st
(for n be Nat holds r <= seq.n) holds r <= lim_inf seq
proof
let seq be ExtREAL_sequence, r be R_eal;
assume
A1: for n be Nat holds r <= seq.n;
deffunc F(Element of NAT) = r;
consider f be Function of NAT,ExtREAL such that
A2: for n be Element of NAT holds f.n = F(n) from FUNCT_2:sch 4;
A4:for n be Nat holds f.n = r
proof
let n be Nat;
n is Element of NAT by ORDINAL1:def 12;
hence f.n = r by A2;
end; then
A5:f is convergent & lim f = r by MESFUNC5:60;
for n be Nat holds f.n <= seq.n
proof
let n be Nat;
f.n = r by A4;
hence f.n <= seq.n by A1;
end; then
lim_inf f <= lim_inf seq by MESFUN10:3;
hence r <= lim_inf seq by A5,RINFSUP2:41;
end;
theorem
for f be nonnegative Function of [:NAT,NAT:],ExtREAL holds
( for i1,i2,j be Nat st i1 <= i2 holds
(Partial_Sums_in_cod1 f).(i1,j) <= (Partial_Sums_in_cod1 f).(i2,j) )
& ( for i,j1,j2 be Nat st j1 <= j2 holds
(Partial_Sums_in_cod2 f).(i,j1) <= (Partial_Sums_in_cod2 f).(i,j2) )
proof
let f be nonnegative Function of [:NAT,NAT:],ExtREAL;
A2:now let i1,i2,j be natural number;
assume i1 <= i2; then
consider k be Nat such that
A3: i2 = i1 + k by NAT_1:10;
defpred P[Nat] means
$1 <= k implies (Partial_Sums_in_cod1 f).(i1,j)
<= (Partial_Sums_in_cod1 f).(i1+$1,j);
A4: P[0];
A5: for l be Nat st P[l] holds P[l+1]
proof
let l be Nat;
assume A6: P[l];
now assume A7: l+1 <= k;
(Partial_Sums_in_cod1 f).(i1+l+1,j)
= (Partial_Sums_in_cod1 f).(i1+l,j) + f.(i1+l+1,j) by DefRSM; then
(Partial_Sums_in_cod1 f).(i1+l,j)
<= (Partial_Sums_in_cod1 f).(i1+l+1,j) by SUPINF_2:51,XXREAL_3:39;
hence (Partial_Sums_in_cod1 f).(i1,j)
<= (Partial_Sums_in_cod1 f).(i1+(l+1),j)
by A6,A7,NAT_1:13,XXREAL_0:2;
end;
hence P[l+1];
end;
for l be Nat holds P[l] from NAT_1:sch 2(A4,A5);
hence (Partial_Sums_in_cod1 f).(i1,j)
<= (Partial_Sums_in_cod1 f).(i2,j) by A3;
end;
now let i,j1,j2 be natural number;
assume j1 <= j2; then
consider k be Nat such that
B3: j2 = j1 + k by NAT_1:10;
defpred P[Nat] means
$1 <= k implies (Partial_Sums_in_cod2 f).(i,j1)
<= (Partial_Sums_in_cod2 f).(i,j1+$1);
B4: P[0];
B5: for l be Nat st P[l] holds P[l+1]
proof
let l be Nat;
assume B6: P[l];
now assume B7: l+1 <= k;
(Partial_Sums_in_cod2 f).(i,j1+l+1)
= (Partial_Sums_in_cod2 f).(i,j1+l) + f.(i,j1+l+1) by DefCSM; then
(Partial_Sums_in_cod2 f).(i,j1+l)
<= (Partial_Sums_in_cod2 f).(i,j1+l+1) by SUPINF_2:51,XXREAL_3:39;
hence (Partial_Sums_in_cod2 f).(i,j1)
<= (Partial_Sums_in_cod2 f).(i,j1+(l+1))
by B6,B7,NAT_1:13,XXREAL_0:2;
end;
hence P[l+1];
end;
for l be Nat holds P[l] from NAT_1:sch 2(B4,B5);
hence (Partial_Sums_in_cod2 f).(i,j1)
<= (Partial_Sums_in_cod2 f).(i,j2) by B3;
end;
hence thesis by A2;
end;
theorem Th89:
for f be Function of [:NAT,NAT:],ExtREAL, i,j,k be Nat st
(for m be Element of NAT holds ProjMap2(f,m) is non-decreasing) & i<=j
holds (Partial_Sums_in_cod2 f).(i,k) <= (Partial_Sums_in_cod2 f).(j,k)
proof
let f be Function of [:NAT,NAT:],ExtREAL, i,j,k be Nat;
assume that
A1: for m be Element of NAT holds ProjMap2(f,m) is non-decreasing and
A2: i <= j;
reconsider i1=i, j1=j as Element of NAT by ORDINAL1:def 12;
defpred P[Nat] means
(Partial_Sums_in_cod2 f).(i,$1) <= (Partial_Sums_in_cod2 f).(j,$1);
ProjMap2(f,0).i1 = f.(i,0) & ProjMap2(f,0).j1 = f.(j,0)
by MESFUNC9:def 7; then
ProjMap2(f,0).i1 = (Partial_Sums_in_cod2 f).(i,0) &
ProjMap2(f,0).j1 = (Partial_Sums_in_cod2 f).(j,0) by DefCSM; then
A4:P[0] by A1,A2,RINFSUP2:7;
A5:for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume A6: P[n];
A7: (Partial_Sums_in_cod2 f).(i,n+1)
= (Partial_Sums_in_cod2 f).(i,n) + f.(i,n+1)
& (Partial_Sums_in_cod2 f).(j,n+1)
= (Partial_Sums_in_cod2 f).(j,n) + f.(j,n+1) by DefCSM;
A8: ProjMap2(f,n+1).i <= ProjMap2(f,n+1).j by A1,A2,RINFSUP2:7;
ProjMap2(f,n+1).i1 = f.(i,n+1) & ProjMap2(f,n+1).j1 = f.(j,n+1)
by MESFUNC9:def 7;
hence P[n+1] by A6,A7,A8,XXREAL_3:36;
end;
for n be Nat holds P[n] from NAT_1:sch 2(A4,A5);
hence thesis;
end;
theorem
for f be Function of [:NAT,NAT:],ExtREAL, i,j,k be Nat st
(for n be Element of NAT holds ProjMap1(f,n) is non-decreasing) & i<=j
holds (Partial_Sums_in_cod1 f).(k,i) <= (Partial_Sums_in_cod1 f).(k,j)
proof
let f be Function of [:NAT,NAT:],ExtREAL, i,j,k be Nat;
assume that
A1: for n be Element of NAT holds ProjMap1(f,n) is non-decreasing and
A2: i <= j;
for n be Element of NAT holds ProjMap2(f@,n) is non-decreasing
proof
let n be Element of NAT;
ProjMap1(f,n) = ProjMap2(f@,n) by Th32;
hence thesis by A1;
end; then
(Partial_Sums_in_cod2 f@).(i,k) <= (Partial_Sums_in_cod2 f@).(j,k)
by A2,Th89; then
(Partial_Sums_in_cod1 f).(k,i) <= (Partial_Sums_in_cod2 f@).(j,k)
by Th39;
hence thesis by Th39;
end;
:: Moonotone Convergence Theorem for Double Sequence
theorem Th91:
for f be nonnegative Function of [:NAT,NAT:],ExtREAL,
seq be ExtREAL_sequence st
(for m be Element of NAT holds
ProjMap2(f,m) is non-decreasing & seq.m = lim ProjMap2(f,m))
holds
lim_in_cod2(Partial_Sums_in_cod2 f) is non-decreasing
& Sum seq = lim lim_in_cod2(Partial_Sums_in_cod2 f)
proof
let f be nonnegative Function of [:NAT,NAT:],ExtREAL,
seq be ExtREAL_sequence;
assume
A1: for m be Element of NAT holds
ProjMap2(f,m) is non-decreasing & seq.m = lim ProjMap2(f,m);
now let m be Element of NAT;
ProjMap2(f,m) is non-decreasing by A1; then
ProjMap2(f,m) is convergent by RINFSUP2:37; then
lim_inf ProjMap2(f,m) = lim ProjMap2(f,m) by RINFSUP2:41;
hence seq.m = lim_inf ProjMap2(f,m) by A1;
end; then
A2:Sum seq <= lim_inf lim_in_cod2(Partial_Sums_in_cod2 f) by Th83;
A3:for n,m be Nat holds f.(n,m) <= seq.m
proof
let n,m be Nat;
reconsider m1=m as Element of NAT by ORDINAL1:def 12;
ProjMap2(f,m1) is non-decreasing by A1; then
lim ProjMap2(f,m1) = sup ProjMap2(f,m1) by RINFSUP2:37; then
A4: seq.m = sup ProjMap2(f,m1) by A1;
A5: n is Element of NAT by ORDINAL1:def 12;
dom(ProjMap2(f,m1)) = NAT by FUNCT_2:def 1; then
ProjMap2(f,m1).n <= sup rng ProjMap2(f,m1) by A5,FUNCT_1:3,XXREAL_2:4; then
ProjMap2(f,m1).n <= sup ProjMap2(f,m1) by RINFSUP2:def 1;
hence thesis by A4,A5,MESFUNC9:def 7;
end;
for n,m be Nat st m <= n holds
(lim_in_cod2(Partial_Sums_in_cod2 f)).m
<= (lim_in_cod2(Partial_Sums_in_cod2 f)).n
proof
let n,m be Nat;
assume C1: m <= n;
reconsider m1=m, n1=n as Element of NAT by ORDINAL1:def 12;
C2: (lim_in_cod2(Partial_Sums_in_cod2 f)).m
= lim ProjMap1(Partial_Sums_in_cod2 f,m1)
& (lim_in_cod2(Partial_Sums_in_cod2 f)).n
= lim ProjMap1(Partial_Sums_in_cod2 f,n1) by D1DEF6;
C3: ProjMap1(Partial_Sums_in_cod2 f,m1) is convergent
& ProjMap1(Partial_Sums_in_cod2 f,n1) is convergent by RINFSUP2:37;
for k be Nat holds ProjMap1(Partial_Sums_in_cod2 f,m1).k
<= ProjMap1(Partial_Sums_in_cod2 f,n1).k
proof
let k be Nat;
reconsider k1=k as Element of NAT by ORDINAL1:def 12;
ProjMap1(Partial_Sums_in_cod2 f,m1).k1 = (Partial_Sums_in_cod2 f).(m1,k1)
& ProjMap1(Partial_Sums_in_cod2 f,n1).k1 = (Partial_Sums_in_cod2 f).(n1,k1)
by MESFUNC9:def 6;
hence thesis by A1,C1,Th89;
end;
hence thesis by C2,C3,RINFSUP2:38;
end;
hence
lim_in_cod2(Partial_Sums_in_cod2 f) is non-decreasing by RINFSUP2:7; then
B1:lim_in_cod2(Partial_Sums_in_cod2 f) is convergent by RINFSUP2:37; then
B3:Sum seq <= lim lim_in_cod2(Partial_Sums_in_cod2 f) by A2,RINFSUP2:41;
for n be Nat holds
(lim_in_cod2(Partial_Sums_in_cod2 f)).n <= Sum seq
proof
let n be Nat;
reconsider n1=n as Element of NAT by ORDINAL1:def 12;
A6: (lim_in_cod2(Partial_Sums_in_cod2 f)).n
= lim ProjMap1(Partial_Sums_in_cod2 f,n1) by D1DEF6;
A7: ProjMap1(Partial_Sums_in_cod2 f,n1) is convergent by RINFSUP2:37;
for m be Element of NAT holds 0 <= seq.m
proof
let m be Element of NAT;
for n be Nat holds 0. <= ProjMap2(f,m).n
proof
let n be Nat;
n is Element of NAT by ORDINAL1:def 12;
hence 0. <= ProjMap2(f,m).n by SUPINF_2:39;
end; then
B2: 0. <= lim_inf ProjMap2(f,m) by Th87;
ProjMap2(f,m) is non-decreasing by A1; then
ProjMap2(f,m) is convergent by RINFSUP2:37; then
lim_inf ProjMap2(f,m) = lim ProjMap2(f,m) by RINFSUP2:41;
hence 0 <= seq.m by B2,A1;
end; then
seq is nonnegative by SUPINF_2:39; then
Partial_Sums seq is non-decreasing by MESFUNC9:16; then
A8: Partial_Sums seq is convergent by RINFSUP2:37;
for m be Nat holds
ProjMap1(Partial_Sums_in_cod2 f,n1).m <= (Partial_Sums seq).m
proof
let m be Nat;
m is Element of NAT by ORDINAL1:def 12; then
ProjMap1(Partial_Sums_in_cod2 f,n1).m
= (Partial_Sums_in_cod2 f).(n,m) by MESFUNC9:def 6;
hence ProjMap1(Partial_Sums_in_cod2 f,n1).m <= (Partial_Sums seq).m
by A3,Th85;
end; then
lim ProjMap1(Partial_Sums_in_cod2 f,n1) <= lim(Partial_Sums seq)
by A7,A8,RINFSUP2:38;
hence (lim_in_cod2(Partial_Sums_in_cod2 f)).n <= Sum seq
by A6,MESFUNC9:def 3;
end; then
lim_sup lim_in_cod2(Partial_Sums_in_cod2 f) <= Sum seq by Th86; then
lim lim_in_cod2(Partial_Sums_in_cod2 f) <= Sum seq by B1,RINFSUP2:41;
hence Sum seq = lim lim_in_cod2(Partial_Sums_in_cod2 f) by B3,XXREAL_0:1;
end;
theorem
for f be nonnegative Function of [:NAT,NAT:],ExtREAL,
seq be ExtREAL_sequence st
(for m be Element of NAT holds
ProjMap1(f,m) is non-decreasing & seq.m = lim ProjMap1(f,m))
holds
lim_in_cod1(Partial_Sums_in_cod1 f) is non-decreasing
& Sum seq = lim lim_in_cod1(Partial_Sums_in_cod1 f)
proof
let f be nonnegative Function of [:NAT,NAT:],ExtREAL,
seq be ExtREAL_sequence;
assume
A1: for m be Element of NAT holds
ProjMap1(f,m) is non-decreasing & seq.m = lim ProjMap1(f,m);
for m be Element of NAT holds
ProjMap2(f@,m) is non-decreasing & seq.m = lim ProjMap2(f@,m)
proof
let m be Element of NAT;
ProjMap1(f,m) is non-decreasing by A1;
hence ProjMap2(f@,m) is non-decreasing by Th32;
seq.m = lim ProjMap1(f,m) by A1;
hence seq.m = lim ProjMap2(f@,m) by Th32;
end; then
A2:lim_in_cod2(Partial_Sums_in_cod2 f@) is non-decreasing
& Sum seq = lim lim_in_cod2(Partial_Sums_in_cod2 f@) by Th91;
for n be Element of NAT holds
(lim_in_cod2(Partial_Sums_in_cod2 f@)).n
= (lim_in_cod1(Partial_Sums_in_cod1 f)).n
proof
let n be Element of NAT;
(lim_in_cod1(Partial_Sums_in_cod1 f)).n
= lim ProjMap2(Partial_Sums_in_cod1 f,n) by D1DEF5
.= lim ProjMap1((Partial_Sums_in_cod1 f)@,n) by Th33
.= lim ProjMap1(Partial_Sums_in_cod2 f@,n) by Th40;
hence thesis by D1DEF6;
end;
hence thesis by A2,FUNCT_2:def 8;
end;
begin :: Pringsheim sense convergence for extended real valued double sequences
theorem Th93:
for f be Function of [:NAT,NAT:],ExtREAL st
f is P-convergent_to_+infty holds
not f is P-convergent_to_-infty &
not f is P-convergent_to_finite_number
proof
let f be Function of [:NAT,NAT:],ExtREAL;
assume A1: f is P-convergent_to_+infty;
hereby assume f is P-convergent_to_-infty; then
consider N1 be Nat such that
A3: for n,m be Nat st n>=N1 & m>=N1 holds f.(n,m) <= -1;
consider N2 be Nat such that
A4: for n,m be Nat st n>=N2 & m>=N2 holds 1 <= f.(n,m) by A1;
reconsider N1,N2 as Element of NAT by ORDINAL1:def 12;
set N = max(N1,N2);
A5: N>=N1 & N>=N2 by XXREAL_0:25; then
f.(N,N) <= -1 by A3;
hence contradiction by A4,A5;
end;
assume f is P-convergent_to_finite_number; then
consider p be Real such that
A6: for e be Real st 0 =N & m>=N
holds |. f.(n,m) - sup rng f .| < p
proof
let p be Real;
assume
A14: 0 < p;
reconsider e=p as R_eal by XXREAL_0:def 1;
sup rng f in REAL by A12,A11,XXREAL_0:14;
then consider y be ExtReal such that
A15: y in rng f and
A16: sup rng f - e < y by A14,MEASURE6:6;
consider x be object such that
A17: x in dom f and
A18: y=f.x by A15,FUNCT_1:def 3;
consider i,j be object such that
B1: i in NAT & j in NAT & x=[i,j] by A17,ZFMISC_1:def 2;
reconsider i,j as Nat by B1;
reconsider Ni=i, Nj=j as Element of NAT by B1;
set N0=max(Ni,n0), M0=max(Nj,m0), N=max(N0,M0);
take N;
hereby
let n,m be Nat;
Ni<=N0 & n0<=N0 & Nj<=M0 & m0<=M0 & N0<=N & M0<=N
by XXREAL_0:25; then
B2: Ni <= N & Nj <= N by XXREAL_0:2;
assume N <= n & N <= m;
then Ni <=n & Nj <= m by B2,XXREAL_0:2;
then f.(Ni,Nj) <= f.(n,m) by A1;
then sup rng f - e < f.(n,m) by A16,A18,B1,XXREAL_0:2;
then sup rng f < f.(n,m) + e by XXREAL_3:54;
then sup rng f - f.(n,m) < e by XXREAL_3:55;
then -e < - (sup rng f - f.(n,m)) by XXREAL_3:38;
then
A20: -e < f.(n,m) -sup rng f by XXREAL_3:26;
A21: f.(n,m) <= sup rng f by A2;
A22: now
assume
A23: sup rng f = sup rng f + e;
e + sup rng f + -sup rng f = e + (sup rng f + -sup
rng f) by A12,A11,XXREAL_3:29
.= e + 0 by XXREAL_3:7
.= e by XXREAL_3:4;
hence contradiction by A14,A23,XXREAL_3:7;
end;
sup rng f + (0 qua ExtReal)
<= sup rng f + e by A14,XXREAL_3:36;
then sup rng f <= sup rng f + e by XXREAL_3:4;
then sup rng f < sup rng f + e by A22,XXREAL_0:1;
then f.(n,m) < sup rng f + e by A21,XXREAL_0:2;
then f.(n,m) -sup rng f < e by XXREAL_3:55;
hence |.f.(n,m)-sup rng f .| < p by A20,EXTREAL1:22;
end;
end;
A24: h = sup rng f;
then
A25: f is P-convergent_to_finite_number by A13;
hence f is P-convergent;
hence thesis by A13,A24,A25,Def5;
end;
suppose
A26: not (ex K be Real st 0 < K & for n,m be Nat holds f.(n,m) < K);
now
let K be Real;
assume 0 < K;
then consider N0,N1 be Nat such that
A27: K <= f.(N0,N1) by A26;
reconsider n0=N0,n1=N1 as Element of NAT by ORDINAL1:def 12;
set N = max(n0,n1);
B3: N >= N0 & N >= N1 by XXREAL_0:25;
reconsider N as Nat;
now
let n,m be Nat;
assume N <=n & N <= m; then
N0 <= n & N1 <= m by B3,XXREAL_0:2;
then f.(N0,N1) <= f.(n,m) by A1;
hence K <= f.(n,m) by A27,XXREAL_0:2;
end;
hence ex N be Nat st for n,m be Nat st N<=n & N<=m
holds K <= f.(n,m);
end;
then
A28: f is P-convergent_to_+infty;
hence
A29: f is P-convergent;
now
assume
A30: sup rng f <> +infty;
f.(n0,m0) <= sup(rng f) by A2;
then reconsider h=sup rng f as Element of REAL
by A8,A30,XXREAL_0:14;
set K=max(0,h);
0 <=K by XXREAL_0:25;
then consider N0,M0 be Nat such that
A31: K+1 <= f.(N0,M0) by A26;
h+0 < K+1 by XREAL_1:8,XXREAL_0:25;
then sup rng f < f.(N0,M0) by A31,XXREAL_0:2;
hence contradiction by A2;
end;
hence thesis by A28,A29,Def5;
end;
end;
end;
theorem
for f1,f2 be Function of [:NAT,NAT:],ExtREAL st
(for n,m be Nat holds f1.(n,m) <= f2.(n,m))
holds sup rng f1 <= sup rng f2
proof
let f1,f2 be Function of [:NAT,NAT:],ExtREAL;
assume A1: for n,m be Nat holds f1.(n,m) <= f2.(n,m);
A2:now let n,m be Element of NAT;
dom f2 = [:NAT,NAT:] by FUNCT_2:def 1; then
[n,m] in dom f2 by ZFMISC_1:87; then
A3: f2.(n,m) in rng f2 by FUNCT_1:def 3;
A4: f1.(n,m) <= f2.(n,m) by A1;
sup rng f2 is UpperBound of rng f2 by XXREAL_2:def 3;
then f2.(n,m) <= sup rng f2 by A3,XXREAL_2:def 1;
hence f1.(n,m) <= sup rng f2 by A4,XXREAL_0:2;
end;
now let x be ExtReal;
assume x in rng f1; then
consider z be object such that
A5: z in dom f1 & x=f1.z by FUNCT_1:def 3;
consider n,m be object such that
A6: n in NAT & m in NAT & z = [n,m] by A5,ZFMISC_1:def 2;
reconsider n,m as Element of NAT by A6;
x = f1.(n,m) by A5,A6;
hence x <= sup rng f2 by A2;
end; then
sup rng f2 is UpperBound of rng f1 by XXREAL_2:def 1;
hence thesis by XXREAL_2:def 3;
end;
theorem
for f be Function of [:NAT,NAT:],ExtREAL holds
for n,m be Nat holds f.(n,m) <= sup rng f
proof
let f be Function of [:NAT,NAT:],ExtREAL;
hereby let n,m be Nat;
A0: n in NAT & m in NAT by ORDINAL1:def 12;
dom f = [:NAT,NAT:] by FUNCT_2:def 1; then
[n,m] in dom f by A0,ZFMISC_1:87; then
A1: f.(n,m) in rng f by FUNCT_1:def 3;
sup rng f is UpperBound of rng f by XXREAL_2:def 3;
hence f.(n,m) <= sup rng f by A1,XXREAL_2:def 1;
end;
end;
theorem
for f be Function of [:NAT,NAT:],ExtREAL, K be R_eal st
(for n,m be Nat holds f.(n,m) <= K) holds
sup rng f <= K
proof
let f be Function of [:NAT,NAT:],ExtREAL, K be R_eal;
assume A1: for n,m be Nat holds f.(n,m) <= K;
now let x be ExtReal;
assume x in rng f; then
consider z be object such that
A2: z in dom f & x = f.z by FUNCT_1:def 3;
consider n,m be object such that
A3: n in NAT & m in NAT & z = [n,m] by A2,ZFMISC_1:def 2;
reconsider n,m as Element of NAT by A3;
x = f.(n,m) by A2,A3;
hence x <= K by A1;
end; then
K is UpperBound of rng f by XXREAL_2:def 1;
hence thesis by XXREAL_2:def 3;
end;
theorem
for f be Function of [:NAT,NAT:],ExtREAL, K be R_eal st
K <> +infty & (for n,m be Nat holds f.(n,m) <= K) holds
sup rng f < +infty
proof
let f be Function of [:NAT,NAT:],ExtREAL, K be R_eal;
assume A1: K <> +infty & (for n,m be Nat holds f.(n,m) <= K);
now let x be ExtReal;
assume x in rng f; then
consider z be object such that
A2: z in dom f & x = f.z by FUNCT_1:def 3;
consider n,m be object such that
A3: n in NAT & m in NAT & z = [n,m] by A2,ZFMISC_1:def 2;
reconsider n,m as Element of NAT by A3;
x = f.(n,m) by A2,A3;
hence x <= K by A1;
end; then
K is UpperBound of rng f by XXREAL_2:def 1; then
sup rng f <= K by XXREAL_2:def 3;
hence thesis by A1,XXREAL_0:2,4;
end;
theorem Th101:
for f be without-infty Function of [:NAT,NAT:],ExtREAL holds
sup rng f <> +infty
iff ex K be Real st 0 < K & for n,m be Nat holds f.(n,m) <= K
proof
let f be without-infty Function of [:NAT,NAT:],ExtREAL;
A1: -infty < f.(1,1) by MESFUNC5:def 5;
A2:dom f = [:NAT,NAT:] by FUNCT_2:def 1; then
[1,1] in dom f by ZFMISC_1:87; then
A3:f.(1,1) <= sup rng f by FUNCT_1:3,XXREAL_2:4;
A4:now assume sup rng f <> +infty; then
not sup rng f in {-infty,+infty} by A1,A3,TARSKI:def 2; then
sup rng f in REAL by XBOOLE_0:def 3,XXREAL_0:def 4; then
reconsider S = sup rng f as Real;
take K = max(S,1);
thus 0 < K by XXREAL_0:25;
let n,m be Nat;
n in NAT & m in NAT by ORDINAL1:def 12; then
[n,m] in [:NAT,NAT:] by ZFMISC_1:87; then
A5: f.(n,m) <= sup rng f by A2,FUNCT_1:3,XXREAL_2:4;
S <= K by XXREAL_0:25;
hence f.(n,m) <= K by A5,XXREAL_0:2;
end;
now given K be Real such that
0 < K and
A6: for n,m be Nat holds f.(n,m) <= K;
now let w be ExtReal;
assume w in rng f; then
consider z be object such that
A7: z in dom f & w = f.z by FUNCT_1:def 3;
consider n,m be object such that
A8: n in NAT & m in NAT & z = [n,m] by A7,ZFMISC_1:def 2;
reconsider n,m as Element of NAT by A8;
w = f.(n,m) by A7,A8;
hence w <= K by A6;
end; then
K is UpperBound of rng f by XXREAL_2:def 1; then
sup rng f <= K by XXREAL_2:def 3;
hence sup rng f <> +infty by XXREAL_0:9,XREAL_0:def 1;
end;
hence thesis by A4;
end;
theorem Th102:
for f be Function of [:NAT,NAT:],ExtREAL, c be ExtReal st
(for n,m be Nat holds f.(n,m) = c) holds
f is P-convergent & P-lim f = c & P-lim f = sup rng f
proof
let f be Function of [:NAT,NAT:],ExtREAL, c be ExtReal;
reconsider cc = c as R_eal by XXREAL_0:def 1;
A1:dom f = [:NAT,NAT:] by FUNCT_2:def 1;
c in ExtREAL by XXREAL_0:def 1; then
A2:c in REAL or c in {-infty,+infty} by XBOOLE_0:def 3,XXREAL_0:def 4;
assume A3:for n,m be Nat holds f.(n,m) = c; then
A4:f.(1,1) = c;
now let v be ExtReal;
assume v in rng f; then
consider z be object such that
A7: z in dom f & v = f.z by FUNCT_1:def 3;
consider n,m be object such that
A8: n in NAT & m in NAT & z = [n,m] by A7,ZFMISC_1:def 2;
reconsider n,m as Element of NAT by A8;
v = f.(n,m) by A7,A8;
hence v <= c by A3;
end; then
A5:c is UpperBound of rng f by XXREAL_2:def 1;
per cases by A2,TARSKI:def 2;
suppose c in REAL; then
reconsider rc = c as Real;
A6: now reconsider N=0 as Nat;
let p be Real;
assume A7: 0 < p;
take N;
let n1,m1 be Nat such that
N <= n1 & N <= m1;
f.(n1,m1) - rc = f.(n1,m1) - f.(n1,m1) by A3;
hence |. f.(n1,m1) - rc .| < p by A7,EXTREAL1:16,XXREAL_3:7;
end; then
A8: f is P-convergent_to_finite_number;
hence f is P-convergent;
hence
A9: P-lim f = c by A6,A8,Def5;
[1,1] in dom f by A1,ZFMISC_1:87;
hence thesis by A9,A5,A4,FUNCT_1:3,XXREAL_2:55;
end;
suppose A10: c = -infty;
for p be Real st p < 0 ex N be Nat st
for n,m be Nat st n >= N & m >= N holds f.(n,m) <= p
proof
let p be Real such that p < 0;
take 0;
now let n,m be Nat such that 0 <= n & 0 <= m;
f.(n,m) = -infty by A3,A10;
hence f.(n,m) <= p by XREAL_0:def 1,XXREAL_0:12;
end;
hence thesis;
end; then
A12:f is P-convergent_to_-infty;
hence f is P-convergent;
hence
A13: P-lim f = c by A10,A12,Def5;
[1,1] in dom f by A1,ZFMISC_1:87;
hence thesis by A5,A4,A13,FUNCT_1:3,XXREAL_2:55;
end;
suppose A14: c = +infty;
for p be Real st 0 < p ex N be Nat st
for n,m be Nat st n >= N & m >= N holds p <= f.(n,m)
proof
let p be Real such that 0 < p;
take 0;
now let n,m be Nat such that n >= 0 & m >= 0;
f.(n,m) = +infty by A3,A14;
hence p <= f.(n,m) by XREAL_0:def 1,XXREAL_0:9;
end;
hence thesis;
end; then
A16:f is P-convergent_to_+infty;
hence f is P-convergent;
hence
A17: P-lim f = c by A14,A16,Def5;
[1,1] in dom f by A1,ZFMISC_1:87;
hence thesis by A5,A4,A17,FUNCT_1:3,XXREAL_2:55;
end;
end;
Lm8:
for f be without-infty Function of [:NAT,NAT:],ExtREAL
holds sup rng f in REAL or sup rng f = +infty
proof
let f be without-infty Function of [:NAT,NAT:],ExtREAL;
A1:not -infty in rng f by MESFUNC5:def 3;
dom f = [:NAT,NAT:] by FUNCT_2:def 1; then
[1,1] in dom f by ZFMISC_1:87; then
f.(1,1) in rng f by FUNCT_1:3; then
not -infty is UpperBound of rng f by A1,XXREAL_0:6,XXREAL_2:def 1; then
sup rng f <> -infty by XXREAL_2:def 3;
hence thesis by XXREAL_0:14;
end;
theorem
for f be Function of [:NAT,NAT:],ExtREAL,
f1,f2 be without-infty Function of [:NAT,NAT:],ExtREAL st
(for n1,m1,n2,m2 be Nat st n1 <= n2 & m1 <= m2 holds
f1.(n1,m1) <= f1.(n2,m2) )
& (for n1,m1,n2,m2 be Nat st n1 <= n2 & m1 <= m2 holds
f2.(n1,m1) <= f2.(n2,m2) )
& (for n,m be Nat holds f1.(n,m) + f2.(n,m) = f.(n,m) )
holds f is P-convergent & P-lim f = sup rng f
& P-lim f = P-lim f1 + P-lim f2 & sup rng f = sup rng f1 + sup rng f2
proof
let f be Function of [:NAT,NAT:],ExtREAL,
f1,f2 be without-infty Function of [:NAT,NAT:],ExtREAL;
assume that
A1: for n1,m1,n2,m2 be Nat st n1 <= n2 & m1 <= m2 holds
f1.(n1,m1) <= f1.(n2,m2) and
A2: for n1,m1,n2,m2 be Nat st n1 <= n2 & m1 <= m2 holds
f2.(n1,m1) <= f2.(n2,m2) and
A5: for n,m be Nat holds f1.(n,m) + f2.(n,m) = f.(n,m);
A6:dom f1 = [:NAT,NAT:] & dom f2 = [:NAT,NAT:] by FUNCT_2:def 1;
B0:f1 is P-convergent & P-lim f1 = sup rng f1 &
f2 is P-convergent & P-lim f2 = sup rng f2 by A1,A2,Th96;
now let n1,m1,n2,m2 be Nat;
assume n1<=n2 & m1<=m2; then
f1.(n1,m1) <= f1.(n2,m2) & f2.(n1,m1) <= f2.(n2,m2) by A1,A2; then
f1.(n1,m1) + f2.(n1,m1) <= f1.(n2,m2) + f2.(n2,m2) by XXREAL_3:36; then
f.(n1,m1) <= f1.(n2,m2) + f2.(n2,m2) by A5;
hence f.(n1,m1) <= f.(n2,m2) by A5;
end;
hence
A7: f is P-convergent & P-lim f = sup rng f by Th96;
P1:now per cases by Lm8;
suppose A9: sup rng f1 in REAL;
set SE1 = sup rng f1;
per cases by Lm8;
suppose A10: sup rng f2 in REAL;
set SE2 = sup rng f2;
B1: now let p be Real;
assume A11: 0 < p; then
consider x1 be ExtReal such that
A12: x1 in rng f1 & sup rng f1 - p/2 < x1 by A9,MEASURE6:6;
consider z1 be object such that
A13: z1 in dom f1 & x1 = f1.z1 by A12,FUNCT_1:def 3;
consider n1,m1 be object such that
A14: n1 in NAT & m1 in NAT & z1 = [n1,m1] by A13,ZFMISC_1:def 2;
reconsider n1,m1 as Element of NAT by A14;
consider x2 be ExtReal such that
A15: x2 in rng f2 & sup rng f2 - p/2 < x2 by A10,A11,MEASURE6:6;
consider z2 be object such that
A16: z2 in dom f2 & x2 = f2.z2 by A15,FUNCT_1:def 3;
consider n2,m2 be object such that
A17: n2 in NAT & m2 in NAT & z2 = [n2,m2] by A16,ZFMISC_1:def 2;
reconsider n2,m2 as Element of NAT by A17;
reconsider N = max(max(n1,m1),max(n2,m2)) as Nat;
take N;
hereby let n,m be Nat;
assume A18: n>= N & m >= N;
N >= max(n1,m1) & N >= max(n2,m2)
& max(n1,m1) >= n1 & max(n1,m1) >= m1
& max(n2,m2) >= n2 & max(n2,m2) >= m2 by XXREAL_0:25; then
N >= n1 & N >= m1 & N >= n2 & N >= m2 by XXREAL_0:2; then
n >= n1 & n >= n2 & m >= m1 & m >= m2 by A18,XXREAL_0:2; then
A22: f1.(n1,m1) <= f1.(n,m) & f2.(n2,m2) <= f2.(n,m) by A1,A2; then
SE1 - f1.(n,m) <= SE1 - x1 & SE2 - f2.(n,m) <= SE2 - x2
by A13,A14,A16,A17,XXREAL_3:37; then
A19: (SE1 - f1.(n,m)) + (SE2 - f2.(n,m))
<= (SE1 - x1) + (SE2 - x2) by XXREAL_3:36;
A20: p/2 in REAL by XREAL_0:def 1;
SE1 < p/2 + x1 & SE2 < p/2 + x2 by A12,A15,XXREAL_3:54; then
A21: SE1 - x1 < p/2 & SE2 - x2 < p/2 by XXREAL_3:55; then
A24: p/2 + (SE2 - x2) < p/2 + p/2 by A20,XXREAL_3:43;
n in NAT & m in NAT by ORDINAL1:def 12; then
[n,m] in [:NAT,NAT:] by ZFMISC_1:87; then
B1: f1.(n,m) in rng f1 & f2.(n,m) in rng f2
& f1.(n,m) <= SE1 & f2.(n,m) <= SE2 by A6,FUNCT_1:3,XXREAL_2:4; then
B2: f1.(n,m) < +infty & f2.(n,m) < +infty by A9,A10,XXREAL_0:2,9;
B3: -infty <> f1.(n,m) & -infty <> f2.(n,m) by B1,MESFUNC5:def 3;
-infty <> x1 & -infty <> x2 by A12,A15,MESFUNC5:def 3; then
x1 in REAL & x2 in REAL by B2,A22,A13,A14,A16,A17,XXREAL_0:14; then
SE2 - x2 in REAL by A10,XREAL_0:def 1; then
SE1 - x1 + (SE2 - x2) < p/2 + (SE2 - x2) by A21,XXREAL_3:43; then
SE1 - x1 + (SE2 - x2) < p/2 + p/2 by A24,XXREAL_0:2; then
A26: (SE1 - f1.(n,m)) + (SE2 - f2.(n,m)) < p by A19,XXREAL_0:2;
B5: SE1 - f1.(n,m) + (SE2 - f2.(n,m))
= SE1 - f1.(n,m) + SE2 - f2.(n,m) by A10,B2,B3,XXREAL_3:30
.= (SE2 + SE1 - f1.(n,m)) - f2.(n,m) by A9,A10,XXREAL_3:30
.= (SE1 + SE2) - (f1.(n,m) + f2.(n,m)) by A9,A10,B3,XXREAL_3:31
.= (SE1 + SE2) - f.(n,m) by A5;
SE1 - f1.(n,m) >= 0 & SE2 - f2.(n,m) >= 0 by B1,XXREAL_3:40; then
|. (SE1+SE2) - f.(n,m) .| < p by B5,A26,EXTREAL1:def 1; then
|. -(f.(n,m) - (SE1+SE2)) .| < p by XXREAL_3:26;
hence |. f.(n,m) - (SE1+SE2) .| < p by EXTREAL1:29;
end;
end; then
f is P-convergent_to_finite_number by A9,A10;
hence P-lim f = P-lim f1 + P-lim f2 by A9,A10,B0,B1,A7,Def5;
end;
suppose C1: sup rng f2 = +infty; then
C2: P-lim f1 + P-lim f2 = +infty by B0,A9,XXREAL_3:def 2;
now let g be Real;
assume 0 < g; then
consider e1 be ExtReal such that
C5: e1 in rng f1 & SE1 - g/2 < e1 by A9,MEASURE6:6;
consider z1 be object such that
C6: z1 in dom f1 & e1 = f1.z1 by C5,FUNCT_1:def 3;
consider n1,m1 be object such that
C7: n1 in NAT & m1 in NAT & z1 = [n1,m1] by C6,ZFMISC_1:def 2;
reconsider n1,m1 as Element of NAT by C7;
g - (SE1 - g/2) in REAL & (SE1 - g/2) in REAL by A9,XREAL_0:def 1; then
consider e2 be Element of ExtREAL such that
C8: e2 in rng f2 & g - (SE1 - g/2) < e2 by C1,XXREAL_0:9,XXREAL_2:94;
consider z2 be object such that
C9: z2 in dom f2 & e2 = f2.z2 by C8,FUNCT_1:def 3;
consider n2,m2 be object such that
C10: n2 in NAT & m2 in NAT & z2 = [n2,m2] by C9,ZFMISC_1:def 2;
reconsider n2,m2 as Element of NAT by C10;
reconsider N = max(max(n2,m2),max(n1,m1)) as Nat;
take N;
N >= max(n1,m1) & N >= max(n2,m2) & max(n1,m1) >= n1 & max(n1,m1) >= m1
& max(n2,m2) >= n2 & max(n2,m2) >= m2 by XXREAL_0:25; then
C13: N >= n1 & N >= m1 & N >= n2 & N >= m2 by XXREAL_0:2;
hereby let n,m be Nat;
assume n >= N & m >= N; then
n >= n1 & m >= m1 & n >= n2 & m >= m2 by C13,XXREAL_0:2; then
f1.(n,m) >= f1.(n1,m1) & f2.(n,m) >= f2.(n2,m2) by A1,A2; then
C14: SE1 - g/2 < f1.(n,m) & g - (SE1 - g/2) < f2.(n,m)
by C5,C6,C7,C8,C9,C10,XXREAL_0:2;
g - (SE1 - g/2) + (SE1 - g/2) = g by A9,XXREAL_3:22; then
g < f1.(n,m) + f2.(n,m) by C14,XXREAL_3:64;
hence g <= f.(n,m) by A5;
end;
end; then
f is P-convergent_to_+infty;
hence P-lim f = P-lim f1 + P-lim f2 by C2,A7,Def5;
end;
end;
suppose D1: sup rng f1 = +infty;
per cases by Lm8;
suppose D3: sup rng f2 in REAL;
set SE2 = sup rng f2;
D2: P-lim f1 + P-lim f2 = +infty by B0,D1,D3,XXREAL_3:def 2;
now let g be Real;
assume 0 < g; then
consider e2 be ExtReal such that
D5: e2 in rng f2 & SE2 - g/2 < e2 by D3,MEASURE6:6;
consider z2 be object such that
D6: z2 in dom f2 & e2 = f2.z2 by D5,FUNCT_1:def 3;
consider n1,m1 be object such that
D7: n1 in NAT & m1 in NAT & z2 = [n1,m1] by D6,ZFMISC_1:def 2;
reconsider n1,m1 as Element of NAT by D7;
g - (SE2 - g/2) in REAL & SE2 - g/2 in REAL by D3,XREAL_0:def 1; then
consider e1 be Element of ExtREAL such that
D8: e1 in rng f1 & g - (SE2 - g/2) < e1 by D1,XXREAL_0:9,XXREAL_2:94;
consider z1 be object such that
D9: z1 in dom f1 & e1 = f1.z1 by D8,FUNCT_1:def 3;
consider n2,m2 be object such that
D10: n2 in NAT & m2 in NAT & z1 = [n2,m2] by D9,ZFMISC_1:def 2;
reconsider n2,m2 as Element of NAT by D10;
reconsider N = max(max(n2,m2),max(n1,m1)) as Nat;
take N;
N >= max(n1,m1) & N >= max(n2,m2) & max(n1,m1) >= n1 & max(n1,m1) >= m1
& max(n2,m2) >= n2 & max(n2,m2) >= m2 by XXREAL_0:25; then
D13: N >= n1 & N >= m1 & N >= n2 & N >= m2 by XXREAL_0:2;
hereby let n,m be Nat;
assume n >= N & m >= N; then
n >= n1 & m >= m1 & n >= n2 & m >= m2 by D13,XXREAL_0:2; then
f1.(n,m) >= f1.(n2,m2) & f2.(n,m) >= f2.(n1,m1) by A1,A2; then
D14: SE2 - g/2 < f2.(n,m) & g - (SE2 - g/2) < f1.(n,m)
by D5,D6,D7,D8,D9,D10,XXREAL_0:2;
g - (SE2 - g/2) + (SE2 - g/2) = g by D3,XXREAL_3:22; then
g < f1.(n,m) + f2.(n,m) by D14,XXREAL_3:64;
hence g <= f.(n,m) by A5;
end;
end; then
f is P-convergent_to_+infty;
hence P-lim f = P-lim f1 + P-lim f2 by D2,A7,Def5;
end;
suppose E1: sup rng f2 = +infty;
now let p be Real;
assume E2: 0 < p; then
consider n1,m1 be Nat such that
E3: f1.(n1,m1) > p/2 by D1,Th101;
consider n2,m2 be Nat such that
E4: f2.(n2,m2) > p/2 by E1,E2,Th101;
reconsider n1,n2,m1,m2 as Element of NAT by ORDINAL1:def 12;
reconsider N = max(max(n2,m2),max(n1,m1)) as Nat;
take N;
N >= max(n1,m1) & N >= max(n2,m2) & max(n1,m1) >= n1 & max(n1,m1) >= m1
& max(n2,m2) >= n2 & max(n2,m2) >= m2 by XXREAL_0:25; then
E5: N >= n1 & N >= m1 & N >= n2 & N >= m2 by XXREAL_0:2;
hereby let n,m be Nat;
assume n >= N & m >= N; then
n >= n1 & m >= m1 & n >= n2 & m >= m2 by E5,XXREAL_0:2; then
f1.(n,m) >= f1.(n1,m1) & f2.(n,m) >= f2.(n2,m2)
by A1,A2; then
f1.(n,m) >= p/2 & f2.(n,m) >= p/2 by E3,E4,XXREAL_0:2; then
p/2 + p/2 <= f1.(n,m) + f2.(n,m) by XXREAL_3:36;
hence p <= f.(n,m) by A5;
end;
end; then
f is P-convergent_to_+infty; then
P-lim f = +infty & P-lim f1 = +infty & P-lim f2 = +infty
by A7,Def5,D1,E1,A1,A2,Th96;
hence P-lim f = P-lim f1 + P-lim f2 by XXREAL_3:def 2;
end;
end;
end;
hence P-lim f = P-lim f1 + P-lim f2;
P2:P-lim f1 = sup rng f1 & P-lim f2 = sup rng f2 by A1,A2,Th96;
now let n1,m1,n2,m2 be Nat;
assume n1 <= n2 & m1 <= m2; then
f1.(n1,m1) <= f1.(n2,m2) & f2.(n1,m1) <= f2.(n2,m2) by A1,A2; then
f1.(n1,m1) + f2.(n1,m1) <= f1.(n2,m2) + f2.(n2,m2) by XXREAL_3:36; then
f.(n1,m1) <= f1.(n2,m2) + f2.(n2,m2) by A5;
hence f.(n1,m1) <= f.(n2,m2) by A5;
end;
hence thesis by P1,P2,Th96;
end;
theorem Th104:
for f1 be without-infty Function of [:NAT,NAT:],ExtREAL,
f2 be Function of [:NAT,NAT:],ExtREAL, c be Real
st 0 <= c & (for n,m be Nat holds f2.(n,m) = c * f1.(n,m))
holds sup rng f2 = c * sup rng f1 & f2 is without-infty
proof
let f1 be without-infty Function of [:NAT,NAT:],ExtREAL,
f2 be Function of [:NAT,NAT:],ExtREAL, c be Real;
assume that
A1: 0 <= c and
A3: for n,m be Nat holds f2.(n,m) = c * f1.(n,m);
A6:dom f1 = [:NAT,NAT:] & dom f2 = [:NAT,NAT:] by FUNCT_2:def 1;
C6:now assume -infty in rng f2; then
consider z be object such that
C1: z in dom f2 & -infty = f2.z by FUNCT_1:def 3;
consider n,m be object such that
C2: n in NAT & m in NAT & z = [n,m] by C1,ZFMISC_1:def 2;
reconsider n,m as Element of NAT by C2;
f2.(n,m) = -infty by C1,C2; then
C3: c * f1.(n,m) = -infty by A3; then
C4: f1.(n,m) = -infty or f1.(n,m) = +infty by XXREAL_3:70;
z in [:NAT,NAT:] by C1; then
[n,m] in dom f1 by C2,FUNCT_2:def 1; then
-infty in rng f1 by A1,C3,C4,FUNCT_1:3;
hence contradiction by MESFUNC5:def 3;
end; then
C6a:f2 is without-infty by MESFUNC5:def 3;
now per cases by Lm8;
suppose A4: sup rng f1 in REAL;
A5: for y be UpperBound of rng f2 holds c * sup rng f1 <= y
proof
let y be UpperBound of rng f2;
reconsider y as R_eal by XXREAL_0:def 1;
per cases;
suppose A8: c = 0;
[1,1] in [:NAT,NAT:] by ZFMISC_1:87; then
f2.(1,1) <= y by A6,FUNCT_1:3,XXREAL_2:def 1; then
c * f1.(1,1) <= y by A3;
hence thesis by A8;
end;
suppose A10: c <> 0;
now let x be ExtReal;
assume x in rng f1; then
consider z be object such that
A11: z in dom f1 & x = f1.z by FUNCT_1:def 3;
consider n,m be object such that
A12: n in NAT & m in NAT & z = [n,m] by A11,ZFMISC_1:def 2;
reconsider n,m as Element of NAT by A12;
A14: f2.(n,m) in rng f2 by A11,A12,A6,FUNCT_1:3;
f2.(n,m) = c * f1.(n,m) by A3; then
c * f1.(n,m) / c <= y / c by A1,A10,A14,XXREAL_2:def 1,XXREAL_3:79;
hence x <= y / c by A10,A11,A12,XXREAL_3:88;
end; then
B14: y / c is UpperBound of rng f1 by XXREAL_2:def 1;
A15: now assume A16: y = -infty;
A17: [1,1] in [:NAT,NAT:] by ZFMISC_1:87; then
f2.(1,1) in rng f2 by A6,FUNCT_1:3; then
f2.(1,1) = -infty by A16,XXREAL_0:6,XXREAL_2:def 1; then
A19: c * f1.(1,1) = -infty by A3;
f1.(1,1) <= sup rng f1 by A6,A17,FUNCT_1:3,XXREAL_2:4; then
A20: f1.(1,1) < +infty by A4,XXREAL_0:2,9;
A21: not -infty in rng f1 by MESFUNC5:def 3;
f1.(1,1) in rng f1 by A6,A17,FUNCT_1:3;
hence contradiction by A19,A20,A21,XXREAL_3:70;
end;
per cases by A15,XXREAL_0:14;
suppose y = +infty;
hence thesis by XXREAL_0:4;
end;
suppose y in REAL; then
reconsider ry = y as Real;
reconsider SE1 = sup rng f1 as Real by A4;
y/c = ry/c; then
SE1 * c <= ry by A1,A10,B14,XXREAL_2:def 3,XREAL_1:83;
hence thesis by XXREAL_3:def 5;
end;
end;
end;
now let x be ExtReal;
assume x in rng f2; then
consider z2 be object such that
A22: z2 in dom f2 & x = f2.z2 by FUNCT_1:def 3;
consider n2,m2 be object such that
A23: n2 in NAT & m2 in NAT & z2 = [n2,m2] by A22,ZFMISC_1:def 2;
reconsider n2,m2 as Element of NAT by A23;
A24: sup rng f1 is UpperBound of rng f1 by XXREAL_2:def 3;
[n2,m2] in dom f1 by A6,ZFMISC_1:87; then
A25: f1.(n2,m2) <= sup rng f1 by A24,XXREAL_2:def 1,FUNCT_1:3;
x = f2.(n2,m2) by A22,A23; then
x = c * f1.(n2,m2) by A3;
hence x <= c * sup rng f1 by A1,A25,XXREAL_3:71;
end; then
c * sup rng f1 is UpperBound of rng f2 by XXREAL_2:def 1;
hence sup rng f2 = c * sup rng f1 by A5,XXREAL_2:def 3;
end;
suppose A30: sup rng f1 = +infty;
per cases;
suppose A27: c = 0;
A28: now let n,m be Nat;
f2.(n,m) = c * f1.(n,m) by A3;
hence f2.(n,m) = 0 by A27;
end; then
P-lim f2 = sup rng f2 by Th102;
hence sup rng f2 = c * sup rng f1 by A27,A28,Th102;
end;
suppose A29: c <> 0;
A34: now let k be Real;
reconsider k1 = k as Real;
assume C5: 0 < k; then
consider n,m be Nat such that
A31: k/c < f1.(n,m) by A1,A29,A30,Th101;
C10: f2.(n,m) = c * f1.(n,m) by A3;
n in NAT & m in NAT by ORDINAL1:def 12; then
[n,m] in dom f2 by A6,ZFMISC_1:87; then
C3: f2.(n,m) <> -infty by C6,FUNCT_1:3;
now per cases by C3,XXREAL_0:14;
suppose C7: f2.(n,m) in REAL;
f1.(n,m) > 0 & 0 >= -infty by A1,C5,A31; then
C9: f1.(n,m) in REAL or f1.(n,m) = +infty by XXREAL_0:14;
now assume f1.(n,m) = +infty; then
c * f1.(n,m) = +infty by A1,A29,XXREAL_3:def 5;
hence contradiction by A3,C7;
end; then
reconsider ES1 = f1.(n,m) as Real by C9;
k < c * ES1 by A1,A29,A31,XREAL_1:77;
hence k < f2.(n,m) by C10,XXREAL_3:def 5;
end;
suppose f2.(n,m) = +infty;
hence k < f2.(n,m) by XREAL_0:def 1,XXREAL_0:9;
end;
end;
hence ex n,m be Nat st not f2.(n,m) <= k;
end;
c * sup rng f1 = +infty by A1,A29,A30,XXREAL_3:def 5;
hence sup rng f2 = c * sup rng f1 by C6a,A34,Th101;
end;
end;
end;
hence sup rng f2 = c * sup rng f1;
thus f2 is without-infty by C6,MESFUNC5:def 3;
end;
theorem
for f1 be without-infty Function of [:NAT,NAT:],ExtREAL,
f2 be Function of [:NAT,NAT:],ExtREAL, c be Real
st 0 <= c
& ( for n1,m1,n2,m2 be Nat st n1 <= n2 & m1 <= m2 holds
f1.(n1,m1) <= f1.(n2,m2) )
& ( for n,m be Nat holds f2.(n,m) = c * f1.(n,m) )
holds
(for n1,m1,n2,m2 be Nat st n1 <= n2 & m1 <= m2 holds
f2.(n1,m1) <= f2.(n2,m2) )
& f2 is without-infty & f2 is P-convergent
& P-lim f2 = sup rng f2 & P-lim f2 = c * P-lim f1
proof
let f1 be without-infty Function of [:NAT,NAT:],ExtREAL,
f2 be Function of [:NAT,NAT:],ExtREAL, c be Real;
assume that
A1: 0 <= c and
A2: for n1,m1,n2,m2 be Nat st n1 <= n2 & m1 <= m2 holds
f1.(n1,m1) <= f1.(n2,m2) and
A3: for n,m be Nat holds f2.(n,m) = c * f1.(n,m);
A5:sup rng f1 = P-lim f1 by A2,Th96;
thus
A6: now let n1,m1,n2,m2 be Nat;
assume n1 <= n2 & m1 <= m2; then
c * f1.(n1,m1) <= c * f1.(n2,m2) by A1,A2,XXREAL_3:71; then
f2.(n1,m1) <= c * f1.(n2,m2) by A3;
hence f2.(n1,m1) <= f2.(n2,m2) by A3;
end;
thus f2 is without-infty by A1,A3,Th104;
thus f2 is P-convergent & P-lim f2 = sup rng f2 by A6,Th96;
sup rng f2 = P-lim f2 by A6,Th96;
hence thesis by A1,A3,A5,Th104;
end;