Quelle  atan.pvs

atan: THEORY
%------------------------------------------------------------------------------
%
%  A foundational theory of atan(x) for the interval [0,pi/2]
%
%          David Lester                    Manchester University
% 
%------------------------------------------------------------------------------
BEGIN

%  IMPORTING reals@prelude_aux_reals, 
  IMPORTING reals@sq, reals@sigma, reals@sqrt, reals@poly_rew
  IMPORTING analysis@derivatives, analysis@restrict2_deriv, analysis@deriv_domains
  IMPORTING analysis@derivative_props, analysis@fundamental_theorem
  IMPORTING analysis@chain_rule,  analysis@derivative_props   % , analysis@derivatives_more
  IMPORTING analysis@continuous_functions_props, analysis@integral
  IMPORTING reals@factorial
  IMPORTING analysis@nth_derivatives[real], analysis@taylors[real]
  IMPORTING reals@harmonic_polynomials, analysis@polynomial_deriv
  IMPORTING reals@binomial, analysis@indefinite_integral

  AUTO_REWRITE- abs_0
  AUTO_REWRITE- abs_nat


  posreal_ge1: NONEMPTY_TYPE = {x:real | x >= 1} CONTAINING 1

  x,y:   VAR real
  px,py: VAR posreal
  nx:    VAR negreal
  nnx:   VAR nnreal
  nzx:   VAR nzreal
  n,m:   VAR nat
  pn:    VAR posnat

  atan_deriv_fn(x:real):posreal = 1/(1+x*x)

  one_over_one_plus_t_sq_cont: LEMMA continuous?[real](atan_deriv_fn)

  atan_value(x:real):real = Integral[real](0,x,atan_deriv_fn)

  atan_value_0      : LEMMA atan_value(0)  = 0
  atan_neg_value    : LEMMA atan_value(-x) = -atan_value(x)
  atan_inv_value    : LEMMA atan_value(1/px) = 2*atan_value(1)-atan_value(px)
  atan_inv_neg_value: LEMMA atan_value(1/nx) = -2*atan_value(1)-atan_value(nx)

  atan_value_strict_increasing: LEMMA strict_increasing?(atan_value)

  atan_value_minus_x1: LEMMA -1/py < x IMPLIES
             atan_value(x)-atan_value(py) = atan_value((x-py)/(1+x*py))

  atan_value_minus_x2: LEMMA x < -1/py IMPLIES
             4*atan_value(1) + atan_value(x) - atan_value(py)
                                   = atan_value((x-py)/(1+x*py))
  atan_value_minus: LEMMA
  (-1 < x*y => atan_value(x)-atan_value(y) = atan_value((x-y)/(1+x*y))) AND
  (x*y < -1 & y > 0 => atan_value(x)-atan_value(y)+4*atan_value(1)
                                           = atan_value((x-y)/(1+x*y))) AND
  (x*y < -1 & y < 0 => atan_value(x)-atan_value(y)-4*atan_value(1)
                                           = atan_value((x-y)/(1+x*y)))

  pi:posreal = 4*atan_value(1)

%  real_mpi_ppi: NONEMPTY_TYPE = {x:real | abs(x)<2*atan_value(1)} CONTAINING 0
%  real_mpi_ppi: NONEMPTY_TYPE = {x:real | abs(x) < pi/2} CONTAINING 0

%  real_abs_lt_pi2: NONEMPTY_TYPE = {x | abs(x) < pi/2} CONTAINING 0
  real_abs_lt_pi2: NONEMPTY_TYPE = {x | -pi/2 < x AND x < pi/2} CONTAINING 0

%  atan_abs_lt_pi2: JUDGEMENT atan(x) HAS_TYPE real_abs_lt_pi2

  atan(x:real): real_abs_lt_pi2 = atan_value(x)

  pi_value: LEMMA pi = 4*atan(1)

% non-A&S definitions

  atan_strict_increasing: LEMMA strict_increasing?(atan)

  atan_bij              : LEMMA bijective?[real,real_abs_lt_pi2](atan)
  atan_0                : LEMMA atan(0) = 0

  atan_inv              : LEMMA atan(1/px) = pi/2-atan(px)
  atan_inv_neg          : LEMMA atan(1/nx) = -pi/2-atan(nx)


% A&S defs

  atan_def: LEMMA atan(x) = Integral(0,x,(LAMBDA (x:real):1/(1+x*x)))  %  4.4.3

  acot(nzx:nzreal):nzreal    = atan(1/nzx)                             %  4.4.8

  atan_neg: LEMMA atan(-x)   = -atan(x)                                % 4.4.16
  acot_neg: LEMMA acot(-nzx) = -acot(nzx)                              % 4.4.19

  atan_minus: LEMMA                                                    % 4.4.34
  (-1 < x*y =>         atan(x)-atan(y)    = atan((x-y)/(1+x*y))) AND
  (x*y < -1 & y > 0 => atan(x)-atan(y)+pi = atan((x-y)/(1+x*y))) AND
  (x*y < -1 & y < 0 => atan(x)-atan(y)-pi = atan((x-y)/(1+x*y)))

  atan_plus:  LEMMA                                                    % 4.4.34
  (x*y < 1 => atan(x)+atan(y)            = atan((x+y)/(1-x*y))) AND
  (1 < x*y & y > 0 => atan(x)+atan(y)-pi = atan((x+y)/(1-x*y))) AND
  (1 < x*y & y < 0 => atan(x)+atan(y)+pi = atan((x+y)/(1-x*y)))

  atan_sub_swap : LEMMA
    x /= 0 AND y /= 0 IMPLIES
    atan(x/y)-atan(y/x) = atan((x^2-y^2)/(2*x*y))

  deriv_atan_fun: LEMMA derivable?(atan) AND
                        deriv(atan) = (LAMBDA (x:real): 1/(1+x*x))     % 4.4.54

  continuous_atan: LEMMA continuous?[real](atan)

% more non-A&S definitions

  atan_1:    LEMMA atan(1) = 4*atan(1/5) - atan(1/239)
  atan_bnds: LEMMA px/(1+px*px) < atan(px) AND atan(px) < px
  pi_bnds:   LEMMA 306/100 < pi AND pi < 319/100

% 5/26 < atan(1/5) < 1/5
% 239/57122 < atan(1/239) < 1/239
% 40/13-4/239 < pi < 16/5 - 4*239/57122

% atan Taylor's Theorem

  atanS(n:nat)(x:real):real = harmonic_poly_real(2*n+1,1,x)
  atanD(n:nat)(x:real):real = (1+x*x)^(2*n+1)
  atanF(n:nat)(i:nat ):int
    = IF i > 2*n OR odd?(i) THEN 0
      ELSE (-1)^(i/2+n)*factorial(2*n)*C(2*n+1,i) ENDIF
   atanN(n:nat):[real->real] = polynomial(atanF(n),2*n)

  atan_taylors_prep1: LEMMA
    abs(atanS(n)(x)) <= (1+x*x)^n * sqrt(1+x*x)

  atan_taylors_prep2: LEMMA
    (-1)^n*factorial(2*n)*atanS(n) = atanN(n)

  atan_taylors_prep3: LEMMA   %% bug %%
    derivable_n_times?(atanN(n),m) AND derivable_n_times?(atanD(n),m)

  atanN_derivable   : LEMMA derivable?(atanN(n))
  atanD_derivable   : LEMMA derivable?(atanD(n))

  atan_taylors_prep4: LEMMA
    deriv(atanN(n))
      = IF n = 0 THEN const_fun(0)
                 ELSE polynomial(LAMBDA (i:nat): (i+1)*atanF(n)(i+1),2*n-1)
        ENDIF

  atan_taylors_prep5: LEMMA
    deriv(atanD(n)) = (LAMBDA (x:real): (4*n+2)*x*(1+x*x)^(2*n))

  atan_taylors_prep6: LEMMA
    deriv(deriv(atanN(n)))
      = IF n = 0 THEN const_fun(0)
                 ELSE polynomial(LAMBDA (i:nat): (i+2)*(i+1)*atanF(n)(i+2),2*n-2)
        ENDIF

  atan_taylors_prep7: LEMMA FORALL (f:[real->real], g:[real->nzreal]):
    derivable?(f) AND derivable?(g) IMPLIES
    derivable?(f/g^pn) AND deriv(f/g^pn) = (deriv(f)*g-pn*f*deriv(g))/(g^(pn+1))

  atan_taylors_prep8: LEMMA 
    deriv(deriv(atanN(n)/atanD(n))) = atanN(n+1)/atanD(n+1)

  atan_series_prep4: LEMMA derivable_n_times?(atanN(n)/atanD(n),2*m)

  atan_series_prep5: LEMMA nderiv(2*m,atanN(n)/atanD(n))=atanN(n+m)/atanD(n+m)

  atan_series_prep6: LEMMA 
     derivable_n_times?(LAMBDA (x:real): 1/(1+x*x),2*n) AND
     nderiv(2*n,LAMBDA (x:real): 1/(1+x*x)) = atanN(n)/atanD(n)

  atan_nderiv: LEMMA
    nderiv(n,atan)
      = IF n = 0 THEN atan ELSIF even?(n)
                 THEN (deriv(atanN(n/2-1))*(LAMBDA (x:real): (1+x*x)) -
                          atanN(n/2-1)*(LAMBDA (x:real): (2*n-2)*x))      /
                      (atanD(n/2-1)*(LAMBDA (x:real): (1+x*x)))
                 ELSE atanN((n-1)/2)/atanD((n-1)/2) ENDIF

  atan_nderiv_0: LEMMA
    nderiv(n,atan)(0)
            = IF even?(n) THEN 0 ELSE (-1)^((n-1)/2) * factorial(n-1) ENDIF

  atan_n_times_derivable: LEMMA derivable_n_times?(atan,n)

  atan_series_prep7: LEMMA
    abs(atanN(n)(x)) <= factorial(2*n)*(1+x*x)^(2*n+1)

  atan_series_prep8: LEMMA abs(nderiv(2*n+1,atan)(x)) <= factorial(2*n)

  atan_series_coef(n:nat):rat = ((-1)^n)/(2*n+1)
  atan_series_term(x:real):[nat->real]
     = (LAMBDA (n:nat): x^(2*n+1) * atan_series_coef(n))
  atan_series_n(x:real,n:nat):real = sigma(0,n,atan_series_term(x))

  atan_series_n_increasing: LEMMA
    FORALL (x,y:nnreal): x<=y AND y<=1 IMPLIES
    atan_series_n(x,n) <= atan_series_n(y,n)

  atan_series_n_a0: LEMMA
    atan_series_n(0,n) = 0

  atan_series_eqv: LEMMA
   atan_series_n(x,n) = sigma(0,2*n+2,
      LAMBDA (nn:nat): IF nn > 2*n+2 OR nn = 0 THEN 0 ELSE
                         nderiv(nn,atan)(0)*x^nn/factorial(nn) ENDIF)

  atan_taylors: LEMMA (EXISTS (c: between(0,x)): 
               atan(x) = atan_series_n(x,n)
                      +  nderiv(2*n+3,atan)(c)*x^(2*n+3)/factorial(2*n+3))

  atan_series: LEMMA abs(atan(x)-atan_series_n(x,n)) <= abs(x^(2*n+3))/(2*n+3)

END atan