:: Leibniz's Series for Pi
:: by Karol P\kak
::
:: Received October 18, 2016
:: Copyright (c) 2016-2021 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
cluster arctan -> total ;
coherence
arctan is total
proof end;
cluster arctan -> differentiable ;
coherence
arctan is differentiable
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
(arctan `| Z) . 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;
cluster #Z n -> continuous ;
coherence
#Z n is continuous
proof end;
end;

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

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

theorem Th4: :: LEIBNIZ1:4
for n being Nat
for r being Real holds
( 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 end;

theorem Th5: :: LEIBNIZ1:5
for A being non empty closed_interval Subset of REAL holds integral (((#Z 0) / ((#Z 0) + (#Z 2))),A) = (arctan . (upper_bound A)) - (arctan . (lower_bound 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 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 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 0) + (#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
( (Partial_Sums (alternating_series a)) . (2 * n) >= Sum (alternating_series a) & Sum (alternating_series a) >= (Partial_Sums (alternating_series a)) . ((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
func Leibniz_Series -> Real_Sequence equals :: LEIBNIZ1:def 3
 Leibniz_Series_of 1;
coherence
Leibniz_Series_of 1 is Real_Sequence ;
end;

:: deftheorem defines Leibniz_Series LEIBNIZ1:def 3 :
Leibniz_Series = Leibniz_Series_of 1;

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

theorem Th10: :: LEIBNIZ1:10
for r being Real holds
( ( 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 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 = ((Partial_Sums (Leibniz_Series_of r)) . n) + (integral ((((- 1) |^ (n + 1)) (#) ((#Z (2 * (n + 1))) / ((#Z 0) + (#Z 2)))),A))
proof end;

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

:: WP: Leibniz's Series for $\pi$
theorem Th14: :: LEIBNIZ1:14
PI / 4 = Sum Leibniz_Series by Th13, SIN_COS9:39;

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

theorem Th16: :: LEIBNIZ1:16
for n being Nat holds
( (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 end;

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