%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % General convergence of functions [T -> real] % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% convergence_functions [T : TYPE FROM real] : THEORY BEGIN IMPORTING real_fun_ops, epsilon_lemmas epsilon, delta : VAR posreal e, e1, e2 : VAR posreal E, E1, E2 : VAR setof[real] f, f1, f2 : VAR [T -> real] g : VAR [T -> nzreal] l, l1, l2, a, b, z : VAR real x, y : VAR T %--------------------------- % Reals adherent to a set %--------------------------- adh(E) : setof[real] = { z | FORALL e : EXISTS x : E(x) AND abs(x - z) < e } member_adherent : LEMMA E(x) IMPLIES adh(E)(x) adherence_subset1 : LEMMA subset?(E1, E2) AND adh(E1)(z) IMPLIES adh(E2)(z) adherence_subset2 : LEMMA subset?(E1, E2) IMPLIES subset?(adh(E1), adh(E2)) adherence_prop1 : LEMMA FORALL e, E, (a : (adh(E))) : EXISTS x : E(x) AND abs(x - a) < e adherence_prop2 : LEMMA FORALL e1, e2, E, (a : (adh(E))) : EXISTS x : E(x) AND abs(x - a) < e1 AND abs(x - a) < e2 %------------------------------------------------------ % Definition of convergence and immediate properties %------------------------------------------------------ convergence(f, E, a, l) : bool = adh(E)(a) AND FORALL epsilon : EXISTS delta : FORALL x : E(x) AND abs(x - a) < delta IMPLIES abs(f(x) - l) < epsilon convergence_unicity : PROPOSITION FORALL E, f, a, l1, l2 : convergence(f, E, a, l1) AND convergence(f, E, a, l2) IMPLIES l1 = l2 subset_convergence : PROPOSITION subset?(E1, E2) IMPLIES FORALL f, (a : (adh(E1))), l : convergence(f, E2, a, l) IMPLIES convergence(f, E1, a, l) subset_convergence2 : PROPOSITION FORALL E1, E2, f, (a : (adh(E1))), l : subset?(E1, E2) AND convergence(f, E2, a, l) IMPLIES convergence(f, E1, a, l) convergence_in_domain : PROPOSITION FORALL f, x, l : E(x) AND convergence(f, E, x, l) IMPLIES l = f(x) %---------------------------------- % Limits and function operations %---------------------------------- convergence_sum : PROPOSITION FORALL E, f1, f2, a, l1, l2 : convergence(f1, E, a, l1) AND convergence(f2, E, a, l2) IMPLIES convergence(f1 + f2, E, a, l1 + l2) convergence_opposite : PROPOSITION FORALL E, f1, a, l1 : convergence(f1, E, a, l1) IMPLIES convergence(- f1, E, a, - l1) convergence_diff : PROPOSITION FORALL E, f1, f2, a, l1, l2 : convergence(f1, E, a, l1) AND convergence(f2, E, a, l2) IMPLIES convergence(f1 - f2, E, a, l1 - l2) convergence_prod : PROPOSITION FORALL E, f1, f2, a, l1, l2 : convergence(f1, E, a, l1) AND convergence(f2, E, a, l2) IMPLIES convergence(f1 * f2, E, a, l1 * l2) convergence_const : PROPOSITION FORALL E, (a : (adh(E))), b : convergence(b, E, a, b) convergence_scal : PROPOSITION FORALL E, f1, a, l1, b : convergence(f1, E, a, l1) IMPLIES convergence(b * f1, E, a, b * l1) convergence_inv : PROPOSITION FORALL E, g, a, l1: convergence(g, E, a, l1) AND l1 /= 0 IMPLIES convergence(1/g, E, a, 1/l1) convergence_div : PROPOSITION FORALL E, f, g, a, l1, l2 : convergence(f, E, a, l1) AND convergence(g, E, a, l2) AND l2 /= 0 IMPLIES convergence(f/g, E, a, l1/l2) %--------------------- % Identity function %--------------------- convergence_identity : PROPOSITION FORALL E, (a : (adh(E))) : convergence(I[T], E, a, a) %----------------------------- % Limit preserve order %----------------------------- convergence_order : PROPOSITION FORALL E, f1, f2, a, l1, l2 : convergence(f1, E, a, l1) AND convergence(f2, E, a, l2) AND (FORALL x : E(x) IMPLIES f1(x) <= f2(x)) IMPLIES l1 <= l2 %------------------------------------------- % Bounds on function are bounds on limits %------------------------------------------- convergence_lower_bound : COROLLARY FORALL E, f, b, a, l : convergence(f, E, a, l) AND (FORALL x : E(x) IMPLIES b <= f(x)) IMPLIES b <= l convergence_upper_bound : COROLLARY FORALL E, f, b, a, l : convergence(f, E, a, l) AND (FORALL x : E(x) IMPLIES f(x) <= b) IMPLIES l <= b %-------------------------- % Function constant on E %-------------------------- convergence_locally_constant : PROPOSITION FORALL E, f, b, (a : (adh(E))) : (FORALL x : E(x) IMPLIES f(x) = b) IMPLIES convergence(f, E, a, b) %------------- % Squeezing %------------- convergence_squeezing : PROPOSITION FORALL f1, f2, f, a, l : convergence(f1, E, a, l) AND convergence(f2, E, a, l) AND (FORALL x : E(x) IMPLIES f1(x) <= f(x) AND f(x) <= f2(x)) IMPLIES convergence(f, E, a, l) END convergence_functions