series: THEORY BEGIN IMPORTING prelude_auxVAR realVAR [nat-> real]VAR natRECURSIVE realIF n = 0 THEN xs(0) ELSE sum(xs,n-1) + xs(n) ENDIF )MEASURE (LAMBDA xs,n: n)LEMMA (FORALL (m:nat): xs(m) = ys(m) * x) =>LAMBDA (n:nat): IF n=0 THEN 1 ELSE x^n ENDIF )LEMMA -1 < x AND x < 1 =>LEMMA odd?(n) AND -1 < x AND x < 1 =>LEMMA even?(n) AND n > 0 AND -1 < x AND x < 1 =>EXISTS (n:nat): y = sum(geometric_series(x),n)}LEMMA member(1,geometric_series_approx_set(x))LEMMA nonempty ?(geometric_series_approx_set(x))LEMMA 0 <= x AND x < 1 =>LEMMA 0 <= x AND x < 1 =>LEMMA 0 <= x AND x < 1 =>% geometric_series_pos_limit: LEMMA 0 < x AND x < 1 => % lub(geometric_series_approx_set(x)) = 1/(1-x) END seriesquality 96%
¤ Dauer der Verarbeitung: 0.10 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
