let A be closed-interval Subset of REAL ; :: thesis: for f being Function of A,REAL
for T being DivSequence of A st f | A is bounded & delta T is convergent & lim (delta T) = 0 holds
( lower_sum f,T is convergent & lim (lower_sum f,T) = lower_integral f )
let f be Function of A,REAL ; :: thesis: for T being DivSequence of A st f | A is bounded & delta T is convergent & lim (delta T) = 0 holds
( lower_sum f,T is convergent & lim (lower_sum f,T) = lower_integral f )
let T be DivSequence of A; :: thesis: ( f | A is bounded & delta T is convergent & lim (delta T) = 0 implies ( lower_sum f,T is convergent & lim (lower_sum f,T) = lower_integral f ) )
assume A1:
f | A is bounded
; :: thesis: ( not delta T is convergent or not lim (delta T) = 0 or ( lower_sum f,T is convergent & lim (lower_sum f,T) = lower_integral f ) )
assume A2:
delta T is convergent
; :: thesis: ( not lim (delta T) = 0 or ( lower_sum f,T is convergent & lim (lower_sum f,T) = lower_integral f ) )
assume A3:
lim (delta T) = 0
; :: thesis: ( lower_sum f,T is convergent & lim (lower_sum f,T) = lower_integral f )
now per cases
( vol A <> 0 or vol A = 0 )
;
suppose A4:
vol A <> 0
;
:: thesis: ( lower_sum f,T is convergent & lim (lower_sum f,T) = lower_integral f )
for
n being
Element of
NAT holds
(delta T) . n <> 0
proof
let n be
Element of
NAT ;
:: thesis: (delta T) . n <> 0
assume A5:
(delta T) . n = 0
;
:: thesis: contradiction
reconsider mm =
rng (upper_volume (chi A,A),(T . n)) as non
empty finite Subset of
REAL ;
delta (T . n) = 0
by A5, INTEGRA2:def 3;
then A6:
max mm = 0
by INTEGRA1:def 19;
reconsider D =
T . n as
Division of
A ;
A7:
for
k being
Element of
NAT st
k in dom D holds
vol (divset D,k) = 0
proof
let k be
Element of
NAT ;
:: thesis: ( k in dom D implies vol (divset D,k) = 0 )
assume
k in dom D
;
:: thesis: vol (divset D,k) = 0
then A8:
k in Seg (len D)
by FINSEQ_1:def 3;
then B8:
k in dom D
by FINSEQ_1:def 3;
k in Seg (len (upper_volume (chi A,A),D))
by A8, INTEGRA1:def 7;
then
k in dom (upper_volume (chi A,A),D)
by FINSEQ_1:def 3;
then
(upper_volume (chi A,A),D) . k in rng (upper_volume (chi A,A),D)
by FUNCT_1:def 5;
then
(upper_volume (chi A,A),D) . k <= 0
by A6, XXREAL_2:def 8;
then
vol (divset D,k) <= 0
by B8, INTEGRA1:22;
hence
vol (divset D,k) = 0
by INTEGRA1:11;
:: thesis: verum
end;
upper_volume (chi A,A),
D = (len D) |-> 0
proof
len (upper_volume (chi A,A),D) = len D
by INTEGRA1:def 7;
then A9:
len (upper_volume (chi A,A),D) = len ((len D) |-> 0 )
by FINSEQ_1:def 18;
for
j being
Nat st 1
<= j &
j <= len (upper_volume (chi A,A),D) holds
(upper_volume (chi A,A),D) . j = ((len D) |-> 0 ) . j
proof
let j be
Nat;
:: thesis: ( 1 <= j & j <= len (upper_volume (chi A,A),D) implies (upper_volume (chi A,A),D) . j = ((len D) |-> 0 ) . j )
assume
( 1
<= j &
j <= len (upper_volume (chi A,A),D) )
;
:: thesis: (upper_volume (chi A,A),D) . j = ((len D) |-> 0 ) . j
then
j in Seg (len (upper_volume (chi A,A),D))
by FINSEQ_1:3;
then A10:
j in Seg (len D)
by INTEGRA1:def 7;
then
j in dom D
by FINSEQ_1:def 3;
then A11:
(upper_volume (chi A,A),D) . j = vol (divset D,j)
by INTEGRA1:22;
j in dom D
by A10, FINSEQ_1:def 3;
then
(upper_volume (chi A,A),D) . j = 0
by A7, A11;
hence
(upper_volume (chi A,A),D) . j = ((len D) |-> 0 ) . j
by A10, FUNCOP_1:13;
:: thesis: verum
end;
hence
upper_volume (chi A,A),
D = (len D) |-> 0
by A9, FINSEQ_1:18;
:: thesis: verum
end;
then
Sum (upper_volume (chi A,A),D) = 0
by RVSUM_1:111;
hence
contradiction
by A4, INTEGRA1:26;
:: thesis: verum
end; then
delta T is
non-zero
by SEQ_1:7;
then
delta T is
convergent_to_0
by A2, A3, FDIFF_1:def 1;
hence
(
lower_sum f,
T is
convergent &
lim (lower_sum f,T) = lower_integral f )
by A1, A4, INTEGRA3:19;
:: thesis: verum suppose A12:
vol A = 0
;
:: thesis: ( lower_sum f,T is convergent & lim (lower_sum f,T) = lower_integral f )A13:
for
n being
Nat holds
(lower_sum f,T) . n = 0
proof
let n be
Nat;
:: thesis: (lower_sum f,T) . n = 0
reconsider nn =
n as
Element of
NAT by ORDINAL1:def 13;
reconsider D =
T . nn as
Division of
A ;
lower_sum f,
D = 0
proof
rng D <> {}
;
then A14:
(
len D = 1 & 1
in dom D )
by A12, Th1, FINSEQ_3:34;
then A15:
len (lower_volume f,D) = 1
by INTEGRA1:def 8;
A16:
divset D,1
= A
proof
A17:
upper_bound (divset D,(len D)) =
D . (len D)
by A14, INTEGRA1:def 5
.=
upper_bound A
by INTEGRA1:def 2
;
divset D,1 =
[.(lower_bound (divset D,(len D))),(upper_bound (divset D,(len D))).]
by A14, INTEGRA1:5
.=
[.(lower_bound A),(upper_bound A).]
by A14, A17, INTEGRA1:def 5
;
hence
divset D,1
= A
by INTEGRA1:5;
:: thesis: verum
end;
1
in Seg (len D)
by A14, FINSEQ_1:3;
then
1
in dom D
by FINSEQ_1:def 3;
then (lower_volume f,D) . 1 =
(lower_bound (rng (f | (divset D,1)))) * (vol A)
by A16, INTEGRA1:def 8
.=
0
by A12
;
then
lower_volume f,
D = <*0 *>
by A15, FINSEQ_1:57;
then
Sum (lower_volume f,D) = 0
by FINSOP_1:12;
hence
lower_sum f,
D = 0
by INTEGRA1:def 10;
:: thesis: verum
end;
hence
(lower_sum f,T) . n = 0
by INTEGRA2:def 5;
:: thesis: verum
end; then A18:
lower_sum f,
T is
constant
by VALUED_0:def 18;
hence
lower_sum f,
T is
convergent
;
:: thesis: lim (lower_sum f,T) = lower_integral f
(lower_sum f,T) . 1
= 0
by A13;
then
lim (lower_sum f,T) = 0
by A18, SEQ_4:40;
hence
lim (lower_sum f,T) = lower_integral f
by A12, Lm2;
:: thesis: verum end;
hence
( lower_sum f,T is convergent & lim (lower_sum f,T) = lower_integral f )
; :: thesis: verum