let X be set ; 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; 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; 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; ( 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 )
; 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
let x be
ExtReal;
( x in rng (M * F) implies (M . (F . 0)) - (sup (rng (M * G))) <= x )
assume A4:
x in rng (M * F)
;
(M . (F . 0)) - (sup (rng (M * G))) <= x
(
x <> +infty implies
(M . (F . 0)) - (sup (rng (M * G))) <= x )
proof
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
;
(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))
(M . (F . 0)) - x = a - b
by A11, A12, SUPINF_2:3;
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;
verum
end;
hence
(M . (F . 0)) - (sup (rng (M * G))) <= x
by XXREAL_0:4;
verum
end;
then A22:
(M . (F . 0)) - (sup (rng (M * G))) is LowerBound of rng (M * F)
by XXREAL_2:def 2;
for y being LowerBound of rng (M * F) holds y <= (M . (F . 0)) - (sup (rng (M * G)))
proof
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);
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;
verum
end;
hence
inf (rng (M * F)) = (M . (F . 0)) - (sup (rng (M * G)))
by A22, XXREAL_2:def 4; verum