|
trig_approx: THEORY
%-----------------------------------------------------------------------------
% trig_approx
% -----------
% - taylor series approximations to trig functions:
% sin_approx(a,n): sum first n terms of taylor expansion of sin
% cos_approx(a,n): sum first n terms of taylor expansion of cos
% - defines upper and lower bounds on trig functions:
%
% Version 2 Foundational (DRL) 4/4/05
%
% CHANGES
% - Redefined sin_lb,sin_ub,cos_lb,cos_ub,tan_lb,tan_ub to make it
% suitable for interval theory.
% - Removed lemmas SIN,COS,TAN. Use sin_bound_0_pi, cos_bound_npi2_pi2,
% tan_bound_0_pi2. Cesar Munoz (Nov 28 2003).
% - Added Hanne Gottliebsen's proofs for sin_bound_npi_0 and
% cos_bound_npi_pi.
% Cesar Munoz (Feb 6 2004).
% - Tan approximations moved to tan_approx due to circularity problems with
% trig_ineq. Cear Munoz (Feb 6 2004)
% - The theory has been completely revisited by David Lester (4/4/05)
%
%-----------------------------------------------------------------------------
BEGIN
IMPORTING exp_term, sincos, trig_ineq, reals@sigma_nat,
analysis@derivatives,trig_extra,analysis@derivative_props
m,n: VAR nat
pm: VAR posnat
a: VAR real
px: VAR posreal
n0x: VAR nzreal
nnx: VAR nnreal
IMPORTING analysis@deriv_domains
sin_term(a)(n): real = (-1)^n*a^(2*n+1)/factorial(2*n+1)
sin_term_next : LEMMA sin_term(a)(n+1) =
sin_term(a)(n) * -1 * a*a / ((2*n+3)*(2*n+2))
sin_term_neg : LEMMA sin_term(-a)(n) = -sin_term(a)(n)
sin_terms_alternate : LEMMA 0 /= a IMPLIES (sin_term(a)(n+1) < 0 IFF
sin_term(a)(n) > 0)
sin_term_nonzero : LEMMA sin_term(a)(n) /= 0 IFF a /= 0
sin_term_zero : LEMMA sin_term(a)(n) = 0 IFF a = 0
sin_term_gt0 : LEMMA sin_term(a)(n) > 0 IFF
((even?(n) AND a > 0) OR (odd?(n) AND a < 0))
sin_term_lt0 : LEMMA sin_term(a)(n) < 0 IFF
((even?(n) AND a < 0) OR (odd?(n) AND a > 0))
sin_tends_to_0 : LEMMA tends_to_0?(sin_term(a))
cos_term(a)(n): real = IF n=0 THEN 1 ELSE (-1)^n*a^(2*n)/factorial(2*n) ENDIF
cos_term_next : LEMMA cos_term(a)(n+1) =
cos_term(a)(n) * -1 * a*a / ((2*n+2)*(2*n+1))
cos_term_neg : LEMMA cos_term(-a)(n) = cos_term(a)(n)
cos_terms_alternate : LEMMA 0 /= a IMPLIES (cos_term(a)(n+1) < 0 IFF
cos_term(a)(n) > 0)
cos_term_nonzero : LEMMA cos_term(a)(n) /= 0 IFF (n = 0 OR a /= 0)
cos_term_zero : LEMMA cos_term(a)(n) = 0 IFF (n /= 0 AND a = 0)
cos_term_gt0 : LEMMA cos_term(a)(n) > 0 IFF
(even?(n) AND (a /= 0 OR n = 0))
cos_term_lt0 : LEMMA cos_term(a)(n) < 0 IFF (odd?(n) AND a /= 0)
cos_tends_to_0 : LEMMA tends_to_0?(cos_term(n0x))
sin_term_deriv: LEMMA derivable?[real](LAMBDA a: sin_term(a)(n)) AND
deriv[real](LAMBDA a: sin_term(a)(n)) = (LAMBDA a: cos_term(a)(n))
cos_term_deriv: LEMMA derivable?[real](LAMBDA a: cos_term(a)(n)) AND
deriv[real](LAMBDA a: cos_term(a)(n)) =
(LAMBDA a: IF n = 0 THEN 0 ELSE -sin_term(a)(n-1) ENDIF)
sin_approx(a,n):real = sigma(0,n,sin_term(a))
sin_approx_a0: LEMMA sin_approx(0,n) = 0
sin_approx_neg: LEMMA sin_approx(-a,n) = -sin_approx(a,n)
sin_approx_next: LEMMA sin_approx(a,n+2) - sin_approx(a,n) =
sin_term(a)(n+1) * (1 - a*a/((2*n+5)*(2*n+4)))
sin_approx_eq: LEMMA a*a = (2*n+5)*(2*n+4) IMPLIES
sin_approx(a,n+2) = sin_approx(a,n)
sin_approx_sin: LEMMA abs(sin(a)-sin_approx(a,n)) <= abs(sin_term(a)(n+1))
cos_approx(a,n):real = sigma(0,n,cos_term(a))
cos_approx_a0: LEMMA cos_approx(0,n) = 1
cos_approx_neg: LEMMA cos_approx(-a,n) = cos_approx(a,n)
cos_approx_cos: LEMMA abs(cos(a)-cos_approx(a,n)) <= abs(cos_term(a)(n+1))
cos_approx_next: LEMMA cos_approx(a,n+2) - cos_approx(a,n) =
cos_term(a)(n+1) * (1 - a*a/((2*n+4)*(2*n+3)))
cos_approx_eq: LEMMA a*a = (2*n+4)*(2*n+3) IMPLIES
cos_approx(a,n+2) = cos_approx(a,n)
sin_approx_deriv: LEMMA derivable?[real](LAMBDA a: sin_approx(a,n)) AND
deriv[real](LAMBDA a: sin_approx(a,n))
= (LAMBDA a: cos_approx(a,n))
cos_approx_deriv: LEMMA derivable?[real](LAMBDA a: cos_approx(a,n)) AND
deriv[real](LAMBDA a: cos_approx(a,n)) =
(LAMBDA a: IF n = 0 THEN 0 ELSE -sin_approx(a,n-1) ENDIF)
sin_ub(a,n):real = IF a < 0 THEN sin_approx(a,2*n+1)
ELSE sin_approx(a,2*n) ENDIF
sin_lb(a,n):real = IF a < 0 THEN sin_approx(a,2*n)
ELSE sin_approx(a,2*n+1) ENDIF
sin_lb_neg: LEMMA sin_lb(-a,n) = -sin_ub(a,n)
sin_ub_neg: LEMMA sin_ub(-a,n) = -sin_lb(a,n)
sin_lb_a0 : LEMMA sin_lb(0,n) = 0
sin_ub_a0 : LEMMA sin_ub(0,n) = 0
sin_lb_ub : LEMMA sin_lb(n0x,n) < sin_ub(n0x,n)
sin_lb_inc: LEMMA px*px < (4*n+7)*(4*n+6) => sin_lb(px,n) < sin_lb(px,n+pm)
sin_ub_dec: LEMMA px*px < (4*n+5)*(4*n+4) => sin_ub(px,n+pm) < sin_ub(px,n)
sin_lb_lt : LEMMA px*px < (4*n+7)*(4*n+6) => sin_lb(px,n) < sin(px)
sin_ub_lt : LEMMA px*px < (4*n+5)*(4*n+4) => sin(px) < sin_ub(px,n)
sin_lb_gt : LEMMA px*px > (4*n+7)*(4*n+6) => sin_lb(px,n) < -1
sin_ub_gt : LEMMA px*px > (4*n+5)*(4*n+4) => sin_ub(px,n) > 1
sin_lb : LEMMA sin_lb(n0x,n) < sin(n0x)
sin_ub : LEMMA sin(n0x) < sin_ub(n0x,n)
sin_bounds : LEMMA sin_lb(a,n) <= sin(a) AND sin(a) <= sin_ub(a,n)
sin_lb_gt0: LEMMA px*px < 6 => sin_lb(px,n) > 0
cos_ub(a,n):real = cos_approx(a,2*n)
cos_lb(a,n):real = cos_approx(a,2*n+1)
cos_lb_neg: LEMMA cos_lb(-a,n) = cos_lb(a,n)
cos_ub_neg: LEMMA cos_ub(-a,n) = cos_ub(a,n)
cos_lb_a0 : LEMMA cos_lb(0,n) = 1
cos_ub_a0 : LEMMA cos_ub(0,n) = 1
cos_lb_ub: LEMMA cos_lb(n0x,n) < cos_ub(n0x,n)
cos_lb_inc: LEMMA n0x*n0x<(4*n+6)*(4*n+5) => cos_lb(n0x,n) < cos_lb(n0x,n+pm)
cos_ub_dec: LEMMA n0x*n0x<(4*n+4)*(4*n+3) => cos_ub(n0x,n+pm) < cos_ub(n0x,n)
cos_lb_lt: LEMMA n0x*n0x < (4*n+6)*(4*n+5) => cos_lb(n0x,n) < cos(n0x)
cos_ub_lt: LEMMA n0x*n0x < (4*n+4)*(4*n+3) => cos(n0x) < cos_ub(n0x,n)
cos_lb_gt: LEMMA n0x*n0x > (4*n+6)*(4*n+5) => cos_lb(n0x,n) < -1
cos_ub_gt: LEMMA n0x*n0x > (4*n+4)*(4*n+3) & n>=1 => cos_ub(n0x,n) > 1
cos_lb: LEMMA cos_lb(n0x,n) < cos(n0x)
cos_ub: LEMMA cos(n0x) < cos_ub(n0x,pm)
cos_bounds: LEMMA cos_lb(a,n) <= cos(a) AND cos(a) <= cos_ub(a,n)
sin_lb_deriv: LEMMA derivable?[nnreal](LAMBDA nnx: sin_lb(nnx,n)) AND
deriv[nnreal](LAMBDA nnx: sin_lb(nnx,n)) = (LAMBDA nnx: cos_lb(nnx,n))
sin_ub_deriv: LEMMA derivable?[nnreal](LAMBDA nnx: sin_ub(nnx,n)) AND
deriv[nnreal](LAMBDA nnx: sin_ub(nnx,n)) = (LAMBDA nnx: cos_ub(nnx,n))
cos_lb_deriv: LEMMA derivable?[real](LAMBDA a: cos_lb(a,n)) AND
deriv[real](LAMBDA a: cos_lb(a,n))
= (LAMBDA a: IF a < 0 THEN -sin_lb(a,n) ELSE -sin_ub(a,n) ENDIF)
cos_ub_deriv: LEMMA derivable?[real](LAMBDA a: cos_ub(a,n)) AND
deriv[real](LAMBDA a: cos_ub(a,n))
= (LAMBDA a: IF n = 0 THEN 0 ELSIF
a < 0 THEN -sin_ub(a,n-1) ELSE -sin_lb(a,n-1) ENDIF)
cos_lb_nn_strict_decreasing:
LEMMA strict_decreasing?(LAMBDA (x:{x:nnreal| x <= pi}): cos_lb(x,n))
cos_lb_np_strict_increasing:
LEMMA strict_increasing?(LAMBDA (x:{x:npreal| x >= -pi}): cos_lb(x,n))
sin_px: LEMMA 1/500 > px => sin(px) > px*(1-1/1500000)
% Approximation to guarantee cos_lb > 0
Cos_pos_n : MACRO posnat = 5
cos_term_pi_lb: LEMMA n >= Cos_pos_n IMPLIES
cos_term(pi_lbn(n)/2)(2*n+2) < cos(pi_lbn(n)/2)
cos_lb_pi2_eps: LEMMA px <= pi/2 AND
abs(cos_term(pi/2-px)(2*n+2)) < sin(px) =>
cos_lb(pi/2-px,n) > 0
cos_lb_pi2_pos0 : LEMMA n=0 => NOT cos_lb(pi_lbn(n)/2,n) > 0
cos_lb_pi2_pos1 : LEMMA n=1 => NOT cos_lb(pi_lbn(n)/2,n) > 0
cos_lb_pi2_pos2 : LEMMA n=2 => NOT cos_lb(pi_lbn(n)/2,n) > 0
cos_lb_pi2_pos : LEMMA
n >= Cos_pos_n IMPLIES
cos_lb(pi_lbn(n)/2,n) > 0
% Approximation to guarantee sin_lb > 0
Sin_pos_n : MACRO posnat = 11
sin_term_pi_lb: LEMMA n >= Sin_pos_n IMPLIES
sin_term(pi_lbn(n+1))(2*n+2) < sin(pi_lbn(n+1))
sin_lb_pi_not_pos: LEMMA
FORALL (b9:below(11)):
NOT sin_lb(pi_lbn(b9+1),b9) > 0
sin_lb_pi_pos: LEMMA
n >= Sin_pos_n IMPLIES
sin_lb(pi_lbn(n+1),n) > 0
pi_lb_est(n:nat): {rr:nnreal | rr < pi} =
IF n < 12 THEN pi_lbn(n)-2/(n^3+1)
ELSE pi_lbn(n) ENDIF
pi_lb_est_le: LEMMA pi_lb_est(n) <= pi_lbn(n) AND pi_lb_est(n) <= pi
sin_lb_pi_est_pos: LEMMA sin_lb(pi_lb_est(n+1),n) > 0
sin_lb_pi_range_pos: LEMMA
px <= pi_lb_est(n+1) IMPLIES sin_lb(px,n) > 0
% Monotonicity of cos_ub
cos_ub_nn_strict_decreasing:
LEMMA n>=1 IMPLIES
strict_decreasing?(LAMBDA (x:{x:nnreal| x <= pi_lb_est(n)}): cos_ub(x,n))
cos_ub_np_strict_increasing:
LEMMA n>=1 IMPLIES
strict_increasing?(LAMBDA (x:{x:npreal| x >= -pi_lb_est(n)}): cos_ub(x,n))
% Monotonicity of sin_lb and sin_ub
sin_lb_increasing: LEMMA
strict_increasing?(LAMBDA (x:{x:real| -pi_lb_est(n)/2 <= x AND x <= pi_lb_est(n)/2}): sin_lb(x,n))
sin_ub_increasing: LEMMA
strict_increasing?(LAMBDA (x:{x:real| -pi_lb_est(n)/2 <= x AND x <= pi_lb_est(n)/2}): sin_ub(x,n))
sin_lb_nn_decreasing: LEMMA
strict_decreasing?(LAMBDA (x:{x:real | pi/2 <= x AND x <= pi}): sin_lb(x,n))
cos_term_pi_ub: LEMMA n >= Cos_pos_n IMPLIES
-cos_term(pi_ubn(n)/2)(2*n+1) < -cos(pi_ubn(n)/2)
cos_ub_pi2_neg : LEMMA
n >= Cos_pos_n IMPLIES
cos_ub(pi_ubn(n)/2,n) < 0
pi_ub_est(n:nat): {rr:nnreal | pi < rr AND rr < 3*pi/2} =
IF n < 5 THEN pi_ubn(n)+1/(n+1)^4
ELSE pi_ubn(n) ENDIF
sin_ub_nn_decreasing: LEMMA n>=1 IMPLIES
strict_decreasing?(LAMBDA (x:{x:real | pi_ub_est(n)/2 <= x AND x <= pi_lb_est(n)}): sin_ub(x,n))
END trig_approx
[ Seitenstruktur0.720Drucken
etwas mehr zur Ethik
]
|
