Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: atan.pvs Sprache: PVS

Original von: 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

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.