|
sigma_posnat: THEORY
%------------------------------------------------------------------------------
% The summations theory introduces and defines properties of the sigma
% function that sums an arbitrary function F: [T -> real] over a range
% from low to high
%
% high
% ----
% sigma(low, high, F) = \ F(j)
% /
% ----
% j = low
%
%------------------------------------------------------------------------------
BEGIN
IMPORTING sigma[posnat]
int_is_T_high: JUDGEMENT int SUBTYPE_OF T_high
posnat_is_T_low : JUDGEMENT posnat SUBTYPE_OF T_low
low, n, m: VAR posnat
high: VAR int
F: VAR function[posnat -> real]
% --------- Following Theorems Not Provable In Generic Framework -------
sigma_shift: THEOREM sigma(low+m,high+m,F) =
sigma(low,high, (LAMBDA (n: posnat): F(n+m)))
sigma_shift_neg: THEOREM low - m > 0 IMPLIES
sigma(low-m,high-m,F) =
sigma(low,high, (LAMBDA n: IF n-m <= 0 THEN 0
ELSE F(n-m)
ENDIF))
sigma_split_ge : THEOREM low-1 <= m AND m <= high IMPLIES
sigma(low, high, F) =
sigma(low, m, F) + sigma(m+1, high, F)
END sigma_posnat
¤ Dauer der Verarbeitung: 0.15 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.
|
