let X be set ; :: thesis: for S being SigmaField of X

for M being sigma_Measure of S

for G, F being sequence of S st M . (F . 0) < +infty & G . 0 = {} & ( for n being Nat holds

( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) holds

inf (rng (M * F)) = (M . (F . 0)) - (sup (rng (M * G)))

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for G, F being sequence of S st M . (F . 0) < +infty & G . 0 = {} & ( for n being Nat holds

( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) holds

inf (rng (M * F)) = (M . (F . 0)) - (sup (rng (M * G)))

let M be sigma_Measure of S; :: thesis: for G, F being sequence of S st M . (F . 0) < +infty & G . 0 = {} & ( for n being Nat holds

( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) holds

inf (rng (M * F)) = (M . (F . 0)) - (sup (rng (M * G)))

let G, F be sequence of S; :: thesis: ( M . (F . 0) < +infty & G . 0 = {} & ( for n being Nat holds

( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) implies inf (rng (M * F)) = (M . (F . 0)) - (sup (rng (M * G))) )

assume that

A1: M . (F . 0) < +infty and

A2: G . 0 = {} and

A3: for n being Nat holds

( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ; :: thesis: inf (rng (M * F)) = (M . (F . 0)) - (sup (rng (M * G)))

set l = (M . (F . 0)) - (sup (rng (M * G)));

for x being ExtReal st x in rng (M * F) holds

(M . (F . 0)) - (sup (rng (M * G))) <= x

for y being LowerBound of rng (M * F) holds y <= (M . (F . 0)) - (sup (rng (M * G)))

for M being sigma_Measure of S

for G, F being sequence of S st M . (F . 0) < +infty & G . 0 = {} & ( for n being Nat holds

( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) holds

inf (rng (M * F)) = (M . (F . 0)) - (sup (rng (M * G)))

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for G, F being sequence of S st M . (F . 0) < +infty & G . 0 = {} & ( for n being Nat holds

( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) holds

inf (rng (M * F)) = (M . (F . 0)) - (sup (rng (M * G)))

let M be sigma_Measure of S; :: thesis: for G, F being sequence of S st M . (F . 0) < +infty & G . 0 = {} & ( for n being Nat holds

( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) holds

inf (rng (M * F)) = (M . (F . 0)) - (sup (rng (M * G)))

let G, F be sequence of S; :: thesis: ( M . (F . 0) < +infty & G . 0 = {} & ( for n being Nat holds

( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) implies inf (rng (M * F)) = (M . (F . 0)) - (sup (rng (M * G))) )

assume that

A1: M . (F . 0) < +infty and

A2: G . 0 = {} and

A3: for n being Nat holds

( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ; :: thesis: inf (rng (M * F)) = (M . (F . 0)) - (sup (rng (M * G)))

set l = (M . (F . 0)) - (sup (rng (M * G)));

for x being ExtReal st x in rng (M * F) holds

(M . (F . 0)) - (sup (rng (M * G))) <= x

proof

then A22:
(M . (F . 0)) - (sup (rng (M * G))) is LowerBound of rng (M * F)
by XXREAL_2:def 2;
let x be ExtReal; :: thesis: ( x in rng (M * F) implies (M . (F . 0)) - (sup (rng (M * G))) <= x )

assume A4: x in rng (M * F) ; :: thesis: (M . (F . 0)) - (sup (rng (M * G))) <= x

( x <> +infty implies (M . (F . 0)) - (sup (rng (M * G))) <= x )

end;assume A4: x in rng (M * F) ; :: thesis: (M . (F . 0)) - (sup (rng (M * G))) <= x

( x <> +infty implies (M . (F . 0)) - (sup (rng (M * G))) <= x )

proof

hence
(M . (F . 0)) - (sup (rng (M * G))) <= x
by XXREAL_0:4; :: thesis: verum
A5:
dom (M * F) = NAT
by FUNCT_2:def 1;

then consider n being object such that

A6: n in NAT and

A7: (M * F) . n = x by A4, FUNCT_1:def 3;

M * F is V92() by MEASURE2:1;

then A8: 0. <= x by A6, A7, SUPINF_2:39;

assume A9: x <> +infty ; :: thesis: (M . (F . 0)) - (sup (rng (M * G))) <= x

reconsider x = x as R_eal by XXREAL_0:def 1;

x <= +infty by XXREAL_0:3;

then x < +infty by A9, XXREAL_0:1;

then A10: x in REAL by A8, XXREAL_0:14, XXREAL_0:46;

( M . (F . 0) in REAL & sup (rng (M * G)) in REAL ) by A1, A2, A3, Th9;

then consider a, b, c being Real such that

A11: a = M . (F . 0) and

A12: b = x and

A13: c = sup (rng (M * G)) by A10;

(sup (rng (M * G))) + x = c + b by A12, A13, SUPINF_2:1;

then A14: ((sup (rng (M * G))) + x) - (sup (rng (M * G))) = (b + c) - c by A13, SUPINF_2:3

.= x by A12 ;

reconsider n = n as Element of NAT by A6;

A15: dom (M * G) = NAT by FUNCT_2:def 1;

A16: (M . (F . 0)) - x <= sup (rng (M * G))

then ((M . (F . 0)) - x) + x = (a - b) + b by A12, SUPINF_2:1

.= M . (F . 0) by A11 ;

then M . (F . 0) <= (sup (rng (M * G))) + x by A16, XXREAL_3:36;

hence (M . (F . 0)) - (sup (rng (M * G))) <= x by A14, XXREAL_3:37; :: thesis: verum

end;then consider n being object such that

A6: n in NAT and

A7: (M * F) . n = x by A4, FUNCT_1:def 3;

M * F is V92() by MEASURE2:1;

then A8: 0. <= x by A6, A7, SUPINF_2:39;

assume A9: x <> +infty ; :: thesis: (M . (F . 0)) - (sup (rng (M * G))) <= x

reconsider x = x as R_eal by XXREAL_0:def 1;

x <= +infty by XXREAL_0:3;

then x < +infty by A9, XXREAL_0:1;

then A10: x in REAL by A8, XXREAL_0:14, XXREAL_0:46;

( M . (F . 0) in REAL & sup (rng (M * G)) in REAL ) by A1, A2, A3, Th9;

then consider a, b, c being Real such that

A11: a = M . (F . 0) and

A12: b = x and

A13: c = sup (rng (M * G)) by A10;

(sup (rng (M * G))) + x = c + b by A12, A13, SUPINF_2:1;

then A14: ((sup (rng (M * G))) + x) - (sup (rng (M * G))) = (b + c) - c by A13, SUPINF_2:3

.= x by A12 ;

reconsider n = n as Element of NAT by A6;

A15: dom (M * G) = NAT by FUNCT_2:def 1;

A16: (M . (F . 0)) - x <= sup (rng (M * G))

proof

(M . (F . 0)) - x = a - b
by A11, A12, SUPINF_2:3;
set k = n + 1;

A17: for n being Nat holds F . n c= F . 0

then A21: M . (F . n) < +infty by A1, XXREAL_0:2;

(M . (F . 0)) - x = (M . (F . 0)) - (M . (F . n)) by A5, A7, FUNCT_1:12

.= M . ((F . 0) \ (F . n)) by A17, A21, MEASURE1:32

.= M . (G . (n + 1)) by A3 ;

then (M . (F . 0)) - x = (M * G) . (n + 1) by A15, FUNCT_1:12;

hence (M . (F . 0)) - x <= sup (rng (M * G)) by FUNCT_2:4, XXREAL_2:4; :: thesis: verum

end;A17: for n being Nat holds F . n c= F . 0

proof

then
M . (F . n) <= M . (F . 0)
by MEASURE1:31;
defpred S_{1}[ Nat] means F . $1 c= F . 0;

A18: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
;

thus for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A20, A18); :: thesis: verum

end;A18: for k being Nat st S

S

proof

A20:
S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A19: F . k c= F . 0 ; :: thesis: S_{1}[k + 1]

F . (k + 1) c= F . k by A3;

hence S_{1}[k + 1]
by A19, XBOOLE_1:1; :: thesis: verum

end;assume A19: F . k c= F . 0 ; :: thesis: S

F . (k + 1) c= F . k by A3;

hence S

thus for k being Nat holds S

then A21: M . (F . n) < +infty by A1, XXREAL_0:2;

(M . (F . 0)) - x = (M . (F . 0)) - (M . (F . n)) by A5, A7, FUNCT_1:12

.= M . ((F . 0) \ (F . n)) by A17, A21, MEASURE1:32

.= M . (G . (n + 1)) by A3 ;

then (M . (F . 0)) - x = (M * G) . (n + 1) by A15, FUNCT_1:12;

hence (M . (F . 0)) - x <= sup (rng (M * G)) by FUNCT_2:4, XXREAL_2:4; :: thesis: verum

then ((M . (F . 0)) - x) + x = (a - b) + b by A12, SUPINF_2:1

.= M . (F . 0) by A11 ;

then M . (F . 0) <= (sup (rng (M * G))) + x by A16, XXREAL_3:36;

hence (M . (F . 0)) - (sup (rng (M * G))) <= x by A14, XXREAL_3:37; :: thesis: verum

for y being LowerBound of rng (M * F) holds y <= (M . (F . 0)) - (sup (rng (M * G)))

proof

hence
inf (rng (M * F)) = (M . (F . 0)) - (sup (rng (M * G)))
by A22, XXREAL_2:def 4; :: thesis: verum
A23:
inf (rng (M * F)) in REAL
by A1, A2, A3, Th9;

( sup (rng (M * G)) in REAL & M . (F . 0) in REAL ) by A1, A2, A3, Th9;

then consider a, b, c being Real such that

A24: a = sup (rng (M * G)) and

A25: b = M . (F . 0) and

A26: c = inf (rng (M * F)) by A23;

(sup (rng (M * G))) + (inf (rng (M * F))) = a + c by A24, A26, SUPINF_2:1;

then A27: ((sup (rng (M * G))) + (inf (rng (M * F)))) - (sup (rng (M * G))) = (c + a) - a by A24, SUPINF_2:3

.= inf (rng (M * F)) by A26 ;

let y be LowerBound of rng (M * F); :: thesis: y <= (M . (F . 0)) - (sup (rng (M * G)))

consider s, t, r being R_eal such that

s = sup (rng (M * G)) and

t = (M . (F . 0)) - (inf (rng (M * F))) and

A28: r = inf (rng (M * F)) ;

A29: sup (rng (M * G)) = (M . (F . 0)) - (inf (rng (M * F))) by A1, A2, A3, Th10;

(M . (F . 0)) - (inf (rng (M * F))) = b - c by A25, A26, SUPINF_2:3;

then ((M . (F . 0)) - (inf (rng (M * F)))) + r = (b - c) + c by A26, A28, SUPINF_2:1

.= M . (F . 0) by A25 ;

hence y <= (M . (F . 0)) - (sup (rng (M * G))) by A29, A28, A27, XXREAL_2:def 4; :: thesis: verum

end;( sup (rng (M * G)) in REAL & M . (F . 0) in REAL ) by A1, A2, A3, Th9;

then consider a, b, c being Real such that

A24: a = sup (rng (M * G)) and

A25: b = M . (F . 0) and

A26: c = inf (rng (M * F)) by A23;

(sup (rng (M * G))) + (inf (rng (M * F))) = a + c by A24, A26, SUPINF_2:1;

then A27: ((sup (rng (M * G))) + (inf (rng (M * F)))) - (sup (rng (M * G))) = (c + a) - a by A24, SUPINF_2:3

.= inf (rng (M * F)) by A26 ;

let y be LowerBound of rng (M * F); :: thesis: y <= (M . (F . 0)) - (sup (rng (M * G)))

consider s, t, r being R_eal such that

s = sup (rng (M * G)) and

t = (M . (F . 0)) - (inf (rng (M * F))) and

A28: r = inf (rng (M * F)) ;

A29: sup (rng (M * G)) = (M . (F . 0)) - (inf (rng (M * F))) by A1, A2, A3, Th10;

(M . (F . 0)) - (inf (rng (M * F))) = b - c by A25, A26, SUPINF_2:3;

then ((M . (F . 0)) - (inf (rng (M * F)))) + r = (b - c) + c by A26, A28, SUPINF_2:1

.= M . (F . 0) by A25 ;

hence y <= (M . (F . 0)) - (sup (rng (M * G))) by A29, A28, A27, XXREAL_2:def 4; :: thesis: verum