:: by Karol P\kak

::

:: Received October 18, 2016

:: Copyright (c) 2016-2017 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;

registration
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)) ) )

( 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
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)) )

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))

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))

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;

ex b_{1} being Real_Sequence st

for i being Nat holds b_{1} . i = ((- 1) |^ i) * (a . i)

for b_{1}, b_{2} being Real_Sequence st ( for i being Nat holds b_{1} . i = ((- 1) |^ i) * (a . i) ) & ( for i being Nat holds b_{2} . i = ((- 1) |^ i) * (a . i) ) holds

b_{1} = b_{2}

end;
func alternating_series a -> Real_Sequence means :Def1: :: LEIBNIZ1:def 1

for i being Nat holds it . i = ((- 1) |^ i) * (a . i);

existence for i being Nat holds it . i = ((- 1) |^ i) * (a . i);

ex b

for i being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines alternating_series LEIBNIZ1:def 1 :

for a, b_{2} being Real_Sequence holds

( b_{2} = alternating_series a iff for i being Nat holds b_{2} . i = ((- 1) |^ i) * (a . i) );

for a, b

( b

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) ) ) )

( 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;

ex b_{1} being Real_Sequence st

for n being Nat holds b_{1} . n = (((- 1) |^ n) * (r |^ ((2 * n) + 1))) / ((2 * n) + 1)

for b_{1}, b_{2} being Real_Sequence st ( for n being Nat holds b_{1} . n = (((- 1) |^ n) * (r |^ ((2 * n) + 1))) / ((2 * n) + 1) ) & ( for n being Nat holds b_{2} . n = (((- 1) |^ n) * (r |^ ((2 * n) + 1))) / ((2 * n) + 1) ) holds

b_{1} = b_{2}

end;
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 for n being Nat holds it . n = (((- 1) |^ n) * (r |^ ((2 * n) + 1))) / ((2 * n) + 1);

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def2 defines Leibniz_Series_of LEIBNIZ1:def 2 :

for r being Real

for b_{2} being Real_Sequence holds

( b_{2} = Leibniz_Series_of r iff for n being Nat holds b_{2} . n = (((- 1) |^ n) * (r |^ ((2 * n) + 1))) / ((2 * n) + 1) );

for r being Real

for b

( b

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 )

( 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 ) )

( ( 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 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))

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;

:: Leibniz's Series for $\pi$

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) )

( (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)) ) )

( (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;