|
table_of_integrals[T: TYPE+ FROM real]: THEORY
%------------------------------------------------------------------------------
%
% New experimental: Theorems will be added as they are needed
%
% 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 fundamental_theorem[T], indefinite_integral[T]
a,b,x: VAR T
% ------ Integral c x^n = (c/(n+1))*x^(n+1) -----
antideriv_x_to_n: LEMMA FORALL (n: posnat, c: real):
LET f = (LAMBDA x: c*x^n),
F = (LAMBDA x: (c/(n+1))*x^(n+1)) IN
antiderivative?(F,f)
integral_x_to_n: LEMMA FORALL (n: posnat, c: real):
LET f = (LAMBDA x: c*x^n) IN
Integrable?(a,b,f) AND
LET F = (LAMBDA x: (c/(n+1))*x^(n+1)) IN
Integral(a,b,f) = F(b) - F(a)
integral_linear: LEMMA FORALL (mm: real, bb: real):
LET f = (LAMBDA x: mm*x+bb) IN
Integrable?(a,b,f) AND
LET F = (LAMBDA x: (mm/2)*x^2 +bb*x) IN
Integral(a,b,f) = F(b) - F(a)
integral_quadratic: LEMMA FORALL (A,B,C: real):
Integrable?(a,b, LAMBDA x: A*x^2+B*x+C) AND
LET F =(LAMBDA x: (A/3)*x^3 +(B/2)*x^2 +C*x) IN
Integral(a,b, LAMBDA x: A*x^2+B*x+C) = F(b)-F(a)
% -------
% IMPORTING sqrt_derivative
% integral_a_to_x: LEMMA LET f = (LAMBDA x: a^^x) IN
% Integrable?(a,b,f) AND
% Integral(a,b,f) = F(b) - F(a)
% integral_1_div_sqrt: LEMMA LET f = (LAMBDA (t: nnreal): 1/sqrt(t)) IN
% a > 0 AND b > 0 IMPLIES
% Integrable?(a,b,f) AND
% Integral(a, b, f) = 2*sqrt(b) - 2*sqrt(a)
END table_of_integrals
¤ 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.
|
