Quelle atan.pvs Sprache: PVS

atan: THEORY
%------------------------------------------------------------------------------
%
%  Axiomatic atan
%
%          David Lester                    Manchester University
%
%------------------------------------------------------------------------------
BEGIN

  IMPORTING reals@sq, reals@sigma, reals@sqrt
  IMPORTING reals@factorial
%  IMPORTING reals@harmonic_polynomials %,polynomial_deriv
  IMPORTING reals@binomial, reals@real_fun_preds
%  IMPORTING reals@polynomials         %%% INCLUDING THIS CAUSES BUG
                                       %%% bin out of date when in complex lib

  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

  IMPORTING trig_basic                %% to get value of pi here

% --- from sincos_def ---
  a: VAR real
  tan_value_TCC: AXIOM -pi/2 < a AND a <  pi/2 IMPLIES Tan?(a)

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

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

% non-A&S definitions

  pi_value: AXIOM pi = 4*atan(1)      %%%%% RWB conflicts with trig_basic

  atan_strict_increasing: AXIOM strict_increasing?(atan)

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

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

% A&S defs

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

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

  atan_minus: AXIOM                                                    % 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))

%  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: AXIOM px/(1+px*px) < atan(px) AND atan(px) < px
  pi_bnds:   LEMMA 306/100 < pi AND pi < 319/100

% atan Taylor's Theorem

  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: AXIOM abs(atan(x)-atan_series_n(x,n)) <= abs(x^(2*n+3))/(2*n+3)

END atan

%============================================================================
%  IMPORTING analysis@derivatives, analysis@restrict2_deriv
%  IMPORTING analysis@derivative_props, analysis@fundamental_theorem
%  IMPORTING analysis@chain_rule, analysis@derivatives_more
%  IMPORTING analysis@continuous_functions_props, analysis@integral

%  one_over_one_plus_t_sq_cont: LEMMA continuous[real](atan_deriv_fn)

%  atan_def: LEMMA atan(x)  = Integral(0,x,(LAMBDA (x:real):1/(1+x*x)))  %  4.4.3
%  deriv_atan_fun: LEMMA derivable(atan) AND
%                        deriv(atan) = (LAMBDA (x:real): 1/(1+x*x))     % 4.4.54
%   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
%    derivable_n_times(atanN(n),m) AND derivable_n_times(atanD(n),m)

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

quality100%

¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.