|
rs_integral_prep[T:TYPE+ from real]: THEORY
%------------------------------------------------------------------------------
% Basic Properties of the Riemann-Stieltjes Integral
%------------------------------------------------------------------------------
BEGIN
ASSUMING
IMPORTING deriv_domain_def[T]
connected_domain : ASSUMPTION connected?[T]
not_one_element : ASSUMPTION not_one_element?[T]
ENDASSUMING
IMPORTING rs_integral_def[T], reals@real_fun_ops[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]
%--------------------------------%
integral_const_fun: LEMMA a < b IMPLIES integrable?(a,b,g,const_fun(D))
AND integral(a,b,g, const_fun(D)) = D*(g(b)-g(a))
integral_const_restrict: LEMMA a < b AND
(FORALL (x: closed_interval(a,b)): f(x) = D) IMPLIES
integral?(a,b,g,f,D*(g(b)-g(a)))
IMPORTING continuous_functions, convergence_sequences
% ------------ Linearity Properties of Integral
integral_scal: LEMMA a < b AND integrable?(a,b,g,f) IMPLIES
integrable?(a,b,g,D*f) AND
integral(a,b,g,D*f) = D*integral(a,b,g,f)
integral_scal_g: LEMMA a < b AND integrable?(a,b,g,f) IMPLIES
integrable?(a,b,D*g,f) AND
integral(a,b,D*g,f) = D*integral(a,b,g,f)
integral_sum: LEMMA a < b AND integrable?(a,b,g,f) AND integrable?(a,b,g,h)
IMPLIES
integrable?(a,b,g,(LAMBDA x: f(x) + h(x))) AND
integral(a,b,g,(LAMBDA x: f(x) + h(x))) =
integral(a,b,g,f) + integral(a,b,g,h)
integral_sum_g: LEMMA a < b AND integrable?(a,b,g,f) AND integrable?(a,b,h,f)
IMPLIES
integrable?(a,b,(LAMBDA x: g(x) + h(x)),f) AND
integral(a,b,(LAMBDA x: g(x) + h(x)),f) =
integral(a,b,g,f) + integral(a,b,h,f)
integral?_sum: LEMMA a < b AND integral?(a,b,g,f,v1) AND
integral?(a,b,g,h,v2)
IMPLIES
integral?(a,b,g,(LAMBDA x: f(x) + h(x)),v1+v2)
integral?_sum_g: LEMMA a < b AND integral?(a,b,g,f,v1) AND
integral?(a,b,h,f,v2)
IMPLIES
integral?(a,b,(LAMBDA x:g(x)+h(x)),f,v1+v2)
integral_diff: LEMMA a < b AND integrable?(a,b,g,f) AND integrable?(a,b,g,h)
IMPLIES
integrable?(a,b,g,(LAMBDA x: f(x) - h(x))) AND
integral(a,b,g,(LAMBDA x: f(x) - h(x))) =
integral(a,b,g,f) - integral(a,b,g,h)
integral_diff_g: LEMMA a < b AND integrable?(a,b,g,f) AND integrable?(a,b,h,f)
IMPLIES
integrable?(a,b,(LAMBDA x:g(x)-h(x)),f) AND
integral(a,b,(LAMBDA x:g(x)-h(x)),f) =
integral(a,b,g,f) - integral(a,b,h,f)
integral_ge_0: LEMMA a < b AND increasing?(g) AND
integrable?(a,b,g,f) AND
(FORALL (x: closed_interval(a,b)): f(x) >= 0) IMPLIES
integral(a,b,g,f) >= 0
integral_restr_eq: LEMMA a < b AND
(FORALL x: a <= x AND x <= b IMPLIES
f(x) = h(x)) AND
integrable?(a,b,g,f)
IMPLIES integrable?(a,b,g,h) AND
integral(a,b,g,h) = integral(a,b,g,f)
integral_bound_above: LEMMA a < b AND increasing?(g) AND
integrable?(a,b,g,f) AND
(FORALL (x: closed_interval(a,b)):f(x)<=M)
IMPLIES integral(a,b,g,f) <= M*(g(b)-g(a))
integral_bound_below: LEMMA a < b AND increasing?(g) AND
integrable?(a,b,g,f) AND
(FORALL (x: closed_interval(a,b)): m<=f(x))
IMPLIES m*(g(b)-g(a)) <= integral(a,b,g,f)
integral_le : LEMMA a < b AND increasing?(g) AND
integrable?(a,b,g,f) AND integrable?(a,b,g,h)
AND (FORALL (x: closed_interval(a,b)): f(x) <= h(x))
IMPLIES
integral(a,b,g,f) <= integral(a,b,g,h)
eps: VAR posreal
Lemma_1: LEMMA a < b IMPLIES
(integrable?(a,b,g,f) IMPLIES
(FORALL eps: EXISTS delta:
(FORALL (P1,P2: partition(a,b),
xis1:xis?(a,b,P1),
xis2:xis?(a,b,P2)):
LET S1 = Rie_sum(a,b,g,P1,xis1,f),
S2 = Rie_sum(a,b,g,P2,xis2,f) IN
(width(a,b,P1) < delta AND
width(a,b,P2) < delta)
IMPLIES
abs(S1 - S2) < eps )))
integrable_lem: THEOREM a < b IMPLIES
(integrable?(a,b,g,f) IFF
(FORALL (epsi: posreal): (EXISTS (delta: posreal):
(FORALL (P1,P2: partition(a,b)):
width(a,b,P1) < delta AND
width(a,b,P2) < delta IMPLIES
(FORALL (RS1: (Riemann_sum?(a,b,P1,g,f)),
RS2: (Riemann_sum?(a,b,P2,g,f))):
abs(RS1 - RS2) < epsi )))))
%-------------------------------------------------------------------------%
integrable_lem2_alt: LEMMA a<b IMPLIES LET CI = closed_intv(a,b) IN
(monotonic?[(CI)](g) IMPLIES % Added 8/2010 for RS integral
(integrable?(a,b,g,f) IFF
(FORALL (epsi: posreal): (EXISTS (delta: posreal):
(FORALL (P: partition(a,b)):
width(a,b,P) < delta IMPLIES
(FORALL (RS1: (Riemann_sum?(a,b,P,g,f)),
RS2: (Riemann_sum?(a,b,P,g,f))):
abs(RS1 - RS2) < epsi ))))))
integrable_lem2: LEMMA a<b IMPLIES LET CI = closed_intv(a,b) IN
(monotonic?[(CI)](g) IMPLIES % Added 8/2010 for RS integral
(integrable?(a,b,g,f) IFF
(FORALL (epsi: posreal): (EXISTS (delta: posreal):
(FORALL (P: partition(a,b)):
width(a,b,P) < delta IMPLIES
(FORALL (RS1: (Riemann_sum?(a,b,P,g,f)),
RS2: (Riemann_sum?(a,b,P,g,f))):
abs(RS1 - RS2) < epsi ))))))
END rs_integral_prep
¤ 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.
|
