:: Leibniz's Series for Pi
:: by Karol P\kak
::
:: Received October 18, 2016
:: Copyright (c) 2016-2026 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 RELAT_1, XBOOLE_0, PARTFUN1, FUNCT_1, TARSKI, SUBSET_1, ABIAN,
ASYMPT_1, REAL_1, NUMBERS, INTEGRA1, RCOMP_1, ARYTM_3, CARD_1, SIN_COS,
VALUED_1, ARYTM_1, FDIFF_1, SQUARE_1, PREPOWER, ORDINAL2, XXREAL_2,
XXREAL_1, INTEGRA5, SIN_COS9, XXREAL_0, SEQ_4, MEASURE5, PARTFUN3, SEQ_1,
COMPLEX1, NAT_1, REALSET1, NEWTON, SERIES_1, CARD_3, SEQ_2, VALUED_0,
FUNCOP_1, PBOOLE, LEIBNIZ1;
notations TARSKI, XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1,
PARTFUN1, ABIAN, SIN_COS,
NUMBERS, VALUED_1, XXREAL_0, XCMPLX_0, XREAL_0, PARTFUN3, RCOMP_1,
RFUNCT_1, MEASURE5, FCONT_1, SQUARE_1, INTEGRA1, INTEGRA5, PREPOWER,
TAYLOR_1, FDIFF_1, SEQ_2, SIN_COS4, SIN_COS9, SEQ_4, COMPLEX1, RELSET_1,
FUNCT_2, SEQ_1, SERIES_1, NAT_1, NEWTON, VALUED_0, PBOOLE, FUNCOP_1;
constructors RELSET_1, ABIAN, PARTFUN2, PARTFUN3, SIN_COS, TAYLOR_1, FDIFF_1,
FCONT_1, SQUARE_1, PREPOWER, INTEGRA3, INTEGRA5, SEQ_4, SIN_COS9,
SIN_COS4, COMSEQ_2, COMSEQ_3, SEQ_2, SEQ_1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, RELSET_1, ABIAN, VALUED_1, NAT_1,
NUMBERS, MEMBERED, VALUED_0, INT_1, ORDINAL1, FUNCT_2, RCOMP_1, FCONT_1,
FCONT_3, MEASURE5, XREAL_0, SIN_COS, PREPOWER, SQUARE_1, XCMPLX_0,
XXREAL_0, NEWTON, SEQ_4, SEQ_2, NAT_6, FUNCOP_1, PARTFUN3, SIN_COS6,
SIN_COS9, SEQ_1, NUMPOLY1;
requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
definitions TARSKI;
equalities XCMPLX_0, SIN_COS, SQUARE_1, SIN_COS9, SUBSET_1;
expansions TARSKI, FUNCT_1, PBOOLE;
theorems XREAL_0, XXREAL_0, NAT_1, FUNCT_1, FUNCT_2, ORDINAL1, VALUED_1,
SERIES_1, XREAL_1, SEQM_3, PARTFUN3, SEQ_2, SEQ_4, VALUED_0, RELAT_1,
ABIAN, SIN_COS9, INTEGRA5, FDIFF_1, PARTFUN1, XXREAL_1, FDIFF_2, SIN_COS,
XBOOLE_1, XBOOLE_0, COMPTRIG, FDIFF_7, RFUNCT_1, TARSKI, FCONT_1,
FCONT_2, SIN_COS4, XCMPLX_1, ABSVALUE, SIN_COS6, TAYLOR_1, PREPOWER,
FUNCOP_1, NEWTON, INTEGRA6, INTEGRA9, INTEGRA2, POWER, JORDAN5A,
MEASURE5, COMPLEX1, SERIES_2, TAYLOR_2, POLYFORM, SEQ_1;
schemes NAT_1, FUNCT_2, SEQ_1;
begin :: Preliminaries
reserve i,n,m for Nat,
r,s for Real,
A for non empty closed_interval Subset of REAL;
Lm1: tan is_differentiable_on ].-PI/2,PI/2.[
proof
r in ].-PI/2,PI/2.[ implies tan is_differentiable_in r
proof
assume r in ].-PI/2,PI/2.[;
then cos.r <> 0 by COMPTRIG:11;
hence thesis by FDIFF_7:46;
end;
hence thesis by SIN_COS9:1,FDIFF_1:9;
end;
Lm2: r in ].-PI/2,PI/2.[ implies diff(tan,r) = 1/(cos.r)^2
proof
assume r in ].-PI/2,PI/2.[;
then cos.r <>0 by COMPTRIG:11;
hence thesis by FDIFF_7:46;
end;
Lm3:
r >0 implies ex s be Real st 0<= s < PI/2 & tan.s=r
proof
assume
A1: r>0;
set e= 1/(2*r);
set P=PI/2;
A2: P in REAL by XREAL_0:def 1;
dom sin =REAL by FUNCT_2:def 1;
then consider s1 be Real such that
A3: 0<s1 & for x1 be Real st x1 in dom sin & |.x1-P.|<s1
holds |.sin.x1-sin.P.|<1/2 by A2,FCONT_1:def 2,FCONT_1:3;
A4:dom cos =REAL & dom sin = REAL by FUNCT_2:def 1;
then consider s2 be Real such that
A5: 0<s2 & for x1 be Real st x1 in dom cos & |.x1-P.|<s2
holds |.cos.x1-cos.P.|<e
by A1,FCONT_1:3,A2,FCONT_1:def 2;
set m = min(s1,s2),M=min(m,PI/2),m2=M/2;
0 < m & 0 < PI/2 by A3,A5,XXREAL_0:21;
then
A6: M >0 by XXREAL_0:21;
then
A7: m2 >0 & m2 < M by XREAL_1:216;
set X=P-m2;
A8: X in REAL by XREAL_0:def 1;
A9: X < P by A6,XREAL_1:37;
A10: |.X-P.| = -(X-P) by A6,ABSVALUE:def 1;
A11:M <= m & M <= PI/2 & m <= s1& m <=s2 by XXREAL_0:17;
then M <= s1 & M <=s2 by XXREAL_0:2;
then
A12: m2 < s1 & m2 <s2 & m2 < PI/2 by A11,A7,XXREAL_0:2;
then
A13: |.cos.X-cos.P.|<e by A10,A4,A5,XREAL_0:def 1;
A14: X >0 by A12,XREAL_1:50;
then X in ].0,P.[ by A9,XXREAL_1:4;
then
A15: cos.X >0 & cos.P=0 by SIN_COS:80,77;
cos.X <e by A15,A13,ABSVALUE:def 1;
then
A16:1/(cos.X) > 1/(1/(2*r)) & 1/(1/(2*r))=2*r by XREAL_1:76,A15;
sin X < 1 & sin.P =1 & sin X=sin.X by SIN_COS6:30,A9,A14,SIN_COS:77;
then |.sin.X-1.|=-(sin.X-1) by ABSVALUE:def 1,XREAL_1:49;
then 1-sin.X <1/2 by SIN_COS:77,A10,A3,A4,XREAL_0:def 1,A12;
then sin.X > 1-1/2 by XREAL_1:11;
then
A17: (sin.X)/(cos.X) > (1/2)/(cos.X) by A15,XREAL_1:74;
(1/2)/(cos.X) > 1/2*(2*r) by A16,XREAL_1:68;
then
A18:(sin.X)/(cos.X) > r by A17,XXREAL_0:2;
not cos.X in {0} by A15,TARSKI:def 1;
then not X in cos"{ 0 } by FUNCT_1:def 7;
then X in dom cos\cos " {0} by A8,A4,XBOOLE_0:def 5;
then X in dom sin /\ (dom cos\cos"{0}) by A4,XBOOLE_0:def 4;
then X in dom tan by RFUNCT_1:def 1;
then
A19:tan.X >r by A18,RFUNCT_1:def 1;
A20:[.0,X.] c= ].-P,P.[ by A9,XXREAL_1:47;
A21:tan| [.0,X.] is continuous by A9,XXREAL_1:47,SIN_COS9:5,FCONT_1:16;
A22:[.0,X.] c= dom tan by A20,SIN_COS9:1;
r in [. tan.0,tan.X .] by A1,A19,XXREAL_1:1,SIN_COS9:41;
then r in [. tan.0,tan.X .]\/[. tan.X,tan.0 .] by XBOOLE_0:def 3;
then consider s be Real such that
A23: s in [.0,X.] & r=tan.s by A21,A22,A14,FCONT_2:15;
A24:0 <=s & s <= X by A23,XXREAL_1:1;
then s < P by A6,XREAL_1:37;
hence thesis by A23,A24;
end;
theorem Th1:
rng (tan| ].-PI/2,PI/2.[) = REAL
proof
set P=PI/2,I=].-P,P.[;
REAL c= rng (tan| I)
proof
let r be object;assume r in REAL;then reconsider r as Real;
per cases;
suppose
A1: r>0;
then consider s be Real such that
A2: 0<= s < P & tan.s=r by Lm3;
s in dom tan by A1,A2,FUNCT_1:def 2;
hence thesis by XXREAL_1:4,A2,FUNCT_1:50;
end;
suppose
A3: r<0;
then consider s be Real such that
A4: 0<= s < P & tan.s=-r by Lm3;
A5: s in dom tan by A3,A4,FUNCT_1:def 2;
A6: dom sin=REAL & dom cos = REAL by FUNCT_2:def 1;
then dom tan = REAL /\(REAL \ cos"{0}) by RFUNCT_1:def 1;
then s in REAL\cos"{0} by A5,XBOOLE_0:def 4;
then s in REAL & not s in cos"{0} by XBOOLE_0:def 5;
then not cos.s in {0} by A6,FUNCT_1:def 7;
then cos.s <>0 & cos.s = cos.(-s) by TARSKI:def 1,SIN_COS:30;
then tan.s= tan s & tan.(-s)=tan (-s) & -tan(s)=tan(-s)
by SIN_COS9:15,SIN_COS4:1;
then
A7: -s in dom tan & tan.(-s)=r by A3,A4,FUNCT_1:def 2;
P > -s > -P by A4,XREAL_1:24;
hence thesis by A7,FUNCT_1:50,XXREAL_1:4;
end;
suppose r=0;
then 0 in dom tan & tan.0=r & 0 in I
by XXREAL_1:1,SIN_COS:70,SIN_COS9:41,XXREAL_1:4;
hence thesis by FUNCT_1:50;
end;
end;
hence thesis by XBOOLE_0:def 10;
end;
registration
cluster arctan -> total;
coherence
proof
dom arctan = REAL by Th1,FUNCT_1:33;
hence thesis by PARTFUN1:def 2;
end;
cluster arctan -> differentiable;
coherence
proof
tan.:].-PI/2,PI/2.[ = rng (tan| ].-PI/2,PI/2.[) by RELAT_1:115
.= dom arctan by Th1,FUNCT_2:def 1;
hence thesis by FDIFF_1:def 8,SIN_COS9:71;
end;
end;
theorem Th2:
diff(arctan,r) = 1/(1+r^2)
proof
set g = arctan;
set f = tan | ].-PI/2,PI/2.[;
set x = arctan.r;
A1: (sin.x)^2 + (cos.x)^2 = 1 by SIN_COS:28;
A2: f is_differentiable_on ].-PI/2,PI/2.[ by Lm1,FDIFF_2:16;
A3: now
A4: for x0 be Real st x0 in ].-PI/2,PI/2.[ holds 1/(cos.x0)^2 > 0
proof
let x0 be Real;
assume x0 in ].-PI/2,PI/2.[;
then 0 < cos.x0 by COMPTRIG:11;
hence thesis;
end;
let x0 be Real such that
A5: x0 in ].-PI/2,PI/2.[;
diff(f,x0) = (f`|].-PI/2,PI/2.[).x0 by A2,A5,FDIFF_1:def 7
.= (tan`|].-PI/2,PI/2.[).x0 by Lm1,FDIFF_2:16
.= diff(tan,x0) by A5,Lm1,FDIFF_1:def 7
.= 1/(cos.x0)^2 by A5,Lm2;
hence 0 < diff(f,x0) by A5,A4;
end;
A6:rng g = dom f & dom g = rng f by FUNCT_1:33;
set x = arctan.r;
A7:dom arctan = REAL & r in REAL by FUNCT_2:def 1,XREAL_0:def 1;
then
A8:x in dom f by A6,FUNCT_1:def 3;
then
A9: x in ].-PI/2,PI/2.[ by RELAT_1:57;
A10:cos x <> 0 by A8, RELAT_1:57,COMPTRIG:11;
A11: r = f.x by A7,A6,FUNCT_1:32
.= tan.x by A8,FUNCT_1:47
.= tan x by A10,SIN_COS9:15
.= sin x/cos x by SIN_COS4:def 1;
dom f = dom tan /\ ].-PI/2,PI/2.[ by RELAT_1:61;
then
A12: ].-PI/2,PI/2.[ c= dom f by SIN_COS9:1,XBOOLE_1:19;
A13: f| ].-PI/2,PI/2.[ = f;
r * cos x = sin x by A10,A11,XCMPLX_1:87;
then
A14: 1 = (cos x)^2 * ( r^2 + 1 ) by A1;
f is_differentiable_on ].-PI/2,PI/2.[ by Lm1,FDIFF_2:16;
then diff(f,x) = (f`|].-PI/2,PI/2.[).x by A9,FDIFF_1:def 7
.= (tan`|].-PI/2,PI/2.[).x by Lm1,FDIFF_2:16
.= diff(tan,x) by A9,Lm1,FDIFF_1:def 7
.= 1/(cos x)^2 by A8,RELAT_1:57,Lm2;
then diff(g,r) = 1/(1/(cos x)^2) by A2,A3,A13,A12,A7,FDIFF_2:48
.= 1/(r^2+1) by A14,XCMPLX_1:73;
hence thesis;
end;
theorem Th3:
for Z be open Subset of REAL holds
arctan is_differentiable_on Z &
for r st r in Z holds ((arctan)`|Z).r = 1/(1+r^2)
proof
let Z be open Subset of REAL;
A1: dom arctan = REAL by FUNCT_2:def 1;
A2: arctan is_differentiable_on Z by A1, FDIFF_1:28;
r in Z implies ((arctan)`|Z).r = 1/(1+r^2)
proof
assume r in Z;
hence ((arctan)`|Z).r = diff(arctan,r) by A2,FDIFF_1:def 7
.= 1/(1+r^2) by Th2;
end;
hence thesis by A1,FDIFF_1:28;
end;
Lm4:#Z (n+m) = #Z n (#) #Z m
proof
now let r;
thus ( #Z (n+m)).r = r #Z (n+m) by TAYLOR_1:def 1
.= (r #Z n) * (r #Z m) by TAYLOR_1:1
.= ( #Z n).r * (r #Z m) by TAYLOR_1:def 1
.= ( #Z n).r * ( #Z m).r by TAYLOR_1:def 1
.= (( #Z n) (#) ( #Z m)).r by VALUED_1:5;
end;
hence thesis;
end;
registration
let n;
cluster #Z n -> continuous;
coherence
proof
defpred P[Nat] means #Z $1 is continuous;
now let r;
thus ( #Z 0).r = r #Z 0 by TAYLOR_1:def 1
.= 1 by PREPOWER:34
.= (REAL-->1).r by XREAL_0:def 1,FUNCOP_1:7;
end;
then #Z 0 = REAL -->1;
then
A1: P[0];
A2: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A3: P[n];
set Z1=#Z 1;
r in dom Z1 implies Z1.r = r
proof
Z1.r=r #Z 1 by TAYLOR_1:def 1;
hence thesis by PREPOWER:35;
end;
then Z1 is continuous by FCONT_1:40;
then Z1 (#) #Z n is continuous by A3;
hence thesis by Lm4;
end;
for n holds P[n] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
end;
Lm5:( #Z 0 +#Z 2).r = 1+r*r
proof
A1:r#Z 1= r by PREPOWER:35;
r in REAL by XREAL_0:def 1;
hence ( #Z 0 +#Z 2).r = ( #Z 0).r + ( #Z 2).r by VALUED_1:1
.= (r #Z 0) + ( #Z 2).r by TAYLOR_1:def 1
.= (r #Z 0) + (r #Z 2) by TAYLOR_1:def 1
.= 1 + (r #Z (1+1)) by PREPOWER:34
.= 1 + (r * r) by A1,TAYLOR_1:1;
end;
Lm6: ( #Z 0 +#Z 2)"{0} = {}
proof
assume ( #Z 0 +#Z 2)"{0} <> {};
then consider x be object such that
A1: x in ( #Z 0 +#Z 2)"{0} by XBOOLE_0:def 1;
reconsider x as Element of REAL by A1;
( #Z 0 +#Z 2).x in {0} by A1,FUNCT_1:def 7;
then 0 = ( #Z 0 +#Z 2).x by TARSKI:def 1
.= 1+x*x by Lm5;
hence thesis;
end;
theorem Th4:
dom ( #Z n / ( #Z 0 + #Z 2)) = REAL &
( #Z n / ( #Z 0 + #Z 2)) is continuous &
( #Z n / ( #Z 0 + #Z 2)).r = (r|^n)/(1+r^2)
proof
set Z0=#Z 0,Z2=#Z 2,Zn=#Z n, f=Zn/(Z0+Z2);
A1: dom Zn=REAL=dom (Z0+Z2) by FUNCT_2:def 1;
hence
A2: dom f = REAL/\(REAL\{}) by Lm6,RFUNCT_1:def 1
.= REAL;
A3:Zn|REAL is continuous & (Z0+Z2)|REAL is continuous;
REAL c= dom Zn /\ dom (Z0+Z2) by A1;
then f | REAL is continuous by Lm6,A3,FCONT_1:24;
hence f is continuous;
Zn.r = r #Z n by TAYLOR_1:def 1
.= (r|^n) by PREPOWER:36;
hence f.r = (r|^n) * ((Z0+Z2).r)" by XREAL_0:def 1,A2,RFUNCT_1:def 1
.= (r|^n)/(1+r^2) by Lm5;
end;
theorem Th5:
integral( #Z 0 / ( #Z 0 + #Z 2),A) =
arctan.(upper_bound A) - arctan.(lower_bound A)
proof
set Z0=#Z 0,Z2=#Z 2,f=Z0/(Z0+Z2);
A1:dom f = REAL by Th4;
f is continuous by Th4;
then
A2: f |A is continuous;
A3:r in REAL implies f.r=1/(1+r^2)
proof
r|^0=1 by NEWTON:4;
hence thesis by Th4;
end;
A4:[#]REAL is open;
A5:dom arctan = REAL by FUNCT_2:def 1;
A6: arctan is_differentiable_on REAL by A5,FDIFF_1:def 8;
A7: for x being Element of REAL st x in dom ((arctan)`|REAL)
holds ((arctan)`|REAL).x = f.x
proof
let x be Element of REAL;
assume x in dom ((arctan)`|REAL);
((arctan)`|REAL).x = 1/(1+x^2) by Th3,A4
.= f.x by A3;
hence thesis;
end;
A8: ((arctan)`|REAL) = f by A6,A1,FDIFF_1:def 7, A7;
f is_integrable_on A & f|A is bounded by A1,A2,INTEGRA5:10,11;
hence thesis by A4,A8,INTEGRA5:13,Th3;
end;
theorem Th6:
integral( ((-1)|^i) (#) ( #Z (2*n) / ( #Z 0 + #Z 2)),A)
= ((-1)|^i) * (((1/(2*n+1))*((upper_bound A) |^ (2*n+1)))
- ((1/(2*n+1))*((lower_bound A) |^ (2*n+1))))
+ integral((-1)|^(i+1) (#) ( #Z (2*(n+1)) / ( #Z 0 + #Z 2)),A)
proof
set II =(-1)|^i,i1=i+1,n1=n+1,II1=(-1)|^i1;
set Z0= #Z 0,Z2=#Z 2,Z2n=#Z (2*n);
set f=II (#) Z2n;
set g = II1 (#) ( #Z (2*n1) / ( Z0 + Z2));
A1:dom (Z2n / ( Z0 + Z2)) = dom (II (#) ( Z2n / ( Z0 + Z2)))
by VALUED_1:def 5;
dom ( #Z (2*n1) / ( Z0 + Z2)) = dom (II1 (#) ( #Z (2*n1) / ( Z0 + Z2)))
by VALUED_1:def 5;
then
A2:dom g=REAL by Th4;
A3:dom f=REAL by FUNCT_2:def 1;
then
A4:dom ( f+g )=REAL/\REAL by A2, VALUED_1:def 1;
for x be Element of REAL holds
(II (#) ( Z2n / ( Z0 + Z2))).x = (f+g).x
proof
let x be Element of REAL;
x|^(2*n+1+1) = x* x|^(2*n+1) by NEWTON:6
.=x* (x*(x|^(2*n))) by NEWTON:6;
then x|^(2*n) + x|^(2*n1) =
x|^(2*n) *(1 + x^2);
then
A5: ( x|^(2*n) + x|^(2*n1))/(1+x^2) = x|^(2*n) by XCMPLX_1:89;
A6: - II*((x|^(2*n1))/(1+x^2)) = ((-1) * II)*((x|^(2*n1))/(1+x^2))
.= II1 * ((x|^(2*n1))/(1+x^2)) by NEWTON:6;
x|^(2*n) = x #Z (2*n) by PREPOWER:36
.= Z2n.x by TAYLOR_1:def 1;
then
A7: II*(x|^(2*n)) = f.x by VALUED_1:6;
A8: II1*((x|^(2*n1))/(1+x^2)) = II1 * ( #Z (2*n1) / ( Z0 + Z2)).x by Th4
.= g.x by VALUED_1:6;
thus (II (#) ( Z2n / ( Z0 + Z2))).x
= II * ( Z2n / ( Z0 + Z2)).x by VALUED_1:6
.= II * ((x|^(2*n))/(1+x^2)) by Th4
.= II * (x|^(2*n) - (x|^(2*n1))/(1+x^2)) by A5
.= II * (x|^(2*n)) + II1*((x|^(2*n1))/(1+x^2)) by A6
.= (f+g).x by A7,A8,A4,VALUED_1:def 1;
end;
then
A9:f+g = II (#) ( Z2n / ( Z0 + Z2)) by A1,Th4,A4;
A10:dom Z2n=REAL by FUNCT_2:def 1;
f | A is continuous & Z2n|A is continuous;
then
A11: f is_integrable_on A & f|A is bounded &
Z2n is_integrable_on A & Z2n|A is bounded by A10,INTEGRA5:10,11,A3;
#Z (2*n1) / ( Z0 + Z2) is continuous by Th4;
then g | A is continuous;
then
A12: g is_integrable_on A & g|A is bounded by INTEGRA5:10,11,A2;
A13:2*n in NAT by ORDINAL1:def 12;
thus integral(II (#) ( Z2n / ( Z0 + Z2)),A) = integral(f,A) + integral(g,A)
by A3,A2,A11,A12,A9,INTEGRA6:11
.= II*integral(Z2n,A) + integral(g,A) by A10,A11,INTEGRA6:9
.= II*(((1/(2*n+1))*((upper_bound A) |^ (2*n+1))) - ((1/(2*n+1) )*
((lower_bound A) |^ (2*n+1)))) + integral(g,A)
by INTEGRA9:19,A13;
end;
theorem Th7:
A=[.0,r.] & r >=0 implies
|.integral( #Z (2*n) / ( #Z 0 + #Z 2),A).| <= 1/(2*n+1)*( r |^ (2*n+1))
proof
set Z0= #Z 0,Z2= #Z 2,N=2*n,Zn = #Z N,f = Zn / ( Z0 + Z2);
assume
A1: A=[.0,r.] & r >=0;
A2:f is continuous & dom f=REAL by Th4;
then dom (f|A)=A by RELAT_1:62;
then f|A is total by PARTFUN1:def 2;
then reconsider fA=f||A as Function of A,REAL;
A3: f|A is continuous by A2;
then
A4: f|A is bounded & f is_integrable_on A &fA|A=f|A by INTEGRA5:11,10,A2;
A5: fA is integrable by A3, INTEGRA5:def 1,INTEGRA5:11,A2;
A6:Zn is continuous & dom Zn=REAL by FUNCT_2:def 1;
then dom (Zn|A)=A by RELAT_1:62;
then Zn|A is total by PARTFUN1:def 2;
then reconsider ZnA=Zn||A as Function of A,REAL;
A7: Zn|A is continuous;
then
A8: Zn|A is bounded & Zn is_integrable_on A &ZnA|A=Zn|A
by INTEGRA5:11,10,A6;
A9: ZnA is integrable by A7,INTEGRA5:def 1,INTEGRA5:11,A6;
for r st r in A holds fA.r <= ZnA.r
proof
let r;
assume r in A;
then
A10: fA.r = f.r & ZnA.r = Zn.r by FUNCT_1:49;
A11: Zn.r = r #Z N by TAYLOR_1:def 1
.= r|^ N by PREPOWER:36;
A12: r|^N >= 0 by POWER:3;
r^2 +1 >= 1+0 by XREAL_1:6;
then 1 / (1+r^2) <= 1 by XREAL_1:183;
then (r|^N) * 1 / (1+r^2) <= (r|^N)*1 by A12,XREAL_1:64;
hence thesis by A11,Th4,A10;
end;
then
A13:integral(fA) <= integral(ZnA) by A4,A5,A8,A9,INTEGRA2:34;
A14: integral(f,A) = integral(fA) by INTEGRA5:def 2;
A15:lower_bound A=0 & upper_bound A = r by A1,JORDAN5A:19;
A16:N in NAT by ORDINAL1:def 12;
0|^(N+1) =0 by NEWTON:84;
then
A17:((1/(N+1))*(0 |^ (N+1)))=0;
A18:integral(ZnA) = integral(Zn,A) by INTEGRA5:def 2
.= ((1/(N+1))*(r |^ (N+1)))-0 by A16,A15,A17,INTEGRA9:19;
A19: dom abs f= dom f by VALUED_1:def 11;
for x be object st x in REAL holds f.x=(abs f).x
proof
let x be object;assume x in REAL;
then reconsider r=x as Element of REAL;
N=n+n;
then
A20: r|^N = (r|^n)*(r|^n) by NEWTON:8;
A21: f.r = (r|^N)/(1+r^2) by Th4;
thus (abs f).x = |. f.r .| by A2,A19,VALUED_1:def 11
.= f.x by A20,A21,ABSVALUE:def 1;
end;
then
A22:abs f =f by A19,A2;
|.integral(f,A).| <= integral(abs f, A) by A2,INTEGRA6:7,A4;
hence thesis by A13,A14,A18,XXREAL_0:2,A22;
end;
begin :: Leibniz's test
::$L https://en.wikipedia.org/wiki/Alternating_series Alternating series
definition
let a be Real_Sequence;
func alternating_series a -> Real_Sequence means :Def1:
it.i = (-1) |^ i * a.i;
existence
proof
defpred P[Nat,object] means $2=(-1) |^ $1 * a.$1;
A1:for x be Element of NAT ex y be Element of REAL st P[x,y]
proof
let x be Element of NAT;
((-1) |^ x) *(a.x) 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 * a.i and
A4:for i be Nat holds a2.i = (-1) |^ i * a.i;
now let x be object;
assume x in NAT;
then reconsider i=x as Nat;
thus a1.x= (-1) |^ i * a.i by A3 .= a2.x by A4;
end;
hence thesis;
end;
end;
theorem Th8:
for a be Real_Sequence st a is nonnegative-yielding non-increasing convergent
& lim a = 0
holds
alternating_series a is summable &
for n holds
(Partial_Sums alternating_series a).(2*n)
>= Sum alternating_series a >=
(Partial_Sums alternating_series a).(2*n+1)
proof
let a be Real_Sequence such that
A1:a is nonnegative-yielding non-increasing convergent & lim a = 0;
set A=alternating_series a,P=Partial_Sums A;
defpred Sp[Nat,object] means $2=P.(2*$1);
defpred Sn[Nat,object] means $2=P.(2*$1+1);
A2:for x be Element of NAT ex y be Element of REAL st Sp[x,y];
A3:for x be Element of NAT ex y be Element of REAL st Sn[x,y];
consider Sp be Function of NAT,REAL such that
A4:for x being Element of NAT holds Sp[x,Sp.x] from FUNCT_2:sch 3(A2);
consider Sn be Function of NAT,REAL such that
A5:for x being Element of NAT holds Sn[x,Sn.x] from FUNCT_2:sch 3(A3);
A6:for n be Nat holds Sn.n <= Sn.(n+1)
proof
let n be Nat;set n1=n+1;
A7: n1 in NAT & n in NAT by ORDINAL1:def 12;
A8: Sn.(n+1) = P.(2*n1+1) by A5
.= P.(2*n+1+1) + A.(2*n1+1) by SERIES_1:def 1
.= P.(2*n+1) + A.(2*n1)+A.(2*n1+1) by SERIES_1:def 1
.= P.(2*n+1) + (A.(2*n1)+A.(2*n1+1));
A9: Sn.n=P.(2*n+1) by A7,A5;
A10: a.(2*n1) - a.(2*n1+1) >=0 by XREAL_1:48,A1,VALUED_1:def 16;
(-1)|^(2*n1)=1 & (-1)|^(2*n1+1)= -1;
then A.(2*n1) = 1*a.(2*n1) & A.(2*n1+1) = (-1)*a.(2*n1+1) by Def1;
hence thesis by A10,A9,A8,XREAL_1:31;
end;
then
A11:Sn is non-decreasing by VALUED_1:def 15;
A12:for n be Nat holds Sp.n >= Sp.(n+1)
proof
let n be Nat;
set n1=n+1;
A13: n1 in NAT & n in NAT & 2*n1=2*n+1+1 by ORDINAL1:def 12;
then
A14:Sp.(n+1) = P.(2*n+1+1) by A4
.= P.(2*n+1) + A.(2*n+1+1) by SERIES_1:def 1
.= P.(2*n) + A.(2*n+1)+A.(2*n+1+1) by SERIES_1:def 1
.= P.(2*n) + (A.(2*n+1)+A.(2*n1));
A15:Sp.n=P.(2*n) by A13,A4;
a.(2*n+1) >= a.(2*n+1+1) by A1,VALUED_1:def 16;
then
A16: a.(2*n1)-a.(2*n+1) <=0 by XREAL_1:47;
(-1)|^(2*n1)=1 & (-1)|^(2*n+1)= -1;
then A.(2*n1) = 1*a.(2*n1) & A.(2*n+1) = (-1)*a.(2*n+1) by Def1;
hence thesis by A15,A14,XREAL_1:32,A16;
end;
then
A17:Sp is non-increasing by VALUED_1:def 16;
A18: for n be Nat holds Sp.n >= Sn.n
proof
let n be Nat;
n in NAT by ORDINAL1:def 12;
then Sp.n=P.(2*n) & Sn.n=P.(2*n+1) by A4,A5;
then
A19:Sn.n = Sp.n + A.(2*n+1) by SERIES_1:def 1;
dom a = NAT by FUNCT_2:def 1;
then a.(2*n+1) in rng a by FUNCT_1:def 3;
then
A20:a.(2*n+1) >=0 by A1,PARTFUN3:def 4;
(-1)|^(2*n+1)= -1;
then A.(2*n+1) = (-1)*a.(2*n+1) by Def1;
hence thesis by A19, XREAL_1:32,A20;
end;
for n be Nat holds Sp.n > Sn.0-1
proof
let n be Nat;
Sp.n >= Sn.n >= Sn.0 by A18,A6, VALUED_1:def 15,SEQM_3:6;
then Sp.n >= Sn.0 & Sn.0 > Sn.0-1 by XXREAL_0:2,XREAL_1:44;
hence thesis by XXREAL_0:2;
end;
then
A21: Sp is bounded_below by SEQ_2:def 4;
A22:for n be Nat holds Sn.n < Sp.0+1
proof
let n be Nat;
Sn.n <= Sp.n <= Sp.0 by A18,A12,VALUED_1:def 16,SEQM_3:8;
then Sn.n <= Sp.0 & Sp.0 < Sp.0+1 by XXREAL_0:2,XREAL_1:29;
hence thesis by XXREAL_0:2;
end;
then
A23: Sn is bounded_above by SEQ_2:def 3;
deffunc double(Nat)=2 * $1+1;
A24:for x be Element of NAT holds double(x) in NAT;
consider Double be Function of NAT,NAT such that
A25:for x be Element of NAT holds Double.x=double(x) from FUNCT_2:sch 8(A24);
reconsider Double1=Double as ManySortedSet of NAT;
for n being Nat holds Double.n < Double.(n+1)
proof
let n be Nat;set n1=n+1;
n in NAT & n1 in NAT by ORDINAL1:def 12;
then
A26: Double.n=double(n) & Double.n1=double(n1) by A25;
n < n1 by NAT_1:13;
then 2*n < 2*n1 by XREAL_1:97;
hence thesis by A26, XREAL_1:8;
end;
then
A27:Double1 is increasing sequence of NAT by VALUED_1:def 13;
A28:rng (a*Double1) c= REAL;
rng Double c= NAT & dom a = NAT & dom Double=NAT by FUNCT_2:def 1;
then
A29:dom (a*Double1)=NAT by RELAT_1:27;
then reconsider aD=a*Double1 as Real_Sequence by A28,FUNCT_2:2;
reconsider aD as subsequence of a by VALUED_0:def 17,A27;
A30: aD is convergent & lim aD = 0 by SEQ_4:16,17,A1;
A31: Sp-Sn is convergent & lim (Sp-Sn) = lim (Sp) - lim (Sn)
by A21,A17,A23,A11,SEQ_2:12;
for x be object st x in NAT holds aD.x= (Sp-Sn).x
proof
let x be object such that
A32:x in NAT;
reconsider n=x as Element of NAT by A32;
A33: Double.n = 2*n+1 by A25;
dom (Sp-Sn) = NAT by FUNCT_2:def 1;
then
A34: (Sp-Sn).n = (Sp.n) -(Sn.n) by VALUED_1:13;
Sp.n=P.(2*n) & Sn.n = P.(2*n+1) by A4,A5;
then
A35: Sn.n = Sp.n+ A.(2*n+1) by SERIES_1:def 1;
(-1)|^(2*n+1)= -1;
then A.(2*n+1) = (-1)*a.(2*n+1) by Def1;
hence thesis by A29,A34,A35,FUNCT_1:12,A33;
end;
then
A36:aD = Sp-Sn;
A37: for p be Real st 0<p ex n be Nat st for m be Nat st n<=m
holds |.P.m-lim Sp.| < p
proof
let p be Real such that
A38: 0<p;
consider n1 be Nat such that
A39: for m be Nat st n1<=m holds |.Sp.m-lim Sp.| < p
by A38,A21,A17,SEQ_2:def 7;
consider n2 be Nat such that
A40: for m be Nat st n2<=m holds |.Sn.m-lim Sp.| < p
by A38,A23,A11,SEQ_2:def 7,A36,A30,A31;
set N = max(2*n1,2*n2+1);
reconsider N as Nat by XXREAL_0:def 10;
take N;
let m be Nat such that
A41: N <= m;
per cases;
suppose m is even;
then consider m2 be Nat such that
A42: m=2*m2 by ABIAN:def 2;
2*n1 <= N by XXREAL_0:25;
then 2*n1 <= 2*m2 by A41,A42,XXREAL_0:2;
then n1 <= m2 by XREAL_1:68;
then
A43: |.Sp.m2-lim Sp.| < p by A39;
m2 in NAT by ORDINAL1:def 12;
hence thesis by A4,A43,A42;
end;
suppose m is odd;
then consider m2 be Nat such that
A44: m=2*m2+1 by ABIAN:9;
2*n2+1 <= N by XXREAL_0:25;
then 2*n2+1 <= 2*m2+1 by A41,A44,XXREAL_0:2;
then 2*n2 <= 2*m2 by XREAL_1:6;
then n2 <= m2 by XREAL_1:68;
then
A45: |.Sn.m2-lim Sp.| < p by A40;
m2 in NAT by ORDINAL1:def 12;
hence thesis by A45,A44,A5;
end;
end;
hence A is summable by SERIES_1:def 2,SEQ_2:def 6;
let n;
n in NAT by ORDINAL1:def 12;
then
A46:Sp.n=P.(2*n) & Sn.n=P.(2*n+1) by A4,A5;
P is convergent by A37,SEQ_2:def 6;
then lim P = lim Sp & lim P = Sum A
by A37,SEQ_2:def 7,SERIES_1:def 3;
hence thesis by A46,A11,A12,VALUED_1:def 16,A36,A30,A31,A22,SEQ_2:def 3,
A21,SEQ_4:37,38;
end;
begin :: Leibniz series
definition
let r;
func Leibniz_Series_of r -> 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
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,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 <s ex n st for m st n <=m holds |.P.m - A .|<s
proof
let s;
assume
A3: 0 <s;
consider n such that
A4: 1/s < n by SEQ_4:3;
take n;
let m such that
A5: n<=m;set m1=m+1;
reconsider R=[.0,r.] as non empty
closed_interval Subset of REAL by MEASURE5:def 3,A1,XXREAL_1:1;
A6: I(m1) is continuous & dom I(m1)=REAL by Th4;
then I(m1) |R is continuous;
then
A7: I(m1) is_integrable_on R & I(m1) |R is bounded
by A6,INTEGRA5:11,10;
A8: A = P.m+integral( (-1)|^m1 (#) I(m1),R) by A1,Th12;
integral( (-1)|^m1 (#) I(m1),R) =
(-1)|^m1 * integral( I(m1),R) by A7,A6,INTEGRA6:9;
then
A9: |.- integral( (-1)|^(m+1) (#) I(m1),R).|
=|.(-1)|^(m+1) * integral( I(m1),R) .| by COMPLEX1:52
.= |.(-1)|^(m+1).| * |.integral( I(m1),R) .| by COMPLEX1:65
.= 1 * |.integral( I(m1),R) .| by SERIES_2:1;
A10: |. P.m -A.| <= 1/(2*m1+1)*( r |^ (2*m1+1)) by A1,Th7,A8,A9;
0|^ (2*m1+1) = 0 & 1|^(2*m1+1) =1 & (r=0 or r>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's Series for $\pi$
::$L https://en.wikipedia.org/wiki/Leibniz_formula_for_%CF%80 Leibniz formula 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
::$L https://en.wikipedia.org/wiki/Approximations_of_%CF%80 Approximations of PI
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;