|
integral_cont_scaf[T: TYPE FROM real]: THEORY
%----------------------------------------------------------------------------
% scaffolding: not intended for users
%----------------------------------------------------------------------------
BEGIN
ASSUMING
IMPORTING deriv_domain_def[T]
connected_domain : ASSUMPTION connected?[T]
not_one_element : ASSUMPTION not_one_element?[T]
ENDASSUMING
IMPORTING integral_prep[T], integral_step[T], interval_minmax[T],
unif_cont_fun, continuity_interval
f: VAR [T -> real]
x,y,a,b: VAR T
adh_lem: LEMMA a <= x AND x <= b
IMPLIES adh[closed_interval(a, b)](fullset[real])(x)
fun_cont_on(a:T,b:{x:T|a<x}): TYPE = {f |
(FORALL (x: closed_interval(a,b)):
continuous?(restrict[T,closed_interval(a,b),real](f),x))}
cont_restrict: LEMMA FORALL (x: closed_interval(a, b) ):
continuous?(f, x)
IMPLIES
continuous?(restrict[T, closed_interval(a, b), real](f), x)
cont_interv: LEMMA (FORALL (P: partition(a,b), xx: [below(length(P)) -> T]):
continuous?(restrict[T, closed_interval(a, b), real](f))
AND xx = seq(P) IMPLIES
(FORALL (ii : below(length(P)-1)):
continuous?[closed_interval(xx(ii), xx(1 + ii))]
(restrict[T, closed_interval(xx(ii), xx(1 + ii)), real](f))))
% The following is now in interval_minmax
%
% min_x(a:T,b:{x:T|a<x}, f: fun_cont_on(a,b)):
% {mx: T | a <= mx AND mx <= b AND
% (FORALL (x: T): a <= x AND x <= b IMPLIES
% f(mx) <= f(x))}
%
%
% max_x(a:T,b:{x:T|a<x}, f: fun_cont_on(a,b)):
% {mx: T | a <= mx AND mx <= b AND
% (FORALL (x: T): a <= x AND x <= b IMPLIES
% f(mx) >= f(x))}
fmin_nonempty: LEMMA FORALL (P: partition(a,b), f: fun_cont_on(a,b)):
nonempty?({fv: real |
FORALL (ii: below(length(P) - 1)):
(seq(P)(ii) < x AND x < seq(P)(1 + ii) IMPLIES
fv = f(min_x(seq(P)(ii), seq(P)(1 + ii), f)))
AND
((seq(P)(ii) = x OR x = seq(P)(1 + ii)) IMPLIES
fv = f(x))})
fmax_nonempty: LEMMA FORALL (P: partition(a,b), f: fun_cont_on(a,b)):
nonempty?({fv: real |
FORALL (ii: below(length(P) - 1)):
(seq(P)(ii) < x AND x < seq(P)(1 + ii) IMPLIES
fv = f(max_x(seq(P)(ii), seq(P)(1 + ii), f)))
AND
((seq(P)(ii) = x OR x = seq(P)(1 + ii)) IMPLIES
fv = f(x))})
fmin(a:T,b:{x:T|a<x},P: partition(a,b), f: fun_cont_on(a,b)):
{ff: [T -> real] | LET xx = seq(P) IN
FORALL (ii : below(length(P)-1)):
FORALL (x: T): (xx(ii) < x AND x < xx(ii+1) IMPLIES
ff(x) = f(min_x(xx(ii),xx(ii+1),f))) AND
((xx(ii) = x OR x = xx(ii+1)) IMPLIES
ff(x) = f(x))}
fmax(a:T,b:{x:T|a<x},P: partition(a,b), f: fun_cont_on(a,b)):
{ff: [T -> real] | LET xx = seq(P) IN
FORALL (ii : below(length(P)-1)):
FORALL (x: T): (xx(ii) < x AND x < xx(ii+1) IMPLIES
ff(x) = f(max_x(xx(ii),xx(ii+1),f))) AND
((xx(ii) = x OR x = xx(ii+1)) IMPLIES
ff(x) = f(x))}
fmax_step: LEMMA FORALL (PP: partition(a,b), f: fun_cont_on(a,b)):
a < b IMPLIES step_function?(a, b, fmax(a, b, PP, f))
fmin_step: LEMMA FORALL (PP: partition(a,b), f: fun_cont_on(a,b)):
a < b IMPLIES step_function?(a, b, fmin(a, b, PP, f))
fmax_ge : LEMMA FORALL (PP: partition(a,b), f: fun_cont_on(a,b),
x: closed_interval(a,b)):
a < b IMPLIES
fmax(a, b, PP, f)(x) - fmin(a, b, PP, f)(x) >= 0
END integral_cont_scaf
¤ Dauer der Verarbeitung: 0.0 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.
|
