|
countable_convergence[T:TYPE]: THEORY
%------------------------------------------------------------------------------
% Convergence properties for countable sums.
%
% MODIFICATIONS:
%
% Author: David Lester, Manchester University 20/4/05
%
%------------------------------------------------------------------------------
BEGIN
IMPORTING sets_aux@countable_props[T],
denumerable_enumeration[T],
finite_enumeration[T],
sigma_bijection_nat, sigma_bijection,
analysis@convergence_ops,
reals@sigma,
absconv_series_aux,
series@series
a: VAR real
X,Y: VAR countable_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])
convergent?(X)(g): bool
= is_finite(X) OR absconvergent?(g o denumerable_enumeration(X))
convergent_zero: LEMMA convergent?(X)(LAMBDA t: 0)
convergent_plus: LEMMA convergent?(X)(f) AND convergent?(X)(g) =>
convergent?(X)(f+g)
convergent_scal: LEMMA convergent?(X)(f) => convergent?(X)(a*f)
convergent_opp: LEMMA convergent?(X)(f) => convergent?(X)(-f)
convergent_diff: LEMMA convergent?(X)(f) AND convergent?(X)(g) =>
convergent?(X)(f-g)
convergent_le: LEMMA (FORALL t: abs(g(t)) <= abs(f(t))) AND
convergent?(X)(f) => convergent?(X)(g)
convergent_zeros: LEMMA (FORALL (t:(X)): g(t) = 0) => convergent?(X)(g)
convergent_empty: LEMMA convergent?(emptyset[T])(g)
convergent_singleton: LEMMA convergent?(singleton(t))(g)
convergent_subset: LEMMA subset?(X,Y) AND convergent?(Y)(g) =>
convergent?(X)(g)
convergent_intersection: LEMMA
convergent?(X)(g) OR convergent?(Y)(g) =>
convergent?(intersection(X,Y))(g)
convergent_difference: LEMMA
convergent?(X)(g) => convergent?(difference(X,Y))(g)
convergent_disjoint_union: LEMMA
disjoint?(X,Y) AND convergent?(X)(g) AND convergent?(Y)(g) =>
convergent?(union(X,Y))(g)
convergent_union: LEMMA
convergent?(X)(g) AND convergent?(Y)(g) =>
convergent?(union(X,Y))(g)
convergent_add: LEMMA convergent?(X)(g) =>
convergent?(add(t,X))(g)
convergent_remove: LEMMA convergent?(X)(g) =>
convergent?(remove(t,X))(g)
convergent_abs: LEMMA convergent?(X)(g) IFF convergent?(X)(abs(g))
END countable_convergence
¤ Dauer der Verarbeitung: 0.16 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.
|
