|
integral[T: TYPE+ FROM real]: THEORY
%------------------------------------------------------------------------------
%
% Theory and proofs taken from Introduction to Analysis (Maxwell Rosenlight)
%
% This theory provides the basic properties of the Riemann Integral
%
% Author: Rick Butler NASA Langley
%
%------------------------------------------------------------------------------
BEGIN
ASSUMING
IMPORTING deriv_domain_def[T]
connected_domain : ASSUMPTION connected?[T]
not_one_element : ASSUMPTION not_one_element?[T]
ENDASSUMING
IMPORTING integral_def[T], integral_cont[T],
integral_split[T],
reals@real_fun_ops,
continuous_functions_more[T]
a,b,c,x,y: VAR T
D,m,M,yv: VAR real
f,g: VAR [T -> real]
% Closed_interval(a:T,b:{x:T | x /= a}): TYPE = {x: T | (a < b IMPLIES
% (a <= x AND x <= b)) AND
% (b < a IMPLIES
% (b <= x AND x <= a))}
% Closed_interval(a,b:T): TYPE = {x: T | (a <= b IMPLIES
% (a <= x AND x <= b)) AND
% (b < a IMPLIES
% (b <= x AND x <= a))}
Integrable?_a_to_a: LEMMA Integrable?(a,a,f)
Integrable?_inside : LEMMA a <= x AND x <= y AND y <= b AND
Integrable?(a,b,f) IMPLIES Integrable?(x,y,f)
Integral_a_to_a : LEMMA Integral(a,a,f) = 0
Integral_const_fun: LEMMA Integrable?(a, b, const_fun[T](D)) AND
Integral(a,b,const_fun(D)) = D*(b-a)
Integral_const_restrict: LEMMA
(FORALL (x: Closed_interval(a,b)): f(x) = D) IMPLIES
Integrable?(a,b,f) AND
Integral(a,b,f) = D*(b-a)
Integral_rev: LEMMA Integrable?(a, b, f) IMPLIES
Integrable?(b, a, f) AND
Integral(b, a, f) = - Integral(a, b, f)
continuous_Integrable?: LEMMA
(FORALL (x: Closed_interval(a,b)):
continuous?(f,x))
IMPLIES Integrable?(a,b,f)
cont_Integrable?: LEMMA continuous?(f) IMPLIES Integrable?(a,b,f)
cont_fun_Integrable?: COROLLARY continuous?(f)
IMPLIES Integrable?(a,b,f)
% -------------- Linearity Properties of Integral ---------------------
Integral_scal: LEMMA Integrable?(a,b,f) IMPLIES
Integrable?(a,b,D*f) AND
Integral(a,b,D*f) = D*Integral(a,b,f)
Integral_sum: LEMMA Integrable?(a,b,f) AND Integrable?(a,b,g) IMPLIES
Integrable?(a,b,(LAMBDA x: f(x) + g(x)))
AND
Integral(a,b,(LAMBDA x: f(x) + g(x))) =
Integral(a,b,f) + Integral(a,b,g)
Integral_diff: LEMMA Integrable?(a,b,f) AND Integrable?(a,b,g) IMPLIES
Integrable?(a,b,(LAMBDA x: f(x) - g(x)))
AND
Integral(a,b,(LAMBDA x: f(x) - g(x))) =
Integral(a,b,f) - Integral(a,b,g)
Integral_split: LEMMA Integrable?(a,b,f) AND Integrable?(b,c,f)
IMPLIES Integrable?(a,c,f) AND
Integral(a,b,f) + Integral(b,c,f) = Integral(a,c,f)
Integral_chg_one_pt: LEMMA FORALL (y: Closed_interval(a,b)):
Integrable?(a,b,f)
IMPLIES Integrable?(a,b,f WITH [(y) := yv]) AND
Integral(a,b,f WITH [(y) := yv]) = Integral(a,b,f)
% ---------------- Boundedness of Integral -----------------------------
Integral_ge_0: LEMMA a < b AND Integrable?(a,b,f) AND
(FORALL (x: Closed_interval(a,b)): f(x) >= 0) IMPLIES
Integral(a,b,f) >= 0
Integral_ge_0_open: LEMMA a <= b AND Integrable?(a,b,f) AND
(FORALL (x: Open_interval(a,b)): f(x) >= 0) IMPLIES
Integral(a,b,f) >= 0
Integral_bound: LEMMA a < b AND Integrable?(a,b,f) AND
(FORALL (x: Closed_interval(a,b)):
m <= f(x) AND f(x) <= M )
IMPLIES m*(b-a) <= Integral(a,b,f) AND Integral(a,b,f) <= M*(b-a)
Integral_bounded: LEMMA Integrable?(a,b,f) AND
(FORALL (x: Closed_interval(a,b)): abs(f(x)) <= M) IMPLIES
abs(Integral(a,b,f)) <= M*abs(b-a)
Integral_le : LEMMA a < b AND Integrable?(a,b,f) AND Integrable?(a,b,g)
AND (FORALL (x: closed_interval(a,b)): f(x) <= g(x))
IMPLIES
Integral(a,b,f) <= Integral(a,b,g)
% bounded_on?(a,b,f): bool = (EXISTS (B: real):
% (FORALL (x: closed_interval(a,b)): abs(f(x)) <= B))
Integrable_bounded: LEMMA Integrable?(a,b,f)
IMPLIES
LET l = real_defs.min(a,b),
u = real_defs.max(a,b) IN
bounded_on?(l, u, f)
Integral_neg: LEMMA Integrable?(a,b,f) IMPLIES
Integrable?(a,b,-f) AND
Integral(a,b,-f) = -Integral(a,b,f)
Integral_restr_eq: LEMMA (FORALL (x: Open_interval(a,b)): f(x) = g(x))
AND Integrable?(a,b,f)
IMPLIES Integrable?(a,b,g) AND
Integral(a,b,g) = Integral(a,b,f)
END integral
¤ Dauer der Verarbeitung: 0.18 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.
|
