Quelle  series.pvs

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