|
%------------------------------------------------------------------------------
% Non-negative 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 of functions f:[T->nnreal]
%
% Version 1.0 1/5/07 Initial Version
%------------------------------------------------------------------------------
nn_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_props[T,S,m],
measure_theory[T,S,m],
isf[T,S,m]
convergent?: MACRO pred[sequence[real]] = topological_convergence.convergent?
limit: MACRO [convergent->real] = topological_convergence.limit
n: VAR nat
pn: VAR posnat
x: VAR T
c: VAR nnreal
E: VAR measurable_set
F: VAR (mu_fin?)
g: VAR measurable_function
h: VAR nn_bounded_measurable
nn_isf?(i:isf):bool = FORALL x: i(x) >= 0
nn_isf: TYPE+ = (nn_isf?) CONTAINING (lambda x: 0)
i: VAR nn_isf
w: VAR sequence[nn_isf]
increasing_nn_isf?(u:sequence[nn_isf]):bool = pointwise_increasing?(u)
increasing_nn_isf: TYPE+ = (increasing_nn_isf?) CONTAINING
(lambda n: lambda x: 0)
u,u1,u2: VAR increasing_nn_isf
nn_integrable?(g:[T->nnreal]):bool % 4.4.1
= EXISTS u: pointwise_convergence?(u,g) AND convergent?(isf_integral o u)
nn_integrable_zero: LEMMA nn_integrable?(lambda x: 0)
nn_integrable: TYPE+ = (nn_integrable?) CONTAINING (lambda x: 0)
f,f1,f2: VAR nn_integrable
nn_integrable_is_nonneg: LEMMA f(x) >= 0
nn_integrable_is_measurable:
JUDGEMENT nn_integrable SUBTYPE_OF measurable_function % 4.4.1
nn_convergence: LEMMA pointwise_convergence?(u1,f) AND % 4.4.2
pointwise_convergence?(u2,f) AND
convergent?(isf_integral o u1) =>
(convergent?(isf_integral o u2) AND
limit(isf_integral o u1) = limit(isf_integral o u2))
nn_integral(f):nnreal % 4.4.3
= limit(isf_integral o choose({u | pointwise_convergence?(u,f)}))
nn_integrable_add: JUDGEMENT +(f1,f2) HAS_TYPE nn_integrable
nn_integrable_scal: JUDGEMENT *(c,f) HAS_TYPE nn_integrable
nn_isf_is_nn_integrable: JUDGEMENT nn_isf SUBTYPE_OF nn_integrable % 4.4.4
nn_integral_isf: LEMMA nn_integral(i) = isf_integral(i) % 4.4.4
nn_integrable_le: LEMMA (FORALL x: 0 <= g(x) AND g(x) <= f(x)) => % 4.4.5
(nn_integrable?(g) AND
nn_integral(g) <= nn_integral(f))
nn_integral_zero:LEMMA nn_integral(lambda x: 0) = 0
nn_integral_phi: LEMMA nn_integral(phi(F)) = mu(F)
nn_integral_add: LEMMA nn_integral(f1+f2) = nn_integral(f1) + nn_integral(f2)
nn_integral_scal:LEMMA nn_integral(c*f) = c * nn_integral(f)
nn_integrable_prod: JUDGEMENT *(f,h) HAS_TYPE nn_integrable
nn_indefinite_integrable: LEMMA nn_integrable?(phi(E)*f) % 4.4.6
nn_0_le: LEMMA 0 <= nn_integral(f)
nn_integral_def: LEMMA
EXISTS u: pointwise_convergence?(u,f) AND
convergence?(isf_integral o u, nn_integral(f))
END nn_integral
¤ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
