:: Leibniz's Series for Pi
:: by Karol P\kak
::
:: Received October 18, 2016
:: Copyright (c) 2016-2018 Association of Mizar Users

Lm1: tan is_differentiable_on ].(- (PI / 2)),(PI / 2).[
proof end;

Lm2: for r being Real st r in ].(- (PI / 2)),(PI / 2).[ holds
diff (tan,r) = 1 / ((cos . r) ^2)

proof end;

Lm3: for r being Real st r > 0 holds
ex s being Real st
( 0 <= s & s < PI / 2 & tan . s = r )

proof end;

theorem Th1: :: LEIBNIZ1:1
rng (tan | ].(- (PI / 2)),(PI / 2).[) = REAL
proof end;

registration
coherence
proof end;
coherence
proof end;
end;

theorem Th2: :: LEIBNIZ1:2
for r being Real holds diff (arctan,r) = 1 / (1 + (r ^2))
proof end;

theorem Th3: :: LEIBNIZ1:3
for Z being open Subset of REAL holds
( arctan is_differentiable_on Z & ( for r being Real st r in Z holds
() . r = 1 / (1 + (r ^2)) ) )
proof end;

Lm4: for n, m being Nat holds #Z (n + m) = (#Z n) (#) (#Z m)
proof end;

registration
let n be Nat;
coherence
#Z n is continuous
proof end;
end;

Lm5: for r being Real holds (() + (#Z 2)) . r = 1 + (r * r)
proof end;

Lm6: (() + (#Z 2)) " = {}
proof end;

theorem Th4: :: LEIBNIZ1:4
for n being Nat
for r being Real holds
( dom ((#Z n) / (() + (#Z 2))) = REAL & (#Z n) / (() + (#Z 2)) is continuous & ((#Z n) / (() + (#Z 2))) . r = (r |^ n) / (1 + (r ^2)) )
proof end;

theorem Th5: :: LEIBNIZ1:5
for A being non empty closed_interval Subset of REAL holds integral ((() / (() + (#Z 2))),A) = () - ()
proof end;

theorem Th6: :: LEIBNIZ1:6
for i, n being Nat
for A being non empty closed_interval Subset of REAL holds integral ((((- 1) |^ i) (#) ((#Z (2 * n)) / (() + (#Z 2)))),A) = (((- 1) |^ i) * (((1 / ((2 * n) + 1)) * (() |^ ((2 * n) + 1))) - ((1 / ((2 * n) + 1)) * (() |^ ((2 * n) + 1))))) + (integral ((((- 1) |^ (i + 1)) (#) ((#Z (2 * (n + 1))) / (() + (#Z 2)))),A))
proof end;

theorem Th7: :: LEIBNIZ1:7
for n being Nat
for r being Real
for A being non empty closed_interval Subset of REAL st A = [.0,r.] & r >= 0 holds
|.(integral (((#Z (2 * n)) / (() + (#Z 2))),A)).| <= (1 / ((2 * n) + 1)) * (r |^ ((2 * n) + 1))
proof end;

definition
let a be Real_Sequence;
func alternating_series a -> Real_Sequence means :Def1: :: LEIBNIZ1:def 1
for i being Nat holds it . i = ((- 1) |^ i) * (a . i);
existence
ex b1 being Real_Sequence st
for i being Nat holds b1 . i = ((- 1) |^ i) * (a . i)
proof end;
uniqueness
for b1, b2 being Real_Sequence st ( for i being Nat holds b1 . i = ((- 1) |^ i) * (a . i) ) & ( for i being Nat holds b2 . i = ((- 1) |^ i) * (a . i) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines alternating_series LEIBNIZ1:def 1 :
for a, b2 being Real_Sequence holds
( b2 = alternating_series a iff for i being Nat holds b2 . i = ((- 1) |^ i) * (a . i) );

theorem Th8: :: LEIBNIZ1:8
for a being Real_Sequence st a is nonnegative-yielding & a is non-increasing & a is convergent & lim a = 0 holds
( alternating_series a is summable & ( for n being Nat holds
( . (2 * n) >= Sum & Sum >= . ((2 * n) + 1) ) ) )
proof end;

definition
let r be Real;
func Leibniz_Series_of r -> Real_Sequence means :Def2: :: LEIBNIZ1:def 2
for n being Nat holds it . n = (((- 1) |^ n) * (r |^ ((2 * n) + 1))) / ((2 * n) + 1);
existence
ex b1 being Real_Sequence st
for n being Nat holds b1 . n = (((- 1) |^ n) * (r |^ ((2 * n) + 1))) / ((2 * n) + 1)
proof end;
uniqueness
for b1, b2 being Real_Sequence st ( for n being Nat holds b1 . n = (((- 1) |^ n) * (r |^ ((2 * n) + 1))) / ((2 * n) + 1) ) & ( for n being Nat holds b2 . n = (((- 1) |^ n) * (r |^ ((2 * n) + 1))) / ((2 * n) + 1) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines Leibniz_Series_of LEIBNIZ1:def 2 :
for r being Real
for b2 being Real_Sequence holds
( b2 = Leibniz_Series_of r iff for n being Nat holds b2 . n = (((- 1) |^ n) * (r |^ ((2 * n) + 1))) / ((2 * n) + 1) );

definition
coherence ;
end;

:: deftheorem defines Leibniz_Series LEIBNIZ1:def 3 :

theorem Th9: :: LEIBNIZ1:9
for r being Real st r in [.(- 1),1.] holds
( abs is nonnegative-yielding & abs is non-increasing & abs is convergent & lim () = 0 )
proof end;

theorem Th10: :: LEIBNIZ1:10
for r being Real holds
( ( r >= 0 implies alternating_series () = Leibniz_Series_of r ) & ( r < 0 implies (- 1) (#) () = Leibniz_Series_of r ) )
proof end;

theorem Th11: :: LEIBNIZ1:11
for r being Real st r in [.(- 1),1.] holds
Leibniz_Series_of r is summable
proof end;

theorem Th12: :: LEIBNIZ1:12
for n being Nat
for r being Real
for A being non empty closed_interval Subset of REAL st A = [.0,r.] & r >= 0 holds
arctan . r = ( . n) + (integral ((((- 1) |^ (n + 1)) (#) ((#Z (2 * (n + 1))) / (() + (#Z 2)))),A))
proof end;

theorem Th13: :: LEIBNIZ1:13
for r being Real st 0 <= r & r <= 1 holds
arctan . r = Sum
proof end;

:: Leibniz's Series for $\pi$
theorem Th14: :: LEIBNIZ1:14

theorem Th15: :: LEIBNIZ1:15
for n being Nat holds
( . ((2 * n) + 1) <= Sum Leibniz_Series & Sum Leibniz_Series <= . (2 * n) )
proof end;

theorem Th16: :: LEIBNIZ1:16
for n being Nat holds
( . 1 = 2 / 3 & ( n is odd implies . (n + 2) = () + (2 / (((4 * (n ^2)) + (16 * n)) + 15)) ) )
proof end;

:: $\pi$ Approximation
theorem :: LEIBNIZ1:17
( 313 / 100 < PI & PI < 315 / 100 )
proof end;