:: Basel Problem -- Preliminaries
::  by Artur Korni{\l}owicz and Karol P\kak
:: 
:: Received June 27, 2017
:: Copyright (c) 2017-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 XCMPLX_0, SUBSET_1, FUNCT_1, ARYTM_3, ORDINAL4, COMPLEX1, SEQ_4,
      ORDINAL2, NUMBERS, REAL_1, RELAT_1, NAT_1, CARD_3, SQUARE_1, SIN_COS,
      CARD_1, XXREAL_0, SEQ_1, VALUED_0, SEQ_2, VALUED_1, PARTFUN1, XBOOLE_0,
      ARYTM_1, XXREAL_2, FINSEQ_1, RVSUM_1, INT_1, TARSKI, XXREAL_1, SIN_COS4,
      ABIAN, RCOMP_1, MEASURE5, REALSET1, INTEGRA1, PREPOWER, POLYEQ_1,
      COMSEQ_1, FINSEQ_2, BASEL_1;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, RELAT_1, FUNCT_1, RELSET_1,
      PARTFUN1, FUNCT_2, NUMBERS, XXREAL_0, XCMPLX_0, COMPLEX1, XREAL_0, INT_1,
      SQUARE_1, CARD_1, FINSEQ_1, VALUED_0, VALUED_1, RVSUM_1, SEQ_1, SEQ_2,
      SEQ_4, RFUNCT_1, FCONT_1, RCOMP_1, SERIES_1, PREPOWER, ABIAN, TAYLOR_1,
      SIN_COS, SIN_COS4, INTEGRA1, MEASURE5, INTEGRA5, POLYEQ_1, FINSEQ_2,
      COMSEQ_1, COMSEQ_3;
 constructors SEQ_2, SIN_COS, SQUARE_1, COMSEQ_2, RELSET_1, COMSEQ_3, SIN_COS4,
      RFUNCT_1, ABIAN, INTEGRA1, INTEGRA5, FCONT_1, TAYLOR_1, PREPOWER, SEQ_4,
      WSIERP_1, POLYEQ_1;
 registrations XCMPLX_0, XREAL_0, NAT_1, ORDINAL1, SQUARE_1, VALUED_0,
      RELSET_1, VALUED_1, MEMBERED, FUNCT_2, INT_1, NUMBERS, SIN_COS, SEQ_2,
      SIN_COS6, RCOMP_1, FCONT_1, MEASURE5, LEIBNIZ1, DBLSEQ_2, XBOOLE_0,
      XXREAL_0, RELAT_1, FINSEQ_1, CARD_1, RVSUM_1, NEWTON04, POLYEQ_1, NEWTON;
 requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;


begin :: Preliminaries

reserve X for set;
reserve k,m,n for Nat;
reserve i for Integer;
reserve a,b,c,d,e,g,p,r,x,y for Real;
reserve z for Complex;

theorem :: BASEL_1:1
  0 < a implies ex m st 0 < a*m+b;

registration
  let f be real-valued FinSequence;
  let n;
  cluster f|n -> REAL-valued;
end;

registration
  let f be complex-valued FinSequence;
  cluster f^2 -> len f-element;
  cluster f" -> len f-element;
end;

registration
  let f be complex-valued FinSequence;
  let c be Complex;
  cluster c+f -> len f-element;
end;

theorem :: BASEL_1:2
  for c,z being Complex holds c + <*z*> = <*c+z*>;

theorem :: BASEL_1:3
  for f,g being complex-valued FinSequence, c being Complex holds
  c+(f^g) = (c+f)^(c+g);

theorem :: BASEL_1:4
  for f being complex-valued FinSequence, c being Complex holds
  Sum(c+f) = (c*len f) + Sum f;

begin :: Limits of sequences $\frac{an+b}{cn+d}$

definition
  let a,b,c,d be Complex;
  func Rat_Exp_Seq(a,b,c,d) -> Complex_Sequence means
:: BASEL_1:def 1
     it.n = Polynom(a,b,n)/Polynom(c,d,n);
end;

definition
  let a,b,c,d;
  func rseq(a,b,c,d) -> Real_Sequence equals
:: BASEL_1:def 2
    Re (Rat_Exp_Seq(a,b,c,d));
end;

theorem :: BASEL_1:5
  rseq(a,b,c,d).n = (a*n+b)/(c*n+d);

theorem :: BASEL_1:6
  rseq(0,b,0,d).n = b/d;

registration
  let a,b;
  cluster rseq(a,b,0,0) -> constant;
end;

registration
  let b,d;
  cluster rseq(0,b,0,d) -> constant;
end;

theorem :: BASEL_1:7
  rseq(0,b,c,d) = b(#)rseq(0,1,c,d) &
  rseq(0,b,c,d) = (-b)(#)rseq(0,1,-c,-d);

theorem :: BASEL_1:8
  rseq(a,0,c,d) = a(#)rseq(1,0,c,d) &
  rseq(a,0,c,d) = (-a)(#)rseq(1,0,-c,-d);

registration
  let b,c,d;
  cluster rseq(0,b,c,d) -> convergent;
end;

theorem :: BASEL_1:9
  lim(rseq(0,b,0,d)) = b/d;

theorem :: BASEL_1:10
  for c being non zero Real holds lim(rseq(0,b,c,d)) = 0;

registration
  let c be non zero Real;
  let a,b,d;
  cluster rseq(a,b,c,d) -> convergent;
end;

registration
  let a,d be positive Real;
  let b be Real;
  cluster rseq(a,b,0,d) -> non bounded_above;
end;

registration
  let a,d be negative Real;
  let b;
  cluster rseq(a,b,0,d) -> non bounded_above;
end;

registration
  let a be positive Real;
  let b;
  let d be negative Real;
  cluster rseq(a,b,0,d) -> non bounded_below;
 end;

registration
  let a be negative Real;
  let b;
  let d be positive Real;
  cluster rseq(a,b,0,d) -> non bounded_below;
end;

registration
  let a,d be non zero Real;
  let b;
  cluster rseq(a,b,0,d) -> non bounded;
end;

registration
  let a,d be non zero Real;
  let b;
  cluster rseq(a,b,0,d) -> non convergent;
end;

theorem :: BASEL_1:11
  for c being non zero Real holds lim(rseq(a,b,c,d)) = a/c;

theorem :: BASEL_1:12
  for a being non zero Real holds lim(rseq(a,b,a,d)) = 1;

begin :: Trigonometry

theorem :: BASEL_1:13
  sin(PI*i) = 0;

theorem :: BASEL_1:14
  cos(PI/2+PI*i) = 0;

theorem :: BASEL_1:15
  tan r = (cot r)" & cot r = (tan r)";

theorem :: BASEL_1:16
  dom tan = union the set of all ]. -PI/2+PI*i,PI/2+PI*i .[ where i is Integer;

registration
  cluster dom tan -> open for Subset of REAL;
end;

theorem :: BASEL_1:17
  0 <= r implies sin.r <= r;

theorem :: BASEL_1:18
  0 <= r < PI/2 implies r <= tan.r;

begin :: Some special functions and sequences

definition
  let f be real-valued Function;
  func cot(f) -> Function means
:: BASEL_1:def 3
    dom it = dom f &
    for x being object st x in dom f holds it.x = cot(f.x);
  func cosec(f) -> Function means
:: BASEL_1:def 4
    dom it = dom f &
    for x being object st x in dom f holds it.x = cosec(f.x);
end;

registration
  let f be real-valued Function;
  cluster cot(f) -> REAL-valued;
  cluster cosec(f) -> REAL-valued;
end;

registration
  let f be real-valued FinSequence;
  cluster cot(f) -> FinSequence-like;
  cluster cosec(f) -> FinSequence-like;
end;

theorem :: BASEL_1:19
  for f being real-valued FinSequence holds len cot f = len f;

theorem :: BASEL_1:20
  for f being real-valued FinSequence holds len cosec f = len f;

registration
  let f be real-valued FinSequence;
  cluster cot(f) -> len f-element;
  cluster cosec(f) -> len f-element;
end;

definition
  let m;
  func x_r-seq(m) -> FinSequence equals
:: BASEL_1:def 5
    (PI/(2*m+1))(#)(idseq m);
end;

theorem :: BASEL_1:21
  len (x_r-seq m) = m &
  for k st 1 <= k <= m holds x_r-seq(m).k = k*PI/(2*m+1);

theorem :: BASEL_1:22
  rng x_r-seq(m) c= ].0,PI/2.[;

registration
  let m;
  cluster x_r-seq(m) -> REAL-valued;
end;

theorem :: BASEL_1:23
  1 <= k <= m implies 0 < x_r-seq(m).k < PI/2;

registration
  cluster x_r-seq(0) -> empty;
end;

theorem :: BASEL_1:24
  1 <= k <= m implies 2/(k*PI) + (x_r-seq(m))".k = (x_r-seq(m+1))".k;

theorem :: BASEL_1:25
  1 <= k <= m implies (2*m+1)*x_r-seq(m).k = k*PI;

theorem :: BASEL_1:26
  sqr cosec x_r-seq(m) = 1 + sqr cot x_r-seq(m);

theorem :: BASEL_1:27
  x_r-seq(n) is one-to-one;

theorem :: BASEL_1:28
  sqr cot x_r-seq(n) is one-to-one;

theorem :: BASEL_1:29
  Sum sqr cot x_r-seq(m) <= Sum ((sqr x_r-seq(m))");

theorem :: BASEL_1:30
  Sum ((sqr x_r-seq(m))") <= Sum sqr cosec x_r-seq(m);

definition
  func Basel-seq -> Real_Sequence equals
:: BASEL_1:def 6
    rseq(0,1,1,0) (#) rseq(0,1,1,0);
  func Basel-seq1 -> Real_Sequence equals
:: BASEL_1:def 7
    (PI^2/6) (#) rseq(2,0,2,1) (#) rseq(2,-1,2,1);
  func Basel-seq2 -> Real_Sequence equals
:: BASEL_1:def 8
    (PI^2/6) (#) rseq(2,0,2,1) (#) rseq(2,2,2,1);
end;

theorem :: BASEL_1:31
  Basel-seq.n = 1 / (n^2);

theorem :: BASEL_1:32
  Basel-seq1.n = (PI^2/6) * (2*n/(2*n+1)) * ((2*n-1)/(2*n+1));

theorem :: BASEL_1:33
  Basel-seq2.n = (PI^2/6) * (2*n/(2*n+1)) * ((2*n+2)/(2*n+1));

registration
  cluster Basel-seq -> convergent;
  cluster Basel-seq1 -> convergent;
  cluster Basel-seq2 -> convergent;
end;

theorem :: BASEL_1:34
  lim Basel-seq1 = PI^2/6 = lim Basel-seq2;

theorem :: BASEL_1:35
  Sum ((sqr x_r-seq(m))") = (2*m+1)^2 / (PI^2) * Sum(Basel-seq,m);