:: Leibniz's Series for Pi :: by Karol P\kak :: :: Received October 18, 2016 :: Copyright (c) 2016-2021 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; begin :: Preliminaries reserve i,n,m for Nat, r,s for Real, A for non empty closed_interval Subset of REAL; theorem :: LEIBNIZ1:1 rng (tan| ].-PI/2,PI/2.[) = REAL; registration cluster arctan -> total; cluster arctan -> differentiable; end; theorem :: LEIBNIZ1:2 diff(arctan,r) = 1/(1+r^2); theorem :: LEIBNIZ1:3 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); registration let n; cluster #Z n -> continuous; end; theorem :: LEIBNIZ1:4 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); theorem :: LEIBNIZ1:5 integral( #Z 0 / ( #Z 0 + #Z 2),A) = arctan.(upper_bound A) - arctan.(lower_bound A); theorem :: LEIBNIZ1:6 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); theorem :: LEIBNIZ1:7 A=[.0,r.] & r >=0 implies |.integral( #Z (2*n) / ( #Z 0 + #Z 2),A).| <= 1/(2*n+1)*( r |^ (2*n+1)); begin :: Leibniz's test definition let a be Real_Sequence; func alternating_series a -> Real_Sequence means :: LEIBNIZ1:def 1 it.i = (-1) |^ i * a.i; end; theorem :: LEIBNIZ1:8 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); begin :: Leibniz series definition let r; func Leibniz_Series_of r -> Real_Sequence means :: LEIBNIZ1:def 2 it.n = (-1) |^n * (r|^(2*n+1))/ (2*n+1); end; definition func Leibniz_Series -> Real_Sequence equals :: LEIBNIZ1:def 3 Leibniz_Series_of 1; end; theorem :: LEIBNIZ1:9 r in [.-1,1.] implies abs(Leibniz_Series_of r) is nonnegative-yielding non-increasing convergent & lim abs (Leibniz_Series_of r) = 0; theorem :: LEIBNIZ1:10 (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); theorem :: LEIBNIZ1:11 r in [.-1,1.] implies Leibniz_Series_of r is summable; theorem :: LEIBNIZ1:12 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); theorem :: LEIBNIZ1:13 0 <= r <= 1 implies arctan.r = Sum (Leibniz_Series_of r); ::$N Leibniz's Series for $\pi$ theorem :: LEIBNIZ1:14 PI/4 = Sum Leibniz_Series; theorem :: LEIBNIZ1:15 Partial_Sums(Leibniz_Series).(2*n+1) <= Sum Leibniz_Series <= Partial_Sums(Leibniz_Series).(2*n); theorem :: LEIBNIZ1:16 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)); ::$N $\pi$ Approximation theorem :: LEIBNIZ1:17 313/100 < PI < 315/100;