:: by Artur Korni{\l}owicz and Karol P\kak

::

:: Received June 27, 2017

:: Copyright (c) 2017-2021 Association of Mizar Users

set p = (PI ^2) / 6;

Lm1: for f being FinSequence

for h being Function st dom h = dom f holds

h is FinSequence

proof end;

Lm2: for f being FinSequence

for y being object st y in rng f holds

ex n being Nat st

( 1 <= n & n <= len f & y = f . n )

proof end;

Lm3: for f being complex-valued FinSequence holds len (f ") = len f

proof end;

registration

let f be complex-valued FinSequence;

coherence

f ^2 is len f -element

f " is len f -element

end;
coherence

f ^2 is len f -element

proof end;

coherence f " is len f -element

proof end;

registration
end;

theorem :: BASEL_1:4

for f being complex-valued FinSequence

for c being Complex holds Sum (c + f) = (c * (len f)) + (Sum f)

for c being Complex holds Sum (c + f) = (c * (len f)) + (Sum f)

proof end;

definition

let a, b, c, d be Complex;

deffunc H_{1}( Nat) -> set = (Polynom (a,b,$1)) / (Polynom (c,d,$1));

ex b_{1} being Complex_Sequence st

for n being Nat holds b_{1} . n = (Polynom (a,b,n)) / (Polynom (c,d,n))

for b_{1}, b_{2} being Complex_Sequence st ( for n being Nat holds b_{1} . n = (Polynom (a,b,n)) / (Polynom (c,d,n)) ) & ( for n being Nat holds b_{2} . n = (Polynom (a,b,n)) / (Polynom (c,d,n)) ) holds

b_{1} = b_{2}

end;
deffunc H

func Rat_Exp_Seq (a,b,c,d) -> Complex_Sequence means :Def1: :: BASEL_1:def 1

for n being Nat holds it . n = (Polynom (a,b,n)) / (Polynom (c,d,n));

existence for n being Nat holds it . n = (Polynom (a,b,n)) / (Polynom (c,d,n));

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines Rat_Exp_Seq BASEL_1:def 1 :

for a, b, c, d being Complex

for b_{5} being Complex_Sequence holds

( b_{5} = Rat_Exp_Seq (a,b,c,d) iff for n being Nat holds b_{5} . n = (Polynom (a,b,n)) / (Polynom (c,d,n)) );

for a, b, c, d being Complex

for b

( b

:: deftheorem defines rseq BASEL_1:def 2 :

for a, b, c, d being Real holds rseq (a,b,c,d) = Re (Rat_Exp_Seq (a,b,c,d));

for a, b, c, d being Real holds rseq (a,b,c,d) = Re (Rat_Exp_Seq (a,b,c,d));

theorem Th5: :: BASEL_1:5

for n being Nat

for a, b, c, d being Real holds (rseq (a,b,c,d)) . n = ((a * n) + b) / ((c * n) + d)

for a, b, c, d being Real holds (rseq (a,b,c,d)) . n = ((a * n) + b) / ((c * n) + d)

proof end;

theorem Th7: :: BASEL_1:7

for b, c, d being Real holds

( rseq (0,b,c,d) = b (#) (rseq (0,1,c,d)) & rseq (0,b,c,d) = (- b) (#) (rseq (0,1,(- c),(- d))) )

( rseq (0,b,c,d) = b (#) (rseq (0,1,c,d)) & rseq (0,b,c,d) = (- b) (#) (rseq (0,1,(- c),(- d))) )

proof end;

theorem Th8: :: BASEL_1:8

for a, c, d being Real holds

( rseq (a,0,c,d) = a (#) (rseq (1,0,c,d)) & rseq (a,0,c,d) = (- a) (#) (rseq (1,0,(- c),(- d))) )

( rseq (a,0,c,d) = a (#) (rseq (1,0,c,d)) & rseq (a,0,c,d) = (- a) (#) (rseq (1,0,(- c),(- d))) )

proof end;

Lm4: for c, d being Real st 0 < c holds

for p being Real st 0 < p holds

ex n being Nat st

for m being Nat st n <= m holds

|.(((rseq (0,1,c,d)) . m) - 0).| < p

proof end;

Lm5: for c, d being Real st 0 < c holds

rseq (0,1,c,d) is convergent

proof end;

Lm6: for c, d being Real holds rseq (0,1,c,d) is convergent

proof end;

Lm7: for c, d being Real st 0 < c holds

lim (rseq (0,1,c,d)) = 0

proof end;

Lm8: for c, d being Real st c < 0 holds

lim (rseq (0,1,c,d)) = 0

proof end;

Lm9: for c, d being Real st 0 < c holds

for p being Real st 0 < p holds

ex n being Nat st

for m being Nat st n <= m holds

|.(((rseq (1,0,c,d)) . m) - (1 / c)).| < p

proof end;

Lm10: for c, d being Real st 0 < c holds

rseq (1,0,c,d) is convergent

proof end;

Lm11: for c, d being Real st 0 < c holds

lim (rseq (1,0,c,d)) = 1 / c

proof end;

Lm12: for d being Real

for c being non zero Real holds rseq (1,0,c,d) is convergent

proof end;

Lm13: for d being Real

for c being non zero Real holds lim (rseq (1,0,c,d)) = 1 / c

proof end;

registration
end;

registration
end;

registration
end;

registration

let a be positive Real;

let b be Real;

let d be negative Real;

coherence

not rseq (a,b,0,d) is bounded_below

end;
let b be Real;

let d be negative Real;

coherence

not rseq (a,b,0,d) is bounded_below

proof end;

registration

let a be negative Real;

let b be Real;

let d be positive Real;

coherence

not rseq (a,b,0,d) is bounded_below

end;
let b be Real;

let d be positive Real;

coherence

not rseq (a,b,0,d) is bounded_below

proof end;

registration
end;

registration
end;

registration
end;

definition

let f be real-valued Function;

ex b_{1} being Function st

( dom b_{1} = dom f & ( for x being object st x in dom f holds

b_{1} . x = cot (f . x) ) )

for b_{1}, b_{2} being Function st dom b_{1} = dom f & ( for x being object st x in dom f holds

b_{1} . x = cot (f . x) ) & dom b_{2} = dom f & ( for x being object st x in dom f holds

b_{2} . x = cot (f . x) ) holds

b_{1} = b_{2}

ex b_{1} being Function st

( dom b_{1} = dom f & ( for x being object st x in dom f holds

b_{1} . x = cosec (f . x) ) )

for b_{1}, b_{2} being Function st dom b_{1} = dom f & ( for x being object st x in dom f holds

b_{1} . x = cosec (f . x) ) & dom b_{2} = dom f & ( for x being object st x in dom f holds

b_{2} . x = cosec (f . x) ) holds

b_{1} = b_{2}

end;
func cot f -> Function means :Def3: :: BASEL_1:def 3

( dom it = dom f & ( for x being object st x in dom f holds

it . x = cot (f . x) ) );

existence ( dom it = dom f & ( for x being object st x in dom f holds

it . x = cot (f . x) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

func cosec f -> Function means :Def4: :: BASEL_1:def 4

( dom it = dom f & ( for x being object st x in dom f holds

it . x = cosec (f . x) ) );

existence ( dom it = dom f & ( for x being object st x in dom f holds

it . x = cosec (f . x) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def3 defines cot BASEL_1:def 3 :

for f being real-valued Function

for b_{2} being Function holds

( b_{2} = cot f iff ( dom b_{2} = dom f & ( for x being object st x in dom f holds

b_{2} . x = cot (f . x) ) ) );

for f being real-valued Function

for b

( b

b

:: deftheorem Def4 defines cosec BASEL_1:def 4 :

for f being real-valued Function

for b_{2} being Function holds

( b_{2} = cosec f iff ( dom b_{2} = dom f & ( for x being object st x in dom f holds

b_{2} . x = cosec (f . x) ) ) );

for f being real-valued Function

for b

( b

b

registration

let f be real-valued Function;

coherence

cot f is REAL -valued

cosec f is REAL -valued

end;
coherence

cot f is REAL -valued

proof end;

coherence cosec f is REAL -valued

proof end;

registration

let f be real-valued FinSequence;

coherence

cot f is FinSequence-like

cosec f is FinSequence-like

end;
coherence

cot f is FinSequence-like

proof end;

coherence cosec f is FinSequence-like

proof end;

registration

let f be real-valued FinSequence;

coherence

cot f is len f -element

cosec f is len f -element

end;
coherence

cot f is len f -element

proof end;

coherence cosec f is len f -element

proof end;

Lm16: for n being Nat holds (rseq (0,1,1,0)) . n = 1 / n

proof end;

Lm17: lim (rseq (2,0,2,1)) = 1

by Th12;

Lm18: lim (rseq (2,(- 1),2,1)) = 1

by Th12;

Lm19: lim (rseq (2,2,2,1)) = 1

by Th12;

:: deftheorem defines x_r-seq BASEL_1:def 5 :

for m being Nat holds x_r-seq m = (PI / ((2 * m) + 1)) (#) (idseq m);

for m being Nat holds x_r-seq m = (PI / ((2 * m) + 1)) (#) (idseq m);

theorem Th19: :: BASEL_1:21

for m being Nat holds

( len (x_r-seq m) = m & ( for k being Nat st 1 <= k & k <= m holds

(x_r-seq m) . k = (k * PI) / ((2 * m) + 1) ) )

( len (x_r-seq m) = m & ( for k being Nat st 1 <= k & k <= m holds

(x_r-seq m) . k = (k * PI) / ((2 * m) + 1) ) )

proof end;

registration
end;

theorem :: BASEL_1:24

for k, m being Nat st 1 <= k & k <= m holds

(2 / (k * PI)) + (((x_r-seq m) ") . k) = ((x_r-seq (m + 1)) ") . k

(2 / (k * PI)) + (((x_r-seq m) ") . k) = ((x_r-seq (m + 1)) ") . k

proof end;

definition

coherence

(rseq (0,1,1,0)) (#) (rseq (0,1,1,0)) is Real_Sequence ;

(((PI ^2) / 6) (#) (rseq (2,0,2,1))) (#) (rseq (2,(- 1),2,1)) is Real_Sequence ;

(((PI ^2) / 6) (#) (rseq (2,0,2,1))) (#) (rseq (2,2,2,1)) is Real_Sequence ;

end;
(rseq (0,1,1,0)) (#) (rseq (0,1,1,0)) is Real_Sequence ;

func Basel-seq1 -> Real_Sequence equals :: BASEL_1:def 7

(((PI ^2) / 6) (#) (rseq (2,0,2,1))) (#) (rseq (2,(- 1),2,1));

coherence (((PI ^2) / 6) (#) (rseq (2,0,2,1))) (#) (rseq (2,(- 1),2,1));

(((PI ^2) / 6) (#) (rseq (2,0,2,1))) (#) (rseq (2,(- 1),2,1)) is Real_Sequence ;

func Basel-seq2 -> Real_Sequence equals :: BASEL_1:def 8

(((PI ^2) / 6) (#) (rseq (2,0,2,1))) (#) (rseq (2,2,2,1));

coherence (((PI ^2) / 6) (#) (rseq (2,0,2,1))) (#) (rseq (2,2,2,1));

(((PI ^2) / 6) (#) (rseq (2,0,2,1))) (#) (rseq (2,2,2,1)) is Real_Sequence ;

:: deftheorem defines Basel-seq1 BASEL_1:def 7 :

Basel-seq1 = (((PI ^2) / 6) (#) (rseq (2,0,2,1))) (#) (rseq (2,(- 1),2,1));

Basel-seq1 = (((PI ^2) / 6) (#) (rseq (2,0,2,1))) (#) (rseq (2,(- 1),2,1));

:: deftheorem defines Basel-seq2 BASEL_1:def 8 :

Basel-seq2 = (((PI ^2) / 6) (#) (rseq (2,0,2,1))) (#) (rseq (2,2,2,1));

Basel-seq2 = (((PI ^2) / 6) (#) (rseq (2,0,2,1))) (#) (rseq (2,2,2,1));

theorem :: BASEL_1:32

for n being Nat holds Basel-seq1 . n = (((PI ^2) / 6) * ((2 * n) / ((2 * n) + 1))) * (((2 * n) - 1) / ((2 * n) + 1))

proof end;

theorem :: BASEL_1:33

for n being Nat holds Basel-seq2 . n = (((PI ^2) / 6) * ((2 * n) / ((2 * n) + 1))) * (((2 * n) + 2) / ((2 * n) + 1))

proof end;

registration

coherence

Basel-seq is convergent ;

coherence

Basel-seq1 is convergent ;

coherence

Basel-seq2 is convergent ;

end;
Basel-seq is convergent ;

coherence

Basel-seq1 is convergent ;

coherence

Basel-seq2 is convergent ;

theorem :: BASEL_1:35

for m being Nat holds Sum ((sqr (x_r-seq m)) ") = ((((2 * m) + 1) ^2) / (PI ^2)) * (Sum (Basel-seq,m))

proof end;