|
series: THEORY
BEGIN
IMPORTING prelude_aux
x,y: VAR real
xs,ys: VAR [nat-> real]
n,m: VAR nat
sum (xs:[nat->real],n:nat): RECURSIVE real
= (IF n = 0 THEN xs(0) ELSE sum(xs,n-1) + xs(n) ENDIF)
MEASURE (LAMBDA xs,n: n)
sum_lemma1: LEMMA (FORALL (m:nat): xs(m) = ys(m) * x) =>
sum(xs,n) = x * sum(ys,n)
geometric_series(x:real):[nat->real]
= (LAMBDA (n:nat): IF n=0 THEN 1 ELSE x^n ENDIF)
geometric_series_aux1: LEMMA -1 < x AND x < 1 =>
sum(geometric_series(x),n) = (1-x^(n+1))/(1-x)
geometric_series_aux_odd: LEMMA odd?(n) AND -1 < x AND x < 1 =>
sum(geometric_series(x),n) = (1+x)*sum(geometric_series(x*x),(n-1)/2)
geometric_series_aux_even: LEMMA even?(n) AND n > 0 AND -1 < x AND x < 1 =>
sum(geometric_series(x),n) = (1+x)*sum(geometric_series(x*x),n/2-1) + x^n
geometric_series_approx_set(x:real):setof[real]
= {y | EXISTS (n:nat): y = sum(geometric_series(x),n)}
geometric_series_approx_set_contains1:
LEMMA member(1,geometric_series_approx_set(x))
geometric_series_approx_set_nonempty:
LEMMA nonempty?(geometric_series_approx_set(x))
geometric_series_approx_set_pos_upper_bound: LEMMA 0 <= x AND x < 1 =>
upper_bound?(1/(1-x),geometric_series_approx_set(x))
geometric_series_approx_set_pos_least_upper_bound: LEMMA 0 <= x AND x < 1 =>
least_upper_bound?(1/(1-x),geometric_series_approx_set(x))
geometric_series_pos_limit: LEMMA 0 <= x AND x < 1 =>
lub(geometric_series_approx_set(x)) = 1/(1-x)
% geometric_series_pos_limit: LEMMA 0 < x AND x < 1 =>
% lub(geometric_series_approx_set(x)) = 1/(1-x)
END series
¤ Dauer der Verarbeitung: 0.1 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.
|
