Quelle prelude_A4.pvs Sprache: PVS

%------------------------------------------------------------------------------
% Scaffolding for Appendix Lemma 4
%
%     Author: David Lester, Manchester University
%
%     Version 1.0            18/2/09   Initial Release Version
%------------------------------------------------------------------------------

prelude_A4: THEORY

  BEGIN
  IMPORTING prelude_aux,
            reals@sqrt

  i:           VAR int
  l,n:         VAR nat
  pn:          VAR posnat
  e1,e2,x,y,z: VAR real
  nx:          VAR negreal
  n0x,n0y:     VAR nzreal

  expt_neg_even:    LEMMA even?(n) => nx^n = (-nx)^n
  expt_neg_odd:     LEMMA odd?(n)  => nx^n = -((-nx)^n)
  expt_0pn:         LEMMA 0^pn = 0
  expt_inverse_inv: LEMMA (1/n0x)^i = 1/(n0x^i)
  expt_product_n0i: LEMMA (x*y)^pn = x^pn*y^pn
  expt_division:    LEMMA (x/n0y)^pn = x^pn/n0y^pn

  A4_0:   LEMMA -1 < y => 0 <= n/(n+1+y) AND n/(n+1+y) < 1
  A4_1:   LEMMA -1 < y => 0 < pn/(pn+1+y) AND pn/(pn+1+y) < 1
  A4_2:   LEMMA -1 < y AND z = n*y/(n+1+y) => -1 < z
  A4_3_n: LEMMA -1 < y AND y < 0 AND z = pn*y/(pn+1+y) => y < z
  A4_3_0: LEMMA y = 0  AND z = pn*y/(pn+1+y) => z = 0
  A4_3_p: LEMMA 0 < y  AND z = pn*y/(pn+1+y) => z < y
  A4_4:   LEMMA -1 < y AND z = pn*y/(pn+1+y) =>
                   (pn*x*(1+z) < z <=> (pn+1)*x*(1+y) < y)
  A4_5pp: LEMMA 0 < x => (FORALL n: (FORALL y: 0 < y =>
                            ((1+y)*n*x < y => (1+x)^n < 1+y)))

  A4_5nn: LEMMA -1 < x AND x < 0 =>
                (FORALL pn:
                    (FORALL y: -1 < y AND y < 0 =>
                            ((1+y)*pn*x < y => (1+x)^pn < 1+y)))

  A4_5nn_general: LEMMA -1 < x AND x < 0 AND y < 0 AND (1+y)*n*x < y =>
                        (1+x)^n < 1+y

  A4_5:   LEMMA -1 < x AND -1 < y AND (1+y)*pn*x < y => (1+x)^pn < 1+y

  A4_6pp: LEMMA 0 < x => (FORALL n: (FORALL y: 0 < y =>
                            (y*(1+x) < n*x => 1+y < (1+x)^n)))

  A4_6pp_general: LEMMA 0 < x AND y*(1+x) < n*x => 1+y < (1+x)^n

  A4_6nn: LEMMA -1 < x AND x < 0 => (FORALL n: (FORALL y: -1 < y AND y
                            < 0 => (y*(1+x) < n*x => 1+y < (1+x)^n)))

  A4_6nn_general: LEMMA -1 < x AND x < 0 AND y < 0 AND y*(1+x) < n*x => 1+y < (1+x)^n

  A4_sqrt_ineq1: LEMMA 1/2 < 2-sqrt(2)
  A4_sqrt_ineq2: LEMMA 1/sqrt(2) + 2^-3 < 1
  A4_sqrt_ineq3: LEMMA 0 < 1/sqrt(2) - 2^-3

  A4_logsize: LEMMA 2 <= pn AND 1 <= pn*2^-l AND pn*2^-l < 2 => 1 <= l

  A4_lemma_ineq1: LEMMA 1 <= n AND 3 <= pn AND 2^-n/sqrt(2) <= x AND x < 2^-n
                        => x^pn + 2^-n < 2*x

  A4_lemma_ineq2: LEMMA 3 <= pn AND 2^-n <= x AND x < 1 AND
                        1 <= pn*2^-l AND pn*2^-l < 2 =>
                        x^pn + 2^-n < 2*x

  A4_lemma_large_UB_0: LEMMA 3 <= pn AND 1/sqrt(2) <= x AND x < 1 AND
                             1 <= pn*2^-l AND pn*2^-l < 2 =>
                             (x+2^ -(l+2))^pn < x^pn+1

  A4_lemma_large_UB: LEMMA 3 <= pn AND e2/sqrt(2) <= x AND x < 1 AND
                           1 <= pn*2^-l AND pn*2^-l < 2 AND
                           e1 = 2^ -(n+l+2) AND e2 = 2^-n =>
                           (x+e1)^pn < x^pn+e2

  A4_lemma_large_LB: LEMMA 3 <= pn AND e2/sqrt(2) <= x AND x < 1 AND
                           1 <= pn*2^-l AND pn*2^-l < 2 AND
                           e1 = 2^ -(n+l+2) AND e2 = 2^-n =>
                           x^pn-e2 < (x-e1)^pn

  A4_lemma_large_ge3: LEMMA 3 <= pn AND e2/sqrt(2) <= x AND x < 1 AND
                            1 <= pn*2^-l AND pn*2^-l < 2 AND
                            e1 = 2^ -(n+l+2) AND e2 = 2^-n =>
                            x^pn-e2 < (x-e1)^pn AND (x+e1)^pn < x^pn+e2

  A4_lemma_large_lt3: LEMMA (pn = 1 OR pn = 2) AND e2/sqrt(2) <= x AND x < 1 AND
                            1 <= pn*2^-l AND pn*2^-l < 2 AND
                            e1 = 2^ -(n+l+2) AND e2 = 2^-n =>
                            x^pn-e2 < (x-e1)^pn AND (x+e1)^pn < x^pn+e2

  A4_lemma_small_UB: LEMMA 2 <= pn AND 0 < x AND x < e2/sqrt(2) AND
                           1 <= l AND e1 = 2^ -(n+l+2) AND e2 = 2^-n =>
                           (x+e1)^pn < x^pn+e2

  A4_lemma_small_LB: LEMMA 2 <= pn AND 0 < x AND x < e2/sqrt(2) AND
                           1 <= l AND e1 = 2^ -(n+l+2) AND e2 = 2^-n =>
                           x^pn-e2 < (x-e1)^pn

  A4_lemma_small: LEMMA 0 < x AND x < e2/sqrt(2) AND
                        1 <= pn*2^-l AND pn*2^-l < 2 AND
                        e1 = 2^ -(n+l+2) AND e2 = 2^-n =>
                        x^pn-e2 < (x-e1)^pn AND (x+e1)^pn < x^pn+e2

  A4_lemma_px: LEMMA e1 <= x AND x < 1 AND 1 <= pn*2^-l AND pn*2^-l < 2 AND
                     e1 = 2^ -(n+l+2) AND e2 = 2^-n =>
                     x^pn-e2 < (x-e1)^pn AND (x+e1)^pn < x^pn+e2

  A4_lemma_p: LEMMA e1 <= x AND x < 1 AND 1 <= pn*2^-l AND pn*2^-l < 2 AND
                    e1 = 2^ -(n+l+2) AND e2 = 2^-n =>
                    x^pn-e2 < (x-e1)^pn AND x^pn-e2 < (x+e1)^pn AND
                    (x-e1)^pn < x^pn+e2 AND (x+e1)^pn < x^pn+e2

  A4_lemma_0_px: LEMMA 0 < x AND x < e1 AND 1 <= pn*2^-l AND pn*2^-l < 2 AND
                    e1 = 2^ -(n+l+2) AND e2 = 2^-n =>
                    x^pn-e2 < (x-e1)^pn AND (x+e1)^pn < x^pn+e2

  A4_lemma_0_p: LEMMA 0 < x AND x < e1 AND 1 <= pn*2^-l AND pn*2^-l < 2 AND
                    e1 = 2^ -(n+l+2) AND e2 = 2^-n =>
                    x^pn-e2 < (x-e1)^pn AND x^pn-e2 < (x+e1)^pn AND
                    (x-e1)^pn < x^pn+e2 AND (x+e1)^pn < x^pn+e2

  A4_lemma_0: LEMMA -e1 < x AND x < e1 AND 1 <= pn*2^-l AND pn*2^-l < 2 AND
                    e1 = 2^ -(n+l+2) AND e2 = 2^-n =>
                    x^pn-e2 < (x-e1)^pn AND x^pn-e2 < (x+e1)^pn AND
                    (x-e1)^pn < x^pn+e2 AND (x+e1)^pn < x^pn+e2

  A4_lemma_n_even:
              LEMMA even?(pn) AND e1 = 2^ -(n+l+2) AND e2 = 2^-n AND
                    -1 < x AND x <= -e1 AND 1 <= pn*2^-l AND pn*2^-l < 2 =>
                    x^pn-e2 < (x+e1)^pn AND (x-e1)^pn < x^pn+e2

  A4_lemma_n_odd:
              LEMMA odd?(pn) AND e1 = 2^ -(n+l+2) AND e2 = 2^-n AND
                    -1 < x AND x <= -e1 AND 1 <= pn*2^-l AND pn*2^-l < 2 =>
                    x^pn-e2 < (x-e1)^pn AND (x+e1)^pn < x^pn+e2

  A4_lemma_n: LEMMA -1 < x AND x <= -e1 AND 1 <= pn*2^-l AND pn*2^-l < 2 AND
                    e1 = 2^ -(n+l+2) AND e2 = 2^-n =>
                    x^pn-e2 < (x-e1)^pn AND x^pn-e2 < (x+e1)^pn AND
                    (x-e1)^pn < x^pn+e2 AND (x+e1)^pn < x^pn+e2

  END prelude_A4

quality98%

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