sigma_upto[N: nat]: THEORY %------------------------------------------------------------------------------ % The summations theory provides properties of the sigma % function that sums an arbitrary function F: [upto[N] -> real] over a range % from low to high % % high % ---- % sigma(low, high, F) = \ F(j) % / % ---- % j = low % % %------------------------------------------------------------------------------
BEGIN
IMPORTING sigma[upto[N]]
int_upto: TYPE = {i:int | i <= N}
int_upto_T_high: JUDGEMENT int_upto SUBTYPE_OF T_high
nat_is_T_low: JUDGEMENT nat SUBTYPE_OF T_low
low, high, n, m: VAR upto[N]
F: VARfunction[upto[N] -> real]
% --------- Following Theorems Not Provable In Generic Framework -------
sigma_split_ge : THEOREM low-1 <= m AND m <= high IMPLIES
sigma(low, high, F) =
sigma(low, m, F) + sigma(m+1, high, F)
% ---- Auto-rewrites
nn: VAR negint
sigma_0_neg: LEMMA sigma(0,nn,F) = 0
AUTO_REWRITE+ sigma_0_neg
END sigma_upto
¤ 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.0.26Bemerkung:
(vorverarbeitet)
¤
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.
