|
rs_integral_cont[T:TYPE+ from real]: THEORY
%------------------------------------------------------------------------------
% Continuous functions are Riemann-Stieltjes integrable
%------------------------------------------------------------------------------
BEGIN
ASSUMING
IMPORTING deriv_domain_def[T]
connected_domain : ASSUMPTION connected?[T]
not_one_element : ASSUMPTION not_one_element?[T]
ENDASSUMING
IMPORTING real_metric_space,
uniform_continuity,
rs_integral_prep[T],
bounded_variation[T]
a,b,x,y,z: VAR T
c,S: VAR real
D,m,M,v1,v2,cc,RS1,RS2,K: VAR real
delta : VAR posreal
f,g,h,G: VAR [T -> real]
RS_integrable_cont_inc: LEMMA a < b IMPLIES
LET CI = closed_intv[T](a,b) IN
(continuous?[T,real_dist,real,real_dist](f,closed_intv[T](a,b)) AND
increasing?[(CI)](g)
IMPLIES integrable?(a,b,g,f))
RS_integrable_cont_BV: LEMMA a < b IMPLIES
LET CI = closed_intv[T](a,b) IN
(continuous?[T,real_dist,real,real_dist](f,closed_intv[T](a,b)) AND
bounded_variation?(a,b)(g)
IMPLIES integrable?(a,b,g,f))
END rs_integral_cont
¤ Dauer der Verarbeitung: 0.15 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.
|
