| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/sigma_set/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 3 kB |
|
Quelle sigma_set.pvs Sprache: PVS |
|||||||||
|
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.12 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28