let A be non empty closed_interval Subset of REAL; for f being PartFunc of A,REAL st f is bounded & A c= dom f & vol A > 0 holds
ex F being with_the_same_dom Functional_Sequence of REAL,ExtREAL ex I being ExtREAL_sequence st
( A = dom (F . 0) & ( for n being Nat holds
( F . n is_simple_func_in Borel_Sets & Integral (B-Meas,(F . n)) = lower_sum (f,(EqDiv (A,(2 |^ n)))) & ( for x being Real st x in A holds
( lower_bound (rng f) <= (F . n) . x & (F . n) . x <= f . x ) ) ) ) & ( for n, m being Nat st n <= m holds
for x being Element of REAL st x in A holds
(F . n) . x <= (F . m) . x ) & ( for x being Element of REAL st x in A holds
( F # x is convergent & lim (F # x) = sup (F # x) & sup (F # x) <= f . x ) ) & lim F is_integrable_on B-Meas & ( for n being Nat holds I . n = Integral (B-Meas,(F . n)) ) & I is convergent & lim I = Integral (B-Meas,(lim F)) )
let f be PartFunc of A,REAL; ( f is bounded & A c= dom f & vol A > 0 implies ex F being with_the_same_dom Functional_Sequence of REAL,ExtREAL ex I being ExtREAL_sequence st
( A = dom (F . 0) & ( for n being Nat holds
( F . n is_simple_func_in Borel_Sets & Integral (B-Meas,(F . n)) = lower_sum (f,(EqDiv (A,(2 |^ n)))) & ( for x being Real st x in A holds
( lower_bound (rng f) <= (F . n) . x & (F . n) . x <= f . x ) ) ) ) & ( for n, m being Nat st n <= m holds
for x being Element of REAL st x in A holds
(F . n) . x <= (F . m) . x ) & ( for x being Element of REAL st x in A holds
( F # x is convergent & lim (F # x) = sup (F # x) & sup (F # x) <= f . x ) ) & lim F is_integrable_on B-Meas & ( for n being Nat holds I . n = Integral (B-Meas,(F . n)) ) & I is convergent & lim I = Integral (B-Meas,(lim F)) ) )
assume that
A1:
f is bounded
and
A2:
A c= dom f
and
A3:
vol A > 0
; ex F being with_the_same_dom Functional_Sequence of REAL,ExtREAL ex I being ExtREAL_sequence st
( A = dom (F . 0) & ( for n being Nat holds
( F . n is_simple_func_in Borel_Sets & Integral (B-Meas,(F . n)) = lower_sum (f,(EqDiv (A,(2 |^ n)))) & ( for x being Real st x in A holds
( lower_bound (rng f) <= (F . n) . x & (F . n) . x <= f . x ) ) ) ) & ( for n, m being Nat st n <= m holds
for x being Element of REAL st x in A holds
(F . n) . x <= (F . m) . x ) & ( for x being Element of REAL st x in A holds
( F # x is convergent & lim (F # x) = sup (F # x) & sup (F # x) <= f . x ) ) & lim F is_integrable_on B-Meas & ( for n being Nat holds I . n = Integral (B-Meas,(F . n)) ) & I is convergent & lim I = Integral (B-Meas,(lim F)) )
reconsider A1 = A as Element of Borel_Sets by MEASUR12:72;
defpred S1[ Nat, PartFunc of REAL,ExtREAL] means ( A = dom $2 & $2 is_simple_func_in Borel_Sets & Integral (B-Meas,$2) = lower_sum (f,(EqDiv (A,(2 |^ $1)))) & ( for x being Real st x in A holds
( lower_bound (rng f) <= $2 . x & $2 . x <= f . x ) ) & ex K being Finite_Sep_Sequence of Borel_Sets st
( dom K = dom (EqDiv (A,(2 |^ $1))) & union (rng K) = A & ( for k being Nat st k in dom K holds
( ( len (EqDiv (A,(2 |^ $1))) = 1 implies K . k = [.(inf A),(sup A).] ) & ( len (EqDiv (A,(2 |^ $1))) <> 1 implies ( ( k = 1 implies K . k = [.(inf A),((EqDiv (A,(2 |^ $1))) . k).[ ) & ( 1 < k & k < len (EqDiv (A,(2 |^ $1))) implies K . k = [.((EqDiv (A,(2 |^ $1))) . (k -' 1)),((EqDiv (A,(2 |^ $1))) . k).[ ) & ( k = len (EqDiv (A,(2 |^ $1))) implies K . k = [.((EqDiv (A,(2 |^ $1))) . (k -' 1)),((EqDiv (A,(2 |^ $1))) . k).] ) ) ) ) ) & ( for x being Real st x in dom $2 holds
ex k being Nat st
( 1 <= k & k <= len K & x in K . k & $2 . x = lower_bound (rng (f | (divset ((EqDiv (A,(2 |^ $1))),k)))) ) ) ) );
A4:
for n being Element of NAT ex g being Element of PFuncs (REAL,ExtREAL) st S1[n,g]
proof
let n be
Element of
NAT ;
ex g being Element of PFuncs (REAL,ExtREAL) st S1[n,g]
consider K being
Finite_Sep_Sequence of
Borel_Sets ,
g being
PartFunc of
REAL,
ExtREAL such that A5:
(
dom K = dom (EqDiv (A,(2 |^ n))) &
union (rng K) = A & ( for
k being
Nat st
k in dom K holds
( (
len (EqDiv (A,(2 |^ n))) = 1 implies
K . k = [.(inf A),(sup A).] ) & (
len (EqDiv (A,(2 |^ n))) <> 1 implies ( (
k = 1 implies
K . k = [.(inf A),((EqDiv (A,(2 |^ n))) . k).[ ) & ( 1
< k &
k < len (EqDiv (A,(2 |^ n))) implies
K . k = [.((EqDiv (A,(2 |^ n))) . (k -' 1)),((EqDiv (A,(2 |^ n))) . k).[ ) & (
k = len (EqDiv (A,(2 |^ n))) implies
K . k = [.((EqDiv (A,(2 |^ n))) . (k -' 1)),((EqDiv (A,(2 |^ n))) . k).] ) ) ) ) ) &
g is_simple_func_in Borel_Sets & ( for
x being
Real st
x in dom g holds
ex
k being
Nat st
( 1
<= k &
k <= len K &
x in K . k &
g . x = lower_bound (rng (f | (divset ((EqDiv (A,(2 |^ n))),k)))) ) ) &
dom g = A &
Integral (
B-Meas,
g)
= lower_sum (
f,
(EqDiv (A,(2 |^ n)))) & ( for
x being
Real st
x in A holds
(
lower_bound (rng f) <= g . x &
g . x <= f . x ) ) )
by A1, A2, Th19;
g is
Element of
PFuncs (
REAL,
ExtREAL)
by PARTFUN1:45;
hence
ex
g being
Element of
PFuncs (
REAL,
ExtREAL) st
S1[
n,
g]
by A5;
verum
end;
consider F being Function of NAT,(PFuncs (REAL,ExtREAL)) such that
A6:
for n being Element of NAT holds S1[n,F . n]
from FUNCT_2:sch 3(A4);
reconsider F = F as Functional_Sequence of REAL,ExtREAL ;
for n, m being Nat holds dom (F . n) = dom (F . m)
then reconsider F = F as with_the_same_dom Functional_Sequence of REAL,ExtREAL by MESFUNC8:def 2;
take
F
; ex I being ExtREAL_sequence st
( A = dom (F . 0) & ( for n being Nat holds
( F . n is_simple_func_in Borel_Sets & Integral (B-Meas,(F . n)) = lower_sum (f,(EqDiv (A,(2 |^ n)))) & ( for x being Real st x in A holds
( lower_bound (rng f) <= (F . n) . x & (F . n) . x <= f . x ) ) ) ) & ( for n, m being Nat st n <= m holds
for x being Element of REAL st x in A holds
(F . n) . x <= (F . m) . x ) & ( for x being Element of REAL st x in A holds
( F # x is convergent & lim (F # x) = sup (F # x) & sup (F # x) <= f . x ) ) & lim F is_integrable_on B-Meas & ( for n being Nat holds I . n = Integral (B-Meas,(F . n)) ) & I is convergent & lim I = Integral (B-Meas,(lim F)) )
A7:
A = dom (F . 0)
by A6;
A8:
for n being Nat holds
( F . n is_simple_func_in Borel_Sets & Integral (B-Meas,(F . n)) = lower_sum (f,(EqDiv (A,(2 |^ n)))) & ( for x being Real st x in A holds
( lower_bound (rng f) <= (F . n) . x & (F . n) . x <= f . x ) ) )
A9:
for n, m being Nat st n <= m holds
for x being Element of REAL st x in A holds
(F . n) . x <= (F . m) . x
proof
let n,
m be
Nat;
( n <= m implies for x being Element of REAL st x in A holds
(F . n) . x <= (F . m) . x )
assume A10:
n <= m
;
for x being Element of REAL st x in A holds
(F . n) . x <= (F . m) . x
A11:
(
n is
Element of
NAT &
m is
Element of
NAT )
by ORDINAL1:def 12;
let x be
Element of
REAL ;
( x in A implies (F . n) . x <= (F . m) . x )
assume A12:
x in A
;
(F . n) . x <= (F . m) . x
consider Kn being
Finite_Sep_Sequence of
Borel_Sets such that A13:
(
dom Kn = dom (EqDiv (A,(2 |^ n))) &
union (rng Kn) = A & ( for
k being
Nat st
k in dom Kn holds
( (
len (EqDiv (A,(2 |^ n))) = 1 implies
Kn . k = [.(inf A),(sup A).] ) & (
len (EqDiv (A,(2 |^ n))) <> 1 implies ( (
k = 1 implies
Kn . k = [.(inf A),((EqDiv (A,(2 |^ n))) . k).[ ) & ( 1
< k &
k < len (EqDiv (A,(2 |^ n))) implies
Kn . k = [.((EqDiv (A,(2 |^ n))) . (k -' 1)),((EqDiv (A,(2 |^ n))) . k).[ ) & (
k = len (EqDiv (A,(2 |^ n))) implies
Kn . k = [.((EqDiv (A,(2 |^ n))) . (k -' 1)),((EqDiv (A,(2 |^ n))) . k).] ) ) ) ) ) & ( for
x being
Real st
x in dom (F . n) holds
ex
k being
Nat st
( 1
<= k &
k <= len Kn &
x in Kn . k &
(F . n) . x = lower_bound (rng (f | (divset ((EqDiv (A,(2 |^ n))),k)))) ) ) )
by A6, A11;
consider Km being
Finite_Sep_Sequence of
Borel_Sets such that A14:
(
dom Km = dom (EqDiv (A,(2 |^ m))) &
union (rng Km) = A & ( for
k being
Nat st
k in dom Km holds
( (
len (EqDiv (A,(2 |^ m))) = 1 implies
Km . k = [.(inf A),(sup A).] ) & (
len (EqDiv (A,(2 |^ m))) <> 1 implies ( (
k = 1 implies
Km . k = [.(inf A),((EqDiv (A,(2 |^ m))) . k).[ ) & ( 1
< k &
k < len (EqDiv (A,(2 |^ m))) implies
Km . k = [.((EqDiv (A,(2 |^ m))) . (k -' 1)),((EqDiv (A,(2 |^ m))) . k).[ ) & (
k = len (EqDiv (A,(2 |^ m))) implies
Km . k = [.((EqDiv (A,(2 |^ m))) . (k -' 1)),((EqDiv (A,(2 |^ m))) . k).] ) ) ) ) ) & ( for
x being
Real st
x in dom (F . m) holds
ex
k being
Nat st
( 1
<= k &
k <= len Km &
x in Km . k &
(F . m) . x = lower_bound (rng (f | (divset ((EqDiv (A,(2 |^ m))),k)))) ) ) )
by A6, A11;
A15:
(
len (EqDiv (A,(2 |^ n))) = len Kn &
len (EqDiv (A,(2 |^ m))) = len Km )
by A13, A14, FINSEQ_3:29;
x in dom (F . n)
by A6, A11, A12;
then consider k1 being
Nat such that A16:
( 1
<= k1 &
k1 <= len Kn &
x in Kn . k1 &
(F . n) . x = lower_bound (rng (f | (divset ((EqDiv (A,(2 |^ n))),k1)))) )
by A13;
x in dom (F . m)
by A6, A11, A12;
then consider k2 being
Nat such that A17:
( 1
<= k2 &
k2 <= len Km &
x in Km . k2 &
(F . m) . x = lower_bound (rng (f | (divset ((EqDiv (A,(2 |^ m))),k2)))) )
by A14;
A18:
(
k1 - 1
= k1 -' 1 &
k2 - 1
= k2 -' 1 )
by A16, A17, XREAL_1:48, XREAL_0:def 2;
A19:
(
k1 in dom Kn &
k2 in dom Km )
by A16, A17, FINSEQ_3:25;
then
divset (
(EqDiv (A,(2 |^ n))),
k1)
c= A
by A13, INTEGRA1:8;
then A20:
divset (
(EqDiv (A,(2 |^ n))),
k1)
c= dom f
by A2;
f = f | (dom f)
;
then
f | (divset ((EqDiv (A,(2 |^ n))),k1)) is
bounded
by A1, A20, RFUNCT_1:74;
then A21:
rng (f | (divset ((EqDiv (A,(2 |^ n))),k1))) is
real-bounded
by INTEGRA1:15;
divset (
(EqDiv (A,(2 |^ m))),
k2)
c= A
by A14, A19, INTEGRA1:8;
then
divset (
(EqDiv (A,(2 |^ m))),
k2)
c= dom f
by A2;
then
dom (f | (divset ((EqDiv (A,(2 |^ m))),k2))) = divset (
(EqDiv (A,(2 |^ m))),
k2)
by RELAT_1:62;
then A22:
rng (f | (divset ((EqDiv (A,(2 |^ m))),k2))) <> {}
by RELAT_1:42;
A23:
( 2
|^ n > 0 & 2
|^ m > 0 )
by NEWTON:83;
then A24:
(
EqDiv (
A,
(2 |^ n))
divide_into_equal 2
|^ n &
EqDiv (
A,
(2 |^ m))
divide_into_equal 2
|^ m )
by A3, Def1;
then A25:
(
len (EqDiv (A,(2 |^ n))) = 2
|^ n &
len (EqDiv (A,(2 |^ m))) = 2
|^ m )
by INTEGRA4:def 1;
then A26:
(
(EqDiv (A,(2 |^ n))) . k1 = (lower_bound A) + (((vol A) / (2 |^ n)) * k1) &
(EqDiv (A,(2 |^ m))) . k2 = (lower_bound A) + (((vol A) / (2 |^ m)) * k2) )
by A24, A13, A14, A16, A17, FINSEQ_3:25, INTEGRA4:def 1;
A27:
m - n >= 0
by A10, XREAL_1:48;
A28:
m -' n = m - n
by A10, XREAL_1:48, XREAL_0:def 2;
( 2
|^ n >= 1 & 2
|^ m >= 1 )
by A23, NAT_1:14;
then A29:
(
(2 |^ n) -' 1
= (2 |^ n) - 1 &
(2 |^ m) -' 1
= (2 |^ m) - 1 )
by XREAL_0:def 2, XREAL_1:48;
A30:
(2 |^ (m -' n)) * ((2 |^ n) - 1) =
((2 |^ (m -' n)) * (2 |^ n)) - (2 |^ (m -' n))
.=
(2 |^ ((m -' n) + n)) - (2 |^ (m -' n))
by NEWTON:8
.=
(2 |^ m) - (2 |^ (m -' n))
by A27, NAT_D:72
;
A31:
2
|^ (m -' n) <= 2
|^ m
by PREPOWER:93, NAT_D:35;
A32:
now ( 1 <> k1 implies (EqDiv (A,(2 |^ n))) . (k1 -' 1) = (lower_bound A) + (((vol A) / (2 |^ n)) * (k1 -' 1)) )assume
1
<> k1
;
(EqDiv (A,(2 |^ n))) . (k1 -' 1) = (lower_bound A) + (((vol A) / (2 |^ n)) * (k1 -' 1))then
1
< k1
by A16, XXREAL_0:1;
then A33:
k1 -' 1
>= 1
by NAT_1:14, NAT_D:36;
k1 -' 1
<= k1
by NAT_D:35;
then
k1 -' 1
<= len Kn
by A16, XXREAL_0:2;
hence
(EqDiv (A,(2 |^ n))) . (k1 -' 1) = (lower_bound A) + (((vol A) / (2 |^ n)) * (k1 -' 1))
by A24, A25, A33, A13, FINSEQ_3:25, INTEGRA4:def 1;
verum end;
A34:
now ( 1 <> k2 implies (EqDiv (A,(2 |^ m))) . (k2 -' 1) = (lower_bound A) + (((vol A) / (2 |^ m)) * (k2 -' 1)) )assume
1
<> k2
;
(EqDiv (A,(2 |^ m))) . (k2 -' 1) = (lower_bound A) + (((vol A) / (2 |^ m)) * (k2 -' 1))then
1
< k2
by A17, XXREAL_0:1;
then A35:
k2 -' 1
>= 1
by NAT_1:14, NAT_D:36;
k2 -' 1
<= k2
by NAT_D:35;
then
k2 -' 1
<= len Km
by A17, XXREAL_0:2;
hence
(EqDiv (A,(2 |^ m))) . (k2 -' 1) = (lower_bound A) + (((vol A) / (2 |^ m)) * (k2 -' 1))
by A24, A25, A35, A14, FINSEQ_3:25, INTEGRA4:def 1;
verum end;
A36:
2
|^ (m -' n) > 0
by NEWTON:83;
(
(2 |^ n) * (2 |^ (m -' n)) = 2
|^ m &
(2 |^ n) * ((2 |^ (m -' n)) -' 1) < 2
|^ m )
by A10, Lm5;
then A37:
2
|^ n = (2 |^ m) / (2 |^ (m -' n))
by A36, XCMPLX_1:89;
A38:
(vol A) / (2 |^ n) = ((vol A) / (2 |^ m)) * (2 |^ (m -' n))
by A37, XCMPLX_1:81;
then A39:
(
((vol A) / (2 |^ n)) * k1 = ((vol A) / (2 |^ m)) * (k1 * (2 |^ (m -' n))) &
((vol A) / (2 |^ n)) * (k1 -' 1) = ((vol A) / (2 |^ m)) * ((k1 -' 1) * (2 |^ (m -' n))) )
;
divset (
(EqDiv (A,(2 |^ m))),
k2)
c= divset (
(EqDiv (A,(2 |^ n))),
k1)
proof
per cases
( len (EqDiv (A,(2 |^ m))) = 1 or len (EqDiv (A,(2 |^ m))) <> 1 )
;
suppose A40:
len (EqDiv (A,(2 |^ m))) = 1
;
divset ((EqDiv (A,(2 |^ m))),k2) c= divset ((EqDiv (A,(2 |^ n))),k1)then A41:
2
|^ n <= 1
by A10, A25, PREPOWER:93;
len (EqDiv (A,(2 |^ n))) = 1
by A25, A10, A40, PREPOWER:93, NAT_1:25;
then
len Kn = 1
by A13, FINSEQ_3:29;
then
k1 = 1
by A16, XXREAL_0:1;
then
divset (
(EqDiv (A,(2 |^ n))),
k1)
= A
by A3, A41, A25, Lm4, NAT_1:25;
hence
divset (
(EqDiv (A,(2 |^ m))),
k2)
c= divset (
(EqDiv (A,(2 |^ n))),
k1)
by A19, A14, INTEGRA1:8;
verum end; suppose A42:
len (EqDiv (A,(2 |^ m))) <> 1
;
divset ((EqDiv (A,(2 |^ m))),k2) c= divset ((EqDiv (A,(2 |^ n))),k1)per cases
( len (EqDiv (A,(2 |^ n))) = 1 or ( len (EqDiv (A,(2 |^ n))) <> 1 & k2 = 1 ) or ( len (EqDiv (A,(2 |^ n))) <> 1 & k2 = len (EqDiv (A,(2 |^ m))) ) or ( len (EqDiv (A,(2 |^ n))) <> 1 & k2 <> 1 & k2 <> len (EqDiv (A,(2 |^ m))) ) )
;
suppose A43:
len (EqDiv (A,(2 |^ n))) = 1
;
divset ((EqDiv (A,(2 |^ m))),k2) c= divset ((EqDiv (A,(2 |^ n))),k1)then
len Kn = 1
by A13, FINSEQ_3:29;
then
k1 = 1
by A16, XXREAL_0:1;
then
divset (
(EqDiv (A,(2 |^ n))),
k1)
= A
by A3, A43, Lm4;
hence
divset (
(EqDiv (A,(2 |^ m))),
k2)
c= divset (
(EqDiv (A,(2 |^ n))),
k1)
by A19, A14, INTEGRA1:8;
verum end; suppose A44:
(
len (EqDiv (A,(2 |^ n))) <> 1 &
k2 = 1 )
;
divset ((EqDiv (A,(2 |^ m))),k2) c= divset ((EqDiv (A,(2 |^ n))),k1)then
Km . k2 = [.(inf A),((EqDiv (A,(2 |^ m))) . k2).[
by A14, A19, A42;
then A45:
(
inf A <= x &
x < (EqDiv (A,(2 |^ m))) . k2 )
by A17, XXREAL_1:3;
2
|^ n divides 2
|^ m
by A10, NEWTON:89;
then
2
|^ n <= 2
|^ m
by A23, NAT_D:7;
then A46:
((vol A) / (2 |^ m)) * 1
<= ((vol A) / (2 |^ n)) * 1
by A3, A23, XREAL_1:118;
((vol A) / (2 |^ n)) * 1
<= ((vol A) / (2 |^ n)) * k1
by A16, A3, XREAL_1:64;
then
((vol A) / (2 |^ m)) * 1
<= ((vol A) / (2 |^ n)) * k1
by A46, XXREAL_0:2;
then A47:
(EqDiv (A,(2 |^ m))) . k2 <= (EqDiv (A,(2 |^ n))) . k1
by A44, A26, XREAL_1:7;
now not k1 <> 1assume A48:
k1 <> 1
;
contradictionthen
1
< k1
by A16, XXREAL_0:1;
then
k1 -' 1
>= 1
by NAT_1:14, NAT_D:36;
then
((vol A) / (2 |^ n)) * 1
<= ((vol A) / (2 |^ n)) * (k1 -' 1)
by A3, XREAL_1:64;
then
((vol A) / (2 |^ m)) * 1
<= ((vol A) / (2 |^ n)) * (k1 -' 1)
by A46, XXREAL_0:2;
then A49:
(EqDiv (A,(2 |^ m))) . k2 <= (EqDiv (A,(2 |^ n))) . (k1 -' 1)
by A44, A26, A48, A32, XREAL_1:7;
per cases
( ( 1 < k1 & k1 < len (EqDiv (A,(2 |^ n))) ) or k1 = len (EqDiv (A,(2 |^ n))) )
by A48, A16, A15, XXREAL_0:1;
suppose
k1 = len (EqDiv (A,(2 |^ n)))
;
contradictionthen
Kn . k1 = [.((EqDiv (A,(2 |^ n))) . (k1 -' 1)),((EqDiv (A,(2 |^ n))) . k1).]
by A13, A19, A44;
then
(
(EqDiv (A,(2 |^ n))) . (k1 -' 1) <= x &
x <= (EqDiv (A,(2 |^ n))) . k1 )
by A16, XXREAL_1:1;
hence
contradiction
by A45, A49, XXREAL_0:2;
verum end; end; end; then
(
lower_bound (divset ((EqDiv (A,(2 |^ n))),k1)) = lower_bound A &
upper_bound (divset ((EqDiv (A,(2 |^ n))),k1)) = (EqDiv (A,(2 |^ n))) . k1 )
by A13, A19, INTEGRA1:def 4;
then A50:
divset (
(EqDiv (A,(2 |^ n))),
k1)
= [.(lower_bound A),((EqDiv (A,(2 |^ n))) . k1).]
by INTEGRA1:4;
(
lower_bound (divset ((EqDiv (A,(2 |^ m))),k2)) = lower_bound A &
upper_bound (divset ((EqDiv (A,(2 |^ m))),k2)) = (EqDiv (A,(2 |^ m))) . k2 )
by A44, A14, A19, INTEGRA1:def 4;
then
divset (
(EqDiv (A,(2 |^ m))),
k2)
= [.(lower_bound A),((EqDiv (A,(2 |^ m))) . k2).]
by INTEGRA1:4;
hence
divset (
(EqDiv (A,(2 |^ m))),
k2)
c= divset (
(EqDiv (A,(2 |^ n))),
k1)
by A47, A50, XXREAL_1:34;
verum end; suppose A51:
(
len (EqDiv (A,(2 |^ n))) <> 1 &
k2 = len (EqDiv (A,(2 |^ m))) )
;
divset ((EqDiv (A,(2 |^ m))),k2) c= divset ((EqDiv (A,(2 |^ n))),k1)then
Km . k2 = [.((EqDiv (A,(2 |^ m))) . (k2 -' 1)),((EqDiv (A,(2 |^ m))) . k2).]
by A14, A19, A42;
then A52:
(
(lower_bound A) + (((vol A) / (2 |^ m)) * (k2 -' 1)) <= x &
x <= (lower_bound A) + (((vol A) / (2 |^ m)) * k2) )
by A26, A42, A51, A34, A17, XXREAL_1:1;
A53:
now not k1 <> len (EqDiv (A,(2 |^ n)))assume A54:
k1 <> len (EqDiv (A,(2 |^ n)))
;
contradictionper cases
( k1 = 1 or ( 1 < k1 & k1 < len (EqDiv (A,(2 |^ n))) ) )
by A15, A16, A54, XXREAL_0:1;
suppose A55:
k1 = 1
;
contradictionthen
Kn . k1 = [.(inf A),((EqDiv (A,(2 |^ n))) . 1).[
by A51, A13, A19;
then
(
inf A <= x &
x < (EqDiv (A,(2 |^ n))) . 1 )
by A16, XXREAL_1:3;
then A56:
x < (lower_bound A) + (((vol A) / (2 |^ m)) * (2 |^ (m -' n)))
by A55, A26, A37, XCMPLX_1:82;
then
2
|^ (m -' n) < 2
|^ m
by A31, XXREAL_0:1;
then
(2 |^ (m -' n)) + 1
<= 2
|^ m
by NAT_1:13;
then
2
|^ (m -' n) <= k2 -' 1
by A29, A51, A25, XREAL_1:19;
then
((vol A) / (2 |^ m)) * (2 |^ (m -' n)) <= ((vol A) / (2 |^ m)) * (k2 -' 1)
by A3, XREAL_1:64;
then
(lower_bound A) + (((vol A) / (2 |^ m)) * (2 |^ (m -' n))) <= (lower_bound A) + (((vol A) / (2 |^ m)) * (k2 -' 1))
by XREAL_1:6;
hence
contradiction
by A52, A56, XXREAL_0:2;
verum end; suppose A57:
( 1
< k1 &
k1 < len (EqDiv (A,(2 |^ n))) )
;
contradictionthen
Kn . k1 = [.((EqDiv (A,(2 |^ n))) . (k1 -' 1)),((EqDiv (A,(2 |^ n))) . k1).[
by A13, A19;
then A58:
(
(lower_bound A) + (((vol A) / (2 |^ n)) * (k1 -' 1)) <= x &
x < (lower_bound A) + (((vol A) / (2 |^ n)) * k1) )
by A26, A57, A32, A16, XXREAL_1:3;
k1 < len (EqDiv (A,(2 |^ n)))
by A54, A15, A16, XXREAL_0:1;
then
k1 + 1
<= 2
|^ n
by A25, NAT_1:13;
then
k1 <= (2 |^ n) - 1
by XREAL_1:19;
then A59:
((vol A) / (2 |^ n)) * k1 <= ((vol A) / (2 |^ n)) * ((2 |^ n) - 1)
by A3, XREAL_1:64;
(2 |^ m) - (2 |^ (m -' n)) <= k2 -' 1
by A29, A51, A25, A36, NAT_1:14, XREAL_1:10;
then
((vol A) / (2 |^ m)) * ((2 |^ (m -' n)) * ((2 |^ n) - 1)) <= ((vol A) / (2 |^ m)) * (k2 -' 1)
by A30, A3, XREAL_1:64;
then
((vol A) / (2 |^ n)) * k1 <= ((vol A) / (2 |^ m)) * (k2 -' 1)
by A38, A59, XXREAL_0:2;
then
(lower_bound A) + (((vol A) / (2 |^ n)) * k1) <= (lower_bound A) + (((vol A) / (2 |^ m)) * (k2 -' 1))
by XREAL_1:6;
hence
contradiction
by A52, A58, XXREAL_0:2;
verum end; end; end; then A60:
(
lower_bound (divset ((EqDiv (A,(2 |^ n))),k1)) = (lower_bound A) + (((vol A) / (2 |^ n)) * (k1 -' 1)) &
upper_bound (divset ((EqDiv (A,(2 |^ n))),k1)) = (lower_bound A) + (((vol A) / (2 |^ n)) * k1) )
by A26, A32, A51, A18, A19, A13, INTEGRA1:def 4;
A61:
(
lower_bound (divset ((EqDiv (A,(2 |^ m))),k2)) = (lower_bound A) + (((vol A) / (2 |^ m)) * (k2 -' 1)) &
upper_bound (divset ((EqDiv (A,(2 |^ m))),k2)) = (lower_bound A) + (((vol A) / (2 |^ m)) * k2) )
by A26, A34, A18, A51, A42, A19, A14, INTEGRA1:def 4;
(2 |^ m) - (2 |^ (m -' n)) <= (2 |^ m) - 1
by A36, NAT_1:14, XREAL_1:10;
then
((vol A) / (2 |^ m)) * ((k1 -' 1) * (2 |^ (m -' n))) <= ((vol A) / (2 |^ m)) * (k2 -' 1)
by A30, A53, A51, A25, A18, A3, XREAL_1:64;
then A62:
lower_bound (divset ((EqDiv (A,(2 |^ n))),k1)) <= lower_bound (divset ((EqDiv (A,(2 |^ m))),k2))
by A38, A60, A61, XREAL_1:6;
(
((vol A) / (2 |^ n)) * k1 = (vol A) / ((2 |^ n) / (2 |^ n)) &
((vol A) / (2 |^ m)) * k2 = (vol A) / ((2 |^ m) / (2 |^ m)) )
by A53, A51, A25, XCMPLX_1:82;
then A63:
(
((vol A) / (2 |^ n)) * k1 = vol A &
((vol A) / (2 |^ m)) * k2 = vol A )
by A23, XCMPLX_1:51;
(
divset (
(EqDiv (A,(2 |^ n))),
k1)
= [.(lower_bound (divset ((EqDiv (A,(2 |^ n))),k1))),(upper_bound (divset ((EqDiv (A,(2 |^ n))),k1))).] &
divset (
(EqDiv (A,(2 |^ m))),
k2)
= [.(lower_bound (divset ((EqDiv (A,(2 |^ m))),k2))),(upper_bound (divset ((EqDiv (A,(2 |^ m))),k2))).] )
by INTEGRA1:4;
hence
divset (
(EqDiv (A,(2 |^ m))),
k2)
c= divset (
(EqDiv (A,(2 |^ n))),
k1)
by A60, A61, A62, A63, XXREAL_1:34;
verum end; suppose A64:
(
len (EqDiv (A,(2 |^ n))) <> 1 &
k2 <> 1 &
k2 <> len (EqDiv (A,(2 |^ m))) )
;
divset ((EqDiv (A,(2 |^ m))),k2) c= divset ((EqDiv (A,(2 |^ n))),k1)then A65:
( 1
< k2 &
k2 < len (EqDiv (A,(2 |^ m))) )
by A17, A15, XXREAL_0:1;
then
Km . k2 = [.((EqDiv (A,(2 |^ m))) . (k2 -' 1)),((EqDiv (A,(2 |^ m))) . k2).[
by A14, A19;
then A66:
(
(EqDiv (A,(2 |^ m))) . (k2 -' 1) <= x &
x < (EqDiv (A,(2 |^ m))) . k2 )
by A17, XXREAL_1:3;
per cases
( k1 = 1 or ( 1 < k1 & k1 < len (EqDiv (A,(2 |^ n))) ) or k1 = len (EqDiv (A,(2 |^ n))) )
by A16, A15, XXREAL_0:1;
suppose A67:
k1 = 1
;
divset ((EqDiv (A,(2 |^ m))),k2) c= divset ((EqDiv (A,(2 |^ n))),k1)then
Kn . k1 = [.(inf A),((EqDiv (A,(2 |^ n))) . k1).[
by A64, A13, A19;
then A68:
x < (lower_bound A) + (((vol A) / (2 |^ n)) * k1)
by A26, A16, XXREAL_1:3;
then
((vol A) / (2 |^ m)) * k2 <= ((vol A) / (2 |^ n)) * k1
by A39, A3, XREAL_1:64;
then A70:
(EqDiv (A,(2 |^ m))) . k2 <= (EqDiv (A,(2 |^ n))) . k1
by A26, XREAL_1:6;
A71:
(inf A) + 0 <= (lower_bound A) + (((vol A) / (2 |^ m)) * (k2 -' 1))
by A3, XREAL_1:6;
A72:
(
lower_bound (divset ((EqDiv (A,(2 |^ n))),k1)) = lower_bound A &
upper_bound (divset ((EqDiv (A,(2 |^ n))),k1)) = (EqDiv (A,(2 |^ n))) . k1 )
by A19, A13, A67, INTEGRA1:def 4;
A73:
(
lower_bound (divset ((EqDiv (A,(2 |^ m))),k2)) = (EqDiv (A,(2 |^ m))) . (k2 -' 1) &
upper_bound (divset ((EqDiv (A,(2 |^ m))),k2)) = (EqDiv (A,(2 |^ m))) . k2 )
by A19, A14, A18, A64, INTEGRA1:def 4;
(
divset (
(EqDiv (A,(2 |^ n))),
k1)
= [.(lower_bound (divset ((EqDiv (A,(2 |^ n))),k1))),(upper_bound (divset ((EqDiv (A,(2 |^ n))),k1))).] &
divset (
(EqDiv (A,(2 |^ m))),
k2)
= [.(lower_bound (divset ((EqDiv (A,(2 |^ m))),k2))),(upper_bound (divset ((EqDiv (A,(2 |^ m))),k2))).] )
by INTEGRA1:4;
hence
divset (
(EqDiv (A,(2 |^ m))),
k2)
c= divset (
(EqDiv (A,(2 |^ n))),
k1)
by A34, A64, A70, A71, A72, A73, XXREAL_1:34;
verum end; suppose A74:
( 1
< k1 &
k1 < len (EqDiv (A,(2 |^ n))) )
;
divset ((EqDiv (A,(2 |^ m))),k2) c= divset ((EqDiv (A,(2 |^ n))),k1)then
Kn . k1 = [.((EqDiv (A,(2 |^ n))) . (k1 -' 1)),((EqDiv (A,(2 |^ n))) . k1).[
by A13, A19;
then A75:
(
(lower_bound A) + (((vol A) / (2 |^ n)) * (k1 -' 1)) <= x &
x < (lower_bound A) + (((vol A) / (2 |^ n)) * k1) )
by A74, A26, A32, A16, XXREAL_1:3;
then
((vol A) / (2 |^ m)) * k2 <= ((vol A) / (2 |^ n)) * k1
by A39, A3, XREAL_1:64;
then A76:
(EqDiv (A,(2 |^ m))) . k2 <= (EqDiv (A,(2 |^ n))) . k1
by A26, XREAL_1:6;
A77:
k2 -' 1
>= 1
by A65, NAT_D:36, NAT_1:14;
then
((vol A) / (2 |^ n)) * (k1 -' 1) <= ((vol A) / (2 |^ m)) * (k2 -' 1)
by A39, A3, XREAL_1:64;
then A78:
(EqDiv (A,(2 |^ n))) . (k1 -' 1) <= (EqDiv (A,(2 |^ m))) . (k2 -' 1)
by A32, A34, A74, A64, XREAL_1:6;
A79:
(
lower_bound (divset ((EqDiv (A,(2 |^ n))),k1)) = (EqDiv (A,(2 |^ n))) . (k1 -' 1) &
upper_bound (divset ((EqDiv (A,(2 |^ n))),k1)) = (EqDiv (A,(2 |^ n))) . k1 )
by A19, A13, A18, A74, INTEGRA1:def 4;
A80:
(
lower_bound (divset ((EqDiv (A,(2 |^ m))),k2)) = (EqDiv (A,(2 |^ m))) . (k2 -' 1) &
upper_bound (divset ((EqDiv (A,(2 |^ m))),k2)) = (EqDiv (A,(2 |^ m))) . k2 )
by A19, A14, A18, A64, INTEGRA1:def 4;
(
divset (
(EqDiv (A,(2 |^ n))),
k1)
= [.(lower_bound (divset ((EqDiv (A,(2 |^ n))),k1))),(upper_bound (divset ((EqDiv (A,(2 |^ n))),k1))).] &
divset (
(EqDiv (A,(2 |^ m))),
k2)
= [.(lower_bound (divset ((EqDiv (A,(2 |^ m))),k2))),(upper_bound (divset ((EqDiv (A,(2 |^ m))),k2))).] )
by INTEGRA1:4;
hence
divset (
(EqDiv (A,(2 |^ m))),
k2)
c= divset (
(EqDiv (A,(2 |^ n))),
k1)
by A76, A78, A79, A80, XXREAL_1:34;
verum end; suppose A81:
k1 = len (EqDiv (A,(2 |^ n)))
;
divset ((EqDiv (A,(2 |^ m))),k2) c= divset ((EqDiv (A,(2 |^ n))),k1)then
Kn . k1 = [.((EqDiv (A,(2 |^ n))) . (k1 -' 1)),((EqDiv (A,(2 |^ n))) . k1).]
by A64, A13, A19;
then A82:
(
(EqDiv (A,(2 |^ n))) . (k1 -' 1) <= x &
x <= (EqDiv (A,(2 |^ n))) . k1 )
by A16, XXREAL_1:1;
A83:
k2 -' 1
>= 1
by A65, NAT_D:36, NAT_1:14;
then
((vol A) / (2 |^ n)) * (k1 -' 1) <= ((vol A) / (2 |^ m)) * (k2 -' 1)
by A39, A3, XREAL_1:64;
then A84:
(EqDiv (A,(2 |^ n))) . (k1 -' 1) <= (EqDiv (A,(2 |^ m))) . (k2 -' 1)
by A32, A34, A81, A64, XREAL_1:6;
A85:
(
lower_bound (divset ((EqDiv (A,(2 |^ n))),k1)) = (EqDiv (A,(2 |^ n))) . (k1 -' 1) &
upper_bound (divset ((EqDiv (A,(2 |^ n))),k1)) = (EqDiv (A,(2 |^ n))) . k1 )
by A19, A13, A18, A81, A64, INTEGRA1:def 4;
A86:
(
lower_bound (divset ((EqDiv (A,(2 |^ m))),k2)) = (EqDiv (A,(2 |^ m))) . (k2 -' 1) &
upper_bound (divset ((EqDiv (A,(2 |^ m))),k2)) = (EqDiv (A,(2 |^ m))) . k2 )
by A19, A14, A18, A64, INTEGRA1:def 4;
A87:
(
divset (
(EqDiv (A,(2 |^ n))),
k1)
= [.(lower_bound (divset ((EqDiv (A,(2 |^ n))),k1))),(upper_bound (divset ((EqDiv (A,(2 |^ n))),k1))).] &
divset (
(EqDiv (A,(2 |^ m))),
k2)
= [.(lower_bound (divset ((EqDiv (A,(2 |^ m))),k2))),(upper_bound (divset ((EqDiv (A,(2 |^ m))),k2))).] )
by INTEGRA1:4;
A88:
(EqDiv (A,(2 |^ m))) . (k2 -' 1) <= (EqDiv (A,(2 |^ m))) . k2
by A66, XXREAL_0:2;
divset (
(EqDiv (A,(2 |^ m))),
k2)
c= A
by A14, A19, INTEGRA1:8;
then
divset (
(EqDiv (A,(2 |^ m))),
k2)
c= [.(lower_bound A),(upper_bound A).]
by INTEGRA1:4;
then
upper_bound (divset ((EqDiv (A,(2 |^ m))),k2)) <= upper_bound A
by A87, A88, A86, XXREAL_1:50;
then
(EqDiv (A,(2 |^ m))) . k2 <= (EqDiv (A,(2 |^ n))) . k1
by A86, A81, INTEGRA1:def 2;
hence
divset (
(EqDiv (A,(2 |^ m))),
k2)
c= divset (
(EqDiv (A,(2 |^ n))),
k1)
by A84, A85, A86, A87, XXREAL_1:34;
verum end; end; end; end; end; end;
end;
then
f | (divset ((EqDiv (A,(2 |^ m))),k2)) c= f | (divset ((EqDiv (A,(2 |^ n))),k1))
by RELAT_1:75;
hence
(F . n) . x <= (F . m) . x
by A16, A17, A21, A22, SEQ_4:47, RELAT_1:11;
verum
end;
A89:
for x being Element of REAL st x in A holds
( F # x is convergent & lim (F # x) = sup (F # x) & sup (F # x) <= f . x )
consider a, b being Real such that
A92:
a <= b
and
A93:
A = [.a,b.]
by MEASURE5:14;
reconsider a1 = a, b1 = b as R_eal by XXREAL_0:def 1;
A94:
diameter A = b1 - a1
by A92, A93, MEASURE5:6;
B-Meas . A1 = diameter A
by MEASUR12:71;
then A95:
B-Meas . A1 < +infty
by A94, XXREAL_0:4;
A96:
for x being Element of REAL st x in A1 holds
F # x is convergent
by A89;
A97:
for n being Nat holds F . n is A1 -measurable
by A8, MESFUNC2:34;
reconsider K = max (|.(lower_bound (rng f)).|,|.(upper_bound (rng f)).|) as Real ;
A98:
- |.(lower_bound (rng f)).| <= lower_bound (rng f)
by ABSVALUE:4;
- K <= - |.(lower_bound (rng f)).|
by XXREAL_0:25, XREAL_1:24;
then A99:
- K <= lower_bound (rng f)
by A98, XXREAL_0:2;
A100:
upper_bound (rng f) <= |.(upper_bound (rng f)).|
by ABSVALUE:4;
|.(upper_bound (rng f)).| <= K
by XXREAL_0:25;
then A101:
upper_bound (rng f) <= K
by A100, XXREAL_0:2;
for n being Nat
for x being set st x in dom (F . 0) holds
|.((F . n) . x).| <= K
proof
let n be
Nat;
for x being set st x in dom (F . 0) holds
|.((F . n) . x).| <= Klet x be
set ;
( x in dom (F . 0) implies |.((F . n) . x).| <= K )
assume A102:
x in dom (F . 0)
;
|.((F . n) . x).| <= K
then reconsider x0 =
x as
Real ;
n is
Element of
NAT
by ORDINAL1:def 12;
then A103:
(
lower_bound (rng f) <= (F . n) . x0 &
(F . n) . x0 <= f . x0 )
by A102, A6, A7;
A104:
rng f is
bounded_above
by A1, SEQ_2:def 8, INTEGRA1:13;
reconsider K1 =
K as
ExtReal ;
f . x0 in rng f
by A102, A2, A7, FUNCT_1:3;
then
f . x0 <= upper_bound (rng f)
by A104, SEQ_4:def 1;
then
(F . n) . x0 <= upper_bound (rng f)
by A103, XXREAL_0:2;
then
(
- K <= (F . n) . x0 &
(F . n) . x0 <= K )
by A99, A101, A103, XXREAL_0:2;
then
(
- K1 <= (F . n) . x0 &
(F . n) . x0 <= K1 )
by XXREAL_3:def 3;
hence
|.((F . n) . x).| <= K
by EXTREAL1:23;
verum
end;
then A105:
F is uniformly_bounded
by MESFUN10:def 1;
then
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (B-Meas,(F . n)) ) & I is convergent & lim I = Integral (B-Meas,(lim F)) )
by A96, A97, A95, A7, MESFUN10:19;
hence
ex I being ExtREAL_sequence st
( A = dom (F . 0) & ( for n being Nat holds
( F . n is_simple_func_in Borel_Sets & Integral (B-Meas,(F . n)) = lower_sum (f,(EqDiv (A,(2 |^ n)))) & ( for x being Real st x in A holds
( lower_bound (rng f) <= (F . n) . x & (F . n) . x <= f . x ) ) ) ) & ( for n, m being Nat st n <= m holds
for x being Element of REAL st x in A holds
(F . n) . x <= (F . m) . x ) & ( for x being Element of REAL st x in A holds
( F # x is convergent & lim (F # x) = sup (F # x) & sup (F # x) <= f . x ) ) & lim F is_integrable_on B-Meas & ( for n being Nat holds I . n = Integral (B-Meas,(F . n)) ) & I is convergent & lim I = Integral (B-Meas,(lim F)) )
by A7, A8, A9, A89, A105, A96, A97, A95, MESFUN10:19; verum