Real_Sequence means :Def2:
it.n = (-1) |^n * (r|^(2*n+1))/ (2*n+1);
existence
proof
defpred P[Nat,object] means $2=(-1) |^$1 * (r|^(2*$1+1))/ (2*$1+1);
A1: for n be Element of NAT ex y be Element of REAL st P[n,y]
proof
let n be Element of NAT;
(-1) |^n * (r|^(2*n+1))/ (2*n+1) in REAL by XREAL_0:def 1;
hence thesis;
end;
consider f be Function of NAT,REAL such that
A2: for x being Element of NAT holds P[x,f.x] from FUNCT_2:sch 3(A1);
take f;
let i be Nat;
i in NAT by ORDINAL1:def 12;
hence thesis by A2;
end;
uniqueness
proof
let a1,a2 be Real_Sequence such that
A3: for i be Nat holds a1.i = (-1) |^i * (r|^(2*i+1))/ (2*i+1)
and
A4: for i be Nat holds a2.i = (-1) |^i * (r|^(2*i+1))/ (2*i+1);
now let y be object;
assume y in NAT;
then reconsider i=y as Nat;
thus a1.y = (-1) |^i * (r|^(2*i+1))/ (2*i+1) by A3
.= a2.y by A4;
end;
hence thesis;
end;
end;
definition
func Leibniz_Series -> Real_Sequence equals
Leibniz_Series_of 1;
coherence;
end;
theorem Th9:
r in [.-1,1.] implies abs(Leibniz_Series_of r) is
nonnegative-yielding non-increasing convergent
& lim abs (Leibniz_Series_of r) = 0
proof
set rL=Leibniz_Series_of r,A=abs rL;
assume
A1:r in [.-1,1.];
A2:dom A = dom rL & dom rL=NAT by VALUED_1:def 11,FUNCT_2:def 1;
thus A is nonnegative-yielding;
A3: A.n = |.r.| |^ (2*n+1)/ (2*n+1)
proof
--1=1;
then |.-1.| = 1 by ABSVALUE:def 1;
then
A4: |.(-1)|^n.| = 1 |^n by TAYLOR_2:1;
A5: A.n = |.rL.n.| by A2,VALUED_1:def 11,ORDINAL1:def 12;
rL.n = (-1)|^n * (r|^(2*n+1))/ (2*n+1) by Def2;
hence A.n = |.(-1)|^n *(r|^(2*n+1)).|/ |.(2*n+1).| by COMPLEX1:67,A5
.= 1*|.(r|^(2*n+1)).|/ |.(2*n+1).| by A4,COMPLEX1:65
.= 1*(|.r.| |^(2*n+1)) / |.(2*n+1).| by TAYLOR_2:1
.= |.r.| |^(2*n+1) / (2*n+1) by ABSVALUE:def 1;
end;
-1 <=r <= 1 by A1,XXREAL_1:1;
then
A6: |.r.| <= 1 by ABSVALUE:5;
A.n >= A.(n+1)
proof
set n1=n+1;
A7: A.n1 = |.r.| |^ (2*n1+1)*1/(2*n1+1) by A3;
A8: |.r.| >=0 by COMPLEX1:46;
|.(r|^(2*n+1)).| = |.r.||^(2*n+1) by TAYLOR_2:1;
then
A9: |.r.| |^(2*n+1)>=0 by COMPLEX1:46;
A10: |.r.| * |.r.| <=1*1 by A8,A6,XREAL_1:66;
|.r.| |^ (2*n1+1) = |.r.| * |.r.| |^ (2*n+1+1) by NEWTON:6
.= |.r.| *( |.r.| * |.r.| |^(2*n+1)) by NEWTON:6
.= (|.r.|*|.r.|) * (|.r.| |^(2*n+1));
then
A11: |.r.| |^ (2*n1+1) <= |.r.| |^(2*n+1) *1 by A9,A10,XREAL_1:66;
|.(r|^(2*n1+1)).| = |.r.||^(2*n1+1) by TAYLOR_2:1;
then
A12: |.r.| |^ (2*n1+1)>=0 by COMPLEX1:46;
2*n+1 <=2*n+1+1 by NAT_1:13;
then 2*n+1 < 2*n+1+1+1 by NAT_1:13;
then 1/(2*n+1) >= 1/(2*n1+1) by XREAL_1:76;
then |.r.| |^ (2*n+1)*1/(2*n+1) >= |.r.| |^ (2*n1+1) *1/(2*n1+1)
by A12,A11,XREAL_1:66;
hence thesis by A3,A7;
end;
hence A is non-increasing by VALUED_1:def 16;
set C=seq_const 0;
A13: lim C =0;
deffunc F(Nat) = (1/2) / ($1 +1/2);
consider f be Real_Sequence such that
A14: f.n=F(n) from SEQ_1:sch 1;
A15:f is convergent & lim f =0 by A14,SEQ_4:31;
C.n<=A.n<=f.n
proof
A16: C.n = 0 by SEQ_1:57;
A17: |.r.| >=0 by COMPLEX1:46;
A18: 0 |^(2*n+1)=0 by NEWTON:11,NAT_1:11;
|.r.| >0 implies
|.r.| |^ (2*n+1) <= 1 |^ (2*n+1) by A6,PREPOWER:9;
then
A19: |.r.| |^ (2*n+1) <= 1 by A18,A17;
|.(r|^(2*n+1)).| = |.r.||^(2*n+1) by TAYLOR_2:1;
then
A20: |.r.| |^(2*n+1)>=0 by COMPLEX1:46;
(2*n+1)/2=n+1/2;
then
A21: 1/(2*n+1) = F(n) by XCMPLX_1:55
.=f.n by A14;
A.n = |.r.| |^ (2*n+1)/ (2*n+1) by A3
.= |.r.| |^ (2*n+1)*(2*n+1)";
hence thesis by A19, XREAL_1:64,A20,A16,A21;
end;
hence thesis by A13,A15,SEQ_2:19,20;
end;
theorem Th10:
(r >=0 implies alternating_series abs(Leibniz_Series_of r)
= Leibniz_Series_of r) &
(r < 0 implies (-1)(#) alternating_series abs(Leibniz_Series_of r)
= Leibniz_Series_of r)
proof
set rL=Leibniz_Series_of r, A=abs rL,aA=alternating_series A;
A1:dom A = dom rL & dom rL=NAT by VALUED_1:def 11,FUNCT_2:def 1;
A2: aA.n = (-1)|^n * (|.r.| |^(2*n+1) / (2*n+1))
proof
--1 = 1;
then |.-1.| = 1 by ABSVALUE:def 1;
then
A3: |.(-1)|^n.| = 1 |^n by TAYLOR_2:1;
A4: A.n = |.rL.n.| by A1,VALUED_1:def 11,ORDINAL1:def 12;
rL.n = (-1)|^n * (r|^(2*n+1))/ (2*n+1) by Def2;
then A.n = |.(-1)|^n *(r|^(2*n+1)).|/ |.(2*n+1).|
by COMPLEX1:67,A4
.= 1*|.(r|^(2*n+1)).|/ |.(2*n+1).| by A3,COMPLEX1:65
.= 1*(|.r.| |^(2*n+1)) / |.(2*n+1).| by TAYLOR_2:1
.= |.r.| |^(2*n+1) / (2*n+1) by ABSVALUE:def 1;
hence thesis by Def1;
end;
thus r>=0 implies aA=rL
proof
assume r>=0;
then
A5: |.r.| = r by ABSVALUE:def 1;
now let n;
thus aA.n = (-1)|^n * (r |^(2*n+1) / (2*n+1)) by A2,A5
.=(-1)|^n * r |^(2*n+1) / (2*n+1)
.= rL.n by Def2;
end;
hence thesis;
end;
assume r <0;
then
A6: |.r.|=-r by ABSVALUE:def 1;
now let n;
|.r.| |^(2*n+1) = - (r |^ (2*n+1)) by A6,POWER:2;
then aA.n = (-1)|^n * ((- (r |^ (2*n+1))) / (2*n+1)) by A2
.= - (-1)|^n * (r |^ (2*n+1)) / (2*n+1)
.=-rL.n by Def2;
hence rL.n = (-1)*aA.n
.=((-1)(#)aA).n by SEQ_1:9;
end;
hence thesis;
end;
theorem Th11:
r in [.-1,1.] implies Leibniz_Series_of r is summable
proof
set rL=Leibniz_Series_of r,A=abs rL,aA=alternating_series A;
assume r in [.-1,1.];
then A is nonnegative-yielding non-increasing convergent
& lim A = 0 by Th9;
then
A1: aA is summable by Th8;
per cases;
suppose r >=0;
hence thesis by Th10,A1;
end;
suppose r <0;
then rL = (-1)(#)aA by Th10;
hence thesis by A1,SERIES_1:10;
end;
end;
theorem Th12:
A=[.0,r.] & r >=0 implies
arctan.r = Partial_Sums(Leibniz_Series_of r).n +
integral( (-1)|^(n+1) (#) ( #Z (2*(n+1))/ ( #Z 0 + #Z 2)),A)
proof
set Z0 = #Z0,Z2 = #Z2,rL = Leibniz_Series_of r;
assume A=[.0,r.] & r >=0;
then
A1: upper_bound A = r & lower_bound A = 0 by JORDAN5A:19;
defpred P[Nat] means arctan.r = Partial_Sums(rL).$1+
integral((-1)|^($1+1) (#) ( #Z (2*($1+1)) / ( Z0 + Z2)),A);
A2: P[0]
proof
A3: integral( Z0 / ( Z0 + Z2),A) = arctan.r - arctan.0 by Th5,A1
.= arctan.r by SIN_COS9:43;
A4: 2*0+1=1;
A5: ((-1)|^0) * ((1*(r |^ 1)) -(1/1*(0 |^ 1)))
= ((-1) |^0) * (r|^1/ 1)
.= rL.0 by A4,Def2;
(-1)|^0 = 1 by NEWTON:4;
then (-1)|^0 (#) ( Z0/(Z0+Z2)) = Z0/(Z0+Z2) by RFUNCT_1:21;
then arctan.r = rL.0 + integral((-1)|^(0+1) (#)
( #Z (2*(0+1)) / ( #Z 0 + #Z 2)),A) by A3,A1,A4,Th6,A5;
hence thesis by SERIES_1:def 1;
end;
A6: P[i] implies P[i+1]
proof
set i1=i+1,i11=i1+1;
assume
A7: P[i];
A8: 0 |^ (2*i1+1) =0 by NEWTON:11,NAT_1:11;
((-1)|^i1) * (((1/(2*i1+1))*(r |^ (2*i1+1))) -((1/(2*i1+1))*0))
= (-1)|^i1 * (r |^ (2*i1+1))/(2*i1+1)
.= rL.i1 by Def2;
then integral( (-1)|^i1 (#) ( #Z (2*i1) / ( Z0 + Z2)),A)=
rL.i1 +
integral( (-1)|^i11 (#) ( #Z (2*i11) / ( Z0 + Z2)),A) by A8,Th6,A1;
then arctan.r = Partial_Sums(rL).i+rL.i1 +
integral( (-1)|^i11 (#) ( #Z (2*i11) / ( Z0 + Z2)),A) by A7;
hence thesis by SERIES_1:def 1;
end;
P[i] from NAT_1:sch 2(A2,A6);
hence thesis;
end;
theorem Th13:
0 <= r <= 1 implies arctan.r = Sum (Leibniz_Series_of r)
proof
set rL=Leibniz_Series_of r,P=Partial_Sums rL,A=arctan.r;
deffunc I(Nat)=#Z (2*($1))/ ( #Z 0 + #Z 2);
assume
A1: 0<=r<=1;
then r in [.-1,1.] by XXREAL_1:1;
then
A2: P is convergent by Th11,SERIES_1:def 2;
for s st 0 ~~0)
by NAT_1:11,A1,NEWTON:11;
then r |^ (2*m1+1) <= 1 by PREPOWER:9,A1;
then 1/(2*m1+1)*( r |^ (2*m1+1)) <= 1/(2*m1+1) * 1 by XREAL_1:64;
then A11: |. P.m -A.| <= 1/(2*m1+1) by A10,XXREAL_0:2;
m1 <= 1+m1+m1 by NAT_1:11;
then m < (2*m1+1) by NAT_1:13;
then n < (2*m1+1) by A5,XXREAL_0:2;
then 1/s < (2*m1+1) by A4,XXREAL_0:2;
then 1/s*s < (2*m1+1)*s & 1/s*s = 1 by XREAL_1:68,A3,XCMPLX_1:87;
then s > 1/ (2*m1+1) by XREAL_1:83;
hence thesis by A11,XXREAL_0:2;
end;
then A = lim P by A2,SEQ_2:def 7;
hence thesis by SERIES_1:def 3;
end;
::$N Leibniz Series for $\pi$
theorem Th14:
PI/4 = Sum Leibniz_Series by Th13,SIN_COS9:39;
theorem Th15:
Partial_Sums(Leibniz_Series).(2*n+1)
<= Sum Leibniz_Series <=
Partial_Sums(Leibniz_Series).(2*n)
proof
set L=Leibniz_Series,A=abs L,aa = alternating_series A;
1 in [.-1,1.] by XXREAL_1:1;
then
A1: A is nonnegative-yielding non-increasing convergent &
lim A =0 by Th9;
aa = L by Th10;
hence thesis by A1,Th8;
end;
theorem Th16:
Partial_Sums(Leibniz_Series).1 = 2/3 &
(n is odd implies
Partial_Sums(Leibniz_Series).(n+2) =
Partial_Sums(Leibniz_Series).n + 2/(4*n^2 + 16*n +15))
proof
set L=Leibniz_Series,P=Partial_Sums L;
set n1=n+1,n2=n+2;
A1: P.0 = L.0 by SERIES_1:def 1
.= (-1) |^0 * (1|^(2*0+1))/ (2*0+1) by Def2
.= 1;
L.1 = (-1) |^1 * (1|^(2*1+1))/ (2*1+1) by Def2
.= -1/3;
then P.(0+1) = -1/3+ 1 by A1,SERIES_1:def 1;
hence P.1 = 2/3;
assume
A2: n is odd;
A3:P.(n1+1) = P.n1 + L.n2 by SERIES_1:def 1
.= P.n + L.n1 + L.n2 by SERIES_1:def 1;
A4:L.n1 = (-1) |^n1 * (1|^(2*n1+1))/ (2*n1+1) by Def2
.= 1*(1|^(2*n1+1))/ (2*n1+1) by A2,POLYFORM:8
.=(1*(2*n2+1))/((2*n1+1)*(2*n2+1)) by XCMPLX_1:91;
L.n2 = (-1) |^n2 * (1|^(2*n2+1))/ (2*n2+1) by Def2
.= (-1)*(1|^(2*n2+1))/ (2*n2+1) by A2,POLYFORM:9
.=-1/(2*n2+1)
.=-(1*(2*n1+1))/((2*n2+1)*(2*n1+1)) by XCMPLX_1:91;
hence thesis by A3,A4;
end;
::$N $\pi$ Approximation
theorem
313/100 < PI < 315/100
proof
set L=Leibniz_Series,P=Partial_Sums L;
deffunc P(Nat)=2/(4*$1*$1 + 16*$1 +15);
deffunc P10(Nat) = P($1)+P($1+2) + P($1+4)+P($1+6)+P($1+8);
deffunc P50(Nat) = P10($1)+P10($1+10)+P10($1+20)+
P10($1+30)+P10($1+40);
A1:n is odd implies P.(n+2) = P.n + P(n)
proof
assume n is odd;
then P.(n+2) = P.n + 2/(4*n^2 + 16*n +15) by Th16;
hence thesis;
end;
A2: n is odd implies P.(n+10) = P.n +P10(n)
proof
assume A3: n is odd;
8=4*2;
then A4: P.(n+8+2) = P.(n+8)+P(n+8) by A1,A3;
6=3*2;
then A5: P.(n+6+2) = P.(n+6)+P(n+6) by A1,A3;
4=2*2;
then A6: P.(n+4+2) = P.(n+4)+P(n+4) by A1,A3;
A7: P.(n+2+2) = P.(n+2)+P(n+2) by A3,A1;
P.(n+2) = P.(n)+P(n) by A3,A1;
hence thesis by A4,A5,A6,A7;
end;
A8: n is odd implies P.(n+50) = P.n +P50(n)
proof
assume A9: n is odd;
40=20*2;
then A10: P.(n+40+10) = P.(n+40)+P10(n+40) by A2,A9;
30=15*2;
then A11: P.(n+30+10) = P.(n+30)+P10(n+30) by A2,A9;
20=10*2;
then A12: P.(n+20+10) = P.(n+20)+P10(n+20) by A2,A9;
10=5*2;
then A13: P.(n+10+10) = P.(n+10)+P10(n+10) by A2,A9;
P.(n+10) = P.(n)+P10(n) by A9,A2;
hence thesis by A10,A11,A12,A13;
end;
A14: 2*25=50;
A15: 1=1+2*0;
reconsider I=1 as Nat;
A16: 50+1 is odd by A14;
then A17:51+50 is odd by A14;
A18: P.(1+50) = 2/3+P50(1) by Th16,A15,A8;
A19: P.(51+50) = P.(51)+P50(51) by A16,A8;
A20: P.(101+50) = P.(101)+P50(101) by A8,A17;
L.152 = (-1) |^(76*2) * (1|^(2*152+1))/ (2*152+1) by Def2
.= 1/305;
then A21:P.(151+1) = P.(151) + 1/ (305) by SERIES_1:def 1;
A22: 313/400 < P.101 by A18,A19;
A23: P.152 < 315/400 by A18,A19,A21,A20;
P.(50*2+1) <= PI/4 <= P.(76*2) by Th14,Th15;
then 313/400 < PI/4 < 315/400 by A22,A23,XXREAL_0:2;
then 313/400*4 < PI/4*4 < 315/400*4 by XREAL_1:68;
hence thesis;
end;~~