rs_integral_cont[T:TYPE+ from real]: THEORY %------------------------------------------------------------------------------ % Continuous functions are Riemann-Stieltjes integrable %------------------------------------------------------------------------------ BEGIN
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.2 Sekunden
(vorverarbeitet)
¤
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.
