let X be non empty set ; for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL st f is_simple_func_in S & f is nonnegative holds
integral' (M,(f | (eq_dom (f,0)))) = 0
let S be SigmaField of X; for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL st f is_simple_func_in S & f is nonnegative holds
integral' (M,(f | (eq_dom (f,0)))) = 0
let M be sigma_Measure of S; for f being PartFunc of X,ExtREAL st f is_simple_func_in S & f is nonnegative holds
integral' (M,(f | (eq_dom (f,0)))) = 0
let f be PartFunc of X,ExtREAL; ( f is_simple_func_in S & f is nonnegative implies integral' (M,(f | (eq_dom (f,0)))) = 0 )
assume that
A1:
f is_simple_func_in S
and
A2:
f is nonnegative
; integral' (M,(f | (eq_dom (f,0)))) = 0
set A = dom f;
set g = f | ((dom f) /\ (eq_dom (f,0)));
for x being object st x in eq_dom (f,0) holds
x in dom f
by MESFUNC1:def 15;
then
eq_dom (f,0) c= dom f
;
then A3:
f | ((dom f) /\ (eq_dom (f,0))) = f | (eq_dom (f,0))
by XBOOLE_1:28;
A4:
ex G being Finite_Sep_Sequence of S st
( dom (f | ((dom f) /\ (eq_dom (f,0)))) = union (rng G) & ( for n being Nat
for x, y being Element of X st n in dom G & x in G . n & y in G . n holds
(f | ((dom f) /\ (eq_dom (f,0)))) . x = (f | ((dom f) /\ (eq_dom (f,0)))) . y ) )
proof
consider F being
Finite_Sep_Sequence of
S such that A5:
dom f = union (rng F)
and A6:
for
n being
Nat for
x,
y being
Element of
X st
n in dom F &
x in F . n &
y in F . n holds
f . x = f . y
by A1, MESFUNC2:def 4;
deffunc H1(
Nat)
-> Element of
bool X =
(F . $1) /\ ((dom f) /\ (eq_dom (f,0)));
reconsider A =
dom f as
Element of
S by A5, MESFUNC2:31;
consider G being
FinSequence such that A7:
(
len G = len F & ( for
n being
Nat st
n in dom G holds
G . n = H1(
n) ) )
from FINSEQ_1:sch 2();
f is
A -measurable
by A1, MESFUNC2:34;
then
A /\ (less_dom (f,0)) in S
by MESFUNC1:def 16;
then
A \ (A /\ (less_dom (f,0))) in S
by PROB_1:6;
then reconsider A1 =
A /\ (great_eq_dom (f,0.)) as
Element of
S by MESFUNC1:14;
f is
A1 -measurable
by A1, MESFUNC2:34;
then
(A /\ (great_eq_dom (f,0))) /\ (less_eq_dom (f,0)) in S
by MESFUNC1:28;
then reconsider A2 =
A /\ (eq_dom (f,0)) as
Element of
S by MESFUNC1:18;
A8:
dom F = Seg (len F)
by FINSEQ_1:def 3;
dom G = Seg (len F)
by A7, FINSEQ_1:def 3;
then A9:
for
i being
Nat st
i in dom F holds
G . i = (F . i) /\ A2
by A7, A8;
dom G = Seg (len F)
by A7, FINSEQ_1:def 3;
then A10:
dom G = dom F
by FINSEQ_1:def 3;
then reconsider G =
G as
Finite_Sep_Sequence of
S by A9, Th35;
take
G
;
( dom (f | ((dom f) /\ (eq_dom (f,0)))) = union (rng G) & ( for n being Nat
for x, y being Element of X st n in dom G & x in G . n & y in G . n holds
(f | ((dom f) /\ (eq_dom (f,0)))) . x = (f | ((dom f) /\ (eq_dom (f,0)))) . y ) )
for
i being
Nat st
i in dom G holds
G . i = A2 /\ (F . i)
by A7;
then A11:
union (rng G) =
A2 /\ (dom f)
by A5, A10, MESFUNC3:6
.=
dom (f | ((dom f) /\ (eq_dom (f,0))))
by RELAT_1:61
;
for
i being
Nat for
x,
y being
Element of
X st
i in dom G &
x in G . i &
y in G . i holds
(f | ((dom f) /\ (eq_dom (f,0)))) . x = (f | ((dom f) /\ (eq_dom (f,0)))) . y
proof
let i be
Nat;
for x, y being Element of X st i in dom G & x in G . i & y in G . i holds
(f | ((dom f) /\ (eq_dom (f,0)))) . x = (f | ((dom f) /\ (eq_dom (f,0)))) . ylet x,
y be
Element of
X;
( i in dom G & x in G . i & y in G . i implies (f | ((dom f) /\ (eq_dom (f,0)))) . x = (f | ((dom f) /\ (eq_dom (f,0)))) . y )
assume that A12:
i in dom G
and A13:
x in G . i
and A14:
y in G . i
;
(f | ((dom f) /\ (eq_dom (f,0)))) . x = (f | ((dom f) /\ (eq_dom (f,0)))) . y
A15:
G . i = (F . i) /\ A2
by A7, A12;
then A16:
y in F . i
by A14, XBOOLE_0:def 4;
A17:
G . i in rng G
by A12, FUNCT_1:3;
then
x in dom (f | ((dom f) /\ (eq_dom (f,0))))
by A11, A13, TARSKI:def 4;
then A18:
(f | ((dom f) /\ (eq_dom (f,0)))) . x = f . x
by FUNCT_1:47;
y in dom (f | ((dom f) /\ (eq_dom (f,0))))
by A11, A14, A17, TARSKI:def 4;
then A19:
(f | ((dom f) /\ (eq_dom (f,0)))) . y = f . y
by FUNCT_1:47;
x in F . i
by A13, A15, XBOOLE_0:def 4;
hence
(f | ((dom f) /\ (eq_dom (f,0)))) . x = (f | ((dom f) /\ (eq_dom (f,0)))) . y
by A6, A10, A12, A16, A18, A19;
verum
end;
hence
(
dom (f | ((dom f) /\ (eq_dom (f,0)))) = union (rng G) & ( for
n being
Nat for
x,
y being
Element of
X st
n in dom G &
x in G . n &
y in G . n holds
(f | ((dom f) /\ (eq_dom (f,0)))) . x = (f | ((dom f) /\ (eq_dom (f,0)))) . y ) )
by A11;
verum
end;
for x being object st x in dom (f | ((dom f) /\ (eq_dom (f,0)))) holds
0 <= (f | ((dom f) /\ (eq_dom (f,0)))) . x
then a2:
f | ((dom f) /\ (eq_dom (f,0))) is nonnegative
by SUPINF_2:52;
f is real-valued
by A1, MESFUNC2:def 4;
then A22:
f | ((dom f) /\ (eq_dom (f,0))) is_simple_func_in S
by A4, MESFUNC2:def 4;
now ( dom (f | ((dom f) /\ (eq_dom (f,0)))) <> {} implies integral' (M,(f | (eq_dom (f,0)))) = 0 )consider F being
Finite_Sep_Sequence of
S,
a,
x being
FinSequence of
ExtREAL such that A23:
F,
a are_Re-presentation_of f | ((dom f) /\ (eq_dom (f,0)))
and
a . 1
= 0
and
for
n being
Nat st 2
<= n &
n in dom a holds
(
0 < a . n &
a . n < +infty )
and A24:
dom x = dom F
and A25:
for
n being
Nat st
n in dom x holds
x . n = (a . n) * ((M * F) . n)
and A26:
integral (
M,
(f | ((dom f) /\ (eq_dom (f,0)))))
= Sum x
by a2, A22, MESFUNC3:def 2;
A27:
for
x being
set st
x in dom (f | ((dom f) /\ (eq_dom (f,0)))) holds
(f | ((dom f) /\ (eq_dom (f,0)))) . x = 0
A29:
for
n being
Nat holds
( not
n in dom F or
a . n = 0 or
F . n = {} )
A32:
for
n being
Nat st
n in dom x holds
x . n = 0
A34:
Sum x = 0
assume
dom (f | ((dom f) /\ (eq_dom (f,0)))) <> {}
;
integral' (M,(f | (eq_dom (f,0)))) = 0 hence
integral' (
M,
(f | (eq_dom (f,0))))
= 0
by A3, A26, A34, Def14;
verum end;
hence
integral' (M,(f | (eq_dom (f,0)))) = 0
by A3, Def14; verum