Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/PVS/trig/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 28.9.2014 mit Größe 3 kB

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

quality97%

¤ Dauer der Verarbeitung: 0.14 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.