|
%------------------------------------------------------------------------------
% 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
¤ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet)
¤
|
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.
|
