Impressum atan_approx.pvs Sprache: PVS

atan_approx: THEORY
%-----------------------------------------------------------------------------
%      atan_approx by David Lester
%      -----------
%      Defines upper and lower bounds on atan and pi:
%           - atan_lb(a,n) <= atan(a) <= atan_ub(a,n)
%           - pi_lb(a,n) <= pi <= pi_ub(n)
%
%      Additions 2012 by Anthony Narkawicz
%
%-----------------------------------------------------------------------------
  BEGIN

  IMPORTING atan,sincos_def

  m,n   : VAR nat
  x     : VAR real
  px,py : VAR posreal

  atan_pos_le1_ub(n,x): real = atan_series_n(x,2*n)
  atan_pos_le1_lb(n,x): real = atan_series_n(x,2*n+1)

  atan_pos_le1_ub_lt : LEMMA
    0 < x AND x <= 1 IMPLIES
    atan_pos_le1_ub(n+1,x) < atan_pos_le1_ub(n,x)

  atan_pos_le1_lb_lt : LEMMA
    0 < x AND x <= 1 IMPLIES
    atan_pos_le1_lb(n,x) < atan_pos_le1_lb(n+1,x)

  atan_pos_le1_bounds: LEMMA 0 < x AND x <= 1 IMPLIES
    (atan_pos_le1_lb(n,x) < atan(x) AND atan(x) < atan_pos_le1_ub(n,x))

  atan_pos_le1_lb_inc: LEMMA px <= 1 AND n < m =>
                             atan_pos_le1_lb(n,px) < atan_pos_le1_lb(m,px)

  atan_pos_le1_ub_dec: LEMMA px <= 1 AND n < m =>
                             atan_pos_le1_ub(m,px) < atan_pos_le1_ub(n,px)

  pi_lbn(n): real = 4*(4*atan_pos_le1_lb(n,1/5) - atan_pos_le1_ub(n,1/239))
  pi_ubn(n): real = 4*(4*atan_pos_le1_ub(n,1/5) - atan_pos_le1_lb(n,1/239))

  pi_lbn_lt : LEMMA
    pi_lbn(n) < pi_lbn(n+1)

  pi_lbn_LT : LEMMA
    FORALL (k:above(n)):
      pi_lbn(n) < pi_lbn(k)

  pi_bounds: LEMMA pi_lbn(n) < pi AND pi < pi_ubn(n)

  pi_lb_pos : JUDGEMENT
    pi_lbn(n) HAS_TYPE posreal

  pi_ub_pos : JUDGEMENT
    pi_ubn(n) HAS_TYPE posreal

  pi_bounds0: LEMMA pi_lbn(0) = 281476/89625 AND    % > 3.1405
                    pi_ubn(0) = 651864872/204778785 % < 3.1837

  pi_lb : posreal = 31415926/10000000

  pi_ub : posreal = 31415927/10000000

  pi_bounds2: LEMMA pi_lb < pi_lbn(2) AND pi_ubn(2) < pi_ub

  pi_bound : JUDGEMENT pi HAS_TYPE {r:posreal | pi_lb < r AND r < pi_ub}

  pi_lb_inc: LEMMA n < m => pi_lbn(n) < pi_lbn(m)

  pi_ub_dec: LEMMA n < m => pi_ubn(m) < pi_ubn(n)

  atan_pos_lb(n,px): real = IF px <= 1 THEN atan_pos_le1_lb(n,px) ELSE
                            max(atan_pos_le1_lb(n,1),pi_lbn(n)/2 - atan_pos_le1_ub(n,1/px)) ENDIF

  atan_pos_ub(n,px): real = IF px <= 1 THEN atan_pos_le1_ub(n,px) ELSE
                            max(atan_pos_le1_ub(n,1),pi_ubn(n)/2 - atan_pos_le1_lb(n,1/px)) ENDIF

  atan_pos_bounds: LEMMA 0 < x IMPLIES
    (atan_pos_lb(n,x) < atan(x) AND atan(x) < atan_pos_ub(n,x))

  atan_lb(x,n): real = IF    x > 0 THEN atan_pos_lb(n,x)
                       ELSIF x = 0 THEN 0
                                   ELSE -atan_pos_ub(n,-x) ENDIF

  atan_ub(x,n): real = IF    x > 0 THEN atan_pos_ub(n,x)
                       ELSIF x = 0 THEN 0
                                   ELSE -atan_pos_lb(n,-x) ENDIF

  atan_bounds: LEMMA atan_lb(x,n) <= atan(x) AND atan(x) <= atan_ub(x,n)

  atan_lb_increasing: LEMMA increasing?(LAMBDA (x:real): atan_lb(x,n))

  atan_ub_increasing: LEMMA increasing?(LAMBDA (x:real): atan_ub(x,n))

  atan_pos_lb_inc: LEMMA n <= m => atan_pos_lb(n,px) <= atan_pos_lb(m,px)

  atan_pos_ub_dec: LEMMA n <= m => atan_pos_ub(m,px) <= atan_pos_ub(n,px)

  pi_lb_pi: LEMMA pi-pi_lbn(n) <= 16*((1/5)^(4*n+5)/(4*n+5)) +
                                  4*((1/239)^(4*n+3)/(4*n+3))

  pi_ub_pi: LEMMA pi_ubn(n)-pi <= 16*((1/5)^(4*n+3)/(4*n+3)) +
                                  4*((1/239)^(4*n+5)/(4*n+5))

  pi_lb_diff: LEMMA pi_lbn(n+1)-pi_lbn(n) =
                    16*(1/5)^(4*n+5)*(1/(4*n+5) - 1/(25*(4*n+7))) +
                    4*(1/239)^(4*n+3)*(1/(4*n+3) - 1/(57121*(4*n+5)))

  pi_ub_diff: LEMMA pi_ubn(n)-pi_ubn(n+1) =
                   16*(((1/5)^(3+4*n))*(1/(3+4*n)))
     -16*(((1/5)^(5+4*n))*(1/(5+4*n)))
     +4*(((1/239)^(5+4*n))*(1/(5+4*n)))
     -4*(((1/239)^(7+4*n))*(1/(7+4*n)))

  pi_lb_diff_bounds: LEMMA n>=5 IMPLIES
    LET xdiff = pi_lbn(n+1)-pi_lbn(n) IN
    14*(1/5)^(5*n+5) < xdiff AND xdiff < (116/25)*(1/5)^(4*n+3)

  pi_lb_quot_bounds: LEMMA
    LET xquot = pi_lbn(n)/pi_lbn(n+1) IN
    1-14.5*(1/5)^(4*n+3) <= xquot AND xquot <= 1

  pi_ub_diff_bounds: LEMMA n>=5 IMPLIES
    LET xdiff = pi_ubn(n)-pi_ubn(n+1) IN
    32*(1/5)^(5*n+3) < xdiff AND xdiff < (7/5)*(1/5)^(4*n+3)

  pi_ub_quot_bounds: LEMMA
    LET xquot = pi_ubn(n+1)/pi_ubn(n) IN
    1-(9/5)*(1/5)^(4*n+3) <= xquot AND xquot <= 1

  END atan_approx

quality86%

¤ 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.0.0Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

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.