|
%------------------------------------------------------------------------------
% Integrals
%
% Author: David Lester, Manchester University, NIA, Université Perpignan
%
% All references are to SK Berberian "Fundamentals of Real Analysis",
% Springer, 1991
%
% Definition and basic properties of integrals for functions f: [T->real]
%
% Version 1.0 1/5/07 Initial Version
%------------------------------------------------------------------------------
integral[T:TYPE, (IMPORTING subset_algebra_def[T])
S:sigma_algebra, (IMPORTING measure_def[T,S])
m:measure_type]: THEORY
BEGIN
IMPORTING measure_space[T,S],
measure_theory[T,S,m],
nn_integral[T,S,m]
g,g1,g2,g3,g4: VAR nn_integrable
x: VAR T
integrable?(f:[T->real]):bool = EXISTS (g,h:nn_integrable): f = g-h % 4.4.7
integrable: TYPE+ = (integrable?) CONTAINING (lambda x: 0)
nn_integrable_is_integrable:
JUDGEMENT nn_integrable SUBTYPE_OF integrable % 4.4.10
isf_is_integrable:
JUDGEMENT isf SUBTYPE_OF integrable % 4.4.15
integrable_is_measurable:
JUDGEMENT integrable SUBTYPE_OF measurable_function
f,f1,f2: VAR integrable
w: VAR sequence[integrable]
f0: VAR [T->real]
h: VAR measurable_function
epsilon: VAR posreal
c: VAR real
nnc: VAR nnreal
E: VAR measurable_set
F: VAR (mu_fin?)
i: VAR isf
n: VAR nat
integrable_equiv: LEMMA g1 - g3 = g2 - g4 => % 4.4.8
nn_integral(g1) - nn_integral(g3) =
nn_integral(g2) - nn_integral(g4)
integrable_add: JUDGEMENT +(f1,f2) HAS_TYPE integrable
integrable_scal: JUDGEMENT *(c,f) HAS_TYPE integrable
integrable_opp: JUDGEMENT -(f) HAS_TYPE integrable
integrable_diff: JUDGEMENT -(f1,f2) HAS_TYPE integrable
integrable_zero: LEMMA integrable?(lambda x: 0)
integrals(f):set[real]
= {c| EXISTS (g,h:nn_integrable): f = g-h AND
c = nn_integral(g) - nn_integral(h)}
nonempty_integrals: LEMMA nonempty?[real](integrals(f))
singleton_integrals: LEMMA singleton?[real](integrals(f))
integral(f):real = choose[real](integrals(f)) % 4.4.9
nn_integrable_is_nn_integrable:
LEMMA (FORALL x: f(x) >= 0) => nn_integrable?(f)
integral_nn: LEMMA integral(g) = nn_integral(g) % 4.4.10
integral_zero: LEMMA integral(lambda x: 0) = 0 % 4.4.11
integral_phi: LEMMA integral(phi(F)) = mu(F)
integral_add: LEMMA integral(f1+f2) = integral(f1) + integral(f2)
integral_scal: LEMMA integral(c*f) = c*integral(f)
integral_opp: LEMMA integral(-f) = -integral(f)
integral_diff: LEMMA integral(f1-f2 ) = integral(f1) - integral(f2)
integral_nonneg: LEMMA (FORALL x: f(x) >= 0) => integral(f) >= 0
integrable_abs: JUDGEMENT abs(f) HAS_TYPE integrable % 4.4.12
integrable_max: JUDGEMENT max(f1,f2) HAS_TYPE integrable % 4.4.13
integrable_min: JUDGEMENT min(f1,f2) HAS_TYPE integrable % 4.4.13
integrable_plus: JUDGEMENT plus(f) HAS_TYPE integrable % 4.4.12
integrable_minus: JUDGEMENT minus(f) HAS_TYPE integrable % 4.4.12
integral_abs: LEMMA abs(integral(f)) <= integral(abs(f)) % 4.4.12
integrable_pm_def: LEMMA integrable?(f0) <=> % 4.4.12
(integrable?(plus(f0)) AND integrable?(minus(f0)))
integral_pm: LEMMA integral(f) = integral(plus(f))-integral(minus(f))
integrable_abs_def: LEMMA integrable?(abs(h)) <=> integrable?(h) % 4.4.12
integrable_nz_finite: LEMMA % 4.4.14
measurable_set?({x | abs(f(x)) >= epsilon}) AND
mu_fin?({x | abs(f(x)) >= epsilon})
isf_integral: LEMMA integral(i) = isf_integral(i) % 4.4.15
integral_ae_eq: LEMMA ae_eq?(f,h) => % 4.4.16
(integrable?(h) AND integral(f) = integral(h))
integral_prod: LEMMA ae_le?(abs(h),lambda x: nnc) => % 4.4.17
(integrable?(f*h) AND
integral(abs(f*h)) <= nnc * integral(abs(f)))
indefinite_integrable: LEMMA integrable?(phi(E)*f) % 4.4.18
integral_ae_le: LEMMA ae_le?(f1,f2) => % 4.4.19
integral(f1) <= integral(f2)
integral_ae_abs: LEMMA ae_le?(abs(h),abs(f)) => % 4.4.20
(integrable?(h) AND
abs(integral(h)) <= integral(abs(f)))
bounded_is_indefinite_integrable: LEMMA
bounded?(phi(F)*h) =>
(integrable?(phi(F)*h) AND
abs(integral(phi(F)*h)) <= mu(F)*sup_norm(phi(F)*h))
integral_abs_0: LEMMA integral(abs(f)) = 0 => ae_0?(f) % 4.4.21
measurable_ae_0: LEMMA ae_0?(h) =>
(integrable?(h) AND integral(h) = 0)
integral_ae_ge_0: LEMMA ae_nonneg?(f) AND integral(f) = 0 => ae_0?(f)
integrable_maximum: JUDGEMENT maximum(w,n) HAS_TYPE integrable
integrable_minimum: JUDGEMENT minimum(w,n) HAS_TYPE integrable
integrable_split: LEMMA FORALL (h:[T->real]):
integrable?(h) <=>
integrable?(phi(E)*h) AND integrable?(phi(complement(E))*h)
integral_split: LEMMA
integral(f) = integral(phi(E)*f) + integral(phi(complement(E))*f)
END integral
¤ 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.
|
