let A be non empty closed_interval Subset of REAL; for T being sequence of (divs A) st vol A > 0 & ( for n being Nat holds T . n = EqDiv (A,(2 |^ n)) ) holds
( delta T is 0 -convergent & delta T is non-zero )
let T be sequence of (divs A); ( vol A > 0 & ( for n being Nat holds T . n = EqDiv (A,(2 |^ n)) ) implies ( delta T is 0 -convergent & delta T is non-zero ) )
assume that
A1:
vol A > 0
and
A2:
for n being Nat holds T . n = EqDiv (A,(2 |^ n))
; ( delta T is 0 -convergent & delta T is non-zero )
A3:
for n being Nat holds (delta T) . n = (2 * (vol A)) * ((2 ") |^ (n + 1))
proof
let n be
Nat;
(delta T) . n = (2 * (vol A)) * ((2 ") |^ (n + 1))
n is
Element of
NAT
by ORDINAL1:def 12;
then
(delta T) . n = delta (T . n)
by INTEGRA3:def 2;
then
(delta T) . n = delta (EqDiv (A,(2 |^ n)))
by A2;
then A4:
(delta T) . n = max (rng (upper_volume ((chi (A,A)),(EqDiv (A,(2 |^ n))))))
by INTEGRA3:def 1;
A5:
for
k being
Nat st
k in dom (EqDiv (A,(2 |^ n))) holds
(upper_volume ((chi (A,A)),(EqDiv (A,(2 |^ n))))) . k = (2 * (vol A)) * ((2 ") |^ (n + 1))
proof
let k be
Nat;
( k in dom (EqDiv (A,(2 |^ n))) implies (upper_volume ((chi (A,A)),(EqDiv (A,(2 |^ n))))) . k = (2 * (vol A)) * ((2 ") |^ (n + 1)) )
assume A6:
k in dom (EqDiv (A,(2 |^ n)))
;
(upper_volume ((chi (A,A)),(EqDiv (A,(2 |^ n))))) . k = (2 * (vol A)) * ((2 ") |^ (n + 1))
2
|^ n > 0
by NEWTON:83;
then
EqDiv (
A,
(2 |^ n))
divide_into_equal 2
|^ n
by A1, Def1;
then
vol (divset ((EqDiv (A,(2 |^ n))),k)) = (vol A) / (2 |^ n)
by A6, Th15;
then (upper_volume ((chi (A,A)),(EqDiv (A,(2 |^ n))))) . k =
(vol A) / (2 |^ n)
by A6, INTEGRA1:20
.=
((vol A) / ((2 |^ n) * 2)) * 2
by XCMPLX_1:92
.=
((vol A) / (2 |^ (n + 1))) * 2
by NEWTON:6
.=
((vol A) * ((2 |^ (n + 1)) ")) * 2
by XCMPLX_0:def 9
.=
(2 * (vol A)) * ((2 |^ (n + 1)) ")
;
hence
(upper_volume ((chi (A,A)),(EqDiv (A,(2 |^ n))))) . k = (2 * (vol A)) * ((2 ") |^ (n + 1))
by Th16;
verum
end;
now for q being object st q in rng (upper_volume ((chi (A,A)),(EqDiv (A,(2 |^ n))))) holds
q in {((2 * (vol A)) * ((2 ") |^ (n + 1)))}let q be
object ;
( q in rng (upper_volume ((chi (A,A)),(EqDiv (A,(2 |^ n))))) implies q in {((2 * (vol A)) * ((2 ") |^ (n + 1)))} )assume
q in rng (upper_volume ((chi (A,A)),(EqDiv (A,(2 |^ n)))))
;
q in {((2 * (vol A)) * ((2 ") |^ (n + 1)))}then consider p being
Element of
NAT such that A7:
(
p in dom (upper_volume ((chi (A,A)),(EqDiv (A,(2 |^ n))))) &
q = (upper_volume ((chi (A,A)),(EqDiv (A,(2 |^ n))))) . p )
by PARTFUN1:3;
len (upper_volume ((chi (A,A)),(EqDiv (A,(2 |^ n))))) = len (EqDiv (A,(2 |^ n)))
by INTEGRA1:def 6;
then
dom (upper_volume ((chi (A,A)),(EqDiv (A,(2 |^ n))))) = dom (EqDiv (A,(2 |^ n)))
by FINSEQ_3:29;
then
q = (2 * (vol A)) * ((2 ") |^ (n + 1))
by A5, A7;
hence
q in {((2 * (vol A)) * ((2 ") |^ (n + 1)))}
by TARSKI:def 1;
verum end;
then
rng (upper_volume ((chi (A,A)),(EqDiv (A,(2 |^ n))))) c= {((2 * (vol A)) * ((2 ") |^ (n + 1)))}
;
then
rng (upper_volume ((chi (A,A)),(EqDiv (A,(2 |^ n))))) = {((2 * (vol A)) * ((2 ") |^ (n + 1)))}
by ZFMISC_1:33;
hence
(delta T) . n = (2 * (vol A)) * ((2 ") |^ (n + 1))
by A4, XXREAL_2:11;
verum
end;
deffunc H1( Nat) -> object = (2 ") to_power ($1 + 1);
consider seq being Real_Sequence such that
A8:
for n being Nat holds seq . n = H1(n)
from SEQ_1:sch 1();
A9:
( seq is convergent & lim seq = 0 )
by A8, SERIES_1:1;
for n being Nat holds (delta T) . n = (2 * (vol A)) * (seq . n)
then A10:
delta T = (2 * (vol A)) (#) seq
by SEQ_1:9;
then A11:
delta T is convergent
by A8, SERIES_1:1, SEQ_2:7;
A12: lim (delta T) =
(2 * (vol A)) * 0
by A9, A10, SEQ_2:8
.=
0
;
hence
( delta T is 0 -convergent & delta T is non-zero )
by A11, A12, FDIFF_1:def 1, ORDINAL1:def 15; verum