Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: atan_approx.pvs Sprache: PVS

Original von: 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)
%
%-----------------------------------------------------------------------------
  BEGIN

  IMPORTING atan

  m,n:  VAR nat
  x:  VAR real
  px: 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: AXIOM 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: AXIOM 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
                            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
                            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_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: AXIOM 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: AXIOM 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)))

END atan_approx

¤ 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.