|
sigma_set[T:TYPE]: THEORY
%------------------------------------------------------------------------------
% The sigma_set theory introduces and defines properties of the sigma
% function that sums an arbitrary function F: [T -> real] over a
% set of values X. To make this sensible for infinite sets, we will
% require that the subset of X for which f(x)/=0 be countable and absolutely
% convergent in the infinite case.
%
% This notation is a vital simplification for Hilbert Space.
%
% ----
% sigma(X, f) = \ f(x)
% /
% ----
% member(x,X)
%
%
% MODIFICATIONS:
%
% Author: David Lester, Manchester University 2/12/07
%
%------------------------------------------------------------------------------
BEGIN
IMPORTING sigma_countable[T],
convergence_set[T]
a: VAR real
nz: VAR nzreal
X,Y: VAR set[T]
t: VAR T
f,g: VAR [T -> real]
F: VAR non_empty_finite_set[T]
n: VAR nat
phi: VAR (bijective?[nat,nat])
C: VAR countable_set[T]
sigma(X:set[T],f:(convergent?(X))):real = sigma(nonzero_elts(f,X),f)
sigma_countable: LEMMA FORALL (f:(countable_convergence.convergent?(C))):
sigma(C,f) = sigma_countable.sigma(C,f)
sigma_empty: LEMMA sigma(emptyset[T],g) = 0
sigma_finite: LEMMA sigma(F,g) = sigma_countable.sigma(F,g)
sigma_singleton: LEMMA sigma(singleton(t),g) = g(t)
sigma_disjoint_union: LEMMA FORALL (f:(convergent?(union(X,Y)))):
disjoint?(X,Y) => sigma(union(X,Y),f) = sigma(X,f) + sigma(Y,f)
sigma_union: LEMMA FORALL (f:(convergent?(union(X,Y)))):
sigma(union(X,Y),f) = sigma(X,f) + sigma(Y,f) - sigma(intersection(X,Y),f)
sigma_intersection: LEMMA FORALL (f:(convergent?(union(X,Y)))):
sigma(intersection(X,Y),f) = sigma(X,f) + sigma(Y,f) - sigma(union(X,Y),f)
sigma_difference: LEMMA FORALL (f:(convergent?(union(X,Y)))):
sigma(difference(X,Y),f)
= sigma(X,f) - sigma(Y,f) + sigma(difference(Y,X),f)
sigma_subset: LEMMA FORALL (f:(convergent?(Y))):
subset?(X,Y) => sigma(Y,f) = sigma(X,f) + sigma(difference(Y,X),f)
sigma_add: LEMMA FORALL (f:(convergent?(X))):
sigma(add(t,X),f) = IF member(t,X) THEN sigma(X,f)
ELSE f(t) + sigma(X,f) ENDIF
sigma_remove: LEMMA FORALL (f:(convergent?(X))):
sigma(remove(t,X),f) = IF member(t,X) THEN sigma(X,f) - f(t)
ELSE sigma(X,f) ENDIF
sigma_choose_rest: LEMMA FORALL (X:nonempty_set[T],
f:(convergence_set.convergent?(X))):
sigma(X,f) = f(choose(X)) + sigma(rest(X),f)
sigma_zero: LEMMA sigma(X,LAMBDA t: 0) = 0
sigma_scal: LEMMA FORALL (f:(convergent?(X))): sigma(X,a*f) = a*sigma(X,f)
sigma_opp: LEMMA FORALL (f:(convergent?(X))): sigma(X,-f) = -sigma(X,f)
sigma_plus: LEMMA FORALL (f,g:(convergent?(X))):
sigma(X,f+g) = sigma(X,f) + sigma(X,g)
sigma_diff: LEMMA FORALL (f,g:(convergent?(X))):
sigma(X,f-g) = sigma(X,f) - sigma(X,g)
sigma_ge_0: LEMMA FORALL (f:(convergent?(X))):
(FORALL (t:(X)): f(t) >= 0) => sigma(X,f) >= 0
sigma_gt_0: LEMMA FORALL (f:(convergent?(X))):
(FORALL (t:(X)): f(t) >= 0) AND
(EXISTS (t:(X)): f(t) > 0) => sigma(X,f) > 0
sigma_abs: LEMMA FORALL (f:(convergent?(X))):
abs(sigma(X,f)) <= sigma(X,abs(f))
sigma_eq: LEMMA FORALL (f,g:(convergent?(X))):
(FORALL (t:(X)): f(t) = g(t)) => sigma(X,f) = sigma(X,g)
sigma_le: LEMMA FORALL (f,g:(convergent?(X))):
(FORALL (t:(X)): f(t) <= g(t)) => sigma(X,f) <= sigma(X,g)
sigma_lt: LEMMA FORALL (f,g:(convergent?(X))):
(FORALL (t:(X)): f(t) <= g(t)) AND
(EXISTS (t:(X)): f(t) < g(t)) => sigma(X,f) < sigma(X,g)
END sigma_set
¤ 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.
|
