:: The Limit of a Real Function at Infinity. Halflines.
:: Real Sequence Divergent to Infinity
:: by Jaros{\l}aw Kotowicz
::
:: Received August 20, 1990
:: Copyright (c) 1990-2016 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, SEQ_1, PARTFUN1, CARD_1, ARYTM_3, XXREAL_0,
ARYTM_1, RELAT_1, TARSKI, XBOOLE_0, VALUED_1, PROB_1, XXREAL_1, VALUED_0,
XXREAL_2, FUNCT_1, SEQ_2, ORDINAL2, COMPLEX1, REAL_1, NAT_1, SQUARE_1,
SEQM_3, FUNCT_2, ORDINAL4, LIMFUNC1, ASYMPT_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
XXREAL_0, XXREAL_1, COMPLEX1, REAL_1, SQUARE_1, NAT_1, RELSET_1,
PARTFUN1, FUNCT_1, FUNCT_2, FUNCOP_1, VALUED_0, VALUED_1, SEQ_1,
COMSEQ_2, SEQ_2, SEQM_3, PROB_1, FUNCT_3, RFUNCT_1, RECDEF_1;
constructors PARTFUN1, FUNCOP_1, REAL_1, SQUARE_1, NAT_1, COMPLEX1, VALUED_1,
SEQ_2, SEQM_3, PROB_1, RCOMP_1, RFUNCT_1, RFUNCT_2, RECDEF_1, RELSET_1,
BINOP_2, RVSUM_1, COMSEQ_2, SEQ_1;
registrations ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, MEMBERED,
XXREAL_1, VALUED_0, VALUED_1, FUNCT_2, SEQ_2, SEQ_4, SQUARE_1, NAT_1,
SEQ_1, FUNCT_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions SEQ_2, MEMBERED;
equalities SQUARE_1, XBOOLE_0, PROB_1, VALUED_1;
expansions SEQ_2, MEMBERED;
theorems TARSKI, NAT_1, ABSVALUE, SEQ_1, SEQ_2, SEQM_3, SEQ_4, SQUARE_1,
RFUNCT_1, RFUNCT_2, FUNCT_1, FUNCT_2, XREAL_0, XBOOLE_0, XBOOLE_1,
XCMPLX_0, XCMPLX_1, XREAL_1, COMPLEX1, XXREAL_0, ORDINAL1, XXREAL_1,
VALUED_1, VALUED_0, NUMBERS;
schemes SEQ_1, FUNCT_2;
begin
reserve r,r1,g for Real,
n,m,k for Nat,
seq,seq1, seq2 for Real_Sequence,
f,f1,f2 for PartFunc of REAL,REAL,
x for set;
Lm1: 0 Subset of REAL equals
].-infty,r.];
coherence
proof
for x being object st x in ].-infty,r.] holds x in REAL by XREAL_0:def 1;
hence thesis by TARSKI:def 3;
end;
func right_closed_halfline r -> Subset of REAL equals
[.r,+infty.[;
coherence
proof
for x being object st x in [.r,+infty.[ holds x in REAL by XREAL_0:def 1;
hence thesis by TARSKI:def 3;
end;
func right_open_halfline r -> Subset of REAL equals
].r,+infty.[;
coherence
proof
for x being object st x in ].r,+infty.[ holds x in REAL by XREAL_0:def 1;
hence thesis by TARSKI:def 3;
end;
end;
theorem
(seq is non-decreasing implies seq is bounded_below) & (seq is
non-increasing implies seq is bounded_above)
proof
thus seq is non-decreasing implies seq is bounded_below
proof
assume
A1: seq is non-decreasing;
take seq.0-1;
let n;
seq.0-1(seq^\m).k by NAT_1:def 3;
end;
hence seq^\m is non-zero by SEQ_1:5;
end;
suppose
seq is divergent_to-infty;
then consider n such that
A4: for m st n<=m holds seq.m<0;
take n;
let m such that
A5: n<=m;
now
let k;
seq.(k+m)<0 by A4,A5,NAT_1:12;
hence (seq^\m).k<>0 by NAT_1:def 3;
end;
hence seq^\m is non-zero by SEQ_1:5;
end;
end;
hence thesis;
end;
theorem Th7:
(seq^\k is divergent_to+infty implies seq is divergent_to+infty)
& (seq^\k is divergent_to-infty implies seq is divergent_to-infty)
proof
thus seq^\k is divergent_to+infty implies seq is divergent_to+infty
proof
assume
A1: seq^\k is divergent_to+infty;
let r;
consider n1 be Nat such that
A2: for m st n1<=m holds r<(seq^\k).m by A1;
take n=n1+k;
let m;
assume n<=m;
then consider n2 be Nat such that
A3: m=n+n2 by NAT_1:10;
reconsider n2 as Element of NAT by ORDINAL1:def 12;
A4: r<(seq^\k).(n1+n2) by A2,NAT_1:12;
n1+n2+k=m by A3;
hence thesis by A4,NAT_1:def 3;
end;
assume
A5: seq^\k is divergent_to-infty;
let r;
consider n1 be Nat such that
A6: for m st n1<=m holds (seq^\k).m=0 by COMPLEX1:46;
then sqrt |.r.|>=0 by SQUARE_1:def 2;
then (sqrt |.r.|)^20 implies r(#)seq is
divergent_to+infty) & (seq is divergent_to+infty & r<0 implies r(#)seq is
divergent_to-infty) & ( r=0 implies rng (r(#)seq)={0} & r(#) seq is constant)
proof
thus seq is divergent_to+infty & r>0 implies r(#)seq is divergent_to+infty
proof
assume that
A1: seq is divergent_to+infty and
A2: r>0;
let g;
consider n such that
A3: for m st n<=m holds g/r0 implies r(#)seq is
divergent_to-infty) & (seq is divergent_to-infty & r<0 implies r(#)seq is
divergent_to+infty) & ( r=0 implies rng (r(#)seq)={0} & r(#) seq is constant)
proof
thus seq is divergent_to-infty & r>0 implies r(#)seq is divergent_to-infty
proof
assume that
A1: seq is divergent_to-infty and
A2: r>0;
let g;
consider n such that
A3: for m st n<=m holds seq.m0 & for n holds seq2.n>=
r) implies seq1(#)seq2 is divergent_to+infty
proof
assume that
A1: seq1 is divergent_to+infty and
A2: ex r st r>0 & for n holds seq2.n>=r;
consider M be Real such that
A3: M>0 and
A4: for n holds seq2.n>=M by A2;
let r;
A5: 0<=|.r.| by COMPLEX1:46;
consider n such that
A6: for m st n<=m holds |.r.|/M=r)
implies seq1(#)seq2 is divergent_to-infty
proof
assume that
A1: seq1 is divergent_to-infty and
A2: ex r st 0=r;
(-jj)(#)seq1 is divergent_to+infty by A1,Th14;
then
A3: (-jj)(#)seq1(#)seq2 is divergent_to+infty by A2,Th22;
(-1)(#)((-1)(#)seq1(#)seq2)=(-1)(#)((-1)(#)(seq1(#)seq2)) by SEQ_1:18
.=(-1)*(-1)(#)(seq1(#)seq2) by SEQ_1:23
.=seq1(#)seq2 by SEQ_1:27;
hence thesis by A3,Th13;
end;
theorem Th24:
seq1 is divergent_to-infty & seq2 is divergent_to-infty implies
seq1(#)seq2 is divergent_to+infty
proof
assume seq1 is divergent_to-infty & seq2 is divergent_to-infty;
then
A1: (-jj)(#)seq1 is divergent_to+infty &
(-jj)(#)seq2 is divergent_to+infty
by Th14;
(-1)(#)seq1(#)((-1)(#)seq2)=(-1)(#)(seq1(#)((-1)(#)seq2)) by SEQ_1:18
.=(-1)(#)((-1)(#)(seq1(#)seq2)) by SEQ_1:19
.=(-1)*(-1)(#)(seq1(#)seq2) by SEQ_1:23
.=seq1(#)seq2 by SEQ_1:27;
hence thesis by A1,Th10;
end;
theorem Th25:
(seq is divergent_to+infty or seq is divergent_to-infty) implies
abs(seq) is divergent_to+infty
proof
assume
A1: seq is divergent_to+infty or seq is divergent_to-infty;
let r;
now
per cases by A1;
suppose
seq is divergent_to+infty;
then consider n such that
A2: for m st n<=m holds |.r.|=g1;
then consider g such that
A3: 0=g by A1;
defpred X[Nat,Real] means $1<$2 & $2 in dom f & |.f.$2
-g2.|>=g;
A5: for n being Element of NAT ex r being Element of REAL st X[n,r]
proof let n be Element of NAT;
consider r such that
A6: X[n,r] by A4;
reconsider r as Real;
X[n,r] by A6;
hence thesis;
end;
consider s be Real_Sequence such that
A7: for n being Element of NAT holds X[n,s.n] from FUNCT_2:sch 3(A5);
now
let x be object;
assume x in rng s;
then ex n being Element of NAT st s.n=x by FUNCT_2:113;
hence x in dom f by A7;
end;
then
A8: rng s c=dom f;
now
let n;
A9: n in NAT by ORDINAL1:def 12;
then n=g1;
then consider g such that
A3: 0=g by A1;
defpred X[Nat,Real] means $2<-$1 & $2 in dom f & |.f.
$2-g2.|>=g;
A5: for n being Element of NAT ex r being Element of REAL st X[n,r]
proof let n being Element of NAT;
consider r such that
A6: X[n,r] by A4;
reconsider r as Real;
X[n,r] by A6;
hence thesis;
end;
consider s be Real_Sequence such that
A7: for n being Element of NAT holds X[n,s.n] from FUNCT_2:sch 3(A5);
now
let x be object;
assume x in rng s;
then ex n being Element of NAT st s.n=x by FUNCT_2:113;
hence x in dom f by A7;
end;
then
A8: rng s c=dom f;
deffunc U(Nat) = -$1;
consider s1 be Real_Sequence such that
A9: for n holds s1.n=U(n) from SEQ_1:sch 1;
now
let n;
n in NAT by ORDINAL1:def 12;
then s.n<-n by A7;
hence s.n<=s1.n by A9;
end;
then s is divergent_to-infty by A9,Th21,Th43;
then f/*s is convergent & lim(f/*s)=g2 by A2,A8;
then consider n such that
A10: for m st n<=m holds |.(f/*s).m-g2.|=f.r1;
then consider g such that
A2: for r ex r1 st r=f.r1 by A1;
defpred X[Nat,Real] means $1<$2 & $2 in dom f & g >= f.
$2;
A3: for n being Element of NAT ex r being Element of REAL st X[n,r]
proof let n be Element of NAT;
consider r such that
A4: X[n,r] by A2;
reconsider r as Real;
X[n,r] by A4;
hence thesis;
end;
consider s be Real_Sequence such that
A5: for n being Element of NAT holds X[n,s.n] from FUNCT_2:sch 3(A3);
now
let x be object;
assume x in rng s;
then ex n being Element of NAT st s.n=x by FUNCT_2:113;
hence x in dom f by A5;
end;
then
A6: rng s c=dom f;
now
let n;
A7: n in NAT by ORDINAL1:def 12;
n=g;
then consider g such that
A2: for r ex r1 st r=g by A1;
defpred X[Nat,Real] means $1<$2 & $2 in dom f & g <= f.
$2;
A3: for n being Element of NAT ex r being Element of REAL st X[n,r]
proof let n being Element of NAT;
consider r such that
A4: X[n,r] by A2;
reconsider r as Element of REAL by XREAL_0:def 1;
X[n,r] by A4;
hence thesis;
end;
consider s be Real_Sequence such that
A5: for n being Element of NAT holds X[n,s.n] from FUNCT_2:sch 3(A3);
now
let x be object;
assume x in rng s;
then ex n being Element of NAT st s.n=x by FUNCT_2:113;
hence x in dom f by A5;
end;
then
A6: rng s c=dom f;
now
let n;
A7: n in NAT by ORDINAL1:def 12;
n=f.r1;
then consider g such that
A2: for r ex r1 st r1=f.r1 by A1;
defpred X[Nat,Real] means $2<-$1 & $2 in dom f & g >= f.$2;
A3: for n being Element of NAT ex r being Element of REAL st X[n,r]
proof let n being Element of NAT ;
consider r such that
A4: X[n,r] by A2;
reconsider r as Real;
X[n,r] by A4;
hence thesis;
end;
consider s be Real_Sequence such that
A5: for n being Element of NAT holds X[n,s.n] from FUNCT_2:sch 3(A3);
now
let x be object;
assume x in rng s;
then ex n being Element of NAT st s.n=x by FUNCT_2:113;
hence x in dom f by A5;
end;
then
A6: rng s c=dom f;
consider s1 be Real_Sequence such that
A7: for n holds s1.n=U(n) from SEQ_1:sch 1;
now
let n;
A8: n in NAT by ORDINAL1:def 12;
s.n<-n by A5,A8;
hence s.n<=s1.n by A7;
end;
then s is divergent_to-infty by A7,Th21,Th43;
then f/*s is divergent_to+infty by A1,A6;
then consider n such that
A9: for m st n<=m holds g<(f/*s).m;
A10: n in NAT by ORDINAL1:def 12;
g<(f/*s).n by A9;
then g=g;
then consider g such that
A2: for r ex r1 st r1=g by A1;
defpred X[Nat,Real] means $2<-$1 & $2 in dom f & g <= f.
$2;
A3: for n being Element of NAT ex r being Element of REAL st X[n,r]
proof let n being Element of NAT ;
consider r such that
A4: X[n,r] by A2;
reconsider r as Real;
X[n,r] by A4;
hence thesis;
end;
consider s be Real_Sequence such that
A5: for n being Element of NAT holds X[n,s.n] from FUNCT_2:sch 3(A3);
now
let x be object;
assume x in rng s;
then ex n being Element of NAT st s.n=x by FUNCT_2:113;
hence x in dom f by A5;
end;
then
A6: rng s c=dom f;
consider s1 be Real_Sequence such that
A7: for n holds s1.n=U(n) from SEQ_1:sch 1;
now
let n;
A8: n in NAT by ORDINAL1:def 12;
s.n<-n by A5,A8;
hence s.n<=s1.n by A7;
end;
then s is divergent_to-infty by A7,Th21,Th43;
then f/*s is divergent_to-infty by A1,A6;
then consider n such that
A9: for m st n<=m holds (f/*s).m0 implies r(#)f is
divergent_in+infty_to+infty) & (f is divergent_in+infty_to+infty & r<0 implies
r(#)f is divergent_in+infty_to-infty) & (f is divergent_in+infty_to-infty & r>0
implies r(#)f is divergent_in+infty_to-infty) & (f is
divergent_in+infty_to-infty & r<0 implies r(#)f is divergent_in+infty_to+infty)
proof
thus f is divergent_in+infty_to+infty & r>0 implies r(#)f is
divergent_in+infty_to+infty
proof
assume that
A1: f is divergent_in+infty_to+infty and
A2: r>0;
A3: now
let seq;
assume that
A4: seq is divergent_to+infty and
A5: rng seq c=dom(r(#)f);
A6: rng seq c=dom f by A5,VALUED_1:def 5;
then f/*seq is divergent_to+infty by A1,A4;
then r(#)(f/*seq) is divergent_to+infty by A2,Th13;
hence (r(#)f)/*seq is divergent_to+infty by A6,RFUNCT_2:9;
end;
now
let r1;
consider g such that
A7: r10 implies r(#)f is
divergent_in+infty_to-infty
proof
assume that
A15: f is divergent_in+infty_to-infty and
A16: r>0;
A17: now
let seq;
assume that
A18: seq is divergent_to+infty and
A19: rng seq c=dom(r(#)f);
A20: rng seq c=dom f by A19,VALUED_1:def 5;
then f/*seq is divergent_to-infty by A15,A18;
then r(#)(f/*seq) is divergent_to-infty by A16,Th14;
hence (r(#)f)/*seq is divergent_to-infty by A20,RFUNCT_2:9;
end;
now
let r1;
consider g such that
A21: r10 implies r(#)f is
divergent_in-infty_to+infty) & (f is divergent_in-infty_to+infty & r<0 implies
r(#)f is divergent_in-infty_to-infty) & (f is divergent_in-infty_to-infty & r>0
implies r(#)f is divergent_in-infty_to-infty) & (f is
divergent_in-infty_to-infty & r<0 implies r(#)f is divergent_in-infty_to+infty)
proof
thus f is divergent_in-infty_to+infty & r>0 implies r(#)f is
divergent_in-infty_to+infty
proof
assume that
A1: f is divergent_in-infty_to+infty and
A2: r>0;
A3: now
let seq;
assume that
A4: seq is divergent_to-infty and
A5: rng seq c=dom(r(#)f);
A6: rng seq c=dom f by A5,VALUED_1:def 5;
then f/*seq is divergent_to+infty by A1,A4;
then r(#)(f/*seq) is divergent_to+infty by A2,Th13;
hence (r(#)f)/*seq is divergent_to+infty by A6,RFUNCT_2:9;
end;
now
let r1;
consider g such that
A7: g0 implies r(#)f is
divergent_in-infty_to-infty
proof
assume that
A15: f is divergent_in-infty_to-infty and
A16: r>0;
A17: now
let seq;
assume that
A18: seq is divergent_to-infty and
A19: rng seq c=dom(r(#)f);
A20: rng seq c=dom f by A19,VALUED_1:def 5;
then f/*seq is divergent_to-infty by A15,A18;
then r(#)(f/*seq) is divergent_to-infty by A16,Th14;
hence (r(#)f)/*seq is divergent_to-infty by A20,RFUNCT_2:9;
end;
now
let r1;
consider g such that
A21: g Real means
:Def12:
for seq st seq is divergent_to+infty & rng seq c= dom f
holds f/*seq is convergent & lim(f/*seq)= it;
existence
by A1;
uniqueness
proof
defpred X[Nat,Real] means $1<$2 & $2 in dom f;
let g1,g2 be Real such that
A2: for seq st seq is divergent_to+infty & rng seq c= dom f holds f/*
seq is convergent & lim(f/*seq)=g1 and
A3: for seq st seq is divergent_to+infty & rng seq c= dom f holds f/*
seq is convergent & lim(f/*seq)=g2;
A4: for n being Element of NAT ex r being Element of REAL st X[n,r]
proof let n being Element of NAT ;
consider r such that
A5: X[n,r] by A1;
reconsider r as Real;
X[n,r] by A5;
hence thesis;
end;
consider s2 be Real_Sequence such that
A6: for n being Element of NAT holds X[n,s2.n] from FUNCT_2:sch 3(A4);
A7: rng s2 c= dom f
proof
let x be Real;
assume x in rng s2;
then ex n being Element of NAT st x=s2.n by FUNCT_2:113;
hence thesis by A6;
end;
now
let n;
A8: n in NAT by ORDINAL1:def 12;
then n Real means
:Def13:
for seq st seq is
divergent_to-infty & rng seq c= dom f holds f/*seq is convergent & lim(f/*seq)=
it;
existence
by A1;
uniqueness
proof
deffunc U(Nat) = -$1;
defpred X[Nat,Real] means $2<-$1 & $2 in dom f;
let g1,g2 be Real such that
A2: for seq st seq is divergent_to-infty & rng seq c= dom f holds f/*
seq is convergent & lim(f/*seq)=g1 and
A3: for seq st seq is divergent_to-infty & rng seq c= dom f holds f/*
seq is convergent & lim(f/*seq)=g2;
consider s2 be Real_Sequence such that
A4: for n holds s2.n=U(n) from SEQ_1:sch 1;
A5: for n being Element of NAT ex r being Element of REAL st X[n,r]
proof let n being Element of NAT ;
consider r such that
A6: X[n,r] by A1;
reconsider r as Real;
X[n,r] by A6;
hence thesis;
end;
consider s1 be Real_Sequence such that
A7: for n being Element of NAT holds X[n,s1.n] from FUNCT_2:sch 3(A5);
A8: rng s1 c= dom f
proof
let x be Real;
assume x in rng s1;
then ex n being Element of NAT st x=s1.n by FUNCT_2:113;
hence thesis by A7;
end;
now
let n;
n in NAT by ORDINAL1:def 12;
then s1.n<-n by A7;
hence s1.n<=s2.n by A4;
end;
then
A9: s1 is divergent_to-infty by A4,Th21,Th43;
then lim(f/*s1)=g1 by A2,A8;
hence thesis by A3,A9,A8;
end;
end;
theorem
f is convergent_in-infty implies (lim_in-infty f=g iff for g1 st 0=g1;
defpred X[Nat,Real] means $2<-$1 & $2 in dom f & |.f.
$2-g.|>=g1;
A6: for n being Element of NAT ex r being Element of REAL st X[n,r]
proof let n being Element of NAT ;
consider r such that
A7: X[n,r] by A5;
reconsider r as Real;
X[n,r] by A7;
hence thesis;
end;
consider s be Real_Sequence such that
A8: for n being Element of NAT holds X[n,s.n] from FUNCT_2:sch 3(A6);
now
let x be object;
assume x in rng s;
then ex n being Element of NAT st s.n=x by FUNCT_2:113;
hence x in dom f by A8;
end;
then
A9: rng s c=dom f;
now
let n;
n in NAT by ORDINAL1:def 12;
then s.n<-n by A8;
hence s.n<=s1.n by A3;
end;
then s is divergent_to-infty by A3,Th21,Th43;
then f/*s is convergent & lim(f/*s)=g by A1,A2,A9,Def13;
then consider n such that
A10: for m st n<=m holds |.(f/*s).m-g.|=g1;
defpred X[Nat,Real] means $1<$2 & $2 in dom f & |.f.$2
-g.|>=g1;
A5: for n being Element of NAT ex r being Element of REAL st X[n,r]
proof let n being Element of NAT ;
consider r such that
A6: X[n,r] by A4;
reconsider r as Real;
X[n,r] by A6;
hence thesis;
end;
consider s be Real_Sequence such that
A7: for n being Element of NAT holds X[n,s.n] from FUNCT_2:sch 3(A5);
now
let x be object;
assume x in rng s;
then ex n being Element of NAT st s.n=x by FUNCT_2:113;
hence x in dom f by A7;
end;
then
A8: rng s c=dom f;
now
let n;
A9: n in NAT by ORDINAL1:def 12;
then n0 implies f^
is convergent_in+infty & lim_in+infty(f^)=(lim_in+infty f)"
proof
assume that
A1: f is convergent_in+infty and
A2: f"{0}={} and
A3: (lim_in+infty f)<>0;
A4: dom f= dom f\f"{0} by A2
.=dom(f^) by RFUNCT_1:def 2;
A5: now
let seq;
assume that
A6: seq is divergent_to+infty and
A7: rng seq c=dom(f^);
A8: f/*seq is convergent & lim(f/*seq)=lim_in+infty f by A1,A4,A6,A7,Def12;
then (f/*seq)" is convergent by A3,A7,RFUNCT_2:11,SEQ_2:21;
hence (f^)/*seq is convergent by A7,RFUNCT_2:12;
thus lim((f^)/*seq)=lim((f/*seq)") by A7,RFUNCT_2:12
.=(lim_in+infty f)" by A3,A7,A8,RFUNCT_2:11,SEQ_2:22;
end;
for r ex g st r0 & (for r ex g st r
0) implies f^ is convergent_in+infty & lim_in+infty(f^)=
(lim_in+infty f)"
proof
assume that
A1: f is convergent_in+infty and
A2: lim_in+infty f<>0 and
A3: for r ex g st r0;
A4: now
let seq such that
A5: seq is divergent_to+infty and
A6: rng seq c=dom(f^);
dom(f^)=dom f\f"{0} & dom f\f"{0}c=dom f by RFUNCT_1:def 2,XBOOLE_1:36;
then rng seq c=dom f by A6;
then
A7: f/*seq is convergent & lim(f/*seq)=lim_in+infty f by A1,A5,Def12;
then (f/*seq)" is convergent by A2,A6,RFUNCT_2:11,SEQ_2:21;
hence (f^)/*seq is convergent by A6,RFUNCT_2:12;
thus lim((f^)/*seq)=lim((f/*seq)") by A6,RFUNCT_2:12
.=(lim_in+infty f)" by A2,A6,A7,RFUNCT_2:11,SEQ_2:22;
end;
now
let r;
consider g such that
A8: r0 by A3;
take g;
not f.g in {0} by A10,TARSKI:def 1;
then not g in f"{0} by FUNCT_1:def 7;
then g in dom f\f"{0} by A9,XBOOLE_0:def 5;
hence r 0 & (for r ex g st r0 and
A3: for r ex g st r0 by A7,A9,TARSKI:def 1,XBOOLE_0:def 5;
end;
then
A10: f2^ is convergent_in+infty by A2,Th86;
A11: lim_in+infty(f2^)=(lim_in+infty f2)" by A2,A6,Th86;
A12: now
let r;
consider g such that
A13: r0 implies f^
is convergent_in-infty & lim_in-infty(f^)=(lim_in-infty f)"
proof
assume that
A1: f is convergent_in-infty and
A2: f"{0}={} and
A3: (lim_in-infty f)<>0;
A4: dom f= dom f\f"{0} by A2
.=dom(f^) by RFUNCT_1:def 2;
A5: now
let seq;
assume that
A6: seq is divergent_to-infty and
A7: rng seq c=dom(f^);
A8: f/*seq is convergent & lim(f/*seq)=lim_in-infty f by A1,A4,A6,A7,Def13;
then (f/*seq)" is convergent by A3,A7,RFUNCT_2:11,SEQ_2:21;
hence (f^)/*seq is convergent by A7,RFUNCT_2:12;
thus lim((f^)/*seq)=lim((f/*seq)") by A7,RFUNCT_2:12
.=(lim_in-infty f)" by A3,A7,A8,RFUNCT_2:11,SEQ_2:22;
end;
for r ex g st g0 & (for r ex g st g
0) implies f^ is convergent_in-infty & lim_in-infty(f^)=
(lim_in-infty f)"
proof
assume that
A1: f is convergent_in-infty and
A2: lim_in-infty f<>0 and
A3: for r ex g st g0;
A4: now
let seq such that
A5: seq is divergent_to-infty and
A6: rng seq c=dom(f^);
dom(f^)=dom f\f"{0} & dom f\f"{0}c=dom f by RFUNCT_1:def 2,XBOOLE_1:36;
then rng seq c=dom f by A6;
then
A7: f/*seq is convergent & lim(f/*seq)=lim_in-infty f by A1,A5,Def13;
then (f/*seq)" is convergent by A2,A6,RFUNCT_2:11,SEQ_2:21;
hence (f^)/*seq is convergent by A6,RFUNCT_2:12;
thus lim((f^)/*seq)=lim((f/*seq)") by A6,RFUNCT_2:12
.=(lim_in-infty f)" by A2,A6,A7,RFUNCT_2:11,SEQ_2:22;
end;
now
let r;
consider g such that
A8: g0 by A3;
take g;
not f.g in {0} by A10,TARSKI:def 1;
then not g in f"{0} by FUNCT_1:def 7;
then g in dom f\f"{0} by A9,XBOOLE_0:def 5;
hence g 0 & (for r ex g st g0 and
A3: for r ex g st g0 by A7,A9,TARSKI:def 1,XBOOLE_0:def 5;
end;
then
A10: f2^ is convergent_in-infty by A2,Th95;
A11: lim_in-infty(f2^)=(lim_in-infty f2)" by A2,A6,Th95;
A12: now
let r;
consider g such that
A13: g0) implies f^ is convergent_in+infty &
lim_in+infty(f^)=0
proof
assume that
A1: f is divergent_in+infty_to+infty or f is divergent_in+infty_to-infty and
A2: for r ex g st r0;
A3: dom(f^)=dom f\f"{0} by RFUNCT_1:def 2;
A4: now
let r;
consider g such that
A5: r0 by A2;
take g;
not f.g in {0} by A6,TARSKI:def 1;
then not g in f"{0} by FUNCT_1:def 7;
hence r0) implies f^ is convergent_in-infty &
lim_in-infty(f^)=0
proof
assume that
A1: f is divergent_in-infty_to+infty or f is divergent_in-infty_to-infty and
A2: for r ex g st g0;
A3: dom(f^)=dom f\f"{0} by RFUNCT_1:def 2;
A4: now
let r;
consider g such that
A5: g0 by A2;
take g;
not f.g in {0} by A6,TARSKI:def 1;
then not g in f"{0} by FUNCT_1:def 7;
hence g0) & (ex r st for g st g in dom f /\ right_open_halfline(r)
holds 0<=f.g) implies f^ is divergent_in+infty_to+infty
proof
assume that
A1: f is convergent_in+infty & lim_in+infty f=0 and
A2: for r ex g st r0;
given r such that
A3: for g st g in dom f/\ right_open_halfline(r) holds 0<=f.g;
thus for r1 ex g1 st r10 by A2;
take g1;
thus r10 by A14,SEQ_1:5;
hence 0<(f/*(s^\k)).n by A12,A10,A16,FUNCT_2:108,XBOOLE_1:1,A15;
end;
then
A17: for n holds 0<=n implies 0<(f/*(s^\k)).n;
s^\k is divergent_to+infty by A7,Th26;
then f/*(s^\k) is convergent & lim(f/*(s^\k))=0 by A1,A13,Def12;
then
A18: (f/*(s^\k))" is divergent_to+infty by A17,Th35;
(f/*(s^\k))"=((f/*s)^\k)" by A8,A11,VALUED_0:27,XBOOLE_1:1
.=((f/*s)")^\k by SEQM_3:18
.=((f^)/*s)^\k by A8,RFUNCT_2:12;
hence thesis by A18,Th7;
end;
theorem
f is convergent_in+infty & lim_in+infty f=0 & (for r ex g st r0) & (ex r st for g st g in dom f /\ right_open_halfline(r)
holds f.g<=0) implies f^ is divergent_in+infty_to-infty
proof
assume that
A1: f is convergent_in+infty & lim_in+infty f=0 and
A2: for r ex g st r0;
given r such that
A3: for g st g in dom f/\right_open_halfline(r) holds f.g<=0;
thus for r1 ex g1 st r10 by A2;
take g1;
thus r10 by A14,SEQ_1:5;
hence (f/*(s^\k)).n<0 by A12,A10,A16,FUNCT_2:108,XBOOLE_1:1,A15;
end;
then
A17: for n holds 0<=n implies (f/*(s^\k)).n<0;
s^\k is divergent_to+infty by A7,Th26;
then f/*(s^\k) is convergent & lim(f/*(s^\k))=0 by A1,A13,Def12;
then
A18: (f/*(s^\k))" is divergent_to-infty by A17,Th36;
(f/*(s^\k))"=((f/*s)^\k)" by A8,A11,VALUED_0:27,XBOOLE_1:1
.=((f/*s)")^\k by SEQM_3:18
.=((f^)/*s)^\k by A8,RFUNCT_2:12;
hence thesis by A18,Th7;
end;
theorem
f is convergent_in-infty & lim_in-infty f=0 & (for r ex g st g0) & (ex r st for g st g in dom f /\ left_open_halfline(r)
holds 0<=f.g) implies f^ is divergent_in-infty_to+infty
proof
assume that
A1: f is convergent_in-infty & lim_in-infty f=0 and
A2: for r ex g st g0;
given r such that
A3: for g st g in dom f/\left_open_halfline(r) holds 0<=f.g;
thus for r1 ex g1 st g10 by A2;
take g1;
thus g1(f/*(s^\k)).n by A14,SEQ_1:5;
hence 0<(f/*(s^\k)).n by A12,A10,A16,FUNCT_2:108,XBOOLE_1:1,A15;
end;
then
A17: for n holds 0<=n implies 0<(f/*(s^\k)).n;
s^\k is divergent_to-infty by A7,Th27;
then f/*(s^\k) is convergent & lim(f/*(s^\k))=0 by A1,A13,Def13;
then
A18: (f/*(s^\k))" is divergent_to+infty by A17,Th35;
(f/*(s^\k))"=((f/*s)^\k)" by A8,A11,VALUED_0:27,XBOOLE_1:1
.=((f/*s)")^\k by SEQM_3:18
.=((f^)/*s)^\k by A8,RFUNCT_2:12;
hence thesis by A18,Th7;
end;
theorem
f is convergent_in-infty & lim_in-infty f=0 & (for r ex g st g0) & (ex r st for g st g in dom f /\ left_open_halfline(r)
holds f.g<=0) implies f^ is divergent_in-infty_to-infty
proof
assume that
A1: f is convergent_in-infty & lim_in-infty f=0 and
A2: for r ex g st g0;
given r such that
A3: for g st g in dom f/\left_open_halfline(r) holds f.g<=0;
thus for r1 ex g1 st g10 by A2;
take g1;
thus g10 by A14,SEQ_1:5;
hence (f/*(s^\k)).n<0 by A12,A10,A16,FUNCT_2:108,XBOOLE_1:1,A15;
end;
then
A17: for n holds 0<=n implies (f/*(s^\k)).n<0;
s^\k is divergent_to-infty by A7,Th27;
then f/*(s^\k) is convergent & lim(f/*(s^\k))=0 by A1,A13,Def13;
then
A18: (f/*(s^\k))" is divergent_to-infty by A17,Th36;
(f/*(s^\k))"=((f/*s)^\k)" by A8,A11,VALUED_0:27,XBOOLE_1:1
.=((f/*s)")^\k by SEQM_3:18
.=((f^)/*s)^\k by A8,RFUNCT_2:12;
hence thesis by A18,Th7;
end;
theorem
f is convergent_in+infty & lim_in+infty f=0 & (ex r st for g st g in
dom f /\ right_open_halfline(r) holds 0f.g2 by A3;
then not f.g2 in {0} by TARSKI:def 1;
then not g2 in f"{0} by FUNCT_1:def 7;
then g2 in dom f\f"{0} by A7,XBOOLE_0:def 5;
hence g2 in dom(f^) by RFUNCT_1:def 2;
end;
suppose
A8: r<=g1;
consider g2 such that
A9: g1f.g2 by A3;
then not f.g2 in {0} by TARSKI:def 1;
then not g2 in f"{0} by FUNCT_1:def 7;
then g2 in dom f\f"{0} by A10,XBOOLE_0:def 5;
hence g2 in dom(f^) by RFUNCT_1:def 2;
end;
end;
hence thesis;
end;
let s be Real_Sequence;
assume that
A11: s is divergent_to+infty and
A12: rng s c=dom (f^);
consider k such that
A13: for n st k<=n holds rf.g2 by A3;
then not f.g2 in {0} by TARSKI:def 1;
then not g2 in f"{0} by FUNCT_1:def 7;
then g2 in dom f\f"{0} by A7,XBOOLE_0:def 5;
hence g2 in dom(f^) by RFUNCT_1:def 2;
end;
suppose
A8: r<=g1;
consider g2 such that
A9: g1f.g2 by A3;
then not f.g2 in {0} by TARSKI:def 1;
then not g2 in f"{0} by FUNCT_1:def 7;
then g2 in dom f\f"{0} by A10,XBOOLE_0:def 5;
hence g2 in dom(f^) by RFUNCT_1:def 2;
end;
end;
hence thesis;
end;
let s be Real_Sequence;
assume that
A11: s is divergent_to+infty and
A12: rng s c=dom (f^);
consider k such that
A13: for n st k<=n holds rf.g2 by A3;
then not f.g2 in {0} by TARSKI:def 1;
then not g2 in f"{0} by FUNCT_1:def 7;
then g2 in dom f\f"{0} by A7,XBOOLE_0:def 5;
hence g2 in dom(f^) by RFUNCT_1:def 2;
end;
suppose
A8: r<=g1;
consider g2 such that
A9: g2f.g2 by A3;
then not f.g2 in {0} by TARSKI:def 1;
then not g2 in f"{0} by FUNCT_1:def 7;
then g2 in dom f\f"{0} by A10,XBOOLE_0:def 5;
hence g2 in dom(f^) by RFUNCT_1:def 2;
end;
end;
hence thesis;
end;
let s be Real_Sequence;
assume that
A11: s is divergent_to-infty and
A12: rng s c=dom (f^);
consider k such that
A13: for n st k<=n holds s.nf.g2 by A3;
then not f.g2 in {0} by TARSKI:def 1;
then not g2 in f"{0} by FUNCT_1:def 7;
then g2 in dom f\f"{0} by A7,XBOOLE_0:def 5;
hence g2 in dom(f^) by RFUNCT_1:def 2;
end;
suppose
A8: r<=g1;
consider g2 such that
A9: g2f.g2 by A3;
then not f.g2 in {0} by TARSKI:def 1;
then not g2 in f"{0} by FUNCT_1:def 7;
then g2 in dom f\f"{0} by A10,XBOOLE_0:def 5;
hence g2 in dom(f^) by RFUNCT_1:def 2;
end;
end;
hence thesis;
end;
let s be Real_Sequence;
assume that
A11: s is divergent_to-infty and
A12: rng s c=dom (f^);
consider k such that
A13: for n st k<=n holds s.n