let X be non empty set ; for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for f being PartFunc of X,ExtREAL st E = dom f & f is E -measurable & f is nonnegative & M . (E /\ (eq_dom (f,+infty))) <> 0 holds
Integral (M,f) = +infty
let S be SigmaField of X; for M being sigma_Measure of S
for E being Element of S
for f being PartFunc of X,ExtREAL st E = dom f & f is E -measurable & f is nonnegative & M . (E /\ (eq_dom (f,+infty))) <> 0 holds
Integral (M,f) = +infty
let M be sigma_Measure of S; for E being Element of S
for f being PartFunc of X,ExtREAL st E = dom f & f is E -measurable & f is nonnegative & M . (E /\ (eq_dom (f,+infty))) <> 0 holds
Integral (M,f) = +infty
let E be Element of S; for f being PartFunc of X,ExtREAL st E = dom f & f is E -measurable & f is nonnegative & M . (E /\ (eq_dom (f,+infty))) <> 0 holds
Integral (M,f) = +infty
let f be PartFunc of X,ExtREAL; ( E = dom f & f is E -measurable & f is nonnegative & M . (E /\ (eq_dom (f,+infty))) <> 0 implies Integral (M,f) = +infty )
assume that
A1:
E = dom f
and
A2:
f is E -measurable
and
A3:
f is nonnegative
and
A4:
M . (E /\ (eq_dom (f,+infty))) <> 0
; Integral (M,f) = +infty
reconsider EE = E /\ (eq_dom (f,+infty)) as Element of S by A1, A2, MESFUNC1:33;
A5:
dom (f | E) = E
by A1;
E = (dom f) /\ E
by A1;
then A6:
f | E is E -measurable
by A2, MESFUNC5:42;
integral+ (M,(f | EE)) <= integral+ (M,(f | E))
by A1, A2, A3, MESFUNC5:83, XBOOLE_1:17;
then A7:
integral+ (M,(f | EE)) <= Integral (M,(f | E))
by A3, A6, A5, MESFUNC5:15, MESFUNC5:88;
A8:
EE = (dom f) /\ EE
by A1, XBOOLE_1:17, XBOOLE_1:28;
f is EE -measurable
by A2, MESFUNC1:30, XBOOLE_1:17;
then A9:
f | EE is EE -measurable
by A8, MESFUNC5:42;
A10:
f | EE is nonnegative
by A3, MESFUNC5:15;
reconsider ES = {} as Element of S by PROB_1:4;
deffunc H1( Element of NAT ) -> Element of bool [:X,ExtREAL:] = $1 (#) ((chi (EE,X)) | EE);
consider G being Function such that
A11:
( dom G = NAT & ( for n being Element of NAT holds G . n = H1(n) ) )
from FUNCT_1:sch 4();
then
rng G c= PFuncs (X,ExtREAL)
;
then reconsider G = G as Functional_Sequence of X,ExtREAL by A11, FUNCT_2:def 1, RELSET_1:4;
A14:
for n being Nat holds
( dom (G . n) = EE & ( for x being set st x in dom (G . n) holds
(G . n) . x = n ) )
proof
let n be
Nat;
( dom (G . n) = EE & ( for x being set st x in dom (G . n) holds
(G . n) . x = n ) )
reconsider n1 =
n as
Element of
NAT by ORDINAL1:def 12;
EE c= X
;
then
EE c= dom (chi (EE,X))
by FUNCT_3:def 3;
then A15:
dom ((chi (EE,X)) | EE) = EE
by RELAT_1:62;
A16:
G . n = n1 (#) ((chi (EE,X)) | EE)
by A11;
hence A17:
dom (G . n) = EE
by A15, MESFUNC1:def 6;
for x being set st x in dom (G . n) holds
(G . n) . x = n
let x be
set ;
( x in dom (G . n) implies (G . n) . x = n )
assume A18:
x in dom (G . n)
;
(G . n) . x = n
then reconsider x1 =
x as
Element of
X ;
(chi (EE,X)) . x1 = 1.
by A17, A18, FUNCT_3:def 3;
then
((chi (EE,X)) | EE) . x1 = 1.
by A15, A17, A18, FUNCT_1:47;
then
(G . n) . x = n1 * 1.
by A16, A18, MESFUNC1:def 6;
hence
(G . n) . x = n
by XXREAL_3:81;
verum
end;
A19:
for n being Nat holds G . n is nonnegative
deffunc H2( Element of NAT ) -> Element of ExtREAL = integral' (M,(G . $1));
consider K being sequence of ExtREAL such that
A20:
for n being Element of NAT holds K . n = H2(n)
from FUNCT_2:sch 4();
reconsider K = K as ExtREAL_sequence ;
A21:
for n being Nat holds K . n = integral' (M,(G . n))
A22:
dom (f | EE) = EE
by A1, RELAT_1:62, XBOOLE_1:17;
A23:
for n, m being Nat st n <= m holds
for x being Element of X st x in dom (f | EE) holds
(G . n) . x <= (G . m) . x
A27:
for n being Nat holds
( dom (G . n) = dom (f | EE) & G . n is_simple_func_in S )
A29:
for i being Element of NAT holds K . i = i * (M . (dom (G . i)))
M . ES <= M . EE
by MEASURE1:31, XBOOLE_1:2;
then A30:
In (0,REAL) < M . EE
by A4, VALUED_0:def 19;
A31:
not rng K is bounded_above
for n, m being Nat st m <= n holds
K . m <= K . n
then A43:
K is non-decreasing
by RINFSUP2:7;
then A44:
lim K = sup K
by RINFSUP2:37;
A45:
for x being Element of X st x in dom (f | EE) holds
( G # x is convergent & lim (G # x) = (f | EE) . x )
sup (rng K) is UpperBound of rng K
by XXREAL_2:def 3;
then A57:
sup K = +infty
by A31, XXREAL_2:53;
K is convergent
by A43, RINFSUP2:37;
then
integral+ (M,(f | EE)) = +infty
by A10, A22, A9, A27, A19, A23, A45, A21, A44, A57, MESFUNC5:def 15;
then
Integral (M,(f | E)) = +infty
by A7, XXREAL_0:4;
hence
Integral (M,f) = +infty
by A1; verum