|
%----------------------------------------------------------------------------
% Continuous functions [ T -> real]
%
% Defines:
% continuous?(f, x0) ---- continuity at a point
% continuous?(f, E) ---- continuity on a set
%
% I some cases PVS has trouble disambiguating these, so the following are
% defined which helps. See cont_if_fun for an example.
%
% continuous_at?(f, x0) ---- continuity at a point
% continuous_on?(f, E) ---- continuity on a set
%
%
%
%----------------------------------------------------------------------------
continuous_functions [ T : TYPE FROM real ] : THEORY
BEGIN
IMPORTING % lim_of_functions
reals@real_fun_ops
f, f1, f2 : VAR [T -> real]
g : VAR [T -> nzreal]
u : VAR real
x, x0 : VAR T
epsilon, delta : VAR posreal
n : VAR nat
%--------------------
% Continuity at x0
%--------------------
continuous?(f, x0) : bool =
FORALL epsilon : EXISTS delta : FORALL x :
abs(x - x0) < delta IMPLIES abs(f(x) - f(x0)) < epsilon
continuous_at?(f, x0) : MACRO bool = continuous?(f, x0)
%--- equivalent definitions ---%
% continuity_def : LEMMA
% continuous?(f, x0) IFF convergence(f, x0, f(x0))
% continuity_def2 : LEMMA
% continuous?(f, x0) IFF convergent?(f, x0)
%---------------------------------------------
% Continuity of f in a subset of its domain
%---------------------------------------------
E: VAR setof[T]
continuous_on?(f, E): bool = FORALL (x0: (E)): FORALL epsilon:
EXISTS delta: FORALL (x:(E)): abs(x - x0) < delta IMPLIES abs(f(x) - f(x0)) < epsilon
% continuous_on_def: LEMMA
% continuous_on?(f, E) IFF FORALL (y: (E)): convergence(f, E, y, f(y))
%------------------------------------------
% Operations preserving continuity at x0
%------------------------------------------
sum_continuous : AXIOM continuous?(f1, x0) AND continuous?(f2, x0)
IMPLIES continuous?(f1 + f2, x0)
diff_continuous : AXIOM continuous?(f1, x0) AND continuous?(f2, x0)
IMPLIES continuous?(f1 - f2, x0)
prod_continuous : AXIOM continuous?(f1, x0) AND continuous?(f2, x0)
IMPLIES continuous?(f1 * f2, x0)
const_continuous: AXIOM continuous?(const_fun(u), x0)
scal_continuous : AXIOM continuous?(f, x0) IMPLIES continuous?(u * f, x0)
neg_continuous : AXIOM continuous?(f, x0) IMPLIES continuous?(- f, x0)
div_continuous : AXIOM continuous?(f, x0) AND continuous?(g, x0)
IMPLIES continuous?(f/g, x0)
inv_continuous : AXIOM continuous?(g, x0) IMPLIES continuous?(1/g, x0)
identity_continuous: AXIOM continuous?(I[T], x0)
expt_continuous : LEMMA continuous?(f, x0) IMPLIES continuous?(f^n, x0)
%---------------------------------------------
% Continuity of f in a subset of its domain
%---------------------------------------------
F: VAR setof[real]
%--- Operation preserving continuity in E ---%
sum_set_continuous : AXIOM continuous_on?(f1, E) AND continuous_on?(f2, E)
IMPLIES continuous_on?(f1 + f2, E)
diff_set_continuous : AXIOM continuous_on?(f1, E) AND continuous_on?(f2, E)
IMPLIES continuous_on?(f1 - f2, E)
prod_set_continuous : AXIOM continuous_on?(f1, E) AND continuous_on?(f2, E)
IMPLIES continuous_on?(f1 * f2, E)
const_set_continuous: LEMMA continuous_on?(const_fun(u), E)
scal_set_continuous : AXIOM continuous_on?(f, E) IMPLIES continuous_on?(u * f, E)
neg_set_continuous : AXIOM continuous_on?(f, E) IMPLIES continuous_on?(- f, E)
div_set_continuous : AXIOM continuous_on?(f, E) AND continuous_on?(g, E)
IMPLIES continuous_on?(f/g, E)
inv_set_continuous : AXIOM continuous_on?(g, E) IMPLIES continuous_on?(1/g, E)
identity_set_continuous: LEMMA continuous_on?(I[T], E)
%---------------------------------
% Continuity of f in its domain
%---------------------------------
continuous?(f): bool = FORALL x0: continuous?(f, x0)
continuous_def2: LEMMA continuous?(f) IFF continuous_on?(f, T_pred)
continuity_subset2: LEMMA continuous?(f) IMPLIES continuous_on?(f, E)
%--- Properties ---%
continuous_fun: TYPE+ = { f | continuous?(f) }
nz_continuous_fun: TYPE = { g | continuous?(g) }
h, h1, h2: VAR continuous_fun
h3: VAR nz_continuous_fun
sum_fun_continuous : JUDGEMENT +(h1, h2) HAS_TYPE continuous_fun
diff_fun_continuous: JUDGEMENT -(h1, h2) HAS_TYPE continuous_fun
prod_fun_continuous: JUDGEMENT *(h1, h2) HAS_TYPE continuous_fun
const_fun_continuous: JUDGEMENT const_fun(u) HAS_TYPE continuous_fun
scal_fun_continuous: JUDGEMENT *(u, h) HAS_TYPE continuous_fun
neg_fun_continuous : JUDGEMENT -(h) HAS_TYPE continuous_fun
div_fun_continuous : JUDGEMENT /(h, h3) HAS_TYPE continuous_fun
id_fun_continuous : JUDGEMENT I[T] HAS_TYPE continuous_fun
inv_fun_continuous : LEMMA continuous?(1/h3)
m,b: VAR real
linear_fun_cont : LEMMA continuous?(LAMBDA x: m*x + b) %% BUTLER
one_over_x_cont : LEMMA (FORALL x: x /= 0) IMPLIES
continuous?((LAMBDA x: 1 / x))
x_to_n_continuous : LEMMA continuous?(LAMBDA x: x^n) %% BUTLER
expt_fun_continuous: LEMMA continuous?(f) IMPLIES continuous?(f^n)
% ------------ Alternate forms and names for convenience ---------------
sum_cont_fun : LEMMA continuous?(f1) AND continuous?(f2)
IMPLIES continuous?(f1 + f2)
diff_cont_fun : LEMMA continuous?(f1) AND continuous?(f2)
IMPLIES continuous?(f1 - f2)
prod_cont_fun : LEMMA continuous?(f1) AND continuous?(f2)
IMPLIES continuous?(f1 * f2)
const_cont_fun: LEMMA continuous?(const_fun(u))
scal_cont_fun : LEMMA continuous?(f) IMPLIES continuous?(u * f)
neg_cont_fun : LEMMA continuous?(f) IMPLIES continuous?(- f)
div_cont_fun : LEMMA continuous?(f) AND continuous?(g)
IMPLIES continuous?(f/g)
inv_cont_fun : LEMMA continuous?(g) IMPLIES continuous?(1/g)
identity_cont_fun: LEMMA continuous?(I[T])
% id_cont_fun : LEMMA continuous?(LAMBDA (t: posreal): t)
expt_cont_fun : LEMMA continuous?(f) IMPLIES continuous?(f^n)
END continuous_functions
¤ Dauer der Verarbeitung: 0.20 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.
|
