:: INTEGRA4 semantic presentation
begin
theorem Th1: :: INTEGRA4:1
for A being non empty closed_interval Subset of REAL
for D being Division of A st vol A = 0 holds
len D = 1
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for D being Division of A st vol A = 0 holds
len D = 1
let D be Division of A; ::_thesis: ( vol A = 0 implies len D = 1 )
assume that
A1: vol A = 0 and
A2: len D <> 1 ; ::_thesis: contradiction
rng D <> {} ;
then A3: 1 in dom D by FINSEQ_3:32;
then A4: 1 <= len D by FINSEQ_3:25;
then A5: len D in dom D by FINSEQ_3:25;
D . 1 in A by A3, INTEGRA1:6;
then A6: lower_bound A <= D . 1 by INTEGRA2:1;
1 < len D by A2, A4, XXREAL_0:1;
then A7: D . 1 < D . (len D) by A3, A5, SEQM_3:def_1;
(upper_bound A) - (lower_bound A) = 0 by A1, INTEGRA1:def_5;
hence contradiction by A7, A6, INTEGRA1:def_2; ::_thesis: verum
end;
theorem Th2: :: INTEGRA4:2
for A being non empty closed_interval Subset of REAL holds
( chi (A,A) is integrable & integral (chi (A,A)) = vol A )
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: ( chi (A,A) is integrable & integral (chi (A,A)) = vol A )
(divs A) /\ (dom (upper_sum_set (chi (A,A)))) = (divs A) /\ (divs A) by FUNCT_2:def_1;
then A1: divs A meets dom (upper_sum_set (chi (A,A))) by XBOOLE_0:def_7;
A2: for D1 being Element of divs A st D1 in (divs A) /\ (dom (upper_sum_set (chi (A,A)))) holds
(upper_sum_set (chi (A,A))) /. D1 = vol A
proof
let D1 be Element of divs A; ::_thesis: ( D1 in (divs A) /\ (dom (upper_sum_set (chi (A,A)))) implies (upper_sum_set (chi (A,A))) /. D1 = vol A )
reconsider D2 = D1 as Division of A by INTEGRA1:def_3;
assume D1 in (divs A) /\ (dom (upper_sum_set (chi (A,A)))) ; ::_thesis: (upper_sum_set (chi (A,A))) /. D1 = vol A
(upper_sum_set (chi (A,A))) /. D1 = (upper_sum_set (chi (A,A))) . D1
.= upper_sum ((chi (A,A)),D2) by INTEGRA1:def_10
.= Sum (upper_volume ((chi (A,A)),D2)) by INTEGRA1:def_8 ;
hence (upper_sum_set (chi (A,A))) /. D1 = vol A by INTEGRA1:24; ::_thesis: verum
end;
then (upper_sum_set (chi (A,A))) | (divs A) is constant by PARTFUN2:35;
then consider x being Element of REAL such that
A3: rng ((upper_sum_set (chi (A,A))) | (divs A)) = {x} by A1, PARTFUN2:37;
A4: chi (A,A) is upper_integrable by A3, INTEGRA1:def_12;
vol A in rng (upper_sum_set (chi (A,A)))
proof
set D1 = the Element of divs A;
the Element of divs A in divs A ;
then A5: the Element of divs A in dom (upper_sum_set (chi (A,A))) by FUNCT_2:def_1;
then A6: (upper_sum_set (chi (A,A))) . the Element of divs A in rng (upper_sum_set (chi (A,A))) by FUNCT_1:def_3;
A7: (upper_sum_set (chi (A,A))) . the Element of divs A = (upper_sum_set (chi (A,A))) /. the Element of divs A ;
the Element of divs A in (divs A) /\ (dom (upper_sum_set (chi (A,A)))) by A5, XBOOLE_0:def_4;
hence vol A in rng (upper_sum_set (chi (A,A))) by A2, A6, A7; ::_thesis: verum
end;
then A8: x = vol A by A3, TARSKI:def_1;
rng (upper_sum_set (chi (A,A))) = {x} by A3;
then lower_bound (rng (upper_sum_set (chi (A,A)))) = vol A by A8, SEQ_4:9;
then A9: upper_integral (chi (A,A)) = vol A by INTEGRA1:def_14;
(divs A) /\ (dom (lower_sum_set (chi (A,A)))) = (divs A) /\ (divs A) by FUNCT_2:def_1;
then A10: divs A meets dom (lower_sum_set (chi (A,A))) by XBOOLE_0:def_7;
A11: for D1 being Element of divs A st D1 in (divs A) /\ (dom (lower_sum_set (chi (A,A)))) holds
(lower_sum_set (chi (A,A))) /. D1 = vol A
proof
let D1 be Element of divs A; ::_thesis: ( D1 in (divs A) /\ (dom (lower_sum_set (chi (A,A)))) implies (lower_sum_set (chi (A,A))) /. D1 = vol A )
reconsider D2 = D1 as Division of A by INTEGRA1:def_3;
assume D1 in (divs A) /\ (dom (lower_sum_set (chi (A,A)))) ; ::_thesis: (lower_sum_set (chi (A,A))) /. D1 = vol A
(lower_sum_set (chi (A,A))) /. D1 = (lower_sum_set (chi (A,A))) . D1
.= lower_sum ((chi (A,A)),D2) by INTEGRA1:def_11
.= Sum (lower_volume ((chi (A,A)),D2)) by INTEGRA1:def_9 ;
hence (lower_sum_set (chi (A,A))) /. D1 = vol A by INTEGRA1:23; ::_thesis: verum
end;
then (lower_sum_set (chi (A,A))) | (divs A) is constant by PARTFUN2:35;
then consider x being Element of REAL such that
A12: rng ((lower_sum_set (chi (A,A))) | (divs A)) = {x} by A10, PARTFUN2:37;
vol A in rng (lower_sum_set (chi (A,A)))
proof
set D1 = the Element of divs A;
the Element of divs A in divs A ;
then A13: the Element of divs A in dom (lower_sum_set (chi (A,A))) by FUNCT_2:def_1;
then A14: (lower_sum_set (chi (A,A))) . the Element of divs A in rng (lower_sum_set (chi (A,A))) by FUNCT_1:def_3;
A15: (lower_sum_set (chi (A,A))) . the Element of divs A = (lower_sum_set (chi (A,A))) /. the Element of divs A ;
the Element of divs A in (divs A) /\ (dom (lower_sum_set (chi (A,A)))) by A13, XBOOLE_0:def_4;
hence vol A in rng (lower_sum_set (chi (A,A))) by A11, A14, A15; ::_thesis: verum
end;
then A16: x = vol A by A12, TARSKI:def_1;
rng (lower_sum_set (chi (A,A))) = {x} by A12;
then upper_bound (rng (lower_sum_set (chi (A,A)))) = vol A by A16, SEQ_4:9;
then A17: lower_integral (chi (A,A)) = vol A by INTEGRA1:def_15;
chi (A,A) is lower_integrable by A12, INTEGRA1:def_13;
hence ( chi (A,A) is integrable & integral (chi (A,A)) = vol A ) by A4, A9, A17, INTEGRA1:def_16, INTEGRA1:def_17; ::_thesis: verum
end;
theorem Th3: :: INTEGRA4:3
for A being non empty closed_interval Subset of REAL
for f being PartFunc of A,REAL
for r being Real holds
( ( f is total & rng f = {r} ) iff f = r (#) (chi (A,A)) )
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of A,REAL
for r being Real holds
( ( f is total & rng f = {r} ) iff f = r (#) (chi (A,A)) )
let f be PartFunc of A,REAL; ::_thesis: for r being Real holds
( ( f is total & rng f = {r} ) iff f = r (#) (chi (A,A)) )
let r be Real; ::_thesis: ( ( f is total & rng f = {r} ) iff f = r (#) (chi (A,A)) )
A1: ( f = r (#) (chi (A,A)) implies ( f is total & rng f = {r} ) )
proof
assume A2: f = r (#) (chi (A,A)) ; ::_thesis: ( f is total & rng f = {r} )
A3: chi (A,A) is total by RFUNCT_1:62;
hence f is total by A2; ::_thesis: rng f = {r}
A4: dom f = A by A2, A3, PARTFUN1:def_2;
for x being set st x in {r} holds
x in rng f
proof
let x be set ; ::_thesis: ( x in {r} implies x in rng f )
assume x in {r} ; ::_thesis: x in rng f
then A5: x = r by TARSKI:def_1;
consider a being Real such that
A6: a in dom f by A4, SUBSET_1:4;
(chi (A,A)) . a = 1 by A6, RFUNCT_1:63;
then f . a = r * 1 by A2, A6, VALUED_1:def_5;
hence x in rng f by A5, A6, FUNCT_1:def_3; ::_thesis: verum
end;
then A7: {r} c= rng f by TARSKI:def_3;
for x being set st x in rng f holds
x in {r}
proof
let x be set ; ::_thesis: ( x in rng f implies x in {r} )
assume x in rng f ; ::_thesis: x in {r}
then consider a being Element of A such that
A8: a in dom f and
A9: f . a = x by PARTFUN1:3;
(chi (A,A)) . a = 1 by RFUNCT_1:63;
then x = r * 1 by A2, A8, A9, VALUED_1:def_5
.= r ;
hence x in {r} by TARSKI:def_1; ::_thesis: verum
end;
then rng f c= {r} by TARSKI:def_3;
hence rng f = {r} by A7, XBOOLE_0:def_10; ::_thesis: verum
end;
( f is total & rng f = {r} implies f = r (#) (chi (A,A)) )
proof
reconsider g = r (#) (chi (A,A)) as PartFunc of A,REAL ;
assume A10: f is total ; ::_thesis: ( not rng f = {r} or f = r (#) (chi (A,A)) )
A11: chi (A,A) is total by RFUNCT_1:62;
A12: dom g = dom (chi (A,A)) by VALUED_1:def_5
.= A by A11, PARTFUN1:def_2 ;
assume A13: rng f = {r} ; ::_thesis: f = r (#) (chi (A,A))
A14: for x being Element of A st x in dom f holds
f /. x = g /. x
proof
let x be Element of A; ::_thesis: ( x in dom f implies f /. x = g /. x )
assume A15: x in dom f ; ::_thesis: f /. x = g /. x
then f /. x = f . x by PARTFUN1:def_6;
then A16: f /. x in rng f by A15, FUNCT_1:def_3;
g /. x = g . x by A12, PARTFUN1:def_6
.= r * ((chi (A,A)) . x) by A12, VALUED_1:def_5
.= r * 1 by RFUNCT_1:63
.= r ;
hence f /. x = g /. x by A13, A16, TARSKI:def_1; ::_thesis: verum
end;
dom f = dom g by A10, A12, PARTFUN1:def_2;
hence f = r (#) (chi (A,A)) by A14, PARTFUN2:1; ::_thesis: verum
end;
hence ( ( f is total & rng f = {r} ) iff f = r (#) (chi (A,A)) ) by A1; ::_thesis: verum
end;
theorem Th4: :: INTEGRA4:4
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for r being Real st rng f = {r} holds
( f is integrable & integral f = r * (vol A) )
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL
for r being Real st rng f = {r} holds
( f is integrable & integral f = r * (vol A) )
let f be Function of A,REAL; ::_thesis: for r being Real st rng f = {r} holds
( f is integrable & integral f = r * (vol A) )
let r be Real; ::_thesis: ( rng f = {r} implies ( f is integrable & integral f = r * (vol A) ) )
A1: chi (A,A) is Function of A,REAL by FUNCT_2:68, RFUNCT_1:62;
A2: integral (chi (A,A)) = vol A by Th2;
assume rng f = {r} ; ::_thesis: ( f is integrable & integral f = r * (vol A) )
then A3: f = r (#) (chi (A,A)) by Th3;
A4: rng (chi (A,A)) is real-bounded by INTEGRA1:17;
then A5: (chi (A,A)) | A is bounded_above by INTEGRA1:14;
A6: (chi (A,A)) | A is bounded_below by A4, INTEGRA1:12;
chi (A,A) is integrable by Th2;
hence ( f is integrable & integral f = r * (vol A) ) by A3, A2, A1, A5, A6, INTEGRA2:31; ::_thesis: verum
end;
theorem Th5: :: INTEGRA4:5
for A being non empty closed_interval Subset of REAL
for r being Real ex f being Function of A,REAL st
( rng f = {r} & f | A is bounded )
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for r being Real ex f being Function of A,REAL st
( rng f = {r} & f | A is bounded )
let r be Real; ::_thesis: ex f being Function of A,REAL st
( rng f = {r} & f | A is bounded )
r (#) (chi (A,A)) is total by Th3;
then reconsider f = r (#) (chi (A,A)) as Function of A,REAL ;
A1: rng f = {r} by Th3;
then A2: f | A is bounded_below by INTEGRA1:12;
f | A is bounded_above by A1, INTEGRA1:14;
hence ex f being Function of A,REAL st
( rng f = {r} & f | A is bounded ) by A1, A2; ::_thesis: verum
end;
Lm1: for A being non empty closed_interval Subset of REAL
for f being PartFunc of A,REAL
for D being Element of divs A st vol A = 0 holds
( f is upper_integrable & upper_integral f = 0 )
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of A,REAL
for D being Element of divs A st vol A = 0 holds
( f is upper_integrable & upper_integral f = 0 )
let f be PartFunc of A,REAL; ::_thesis: for D being Element of divs A st vol A = 0 holds
( f is upper_integrable & upper_integral f = 0 )
let D be Element of divs A; ::_thesis: ( vol A = 0 implies ( f is upper_integrable & upper_integral f = 0 ) )
(divs A) /\ (dom (upper_sum_set f)) = (divs A) /\ (divs A) by FUNCT_2:def_1;
then A1: divs A meets dom (upper_sum_set f) by XBOOLE_0:def_7;
assume A2: vol A = 0 ; ::_thesis: ( f is upper_integrable & upper_integral f = 0 )
A3: for D1 being Element of divs A st D1 in (divs A) /\ (dom (upper_sum_set f)) holds
(upper_sum_set f) /. D1 = 0
proof
let D1 be Element of divs A; ::_thesis: ( D1 in (divs A) /\ (dom (upper_sum_set f)) implies (upper_sum_set f) /. D1 = 0 )
reconsider D2 = D1 as Division of A by INTEGRA1:def_3;
A4: len (upper_volume (f,D2)) = len D2 by INTEGRA1:def_6
.= 1 by A2, Th1 ;
A5: len D2 = 1 by A2, Th1;
then 1 in Seg (len D1) by FINSEQ_1:1;
then A6: 1 in dom D1 by FINSEQ_1:def_3;
rng D2 <> {} ;
then A7: 1 in dom D2 by FINSEQ_3:32;
then A8: upper_bound (divset (D2,(len D2))) = D2 . (len D2) by A5, INTEGRA1:def_4
.= upper_bound A by INTEGRA1:def_2 ;
divset (D2,1) = [.(lower_bound (divset (D2,(len D2)))),(upper_bound (divset (D2,(len D2)))).] by A5, INTEGRA1:4
.= [.(lower_bound A),(upper_bound A).] by A5, A7, A8, INTEGRA1:def_4 ;
then divset (D2,1) = A by INTEGRA1:4;
then (upper_volume (f,D2)) . 1 = (upper_bound (rng (f | (divset (D2,1))))) * (vol A) by A6, INTEGRA1:def_6
.= 0 by A2 ;
then A9: upper_volume (f,D2) = <*0*> by A4, FINSEQ_1:40;
assume D1 in (divs A) /\ (dom (upper_sum_set f)) ; ::_thesis: (upper_sum_set f) /. D1 = 0
(upper_sum_set f) /. D1 = (upper_sum_set f) . D1
.= upper_sum (f,D2) by INTEGRA1:def_10
.= Sum (upper_volume (f,D2)) by INTEGRA1:def_8 ;
hence (upper_sum_set f) /. D1 = 0 by A9, FINSOP_1:11; ::_thesis: verum
end;
then (upper_sum_set f) | (divs A) is constant by PARTFUN2:35;
then consider x being Element of REAL such that
A10: rng ((upper_sum_set f) | (divs A)) = {x} by A1, PARTFUN2:37;
thus f is upper_integrable by A10, INTEGRA1:def_12; ::_thesis: upper_integral f = 0
0 in rng (upper_sum_set f)
proof
set D1 = the Element of divs A;
the Element of divs A in divs A ;
then A11: the Element of divs A in dom (upper_sum_set f) by FUNCT_2:def_1;
then A12: (upper_sum_set f) . the Element of divs A in rng (upper_sum_set f) by FUNCT_1:def_3;
A13: (upper_sum_set f) . the Element of divs A = (upper_sum_set f) /. the Element of divs A ;
the Element of divs A in (divs A) /\ (dom (upper_sum_set f)) by A11, XBOOLE_0:def_4;
hence 0 in rng (upper_sum_set f) by A3, A12, A13; ::_thesis: verum
end;
then A14: x = 0 by A10, TARSKI:def_1;
rng (upper_sum_set f) = {x} by A10;
then lower_bound (rng (upper_sum_set f)) = 0 by A14, SEQ_4:9;
hence upper_integral f = 0 by INTEGRA1:def_14; ::_thesis: verum
end;
Lm2: for A being non empty closed_interval Subset of REAL
for f being PartFunc of A,REAL
for D being Element of divs A st vol A = 0 holds
( f is lower_integrable & lower_integral f = 0 )
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of A,REAL
for D being Element of divs A st vol A = 0 holds
( f is lower_integrable & lower_integral f = 0 )
let f be PartFunc of A,REAL; ::_thesis: for D being Element of divs A st vol A = 0 holds
( f is lower_integrable & lower_integral f = 0 )
let D be Element of divs A; ::_thesis: ( vol A = 0 implies ( f is lower_integrable & lower_integral f = 0 ) )
(divs A) /\ (dom (lower_sum_set f)) = (divs A) /\ (divs A) by FUNCT_2:def_1;
then A1: divs A meets dom (lower_sum_set f) by XBOOLE_0:def_7;
assume A2: vol A = 0 ; ::_thesis: ( f is lower_integrable & lower_integral f = 0 )
A3: for D1 being Element of divs A st D1 in (divs A) /\ (dom (lower_sum_set f)) holds
(lower_sum_set f) /. D1 = 0
proof
let D1 be Element of divs A; ::_thesis: ( D1 in (divs A) /\ (dom (lower_sum_set f)) implies (lower_sum_set f) /. D1 = 0 )
reconsider D2 = D1 as Division of A by INTEGRA1:def_3;
A4: len (lower_volume (f,D2)) = len D2 by INTEGRA1:def_7
.= 1 by A2, Th1 ;
A5: len D2 = 1 by A2, Th1;
then 1 in Seg (len D2) by FINSEQ_1:1;
then A6: 1 in dom D2 by FINSEQ_1:def_3;
rng D2 <> {} ;
then A7: 1 in dom D2 by FINSEQ_3:32;
then A8: upper_bound (divset (D2,(len D2))) = D2 . (len D2) by A5, INTEGRA1:def_4
.= upper_bound A by INTEGRA1:def_2 ;
divset (D2,1) = [.(lower_bound (divset (D2,(len D2)))),(upper_bound (divset (D2,(len D2)))).] by A5, INTEGRA1:4
.= [.(lower_bound A),(upper_bound A).] by A5, A7, A8, INTEGRA1:def_4 ;
then divset (D2,1) = A by INTEGRA1:4;
then (lower_volume (f,D2)) . 1 = (lower_bound (rng (f | (divset (D2,1))))) * (vol A) by A6, INTEGRA1:def_7
.= 0 by A2 ;
then A9: lower_volume (f,D2) = <*0*> by A4, FINSEQ_1:40;
assume D1 in (divs A) /\ (dom (lower_sum_set f)) ; ::_thesis: (lower_sum_set f) /. D1 = 0
(lower_sum_set f) /. D1 = (lower_sum_set f) . D1
.= lower_sum (f,D2) by INTEGRA1:def_11
.= Sum (lower_volume (f,D2)) by INTEGRA1:def_9 ;
hence (lower_sum_set f) /. D1 = 0 by A9, FINSOP_1:11; ::_thesis: verum
end;
then (lower_sum_set f) | (divs A) is constant by PARTFUN2:35;
then consider x being Element of REAL such that
A10: rng ((lower_sum_set f) | (divs A)) = {x} by A1, PARTFUN2:37;
thus f is lower_integrable by A10, INTEGRA1:def_13; ::_thesis: lower_integral f = 0
0 in rng (lower_sum_set f)
proof
set D1 = the Element of divs A;
the Element of divs A in divs A ;
then A11: the Element of divs A in dom (lower_sum_set f) by FUNCT_2:def_1;
then A12: (lower_sum_set f) . the Element of divs A in rng (lower_sum_set f) by FUNCT_1:def_3;
A13: (lower_sum_set f) . the Element of divs A = (lower_sum_set f) /. the Element of divs A ;
the Element of divs A in (divs A) /\ (dom (lower_sum_set f)) by A11, XBOOLE_0:def_4;
hence 0 in rng (lower_sum_set f) by A3, A12, A13; ::_thesis: verum
end;
then A14: x = 0 by A10, TARSKI:def_1;
rng (lower_sum_set f) = {x} by A10;
then upper_bound (rng (lower_sum_set f)) = 0 by A14, SEQ_4:9;
hence lower_integral f = 0 by INTEGRA1:def_15; ::_thesis: verum
end;
theorem Th6: :: INTEGRA4:6
for A being non empty closed_interval Subset of REAL
for f being PartFunc of A,REAL
for D being Element of divs A st vol A = 0 holds
( f is integrable & integral f = 0 )
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of A,REAL
for D being Element of divs A st vol A = 0 holds
( f is integrable & integral f = 0 )
let f be PartFunc of A,REAL; ::_thesis: for D being Element of divs A st vol A = 0 holds
( f is integrable & integral f = 0 )
let D be Element of divs A; ::_thesis: ( vol A = 0 implies ( f is integrable & integral f = 0 ) )
assume A1: vol A = 0 ; ::_thesis: ( f is integrable & integral f = 0 )
then A2: upper_integral f = 0 by Lm1;
A3: lower_integral f = 0 by A1, Lm2;
A4: f is lower_integrable by A1, Lm2;
f is upper_integrable by A1, Lm1;
hence ( f is integrable & integral f = 0 ) by A2, A4, A3, INTEGRA1:def_16, INTEGRA1:def_17; ::_thesis: verum
end;
theorem :: INTEGRA4:7
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL st f | A is bounded & f is integrable holds
ex a being Real st
( lower_bound (rng f) <= a & a <= upper_bound (rng f) & integral f = a * (vol A) )
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL st f | A is bounded & f is integrable holds
ex a being Real st
( lower_bound (rng f) <= a & a <= upper_bound (rng f) & integral f = a * (vol A) )
let f be Function of A,REAL; ::_thesis: ( f | A is bounded & f is integrable implies ex a being Real st
( lower_bound (rng f) <= a & a <= upper_bound (rng f) & integral f = a * (vol A) ) )
consider g being Function of A,REAL such that
A1: rng g = {(lower_bound (rng f))} and
A2: g | A is bounded by Th5;
consider h being Function of A,REAL such that
A3: rng h = {(upper_bound (rng f))} and
A4: h | A is bounded by Th5;
A5: integral g = (lower_bound (rng f)) * (vol A) by A1, Th4;
assume A6: f | A is bounded ; ::_thesis: ( not f is integrable or ex a being Real st
( lower_bound (rng f) <= a & a <= upper_bound (rng f) & integral f = a * (vol A) ) )
A7: for x being Real st x in dom f holds
( lower_bound (rng f) <= f . x & f . x <= upper_bound (rng f) )
proof
let x be Real; ::_thesis: ( x in dom f implies ( lower_bound (rng f) <= f . x & f . x <= upper_bound (rng f) ) )
assume x in dom f ; ::_thesis: ( lower_bound (rng f) <= f . x & f . x <= upper_bound (rng f) )
then A8: f . x in rng f by FUNCT_1:def_3;
A9: rng f is bounded_below by A6, INTEGRA1:11;
rng f is bounded_above by A6, INTEGRA1:13;
hence ( lower_bound (rng f) <= f . x & f . x <= upper_bound (rng f) ) by A9, A8, SEQ_4:def_1, SEQ_4:def_2; ::_thesis: verum
end;
A10: for x being Real st x in A holds
f . x <= h . x
proof
let x be Real; ::_thesis: ( x in A implies f . x <= h . x )
assume A11: x in A ; ::_thesis: f . x <= h . x
dom h = A by FUNCT_2:def_1;
then A12: h . x in rng h by A11, FUNCT_1:def_3;
dom f = A by FUNCT_2:def_1;
then f . x <= upper_bound (rng f) by A7, A11;
hence f . x <= h . x by A3, A12, TARSKI:def_1; ::_thesis: verum
end;
A13: for x being Real st x in A holds
g . x <= f . x
proof
let x be Real; ::_thesis: ( x in A implies g . x <= f . x )
assume A14: x in A ; ::_thesis: g . x <= f . x
dom g = A by FUNCT_2:def_1;
then A15: g . x in rng g by A14, FUNCT_1:def_3;
dom f = A by FUNCT_2:def_1;
then lower_bound (rng f) <= f . x by A7, A14;
hence g . x <= f . x by A1, A15, TARSKI:def_1; ::_thesis: verum
end;
assume A16: f is integrable ; ::_thesis: ex a being Real st
( lower_bound (rng f) <= a & a <= upper_bound (rng f) & integral f = a * (vol A) )
A17: integral h = (upper_bound (rng f)) * (vol A) by A3, Th4;
A18: h is integrable by A3, Th4;
A19: g is integrable by A1, Th4;
now__::_thesis:_ex_a_being_Real_st_
(_lower_bound_(rng_f)_<=_a_&_a_<=_upper_bound_(rng_f)_&_integral_f_=_a_*_(vol_A)_)
percases ( vol A <> 0 or vol A = 0 ) ;
supposeA20: vol A <> 0 ; ::_thesis: ex a being Real st
( lower_bound (rng f) <= a & a <= upper_bound (rng f) & integral f = a * (vol A) )
reconsider a = (integral f) / (vol A) as Real ;
A21: integral f = a * (vol A) by A20, XCMPLX_1:87;
A22: vol A >= 0 by INTEGRA1:9;
then A23: (integral f) / (vol A) <= upper_bound (rng f) by A6, A16, A4, A18, A17, A10, A20, INTEGRA2:34, XREAL_1:79;
lower_bound (rng f) <= (integral f) / (vol A) by A6, A16, A2, A19, A5, A13, A20, A22, INTEGRA2:34, XREAL_1:77;
hence ex a being Real st
( lower_bound (rng f) <= a & a <= upper_bound (rng f) & integral f = a * (vol A) ) by A23, A21; ::_thesis: verum
end;
supposeA24: vol A = 0 ; ::_thesis: ex a being Real st
( lower_bound (rng f) <= a & a <= upper_bound (rng f) & integral f = a * (vol A) )
A25: lower_bound (rng f) <= upper_bound (rng f)
proof
dom f = A by FUNCT_2:def_1;
then consider x being Real such that
A26: x in dom f by SUBSET_1:4;
A27: f . x <= upper_bound (rng f) by A7, A26;
lower_bound (rng f) <= f . x by A7, A26;
hence lower_bound (rng f) <= upper_bound (rng f) by A27, XXREAL_0:2; ::_thesis: verum
end;
integral f = (lower_bound (rng f)) * (vol A) by A24, Th6;
hence ex a being Real st
( lower_bound (rng f) <= a & a <= upper_bound (rng f) & integral f = a * (vol A) ) by A25; ::_thesis: verum
end;
end;
end;
hence ex a being Real st
( lower_bound (rng f) <= a & a <= upper_bound (rng f) & integral f = a * (vol A) ) ; ::_thesis: verum
end;
begin
theorem Th8: :: INTEGRA4:8
for A being non empty closed_interval Subset of REAL
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 )
proof
let A be non empty 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__::_thesis:_(_lower_sum_(f,T)_is_convergent_&_lim_(lower_sum_(f,T))_=_lower_integral_f_)
percases ( vol A <> 0 or vol A = 0 ) ;
supposeA4: 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
reconsider mm = rng (upper_volume ((chi (A,A)),(T . n))) as non empty finite Subset of REAL ;
reconsider D = T . n as Division of A ;
assume (delta T) . n = 0 ; ::_thesis: contradiction
then delta (T . n) = 0 by INTEGRA3:def_2;
then A5: max mm = 0 by INTEGRA3:def_1;
A6: 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 A7: k in dom D ; ::_thesis: vol (divset (D,k)) = 0
then k in Seg (len D) by FINSEQ_1:def_3;
then k in Seg (len (upper_volume ((chi (A,A)),D))) by INTEGRA1:def_6;
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_3;
then (upper_volume ((chi (A,A)),D)) . k <= 0 by A5, XXREAL_2:def_8;
then vol (divset (D,k)) <= 0 by A7, INTEGRA1:20;
hence vol (divset (D,k)) = 0 by INTEGRA1:9; ::_thesis: verum
end;
A8: 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 that
A9: 1 <= j and
A10: j <= len (upper_volume ((chi (A,A)),D)) ; ::_thesis: (upper_volume ((chi (A,A)),D)) . j = ((len D) |-> 0) . j
j in Seg (len (upper_volume ((chi (A,A)),D))) by A9, A10, FINSEQ_1:1;
then A11: j in Seg (len D) by INTEGRA1:def_6;
then j in dom D by FINSEQ_1:def_3;
then A12: (upper_volume ((chi (A,A)),D)) . j = vol (divset (D,j)) by INTEGRA1:20;
j in dom D by A11, FINSEQ_1:def_3;
then (upper_volume ((chi (A,A)),D)) . j = 0 by A6, A12;
hence (upper_volume ((chi (A,A)),D)) . j = ((len D) |-> 0) . j by A11, FUNCOP_1:7; ::_thesis: verum
end;
len (upper_volume ((chi (A,A)),D)) = len D by INTEGRA1:def_6;
then len (upper_volume ((chi (A,A)),D)) = len ((len D) |-> 0) by CARD_1:def_7;
then upper_volume ((chi (A,A)),D) = (len D) |-> 0 by A8, FINSEQ_1:14;
then Sum (upper_volume ((chi (A,A)),D)) = 0 by RVSUM_1:81;
hence contradiction by A4, INTEGRA1:24; ::_thesis: verum
end;
then delta T is non-zero by SEQ_1:5;
then ( delta T is 0 -convergent & delta T is non-zero ) 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:20; ::_thesis: verum
end;
supposeA13: vol A = 0 ; ::_thesis: ( lower_sum (f,T) is convergent & lim (lower_sum (f,T)) = lower_integral f )
A14: 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_12;
reconsider D = T . nn as Division of A ;
A15: len D = 1 by A13, Th1;
then A16: len (lower_volume (f,D)) = 1 by INTEGRA1:def_7;
rng D <> {} ;
then A17: 1 in dom D by FINSEQ_3:32;
then A18: upper_bound (divset (D,(len D))) = D . (len D) by A15, INTEGRA1:def_4
.= upper_bound A by INTEGRA1:def_2 ;
1 in Seg (len D) by A15, FINSEQ_1:1;
then A19: 1 in dom D by FINSEQ_1:def_3;
divset (D,1) = [.(lower_bound (divset (D,(len D)))),(upper_bound (divset (D,(len D)))).] by A15, INTEGRA1:4
.= [.(lower_bound A),(upper_bound A).] by A15, A17, A18, INTEGRA1:def_4 ;
then divset (D,1) = A by INTEGRA1:4;
then (lower_volume (f,D)) . 1 = (lower_bound (rng (f | (divset (D,1))))) * (vol A) by A19, INTEGRA1:def_7
.= 0 by A13 ;
then lower_volume (f,D) = <*0*> by A16, FINSEQ_1:40;
then Sum (lower_volume (f,D)) = 0 by FINSOP_1:11;
then lower_sum (f,D) = 0 by INTEGRA1:def_9;
hence (lower_sum (f,T)) . n = 0 by INTEGRA2:def_3; ::_thesis: verum
end;
then A20: 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 A14;
then lim (lower_sum (f,T)) = 0 by A20, SEQ_4:25;
hence lim (lower_sum (f,T)) = lower_integral f by A13, Lm2; ::_thesis: verum
end;
end;
end;
hence ( lower_sum (f,T) is convergent & lim (lower_sum (f,T)) = lower_integral f ) ; ::_thesis: verum
end;
theorem Th9: :: INTEGRA4:9
for A being non empty closed_interval Subset of REAL
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
( upper_sum (f,T) is convergent & lim (upper_sum (f,T)) = upper_integral f )
proof
let A be non empty 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
( upper_sum (f,T) is convergent & lim (upper_sum (f,T)) = upper_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
( upper_sum (f,T) is convergent & lim (upper_sum (f,T)) = upper_integral f )
let T be DivSequence of A; ::_thesis: ( f | A is bounded & delta T is convergent & lim (delta T) = 0 implies ( upper_sum (f,T) is convergent & lim (upper_sum (f,T)) = upper_integral f ) )
assume A1: f | A is bounded ; ::_thesis: ( not delta T is convergent or not lim (delta T) = 0 or ( upper_sum (f,T) is convergent & lim (upper_sum (f,T)) = upper_integral f ) )
assume A2: delta T is convergent ; ::_thesis: ( not lim (delta T) = 0 or ( upper_sum (f,T) is convergent & lim (upper_sum (f,T)) = upper_integral f ) )
assume A3: lim (delta T) = 0 ; ::_thesis: ( upper_sum (f,T) is convergent & lim (upper_sum (f,T)) = upper_integral f )
now__::_thesis:_(_upper_sum_(f,T)_is_convergent_&_lim_(upper_sum_(f,T))_=_upper_integral_f_)
percases ( vol A <> 0 or vol A = 0 ) ;
supposeA4: vol A <> 0 ; ::_thesis: ( upper_sum (f,T) is convergent & lim (upper_sum (f,T)) = upper_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
reconsider D = T . n as Division of A ;
assume (delta T) . n = 0 ; ::_thesis: contradiction
then delta (T . n) = 0 by INTEGRA3:def_2;
then A5: max (rng (upper_volume ((chi (A,A)),(T . n)))) = 0 by INTEGRA3:def_1;
A6: 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 A7: k in dom D ; ::_thesis: vol (divset (D,k)) = 0
then k in Seg (len D) by FINSEQ_1:def_3;
then k in Seg (len (upper_volume ((chi (A,A)),D))) by INTEGRA1:def_6;
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_3;
then (upper_volume ((chi (A,A)),D)) . k <= 0 by A5, XXREAL_2:def_8;
then vol (divset (D,k)) <= 0 by A7, INTEGRA1:20;
hence vol (divset (D,k)) = 0 by INTEGRA1:9; ::_thesis: verum
end;
A8: 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 that
A9: 1 <= j and
A10: j <= len (upper_volume ((chi (A,A)),D)) ; ::_thesis: (upper_volume ((chi (A,A)),D)) . j = ((len D) |-> 0) . j
j in Seg (len (upper_volume ((chi (A,A)),D))) by A9, A10, FINSEQ_1:1;
then A11: j in Seg (len D) by INTEGRA1:def_6;
then j in dom D by FINSEQ_1:def_3;
then A12: (upper_volume ((chi (A,A)),D)) . j = vol (divset (D,j)) by INTEGRA1:20;
j in dom D by A11, FINSEQ_1:def_3;
then (upper_volume ((chi (A,A)),D)) . j = 0 by A6, A12;
hence (upper_volume ((chi (A,A)),D)) . j = ((len D) |-> 0) . j by A11, FUNCOP_1:7; ::_thesis: verum
end;
len (upper_volume ((chi (A,A)),D)) = len D by INTEGRA1:def_6;
then len (upper_volume ((chi (A,A)),D)) = len ((len D) |-> 0) by CARD_1:def_7;
then upper_volume ((chi (A,A)),D) = (len D) |-> 0 by A8, FINSEQ_1:14;
then Sum (upper_volume ((chi (A,A)),D)) = 0 by RVSUM_1:81;
hence contradiction by A4, INTEGRA1:24; ::_thesis: verum
end;
then delta T is non-zero by SEQ_1:5;
then ( delta T is 0 -convergent & delta T is non-zero ) by A2, A3, FDIFF_1:def_1;
hence ( upper_sum (f,T) is convergent & lim (upper_sum (f,T)) = upper_integral f ) by A1, A4, INTEGRA3:21; ::_thesis: verum
end;
supposeA13: vol A = 0 ; ::_thesis: ( upper_sum (f,T) is convergent & lim (upper_sum (f,T)) = upper_integral f )
A14: for n being Nat holds (upper_sum (f,T)) . n = 0
proof
let n be Nat; ::_thesis: (upper_sum (f,T)) . n = 0
reconsider nn = n as Element of NAT by ORDINAL1:def_12;
reconsider D = T . nn as Division of A ;
A15: len D = 1 by A13, Th1;
then A16: len (upper_volume (f,D)) = 1 by INTEGRA1:def_6;
rng D <> {} ;
then A17: 1 in dom D by FINSEQ_3:32;
then A18: upper_bound (divset (D,(len D))) = D . (len D) by A15, INTEGRA1:def_4
.= upper_bound A by INTEGRA1:def_2 ;
1 in Seg (len D) by A15, FINSEQ_1:1;
then A19: 1 in dom D by FINSEQ_1:def_3;
divset (D,1) = [.(lower_bound (divset (D,(len D)))),(upper_bound (divset (D,(len D)))).] by A15, INTEGRA1:4
.= [.(lower_bound A),(upper_bound A).] by A15, A17, A18, INTEGRA1:def_4 ;
then divset (D,1) = A by INTEGRA1:4;
then (upper_volume (f,D)) . 1 = (upper_bound (rng (f | (divset (D,1))))) * (vol A) by A19, INTEGRA1:def_6
.= 0 by A13 ;
then upper_volume (f,D) = <*0*> by A16, FINSEQ_1:40;
then Sum (upper_volume (f,D)) = 0 by FINSOP_1:11;
then upper_sum (f,D) = 0 by INTEGRA1:def_8;
hence (upper_sum (f,T)) . n = 0 by INTEGRA2:def_2; ::_thesis: verum
end;
then A20: upper_sum (f,T) is constant by VALUED_0:def_18;
hence upper_sum (f,T) is convergent ; ::_thesis: lim (upper_sum (f,T)) = upper_integral f
(upper_sum (f,T)) . 1 = 0 by A14;
then lim (upper_sum (f,T)) = 0 by A20, SEQ_4:25;
hence lim (upper_sum (f,T)) = upper_integral f by A13, Lm1; ::_thesis: verum
end;
end;
end;
hence ( upper_sum (f,T) is convergent & lim (upper_sum (f,T)) = upper_integral f ) ; ::_thesis: verum
end;
theorem Th10: :: INTEGRA4:10
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL st f | A is bounded holds
( f is upper_integrable & f is lower_integrable )
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL st f | A is bounded holds
( f is upper_integrable & f is lower_integrable )
let f be Function of A,REAL; ::_thesis: ( f | A is bounded implies ( f is upper_integrable & f is lower_integrable ) )
assume A1: f | A is bounded ; ::_thesis: ( f is upper_integrable & f is lower_integrable )
(lower_bound (rng f)) * (vol A) is LowerBound of rng (upper_sum_set f)
proof
let r be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not r in rng (upper_sum_set f) or (lower_bound (rng f)) * (vol A) <= r )
assume r in rng (upper_sum_set f) ; ::_thesis: (lower_bound (rng f)) * (vol A) <= r
then consider D being Element of divs A such that
D in dom (upper_sum_set f) and
A2: (upper_sum_set f) . D = r by PARTFUN1:3;
reconsider D = D as Division of A by INTEGRA1:def_3;
r = upper_sum (f,D) by A2, INTEGRA1:def_10;
then A3: lower_sum (f,D) <= r by A1, INTEGRA1:28;
(lower_bound (rng f)) * (vol A) <= lower_sum (f,D) by A1, INTEGRA1:25;
hence (lower_bound (rng f)) * (vol A) <= r by A3, XXREAL_0:2; ::_thesis: verum
end;
then rng (upper_sum_set f) is bounded_below by XXREAL_2:def_9;
hence f is upper_integrable by INTEGRA1:def_12; ::_thesis: f is lower_integrable
(upper_bound (rng f)) * (vol A) is UpperBound of rng (lower_sum_set f)
proof
let r be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not r in rng (lower_sum_set f) or r <= (upper_bound (rng f)) * (vol A) )
assume r in rng (lower_sum_set f) ; ::_thesis: r <= (upper_bound (rng f)) * (vol A)
then consider D being Element of divs A such that
D in dom (lower_sum_set f) and
A4: (lower_sum_set f) . D = r by PARTFUN1:3;
reconsider D = D as Division of A by INTEGRA1:def_3;
r = lower_sum (f,D) by A4, INTEGRA1:def_11;
then A5: upper_sum (f,D) >= r by A1, INTEGRA1:28;
(upper_bound (rng f)) * (vol A) >= upper_sum (f,D) by A1, INTEGRA1:27;
hence r <= (upper_bound (rng f)) * (vol A) by A5, XXREAL_0:2; ::_thesis: verum
end;
then rng (lower_sum_set f) is bounded_above by XXREAL_2:def_10;
hence f is lower_integrable by INTEGRA1:def_13; ::_thesis: verum
end;
definition
let A be non empty closed_interval Subset of REAL;
let IT be Division of A;
let n be Element of NAT ;
predIT divide_into_equal n means :Def1: :: INTEGRA4:def 1
( len IT = n & ( for i being Element of NAT st i in dom IT holds
IT . i = (lower_bound A) + (((vol A) / (len IT)) * i) ) );
end;
:: deftheorem Def1 defines divide_into_equal INTEGRA4:def_1_:_
for A being non empty closed_interval Subset of REAL
for IT being Division of A
for n being Element of NAT holds
( IT divide_into_equal n iff ( len IT = n & ( for i being Element of NAT st i in dom IT holds
IT . i = (lower_bound A) + (((vol A) / (len IT)) * i) ) ) );
Lm3: for A being non empty closed_interval Subset of REAL
for n being Element of NAT st n > 0 & vol A > 0 holds
ex D being Division of A st
( len D = n & ( for i being Element of NAT st i in dom D holds
D . i = (lower_bound A) + (((vol A) / n) * i) ) )
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for n being Element of NAT st n > 0 & vol A > 0 holds
ex D being Division of A st
( len D = n & ( for i being Element of NAT st i in dom D holds
D . i = (lower_bound A) + (((vol A) / n) * i) ) )
let n be Element of NAT ; ::_thesis: ( n > 0 & vol A > 0 implies ex D being Division of A st
( len D = n & ( for i being Element of NAT st i in dom D holds
D . i = (lower_bound A) + (((vol A) / n) * i) ) ) )
assume that
A1: n > 0 and
A2: vol A > 0 ; ::_thesis: ex D being Division of A st
( len D = n & ( for i being Element of NAT st i in dom D holds
D . i = (lower_bound A) + (((vol A) / n) * i) ) )
deffunc H1( Nat) -> Element of REAL = (lower_bound A) + (((vol A) / n) * $1);
consider D being FinSequence of REAL such that
A3: ( len D = n & ( for i being Nat st i in dom D holds
D . i = H1(i) ) ) from FINSEQ_2:sch_1();
A4: for i, j being Element of NAT st i in dom D & j in dom D & i < j holds
D . i < D . j
proof
let i, j be Element of NAT ; ::_thesis: ( i in dom D & j in dom D & i < j implies D . i < D . j )
assume that
A5: i in dom D and
A6: j in dom D and
A7: i < j ; ::_thesis: D . i < D . j
(vol A) / n > 0 by A1, A2, XREAL_1:139;
then ((vol A) / n) * i < ((vol A) / n) * j by A7, XREAL_1:68;
then (lower_bound A) + (((vol A) / n) * i) < (lower_bound A) + (((vol A) / n) * j) by XREAL_1:6;
then D . i < (lower_bound A) + (((vol A) / n) * j) by A3, A5;
hence D . i < D . j by A3, A6; ::_thesis: verum
end;
A8: dom D = Seg n by A3, FINSEQ_1:def_3;
reconsider D = D as non empty increasing FinSequence of REAL by A1, A3, A4, SEQM_3:def_1;
D . (len D) = (lower_bound A) + (((vol A) / n) * n) by A3, A8, FINSEQ_1:3;
then A9: D . (len D) = (lower_bound A) + (vol A) by A1, XCMPLX_1:87;
for x1 being set st x1 in rng D holds
x1 in A
proof
let x1 be set ; ::_thesis: ( x1 in rng D implies x1 in A )
A10: (lower_bound A) + (vol A) = (lower_bound A) + ((upper_bound A) - (lower_bound A)) by INTEGRA1:def_5
.= upper_bound A ;
assume A11: x1 in rng D ; ::_thesis: x1 in A
then reconsider x1 = x1 as Real ;
consider i being Element of NAT such that
A12: i in dom D and
A13: D . i = x1 by A11, PARTFUN1:3;
A14: 1 <= i by A12, FINSEQ_3:25;
i <= len D by A12, FINSEQ_3:25;
then ((vol A) / n) * i <= ((vol A) / n) * n by A2, A3, XREAL_1:64;
then ((vol A) / n) * i <= vol A by A1, XCMPLX_1:87;
then A15: (lower_bound A) + (((vol A) / n) * i) <= (lower_bound A) + (vol A) by XREAL_1:6;
(vol A) / n > 0 by A1, A2, XREAL_1:139;
then A16: lower_bound A <= (lower_bound A) + (((vol A) / n) * i) by A14, XREAL_1:29, XREAL_1:129;
x1 = (lower_bound A) + (((vol A) / n) * i) by A3, A12, A13;
hence x1 in A by A16, A15, A10, INTEGRA2:1; ::_thesis: verum
end;
then A17: rng D c= A by TARSKI:def_3;
vol A = (upper_bound A) - (lower_bound A) by INTEGRA1:def_5;
then reconsider D = D as Division of A by A17, A9, INTEGRA1:def_2;
take D ; ::_thesis: ( len D = n & ( for i being Element of NAT st i in dom D holds
D . i = (lower_bound A) + (((vol A) / n) * i) ) )
thus ( len D = n & ( for i being Element of NAT st i in dom D holds
D . i = (lower_bound A) + (((vol A) / n) * i) ) ) by A3; ::_thesis: verum
end;
Lm4: for A being non empty closed_interval Subset of REAL st vol A > 0 holds
ex T being DivSequence of A st
( delta T is convergent & lim (delta T) = 0 )
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: ( vol A > 0 implies ex T being DivSequence of A st
( delta T is convergent & lim (delta T) = 0 ) )
defpred S1[ set , set ] means ex n being Element of NAT ex e being Division of A st
( n = $1 & e = $2 & e divide_into_equal n + 1 );
assume A1: vol A > 0 ; ::_thesis: ex T being DivSequence of A st
( delta T is convergent & lim (delta T) = 0 )
A2: for n being Element of NAT ex D being Element of divs A st S1[n,D]
proof
let n be Element of NAT ; ::_thesis: ex D being Element of divs A st S1[n,D]
consider D being Division of A such that
A3: len D = n + 1 and
A4: for i being Element of NAT st i in dom D holds
D . i = (lower_bound A) + (((vol A) / (n + 1)) * i) by A1, Lm3;
A5: D is Element of divs A by INTEGRA1:def_3;
D divide_into_equal n + 1 by A3, A4, Def1;
hence ex D being Element of divs A st S1[n,D] by A5; ::_thesis: verum
end;
consider T being Function of NAT,(divs A) such that
A6: for n being Element of NAT holds S1[n,T . n] from FUNCT_2:sch_3(A2);
reconsider T = T as DivSequence of A ;
A7: for i being Element of NAT holds (delta T) . i = (vol A) / (i + 1)
proof
let i be Element of NAT ; ::_thesis: (delta T) . i = (vol A) / (i + 1)
(delta T) . i = delta (T . i) by INTEGRA3:def_2;
then A8: (delta T) . i = max (rng (upper_volume ((chi (A,A)),(T . i)))) by INTEGRA3:def_1;
for x1 being set st x1 in rng (upper_volume ((chi (A,A)),(T . i))) holds
x1 in {((vol A) / (i + 1))}
proof
reconsider D = T . i as Division of A ;
let x1 be set ; ::_thesis: ( x1 in rng (upper_volume ((chi (A,A)),(T . i))) implies x1 in {((vol A) / (i + 1))} )
assume x1 in rng (upper_volume ((chi (A,A)),(T . i))) ; ::_thesis: x1 in {((vol A) / (i + 1))}
then consider k being Element of NAT such that
A9: k in dom (upper_volume ((chi (A,A)),(T . i))) and
A10: (upper_volume ((chi (A,A)),(T . i))) . k = x1 by PARTFUN1:3;
A11: ex n being Element of NAT ex e being Division of A st
( n = i & e = D & e divide_into_equal n + 1 ) by A6;
k in Seg (len (upper_volume ((chi (A,A)),(T . i)))) by A9, FINSEQ_1:def_3;
then A12: k in Seg (len D) by INTEGRA1:def_6;
A13: (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) = (vol A) / (i + 1)
proof
A14: 1 <= k by A9, FINSEQ_3:25;
now__::_thesis:_(upper_bound_(divset_(D,k)))_-_(lower_bound_(divset_(D,k)))_=_(vol_A)_/_(i_+_1)
percases ( k = 1 or k > 1 ) by A14, XXREAL_0:1;
supposeA15: k = 1 ; ::_thesis: (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) = (vol A) / (i + 1)
A16: len D = i + 1 by A11, Def1;
A17: 1 in dom D by A12, A15, FINSEQ_1:def_3;
then upper_bound (divset (D,k)) = D . 1 by A15, INTEGRA1:def_4;
then upper_bound (divset (D,k)) = (lower_bound A) + (((vol A) / (i + 1)) * 1) by A11, A17, A16, Def1;
then (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) = ((lower_bound A) + ((vol A) / (i + 1))) - (lower_bound A) by A15, A17, INTEGRA1:def_4
.= ((vol A) / (i + 1)) - ((lower_bound A) - (lower_bound A)) ;
hence (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) = (vol A) / (i + 1) ; ::_thesis: verum
end;
supposeA18: k > 1 ; ::_thesis: (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) = (vol A) / (i + 1)
A19: k in dom D by A12, FINSEQ_1:def_3;
then A20: lower_bound (divset (D,k)) = D . (k - 1) by A18, INTEGRA1:def_4;
k - 1 in dom D by A18, A19, INTEGRA1:7;
then A21: D . (k - 1) = (lower_bound A) + (((vol A) / (len D)) * (k - 1)) by A11, Def1;
A22: upper_bound (divset (D,k)) = D . k by A18, A19, INTEGRA1:def_4;
D . k = (lower_bound A) + (((vol A) / (len D)) * k) by A11, A19, Def1;
hence (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) = (vol A) / (i + 1) by A11, A20, A22, A21, Def1; ::_thesis: verum
end;
end;
end;
hence (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) = (vol A) / (i + 1) ; ::_thesis: verum
end;
k in dom D by A12, FINSEQ_1:def_3;
then x1 = vol (divset (D,k)) by A10, INTEGRA1:20;
then x1 = (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) by INTEGRA1:def_5;
hence x1 in {((vol A) / (i + 1))} by A13, TARSKI:def_1; ::_thesis: verum
end;
then A23: rng (upper_volume ((chi (A,A)),(T . i))) c= {((vol A) / (i + 1))} by TARSKI:def_3;
for x1 being set st x1 in {((vol A) / (i + 1))} holds
x1 in rng (upper_volume ((chi (A,A)),(T . i)))
proof
reconsider D = T . i as Division of A ;
let x1 be set ; ::_thesis: ( x1 in {((vol A) / (i + 1))} implies x1 in rng (upper_volume ((chi (A,A)),(T . i))) )
A24: vol (divset (D,1)) = (upper_bound (divset (D,1))) - (lower_bound (divset (D,1))) by INTEGRA1:def_5;
A25: ex n being Element of NAT ex e being Division of A st
( n = i & e = D & e divide_into_equal n + 1 ) by A6;
rng D <> {} ;
then A26: 1 in dom D by FINSEQ_3:32;
then upper_bound (divset (D,1)) = D . 1 by INTEGRA1:def_4;
then upper_bound (divset (D,1)) = (lower_bound A) + (((vol A) / (len D)) * 1) by A26, A25, Def1;
then A27: vol (divset (D,1)) = ((lower_bound A) + ((vol A) / (len D))) - (lower_bound A) by A26, A24, INTEGRA1:def_4
.= (vol A) / (len D) ;
assume x1 in {((vol A) / (i + 1))} ; ::_thesis: x1 in rng (upper_volume ((chi (A,A)),(T . i)))
then A28: x1 = (vol A) / (i + 1) by TARSKI:def_1;
1 in Seg (len D) by A26, FINSEQ_1:def_3;
then 1 in Seg (len (upper_volume ((chi (A,A)),D))) by INTEGRA1:def_6;
then 1 in dom (upper_volume ((chi (A,A)),D)) by FINSEQ_1:def_3;
then A29: (upper_volume ((chi (A,A)),D)) . 1 in rng (upper_volume ((chi (A,A)),D)) by FUNCT_1:def_3;
(upper_volume ((chi (A,A)),D)) . 1 = vol (divset (D,1)) by A26, INTEGRA1:20;
hence x1 in rng (upper_volume ((chi (A,A)),(T . i))) by A28, A29, A25, A27, Def1; ::_thesis: verum
end;
then {((vol A) / (i + 1))} c= rng (upper_volume ((chi (A,A)),(T . i))) by TARSKI:def_3;
then rng (upper_volume ((chi (A,A)),(T . i))) = {((vol A) / (i + 1))} by A23, XBOOLE_0:def_10;
then (delta T) . i in {((vol A) / (i + 1))} by A8, XXREAL_2:def_8;
hence (delta T) . i = (vol A) / (i + 1) by TARSKI:def_1; ::_thesis: verum
end;
A30: for a being Real st 0 < a holds
ex i being Element of NAT st abs (((delta T) . i) - 0) < a
proof
let a be Real; ::_thesis: ( 0 < a implies ex i being Element of NAT st abs (((delta T) . i) - 0) < a )
A31: vol A >= 0 by INTEGRA1:9;
reconsider i1 = [\((vol A) / a)/] + 1 as Integer ;
assume A32: 0 < a ; ::_thesis: ex i being Element of NAT st abs (((delta T) . i) - 0) < a
then [\((vol A) / a)/] + 1 > 0 by A31, INT_1:29;
then reconsider i1 = i1 as Element of NAT by INT_1:3;
i1 < i1 + 1 by NAT_1:13;
then (vol A) / a < 1 * (i1 + 1) by INT_1:29, XXREAL_0:2;
then A33: (vol A) / (i1 + 1) < 1 * a by A32, XREAL_1:113;
A34: (delta T) . i1 = (vol A) / (i1 + 1) by A7;
((vol A) / (i1 + 1)) - 0 = abs (((vol A) / (i1 + 1)) - 0) by A31, ABSVALUE:def_1;
hence ex i being Element of NAT st abs (((delta T) . i) - 0) < a by A33, A34; ::_thesis: verum
end;
A35: for i being Element of NAT holds (delta T) . i >= 0
proof
let i be Element of NAT ; ::_thesis: (delta T) . i >= 0
(delta T) . i = delta (T . i) by INTEGRA3:def_2;
hence (delta T) . i >= 0 by INTEGRA3:9; ::_thesis: verum
end;
A36: for i, j being Element of NAT st i <= j holds
(delta T) . i >= (delta T) . j
proof
let i, j be Element of NAT ; ::_thesis: ( i <= j implies (delta T) . i >= (delta T) . j )
assume i <= j ; ::_thesis: (delta T) . i >= (delta T) . j
then A37: i + 1 <= j + 1 by XREAL_1:6;
vol A >= 0 by INTEGRA1:9;
then (vol A) / (i + 1) >= (vol A) / (j + 1) by A37, XREAL_1:118;
then (delta T) . i >= (vol A) / (j + 1) by A7;
hence (delta T) . i >= (delta T) . j by A7; ::_thesis: verum
end;
A38: for a being real number st 0 < a holds
ex i being Element of NAT st
for j being Element of NAT st i <= j holds
abs (((delta T) . j) - 0) < a
proof
let a be real number ; ::_thesis: ( 0 < a implies ex i being Element of NAT st
for j being Element of NAT st i <= j holds
abs (((delta T) . j) - 0) < a )
assume A39: 0 < a ; ::_thesis: ex i being Element of NAT st
for j being Element of NAT st i <= j holds
abs (((delta T) . j) - 0) < a
a is Real by XREAL_0:def_1;
then consider i being Element of NAT such that
A40: abs (((delta T) . i) - 0) < a by A30, A39;
(delta T) . i >= 0 by A35;
then A41: (delta T) . i < a by A40, ABSVALUE:def_1;
for j being Element of NAT st i <= j holds
abs (((delta T) . j) - 0) < a
proof
let j be Element of NAT ; ::_thesis: ( i <= j implies abs (((delta T) . j) - 0) < a )
assume i <= j ; ::_thesis: abs (((delta T) . j) - 0) < a
then (delta T) . j <= (delta T) . i by A36;
then A42: (delta T) . j < a by A41, XXREAL_0:2;
(delta T) . j >= 0 by A35;
hence abs (((delta T) . j) - 0) < a by A42, ABSVALUE:def_1; ::_thesis: verum
end;
hence ex i being Element of NAT st
for j being Element of NAT st i <= j holds
abs (((delta T) . j) - 0) < a ; ::_thesis: verum
end;
then A43: delta T is convergent by SEQ_2:def_6;
then lim (delta T) = 0 by A38, SEQ_2:def_7;
hence ex T being DivSequence of A st
( delta T is convergent & lim (delta T) = 0 ) by A43; ::_thesis: verum
end;
Lm5: for A being non empty closed_interval Subset of REAL st vol A = 0 holds
ex T being DivSequence of A st
( delta T is convergent & lim (delta T) = 0 )
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: ( vol A = 0 implies ex T being DivSequence of A st
( delta T is convergent & lim (delta T) = 0 ) )
set T = the DivSequence of A;
assume A1: vol A = 0 ; ::_thesis: ex T being DivSequence of A st
( delta T is convergent & lim (delta T) = 0 )
A2: for i being Nat holds (delta the DivSequence of A) . i = 0
proof
let i be Nat; ::_thesis: (delta the DivSequence of A) . i = 0
reconsider ii = i as Element of NAT by ORDINAL1:def_12;
reconsider D = the DivSequence of A . ii as Division of A ;
A3: (delta the DivSequence of A) . i = delta D by INTEGRA3:def_2
.= max (rng (upper_volume ((chi (A,A)),D))) by INTEGRA3:def_1 ;
A4: len D = 1
proof
assume len D <> 1 ; ::_thesis: contradiction
then not len D is trivial by NAT_2:def_1;
then A5: len D >= 2 by NAT_2:29;
then 1 <= len D by XXREAL_0:2;
then A6: 1 in dom D by FINSEQ_3:25;
then A7: D . 1 in A by INTEGRA1:6;
then A8: lower_bound A <= D . 1 by INTEGRA2:1;
A9: 2 in dom D by A5, FINSEQ_3:25;
then D . 2 in A by INTEGRA1:6;
then A10: D . 2 <= upper_bound A by INTEGRA2:1;
A11: D . 1 <= upper_bound A by A7, INTEGRA2:1;
A12: (upper_bound A) - (lower_bound A) = 0 by A1, INTEGRA1:def_5;
D . 1 < D . 2 by A6, A9, SEQM_3:def_1;
hence contradiction by A8, A11, A10, A12, XXREAL_0:1; ::_thesis: verum
end;
for x1 being set st x1 in {0} holds
x1 in rng (upper_volume ((chi (A,A)),D))
proof
let x1 be set ; ::_thesis: ( x1 in {0} implies x1 in rng (upper_volume ((chi (A,A)),D)) )
A13: 1 in Seg (len D) by A4, FINSEQ_1:3;
then 1 in dom D by FINSEQ_1:def_3;
then A14: (upper_volume ((chi (A,A)),D)) . 1 = vol (divset (D,1)) by INTEGRA1:20;
1 in Seg (len (upper_volume ((chi (A,A)),D))) by A13, INTEGRA1:def_6;
then 1 in dom (upper_volume ((chi (A,A)),D)) by FINSEQ_1:def_3;
then A15: (upper_volume ((chi (A,A)),D)) . 1 in rng (upper_volume ((chi (A,A)),D)) by FUNCT_1:def_3;
A16: 1 in dom D by A13, FINSEQ_1:def_3;
then upper_bound (divset (D,1)) = D . (len D) by A4, INTEGRA1:def_4;
then A17: upper_bound (divset (D,1)) = upper_bound A by INTEGRA1:def_2;
lower_bound (divset (D,1)) = lower_bound A by A16, INTEGRA1:def_4;
then A18: vol (divset (D,1)) = (upper_bound A) - (lower_bound A) by A17, INTEGRA1:def_5
.= 0 by A1, INTEGRA1:def_5 ;
assume x1 in {0} ; ::_thesis: x1 in rng (upper_volume ((chi (A,A)),D))
hence x1 in rng (upper_volume ((chi (A,A)),D)) by A15, A14, A18, TARSKI:def_1; ::_thesis: verum
end;
then A19: {0} c= rng (upper_volume ((chi (A,A)),D)) by TARSKI:def_3;
for x1 being set st x1 in rng (upper_volume ((chi (A,A)),D)) holds
x1 in {0}
proof
let x1 be set ; ::_thesis: ( x1 in rng (upper_volume ((chi (A,A)),D)) implies x1 in {0} )
assume A20: x1 in rng (upper_volume ((chi (A,A)),D)) ; ::_thesis: x1 in {0}
then consider k being Element of NAT such that
A21: k in dom (upper_volume ((chi (A,A)),D)) and
A22: (upper_volume ((chi (A,A)),D)) . k = x1 by PARTFUN1:3;
reconsider x1 = x1 as Real by A20;
k in Seg (len (upper_volume ((chi (A,A)),D))) by A21, FINSEQ_1:def_3;
then A23: k in Seg (len D) by INTEGRA1:def_6;
then A24: k in dom D by FINSEQ_1:def_3;
k in dom D by A23, FINSEQ_1:def_3;
then A25: x1 = vol (divset (D,k)) by A22, INTEGRA1:20;
then x1 >= 0 by INTEGRA1:9;
then x1 = 0 by A1, A25, A24, INTEGRA1:8, INTEGRA2:38;
hence x1 in {0} by TARSKI:def_1; ::_thesis: verum
end;
then rng (upper_volume ((chi (A,A)),D)) c= {0} by TARSKI:def_3;
then rng (upper_volume ((chi (A,A)),D)) = {0} by A19, XBOOLE_0:def_10;
then (delta the DivSequence of A) . i in {0} by A3, XXREAL_2:def_8;
hence (delta the DivSequence of A) . i = 0 by TARSKI:def_1; ::_thesis: verum
end;
then A26: delta the DivSequence of A is constant by VALUED_0:def_18;
(delta the DivSequence of A) . 1 = 0 by A2;
then lim (delta the DivSequence of A) = 0 by A26, SEQ_4:25;
hence ex T being DivSequence of A st
( delta T is convergent & lim (delta T) = 0 ) by A26; ::_thesis: verum
end;
theorem Th11: :: INTEGRA4:11
for A being non empty closed_interval Subset of REAL ex T being DivSequence of A st
( delta T is convergent & lim (delta T) = 0 )
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: ex T being DivSequence of A st
( delta T is convergent & lim (delta T) = 0 )
now__::_thesis:_ex_T_being_DivSequence_of_A_st_
(_delta_T_is_convergent_&_lim_(delta_T)_=_0_)
percases ( vol A <> 0 or vol A = 0 ) ;
supposeA1: vol A <> 0 ; ::_thesis: ex T being DivSequence of A st
( delta T is convergent & lim (delta T) = 0 )
vol A >= 0 by INTEGRA1:9;
hence ex T being DivSequence of A st
( delta T is convergent & lim (delta T) = 0 ) by A1, Lm4; ::_thesis: verum
end;
suppose vol A = 0 ; ::_thesis: ex T being DivSequence of A st
( delta T is convergent & lim (delta T) = 0 )
hence ex T being DivSequence of A st
( delta T is convergent & lim (delta T) = 0 ) by Lm5; ::_thesis: verum
end;
end;
end;
hence ex T being DivSequence of A st
( delta T is convergent & lim (delta T) = 0 ) ; ::_thesis: verum
end;
theorem Th12: :: INTEGRA4:12
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL st f | A is bounded holds
( f is integrable iff for T being DivSequence of A st delta T is convergent & lim (delta T) = 0 holds
(lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = 0 )
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL st f | A is bounded holds
( f is integrable iff for T being DivSequence of A st delta T is convergent & lim (delta T) = 0 holds
(lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = 0 )
let f be Function of A,REAL; ::_thesis: ( f | A is bounded implies ( f is integrable iff for T being DivSequence of A st delta T is convergent & lim (delta T) = 0 holds
(lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = 0 ) )
assume A1: f | A is bounded ; ::_thesis: ( f is integrable iff for T being DivSequence of A st delta T is convergent & lim (delta T) = 0 holds
(lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = 0 )
A2: ( f is integrable implies for T being DivSequence of A st delta T is convergent & lim (delta T) = 0 holds
(lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = 0 )
proof
assume A3: f is integrable ; ::_thesis: for T being DivSequence of A st delta T is convergent & lim (delta T) = 0 holds
(lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = 0
for T being DivSequence of A st delta T is convergent & lim (delta T) = 0 holds
(lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = 0
proof
A4: upper_integral f = lower_integral f by A3, INTEGRA1:def_16;
let T be DivSequence of A; ::_thesis: ( delta T is convergent & lim (delta T) = 0 implies (lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = 0 )
assume that
A5: delta T is convergent and
A6: lim (delta T) = 0 ; ::_thesis: (lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = 0
A7: lim (lower_sum (f,T)) = lower_integral f by A1, A5, A6, Th8;
lim (upper_sum (f,T)) = upper_integral f by A1, A5, A6, Th9;
hence (lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = 0 by A7, A4; ::_thesis: verum
end;
hence for T being DivSequence of A st delta T is convergent & lim (delta T) = 0 holds
(lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = 0 ; ::_thesis: verum
end;
( ( for T being DivSequence of A st delta T is convergent & lim (delta T) = 0 holds
(lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = 0 ) implies f is integrable )
proof
consider T being DivSequence of A such that
A8: delta T is convergent and
A9: lim (delta T) = 0 by Th11;
assume for T being DivSequence of A st delta T is convergent & lim (delta T) = 0 holds
(lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = 0 ; ::_thesis: f is integrable
then (lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = 0 by A8, A9;
then (upper_integral f) - (lim (lower_sum (f,T))) = 0 by A1, A8, A9, Th9;
then A10: (upper_integral f) - (lower_integral f) = 0 by A1, A8, A9, Th8;
A11: f is lower_integrable by A1, Th10;
f is upper_integrable by A1, Th10;
hence f is integrable by A11, A10, INTEGRA1:def_16; ::_thesis: verum
end;
hence ( f is integrable iff for T being DivSequence of A st delta T is convergent & lim (delta T) = 0 holds
(lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = 0 ) by A2; ::_thesis: verum
end;
theorem Th13: :: INTEGRA4:13
for C being non empty set
for f being Function of C,REAL holds
( max+ f is total & max- f is total )
proof
let C be non empty set ; ::_thesis: for f being Function of C,REAL holds
( max+ f is total & max- f is total )
let f be Function of C,REAL; ::_thesis: ( max+ f is total & max- f is total )
A1: dom f = C by FUNCT_2:def_1;
then A2: dom (max- f) = C by RFUNCT_3:def_11;
dom (max+ f) = C by A1, RFUNCT_3:def_10;
hence ( max+ f is total & max- f is total ) by A2, PARTFUN1:def_2; ::_thesis: verum
end;
theorem Th14: :: INTEGRA4:14
for C being non empty set
for X being set
for f being PartFunc of C,REAL st f | X is bounded_above holds
(max+ f) | X is bounded_above
proof
let C be non empty set ; ::_thesis: for X being set
for f being PartFunc of C,REAL st f | X is bounded_above holds
(max+ f) | X is bounded_above
let X be set ; ::_thesis: for f being PartFunc of C,REAL st f | X is bounded_above holds
(max+ f) | X is bounded_above
let f be PartFunc of C,REAL; ::_thesis: ( f | X is bounded_above implies (max+ f) | X is bounded_above )
assume f | X is bounded_above ; ::_thesis: (max+ f) | X is bounded_above
then consider b being real number such that
A1: for c being set st c in X /\ (dom f) holds
f . c <= b by RFUNCT_1:70;
A2: dom (max+ f) = dom f by RFUNCT_3:def_10;
ex r being Real st
for c being set st c in X /\ (dom (max+ f)) holds
(max+ f) . c <= r
proof
now__::_thesis:_ex_r_being_Real_st_
for_c_being_set_st_c_in_X_/\_(dom_(max+_f))_holds_
(max+_f)_._c_<=_r
percases ( b < 0 or b >= 0 ) ;
supposeA3: b < 0 ; ::_thesis: ex r being Real st
for c being set st c in X /\ (dom (max+ f)) holds
(max+ f) . c <= r
for c being set st c in X /\ (dom (max+ f)) holds
(max+ f) . c <= 0
proof
let c be set ; ::_thesis: ( c in X /\ (dom (max+ f)) implies (max+ f) . c <= 0 )
assume c in X /\ (dom (max+ f)) ; ::_thesis: (max+ f) . c <= 0
then A4: c in X /\ (dom f) by RFUNCT_3:def_10;
then f . c <= b by A1;
then max ((f . c),0) = 0 by A3, XXREAL_0:def_10;
then A5: max+ (f . c) = 0 by RFUNCT_3:def_1;
c in dom f by A4, XBOOLE_0:def_4;
hence (max+ f) . c <= 0 by A2, A5, RFUNCT_3:def_10; ::_thesis: verum
end;
hence ex r being Real st
for c being set st c in X /\ (dom (max+ f)) holds
(max+ f) . c <= r ; ::_thesis: verum
end;
supposeA6: b >= 0 ; ::_thesis: ex r being Real st
for c being set st c in X /\ (dom (max+ f)) holds
(max+ f) . c <= r
for c being set st c in X /\ (dom (max+ f)) holds
(max+ f) . c <= b
proof
let c be set ; ::_thesis: ( c in X /\ (dom (max+ f)) implies (max+ f) . c <= b )
assume c in X /\ (dom (max+ f)) ; ::_thesis: (max+ f) . c <= b
then A7: c in X /\ (dom f) by RFUNCT_3:def_10;
then f . c <= b by A1;
then max ((f . c),0) <= b by A6, XXREAL_0:28;
then A8: max+ (f . c) <= b by RFUNCT_3:def_1;
c in dom f by A7, XBOOLE_0:def_4;
hence (max+ f) . c <= b by A2, A8, RFUNCT_3:def_10; ::_thesis: verum
end;
then consider r being real number such that
r = b and
A9: for c being set st c in X /\ (dom (max+ f)) holds
(max+ f) . c <= r ;
r is Real by XREAL_0:def_1;
hence ex r being Real st
for c being set st c in X /\ (dom (max+ f)) holds
(max+ f) . c <= r by A9; ::_thesis: verum
end;
end;
end;
hence ex r being Real st
for c being set st c in X /\ (dom (max+ f)) holds
(max+ f) . c <= r ; ::_thesis: verum
end;
hence (max+ f) | X is bounded_above by RFUNCT_1:70; ::_thesis: verum
end;
theorem Th15: :: INTEGRA4:15
for C being non empty set
for X being set
for f being PartFunc of C,REAL holds (max+ f) | X is bounded_below
proof
let C be non empty set ; ::_thesis: for X being set
for f being PartFunc of C,REAL holds (max+ f) | X is bounded_below
let X be set ; ::_thesis: for f being PartFunc of C,REAL holds (max+ f) | X is bounded_below
let f be PartFunc of C,REAL; ::_thesis: (max+ f) | X is bounded_below
for c being set st c in X /\ (dom (max+ f)) holds
(max+ f) . c >= 0 by RFUNCT_3:37;
hence (max+ f) | X is bounded_below by RFUNCT_1:71; ::_thesis: verum
end;
theorem Th16: :: INTEGRA4:16
for C being non empty set
for X being set
for f being PartFunc of C,REAL st f | X is bounded_below holds
(max- f) | X is bounded_above
proof
let C be non empty set ; ::_thesis: for X being set
for f being PartFunc of C,REAL st f | X is bounded_below holds
(max- f) | X is bounded_above
let X be set ; ::_thesis: for f being PartFunc of C,REAL st f | X is bounded_below holds
(max- f) | X is bounded_above
let f be PartFunc of C,REAL; ::_thesis: ( f | X is bounded_below implies (max- f) | X is bounded_above )
assume f | X is bounded_below ; ::_thesis: (max- f) | X is bounded_above
then consider b being real number such that
A1: for c being set st c in X /\ (dom f) holds
f . c >= b by RFUNCT_1:71;
A2: dom (max- f) = dom f by RFUNCT_3:def_11;
ex r being Real st
for c being set st c in X /\ (dom (max- f)) holds
(max- f) . c <= r
proof
now__::_thesis:_ex_r_being_Real_st_
for_c_being_set_st_c_in_X_/\_(dom_(max-_f))_holds_
(max-_f)_._c_<=_r
percases ( b > 0 or b <= 0 ) ;
supposeA3: b > 0 ; ::_thesis: ex r being Real st
for c being set st c in X /\ (dom (max- f)) holds
(max- f) . c <= r
for c being set st c in X /\ (dom (max- f)) holds
(max- f) . c <= 0
proof
let c be set ; ::_thesis: ( c in X /\ (dom (max- f)) implies (max- f) . c <= 0 )
assume c in X /\ (dom (max- f)) ; ::_thesis: (max- f) . c <= 0
then A4: c in X /\ (dom f) by RFUNCT_3:def_11;
then f . c >= b by A1;
then max ((- (f . c)),0) = 0 by A3, XXREAL_0:def_10;
then A5: max- (f . c) = 0 by RFUNCT_3:def_2;
c in dom f by A4, XBOOLE_0:def_4;
hence (max- f) . c <= 0 by A2, A5, RFUNCT_3:def_11; ::_thesis: verum
end;
hence ex r being Real st
for c being set st c in X /\ (dom (max- f)) holds
(max- f) . c <= r ; ::_thesis: verum
end;
supposeA6: b <= 0 ; ::_thesis: ex r being Real st
for c being set st c in X /\ (dom (max- f)) holds
(max- f) . c <= r
for c being set st c in X /\ (dom (max- f)) holds
(max- f) . c <= - b
proof
let c be set ; ::_thesis: ( c in X /\ (dom (max- f)) implies (max- f) . c <= - b )
assume c in X /\ (dom (max- f)) ; ::_thesis: (max- f) . c <= - b
then A7: c in X /\ (dom f) by RFUNCT_3:def_11;
then f . c >= b by A1;
then - (f . c) <= - b by XREAL_1:24;
then max ((- (f . c)),0) <= - b by A6, XXREAL_0:28;
then A8: max- (f . c) <= - b by RFUNCT_3:def_2;
c in dom f by A7, XBOOLE_0:def_4;
hence (max- f) . c <= - b by A2, A8, RFUNCT_3:def_11; ::_thesis: verum
end;
then consider r being real number such that
r = - b and
A9: for c being set st c in X /\ (dom (max- f)) holds
(max- f) . c <= r ;
r is Real by XREAL_0:def_1;
hence ex r being Real st
for c being set st c in X /\ (dom (max- f)) holds
(max- f) . c <= r by A9; ::_thesis: verum
end;
end;
end;
hence ex r being Real st
for c being set st c in X /\ (dom (max- f)) holds
(max- f) . c <= r ; ::_thesis: verum
end;
hence (max- f) | X is bounded_above by RFUNCT_1:70; ::_thesis: verum
end;
theorem Th17: :: INTEGRA4:17
for C being non empty set
for X being set
for f being PartFunc of C,REAL holds (max- f) | X is bounded_below
proof
let C be non empty set ; ::_thesis: for X being set
for f being PartFunc of C,REAL holds (max- f) | X is bounded_below
let X be set ; ::_thesis: for f being PartFunc of C,REAL holds (max- f) | X is bounded_below
let f be PartFunc of C,REAL; ::_thesis: (max- f) | X is bounded_below
for c being set st c in X /\ (dom (max- f)) holds
(max- f) . c >= 0 by RFUNCT_3:40;
hence (max- f) | X is bounded_below by RFUNCT_1:71; ::_thesis: verum
end;
theorem Th18: :: INTEGRA4:18
for A being non empty closed_interval Subset of REAL
for X being set
for f being PartFunc of A,REAL st f | A is bounded_above holds
rng (f | X) is bounded_above
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for X being set
for f being PartFunc of A,REAL st f | A is bounded_above holds
rng (f | X) is bounded_above
let X be set ; ::_thesis: for f being PartFunc of A,REAL st f | A is bounded_above holds
rng (f | X) is bounded_above
let f be PartFunc of A,REAL; ::_thesis: ( f | A is bounded_above implies rng (f | X) is bounded_above )
assume f | A is bounded_above ; ::_thesis: rng (f | X) is bounded_above
then rng f is bounded_above by INTEGRA1:13;
hence rng (f | X) is bounded_above by RELAT_1:70, XXREAL_2:43; ::_thesis: verum
end;
theorem Th19: :: INTEGRA4:19
for A being non empty closed_interval Subset of REAL
for X being set
for f being PartFunc of A,REAL st f | A is bounded_below holds
rng (f | X) is bounded_below
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for X being set
for f being PartFunc of A,REAL st f | A is bounded_below holds
rng (f | X) is bounded_below
let X be set ; ::_thesis: for f being PartFunc of A,REAL st f | A is bounded_below holds
rng (f | X) is bounded_below
let f be PartFunc of A,REAL; ::_thesis: ( f | A is bounded_below implies rng (f | X) is bounded_below )
assume f | A is bounded_below ; ::_thesis: rng (f | X) is bounded_below
then rng f is bounded_below by INTEGRA1:11;
hence rng (f | X) is bounded_below by RELAT_1:70, XXREAL_2:44; ::_thesis: verum
end;
theorem Th20: :: INTEGRA4:20
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL st f | A is bounded & f is integrable holds
max+ f is integrable
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL st f | A is bounded & f is integrable holds
max+ f is integrable
let f be Function of A,REAL; ::_thesis: ( f | A is bounded & f is integrable implies max+ f is integrable )
assume that
A1: f | A is bounded and
A2: f is integrable ; ::_thesis: max+ f is integrable
A3: max+ f is total by Th13;
A4: (max+ f) | A is bounded_below by Th15;
A5: (max+ f) | A is bounded_above by A1, Th14;
for T being DivSequence of A st delta T is convergent & lim (delta T) = 0 holds
(lim (upper_sum ((max+ f),T))) - (lim (lower_sum ((max+ f),T))) = 0
proof
let T be DivSequence of A; ::_thesis: ( delta T is convergent & lim (delta T) = 0 implies (lim (upper_sum ((max+ f),T))) - (lim (lower_sum ((max+ f),T))) = 0 )
assume that
A6: delta T is convergent and
A7: lim (delta T) = 0 ; ::_thesis: (lim (upper_sum ((max+ f),T))) - (lim (lower_sum ((max+ f),T))) = 0
A8: lower_sum (f,T) is convergent by A1, A6, A7, Th8;
A9: upper_sum (f,T) is convergent by A1, A6, A7, Th9;
then A10: (upper_sum (f,T)) - (lower_sum (f,T)) is convergent by A8;
reconsider osc1 = (upper_sum ((max+ f),T)) - (lower_sum ((max+ f),T)) as Real_Sequence ;
reconsider osc = (upper_sum (f,T)) - (lower_sum (f,T)) as Real_Sequence ;
(lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = 0 by A1, A2, A6, A7, Th12;
then A11: lim ((upper_sum (f,T)) - (lower_sum (f,T))) = 0 by A9, A8, SEQ_2:12;
A12: for a being real number st 0 < a holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((osc1 . m) - 0) < a
proof
let a be real number ; ::_thesis: ( 0 < a implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((osc1 . m) - 0) < a )
assume 0 < a ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((osc1 . m) - 0) < a
then consider n being Element of NAT such that
A13: for m being Element of NAT st n <= m holds
abs ((osc . m) - 0) < a by A10, A11, SEQ_2:def_7;
for m being Element of NAT st n <= m holds
abs ((osc1 . m) - 0) < a
proof
let m be Element of NAT ; ::_thesis: ( n <= m implies abs ((osc1 . m) - 0) < a )
reconsider D = T . m as Division of A ;
len (upper_volume (f,D)) = len D by INTEGRA1:def_6;
then reconsider UV = upper_volume (f,D) as Element of (len D) -tuples_on REAL by FINSEQ_2:133;
len (lower_volume (f,D)) = len D by INTEGRA1:def_7;
then reconsider LV = lower_volume (f,D) as Element of (len D) -tuples_on REAL by FINSEQ_2:133;
len (upper_volume ((max+ f),D)) = len D by INTEGRA1:def_6;
then reconsider UV1 = upper_volume ((max+ f),D) as Element of (len D) -tuples_on REAL by FINSEQ_2:133;
len (lower_volume ((max+ f),D)) = len D by INTEGRA1:def_7;
then reconsider LV1 = lower_volume ((max+ f),D) as Element of (len D) -tuples_on REAL by FINSEQ_2:133;
reconsider F = UV1 - LV1 as FinSequence of REAL ;
osc1 . m = ((upper_sum ((max+ f),T)) . m) + ((- (lower_sum ((max+ f),T))) . m) by SEQ_1:7
.= ((upper_sum ((max+ f),T)) . m) + (- ((lower_sum ((max+ f),T)) . m)) by SEQ_1:10
.= ((upper_sum ((max+ f),T)) . m) - ((lower_sum ((max+ f),T)) . m)
.= (upper_sum ((max+ f),(T . m))) - ((lower_sum ((max+ f),T)) . m) by INTEGRA2:def_2
.= (upper_sum ((max+ f),(T . m))) - (lower_sum ((max+ f),(T . m))) by INTEGRA2:def_3
.= (Sum (upper_volume ((max+ f),D))) - (lower_sum ((max+ f),(T . m))) by INTEGRA1:def_8
.= (Sum (upper_volume ((max+ f),D))) - (Sum (lower_volume ((max+ f),D))) by INTEGRA1:def_9 ;
then A14: osc1 . m = Sum (UV1 - LV1) by RVSUM_1:90;
A15: for j being Nat st j in Seg (len D) holds
(UV1 - LV1) . j <= (UV - LV) . j
proof
let j be Nat; ::_thesis: ( j in Seg (len D) implies (UV1 - LV1) . j <= (UV - LV) . j )
set x = (UV1 - LV1) . j;
set y = (UV - LV) . j;
assume A16: j in Seg (len D) ; ::_thesis: (UV1 - LV1) . j <= (UV - LV) . j
then A17: j in dom D by FINSEQ_1:def_3;
then A18: LV1 . j = (lower_bound (rng ((max+ f) | (divset (D,j))))) * (vol (divset (D,j))) by INTEGRA1:def_7;
A19: ( rng (f | (divset (D,j))) is real-bounded & ex r being Real st r in rng (f | (divset (D,j))) )
proof
A20: rng f is bounded_below by A1, INTEGRA1:11;
rng f is bounded_above by A1, INTEGRA1:13;
hence rng (f | (divset (D,j))) is real-bounded by A20, RELAT_1:70, XXREAL_2:45; ::_thesis: ex r being Real st r in rng (f | (divset (D,j)))
consider r being Real such that
A21: r in divset (D,j) by SUBSET_1:4;
j in dom D by A16, FINSEQ_1:def_3;
then divset (D,j) c= A by INTEGRA1:8;
then r in A by A21;
then r in dom f by FUNCT_2:def_1;
then f . r in rng (f | (divset (D,j))) by A21, FUNCT_1:50;
hence ex r being Real st r in rng (f | (divset (D,j))) ; ::_thesis: verum
end;
A22: (upper_bound (rng (f | (divset (D,j))))) - (lower_bound (rng (f | (divset (D,j))))) >= (upper_bound (rng ((max+ f) | (divset (D,j))))) - (lower_bound (rng ((max+ f) | (divset (D,j)))))
proof
set m1 = lower_bound (rng ((max+ f) | (divset (D,j))));
set M1 = upper_bound (rng ((max+ f) | (divset (D,j))));
set m = lower_bound (rng (f | (divset (D,j))));
set M = upper_bound (rng (f | (divset (D,j))));
A23: dom f = dom (max+ f) by RFUNCT_3:def_10;
A24: j in dom D by A16, FINSEQ_1:def_3;
A25: rng (f | (divset (D,j))) is bounded_above by A1, Th18;
dom (f | (divset (D,j))) = (dom f) /\ (divset (D,j)) by RELAT_1:61;
then dom (f | (divset (D,j))) = A /\ (divset (D,j)) by FUNCT_2:def_1;
then dom (f | (divset (D,j))) <> {} by A24, INTEGRA1:8, XBOOLE_1:28;
then A26: rng (f | (divset (D,j))) <> {} by RELAT_1:42;
dom f = A by FUNCT_2:def_1;
then dom ((max+ f) | (divset (D,j))) = A /\ (divset (D,j)) by A23, RELAT_1:61;
then dom ((max+ f) | (divset (D,j))) <> {} by A24, INTEGRA1:8, XBOOLE_1:28;
then A27: rng ((max+ f) | (divset (D,j))) <> {} by RELAT_1:42;
(max+ f) | A is bounded_below by Th15;
then A28: rng ((max+ f) | (divset (D,j))) is bounded_below by Th19;
A29: rng (f | (divset (D,j))) is bounded_below by A1, Th19;
(max+ f) | A is bounded_above by A1, Th14;
then A30: rng ((max+ f) | (divset (D,j))) is bounded_above by Th18;
now__::_thesis:_(upper_bound_(rng_(f_|_(divset_(D,j)))))_-_(lower_bound_(rng_(f_|_(divset_(D,j)))))_>=_(upper_bound_(rng_((max+_f)_|_(divset_(D,j)))))_-_(lower_bound_(rng_((max+_f)_|_(divset_(D,j)))))
percases ( ( upper_bound (rng (f | (divset (D,j)))) > 0 & lower_bound (rng (f | (divset (D,j)))) >= 0 ) or ( upper_bound (rng (f | (divset (D,j)))) > 0 & lower_bound (rng (f | (divset (D,j)))) <= 0 ) or ( upper_bound (rng (f | (divset (D,j)))) <= 0 & lower_bound (rng (f | (divset (D,j)))) <= 0 ) ) by A19, SEQ_4:11;
supposeA31: ( upper_bound (rng (f | (divset (D,j)))) > 0 & lower_bound (rng (f | (divset (D,j)))) >= 0 ) ; ::_thesis: (upper_bound (rng (f | (divset (D,j))))) - (lower_bound (rng (f | (divset (D,j))))) >= (upper_bound (rng ((max+ f) | (divset (D,j))))) - (lower_bound (rng ((max+ f) | (divset (D,j)))))
A32: for r being real number st r in rng ((max+ f) | (divset (D,j))) holds
r <= upper_bound (rng (f | (divset (D,j))))
proof
let r be real number ; ::_thesis: ( r in rng ((max+ f) | (divset (D,j))) implies r <= upper_bound (rng (f | (divset (D,j)))) )
assume r in rng ((max+ f) | (divset (D,j))) ; ::_thesis: r <= upper_bound (rng (f | (divset (D,j))))
then consider x being Element of A such that
A33: x in dom ((max+ f) | (divset (D,j))) and
A34: r = ((max+ f) | (divset (D,j))) . x by PARTFUN1:3;
A35: r = (max+ (f | (divset (D,j)))) . x by A34, RFUNCT_3:44;
A36: x in dom (max+ (f | (divset (D,j)))) by A33, RFUNCT_3:44;
then A37: x in dom (f | (divset (D,j))) by RFUNCT_3:def_10;
now__::_thesis:_r_<=_upper_bound_(rng_(f_|_(divset_(D,j))))
percases ( r = 0 or r > 0 ) by A35, RFUNCT_3:37;
suppose r = 0 ; ::_thesis: r <= upper_bound (rng (f | (divset (D,j))))
hence r <= upper_bound (rng (f | (divset (D,j)))) by A31; ::_thesis: verum
end;
supposeA38: r > 0 ; ::_thesis: r <= upper_bound (rng (f | (divset (D,j))))
r = max+ ((f | (divset (D,j))) . x) by A35, A36, RFUNCT_3:def_10;
then r = max (((f | (divset (D,j))) . x),0) by RFUNCT_3:def_1;
then r = (f | (divset (D,j))) . x by A38, XXREAL_0:def_10;
then r in rng (f | (divset (D,j))) by A37, FUNCT_1:def_3;
hence r <= upper_bound (rng (f | (divset (D,j)))) by A25, SEQ_4:def_1; ::_thesis: verum
end;
end;
end;
hence r <= upper_bound (rng (f | (divset (D,j)))) ; ::_thesis: verum
end;
A39: for s being real number st 0 < s holds
ex r being real number st
( r in rng ((max+ f) | (divset (D,j))) & r < (lower_bound (rng (f | (divset (D,j))))) + s )
proof
let s be real number ; ::_thesis: ( 0 < s implies ex r being real number st
( r in rng ((max+ f) | (divset (D,j))) & r < (lower_bound (rng (f | (divset (D,j))))) + s ) )
assume 0 < s ; ::_thesis: ex r being real number st
( r in rng ((max+ f) | (divset (D,j))) & r < (lower_bound (rng (f | (divset (D,j))))) + s )
then consider r being real number such that
A40: r in rng (f | (divset (D,j))) and
A41: r < (lower_bound (rng (f | (divset (D,j))))) + s by A26, A29, SEQ_4:def_2;
reconsider r = r as Real by XREAL_0:def_1;
r in rng ((max+ f) | (divset (D,j)))
proof
A42: r >= lower_bound (rng (f | (divset (D,j)))) by A29, A40, SEQ_4:def_2;
consider x being Element of A such that
A43: x in dom (f | (divset (D,j))) and
A44: r = (f | (divset (D,j))) . x by A40, PARTFUN1:3;
A45: x in dom (max+ (f | (divset (D,j)))) by A43, RFUNCT_3:def_10;
then (max+ (f | (divset (D,j)))) . x = max+ r by A44, RFUNCT_3:def_10
.= max (r,0) by RFUNCT_3:def_1
.= r by A31, A42, XXREAL_0:def_10 ;
then r in rng (max+ (f | (divset (D,j)))) by A45, FUNCT_1:def_3;
hence r in rng ((max+ f) | (divset (D,j))) by RFUNCT_3:44; ::_thesis: verum
end;
hence ex r being real number st
( r in rng ((max+ f) | (divset (D,j))) & r < (lower_bound (rng (f | (divset (D,j))))) + s ) by A41; ::_thesis: verum
end;
A46: for r being real number st r in rng ((max+ f) | (divset (D,j))) holds
lower_bound (rng (f | (divset (D,j)))) <= r
proof
let r be real number ; ::_thesis: ( r in rng ((max+ f) | (divset (D,j))) implies lower_bound (rng (f | (divset (D,j)))) <= r )
assume r in rng ((max+ f) | (divset (D,j))) ; ::_thesis: lower_bound (rng (f | (divset (D,j)))) <= r
then consider x being Element of A such that
A47: x in dom ((max+ f) | (divset (D,j))) and
A48: r = ((max+ f) | (divset (D,j))) . x by PARTFUN1:3;
A49: x in dom (max+ (f | (divset (D,j)))) by A47, RFUNCT_3:44;
x in dom (max+ (f | (divset (D,j)))) by A47, RFUNCT_3:44;
then x in dom (f | (divset (D,j))) by RFUNCT_3:def_10;
then (f | (divset (D,j))) . x in rng (f | (divset (D,j))) by FUNCT_1:def_3;
then A50: (f | (divset (D,j))) . x >= lower_bound (rng (f | (divset (D,j)))) by A29, SEQ_4:def_2;
r = (max+ (f | (divset (D,j)))) . x by A48, RFUNCT_3:44
.= max+ ((f | (divset (D,j))) . x) by A49, RFUNCT_3:def_10
.= max (((f | (divset (D,j))) . x),0) by RFUNCT_3:def_1 ;
hence lower_bound (rng (f | (divset (D,j)))) <= r by A31, A50, XXREAL_0:def_10; ::_thesis: verum
end;
for s being real number st 0 < s holds
ex r being real number st
( r in rng ((max+ f) | (divset (D,j))) & (upper_bound (rng (f | (divset (D,j))))) - s < r )
proof
let s be real number ; ::_thesis: ( 0 < s implies ex r being real number st
( r in rng ((max+ f) | (divset (D,j))) & (upper_bound (rng (f | (divset (D,j))))) - s < r ) )
assume 0 < s ; ::_thesis: ex r being real number st
( r in rng ((max+ f) | (divset (D,j))) & (upper_bound (rng (f | (divset (D,j))))) - s < r )
then consider r being real number such that
A51: r in rng (f | (divset (D,j))) and
A52: (upper_bound (rng (f | (divset (D,j))))) - s < r by A26, A25, SEQ_4:def_1;
r in rng ((max+ f) | (divset (D,j)))
proof
reconsider r1 = r as Real by XREAL_0:def_1;
consider x being Element of A such that
A53: x in dom (f | (divset (D,j))) and
A54: r = (f | (divset (D,j))) . x by A51, PARTFUN1:3;
A55: r >= lower_bound (rng (f | (divset (D,j)))) by A29, A51, SEQ_4:def_2;
A56: x in dom (max+ (f | (divset (D,j)))) by A53, RFUNCT_3:def_10;
then (max+ (f | (divset (D,j)))) . x = max+ r1 by A54, RFUNCT_3:def_10
.= max (r,0) by RFUNCT_3:def_1
.= r by A31, A55, XXREAL_0:def_10 ;
then r in rng (max+ (f | (divset (D,j)))) by A56, FUNCT_1:def_3;
hence r in rng ((max+ f) | (divset (D,j))) by RFUNCT_3:44; ::_thesis: verum
end;
hence ex r being real number st
( r in rng ((max+ f) | (divset (D,j))) & (upper_bound (rng (f | (divset (D,j))))) - s < r ) by A52; ::_thesis: verum
end;
then upper_bound (rng ((max+ f) | (divset (D,j)))) = upper_bound (rng (f | (divset (D,j)))) by A27, A30, A32, SEQ_4:def_1;
hence (upper_bound (rng (f | (divset (D,j))))) - (lower_bound (rng (f | (divset (D,j))))) >= (upper_bound (rng ((max+ f) | (divset (D,j))))) - (lower_bound (rng ((max+ f) | (divset (D,j))))) by A27, A28, A46, A39, SEQ_4:def_2; ::_thesis: verum
end;
supposeA57: ( upper_bound (rng (f | (divset (D,j)))) > 0 & lower_bound (rng (f | (divset (D,j)))) <= 0 ) ; ::_thesis: (upper_bound (rng (f | (divset (D,j))))) - (lower_bound (rng (f | (divset (D,j))))) >= (upper_bound (rng ((max+ f) | (divset (D,j))))) - (lower_bound (rng ((max+ f) | (divset (D,j)))))
A58: for s being real number st 0 < s holds
ex r being real number st
( r in rng ((max+ f) | (divset (D,j))) & r < 0 + s )
proof
let s be real number ; ::_thesis: ( 0 < s implies ex r being real number st
( r in rng ((max+ f) | (divset (D,j))) & r < 0 + s ) )
assume A59: s > 0 ; ::_thesis: ex r being real number st
( r in rng ((max+ f) | (divset (D,j))) & r < 0 + s )
then consider r being real number such that
A60: r in rng (f | (divset (D,j))) and
A61: r < (lower_bound (rng (f | (divset (D,j))))) + s by A26, A29, SEQ_4:def_2;
consider x being Element of A such that
A62: x in dom (f | (divset (D,j))) and
A63: r = (f | (divset (D,j))) . x by A60, PARTFUN1:3;
A64: x in dom (max+ (f | (divset (D,j)))) by A62, RFUNCT_3:def_10;
then A65: (max+ (f | (divset (D,j)))) . x = max+ ((f | (divset (D,j))) . x) by RFUNCT_3:def_10
.= max (((f | (divset (D,j))) . x),0) by RFUNCT_3:def_1 ;
(max+ (f | (divset (D,j)))) . x in rng (max+ (f | (divset (D,j)))) by A64, FUNCT_1:def_3;
then A66: (max+ (f | (divset (D,j)))) . x in rng ((max+ f) | (divset (D,j))) by RFUNCT_3:44;
A67: r - s < lower_bound (rng (f | (divset (D,j)))) by A61, XREAL_1:19;
now__::_thesis:_ex_r_being_Real_st_
(_r_in_rng_((max+_f)_|_(divset_(D,j)))_&_r_<_0_+_s_)
percases ( r < 0 or r >= 0 ) ;
suppose r < 0 ; ::_thesis: ex r being Real st
( r in rng ((max+ f) | (divset (D,j))) & r < 0 + s )
then 0 in rng ((max+ f) | (divset (D,j))) by A63, A66, A65, XXREAL_0:def_10;
hence ex r being Real st
( r in rng ((max+ f) | (divset (D,j))) & r < 0 + s ) by A59; ::_thesis: verum
end;
supposeA68: r >= 0 ; ::_thesis: ex r being Real st
( r in rng ((max+ f) | (divset (D,j))) & r < 0 + s )
A69: r < 0 + s by A57, A67, XREAL_1:19;
r in rng ((max+ f) | (divset (D,j))) by A63, A66, A65, A68, XXREAL_0:def_10;
hence ex r being Real st
( r in rng ((max+ f) | (divset (D,j))) & r < 0 + s ) by A69; ::_thesis: verum
end;
end;
end;
hence ex r being real number st
( r in rng ((max+ f) | (divset (D,j))) & r < 0 + s ) ; ::_thesis: verum
end;
for r being real number st r in rng ((max+ f) | (divset (D,j))) holds
0 <= r
proof
let r be real number ; ::_thesis: ( r in rng ((max+ f) | (divset (D,j))) implies 0 <= r )
assume r in rng ((max+ f) | (divset (D,j))) ; ::_thesis: 0 <= r
then r in rng (max+ (f | (divset (D,j)))) by RFUNCT_3:44;
then ex x being Element of A st
( x in dom (max+ (f | (divset (D,j)))) & r = (max+ (f | (divset (D,j)))) . x ) by PARTFUN1:3;
hence 0 <= r by RFUNCT_3:37; ::_thesis: verum
end;
then A70: lower_bound (rng ((max+ f) | (divset (D,j)))) = 0 by A27, A28, A58, SEQ_4:def_2;
for r being Real st r in rng ((max+ f) | (divset (D,j))) holds
r <= upper_bound (rng (f | (divset (D,j))))
proof
let r be Real; ::_thesis: ( r in rng ((max+ f) | (divset (D,j))) implies r <= upper_bound (rng (f | (divset (D,j)))) )
assume r in rng ((max+ f) | (divset (D,j))) ; ::_thesis: r <= upper_bound (rng (f | (divset (D,j))))
then consider x being Element of A such that
A71: x in dom ((max+ f) | (divset (D,j))) and
A72: r = ((max+ f) | (divset (D,j))) . x by PARTFUN1:3;
A73: r = (max+ (f | (divset (D,j)))) . x by A72, RFUNCT_3:44;
A74: x in dom (max+ (f | (divset (D,j)))) by A71, RFUNCT_3:44;
then A75: x in dom (f | (divset (D,j))) by RFUNCT_3:def_10;
now__::_thesis:_r_<=_upper_bound_(rng_(f_|_(divset_(D,j))))
percases ( r = 0 or r > 0 ) by A73, RFUNCT_3:37;
suppose r = 0 ; ::_thesis: r <= upper_bound (rng (f | (divset (D,j))))
hence r <= upper_bound (rng (f | (divset (D,j)))) by A57; ::_thesis: verum
end;
supposeA76: r > 0 ; ::_thesis: r <= upper_bound (rng (f | (divset (D,j))))
r = max+ ((f | (divset (D,j))) . x) by A73, A74, RFUNCT_3:def_10;
then r = max (((f | (divset (D,j))) . x),0) by RFUNCT_3:def_1;
then r = (f | (divset (D,j))) . x by A76, XXREAL_0:def_10;
then r in rng (f | (divset (D,j))) by A75, FUNCT_1:def_3;
hence r <= upper_bound (rng (f | (divset (D,j)))) by A25, SEQ_4:def_1; ::_thesis: verum
end;
end;
end;
hence r <= upper_bound (rng (f | (divset (D,j)))) ; ::_thesis: verum
end;
then A77: for r being real number st r in rng ((max+ f) | (divset (D,j))) holds
r <= upper_bound (rng (f | (divset (D,j)))) ;
for s being real number st 0 < s holds
ex r being real number st
( r in rng ((max+ f) | (divset (D,j))) & (upper_bound (rng (f | (divset (D,j))))) - s < r )
proof
assume ex s being real number st
( 0 < s & ( for r being real number holds
( not r in rng ((max+ f) | (divset (D,j))) or not (upper_bound (rng (f | (divset (D,j))))) - s < r ) ) ) ; ::_thesis: contradiction
then consider s being real number such that
A78: s > 0 and
A79: for r being real number st r in rng ((max+ f) | (divset (D,j))) holds
(upper_bound (rng (f | (divset (D,j))))) - s >= r ;
consider r1 being real number such that
A80: r1 in rng (f | (divset (D,j))) and
A81: (upper_bound (rng (f | (divset (D,j))))) - s < r1 by A26, A25, A78, SEQ_4:def_1;
consider x being Element of A such that
A82: x in dom (f | (divset (D,j))) and
A83: r1 = (f | (divset (D,j))) . x by A80, PARTFUN1:3;
A84: x in dom (max+ (f | (divset (D,j)))) by A82, RFUNCT_3:def_10;
then x in dom ((max+ f) | (divset (D,j))) by RFUNCT_3:44;
then A85: ((max+ f) | (divset (D,j))) . x in rng ((max+ f) | (divset (D,j))) by FUNCT_1:def_3;
(max+ (f | (divset (D,j)))) . x >= 0 by RFUNCT_3:37;
then ((max+ f) | (divset (D,j))) . x >= 0 by RFUNCT_3:44;
then A86: (upper_bound (rng (f | (divset (D,j))))) - s >= 0 by A79, A85;
((max+ f) | (divset (D,j))) . x = (max+ (f | (divset (D,j)))) . x by RFUNCT_3:44
.= max+ ((f | (divset (D,j))) . x) by A84, RFUNCT_3:def_10
.= max (r1,0) by A83, RFUNCT_3:def_1
.= r1 by A81, A86, XXREAL_0:def_10 ;
hence contradiction by A79, A81, A85; ::_thesis: verum
end;
then upper_bound (rng ((max+ f) | (divset (D,j)))) = upper_bound (rng (f | (divset (D,j)))) by A27, A30, A77, SEQ_4:def_1;
hence (upper_bound (rng (f | (divset (D,j))))) - (lower_bound (rng (f | (divset (D,j))))) >= (upper_bound (rng ((max+ f) | (divset (D,j))))) - (lower_bound (rng ((max+ f) | (divset (D,j))))) by A57, A70, XREAL_1:13; ::_thesis: verum
end;
supposeA87: ( upper_bound (rng (f | (divset (D,j)))) <= 0 & lower_bound (rng (f | (divset (D,j)))) <= 0 ) ; ::_thesis: (upper_bound (rng (f | (divset (D,j))))) - (lower_bound (rng (f | (divset (D,j))))) >= (upper_bound (rng ((max+ f) | (divset (D,j))))) - (lower_bound (rng ((max+ f) | (divset (D,j)))))
A88: for s being real number st 0 < s holds
ex r being real number st
( r in rng ((max+ f) | (divset (D,j))) & r < 0 + s )
proof
let s be real number ; ::_thesis: ( 0 < s implies ex r being real number st
( r in rng ((max+ f) | (divset (D,j))) & r < 0 + s ) )
assume A89: s > 0 ; ::_thesis: ex r being real number st
( r in rng ((max+ f) | (divset (D,j))) & r < 0 + s )
consider r being Real such that
A90: r in rng ((max+ f) | (divset (D,j))) by A27, SUBSET_1:4;
consider x being Element of A such that
A91: x in dom ((max+ f) | (divset (D,j))) and
A92: r = ((max+ f) | (divset (D,j))) . x by A90, PARTFUN1:3;
A93: x in dom (max+ (f | (divset (D,j)))) by A91, RFUNCT_3:44;
then x in dom (f | (divset (D,j))) by RFUNCT_3:def_10;
then (f | (divset (D,j))) . x in rng (f | (divset (D,j))) by FUNCT_1:def_3;
then A94: (f | (divset (D,j))) . x <= upper_bound (rng (f | (divset (D,j)))) by A25, SEQ_4:def_1;
r = (max+ (f | (divset (D,j)))) . x by A92, RFUNCT_3:44;
then r = max+ ((f | (divset (D,j))) . x) by A93, RFUNCT_3:def_10
.= max (((f | (divset (D,j))) . x),0) by RFUNCT_3:def_1 ;
then r = 0 by A87, A94, XXREAL_0:def_10;
hence ex r being real number st
( r in rng ((max+ f) | (divset (D,j))) & r < 0 + s ) by A89, A90; ::_thesis: verum
end;
for r being real number st r in rng ((max+ f) | (divset (D,j))) holds
0 <= r
proof
let r be real number ; ::_thesis: ( r in rng ((max+ f) | (divset (D,j))) implies 0 <= r )
assume r in rng ((max+ f) | (divset (D,j))) ; ::_thesis: 0 <= r
then consider x being Element of A such that
x in dom ((max+ f) | (divset (D,j))) and
A95: r = ((max+ f) | (divset (D,j))) . x by PARTFUN1:3;
r = (max+ (f | (divset (D,j)))) . x by A95, RFUNCT_3:44;
hence 0 <= r by RFUNCT_3:37; ::_thesis: verum
end;
then A96: lower_bound (rng ((max+ f) | (divset (D,j)))) = 0 by A27, A28, A88, SEQ_4:def_2;
A97: for r being real number st r in rng ((max+ f) | (divset (D,j))) holds
r <= 0
proof
let r be real number ; ::_thesis: ( r in rng ((max+ f) | (divset (D,j))) implies r <= 0 )
assume r in rng ((max+ f) | (divset (D,j))) ; ::_thesis: r <= 0
then consider x being Element of A such that
A98: x in dom ((max+ f) | (divset (D,j))) and
A99: r = ((max+ f) | (divset (D,j))) . x by PARTFUN1:3;
A100: x in dom (max+ (f | (divset (D,j)))) by A98, RFUNCT_3:44;
then x in dom (f | (divset (D,j))) by RFUNCT_3:def_10;
then (f | (divset (D,j))) . x in rng (f | (divset (D,j))) by FUNCT_1:def_3;
then A101: (f | (divset (D,j))) . x <= upper_bound (rng (f | (divset (D,j)))) by A25, SEQ_4:def_1;
r = (max+ (f | (divset (D,j)))) . x by A99, RFUNCT_3:44;
then r = max+ ((f | (divset (D,j))) . x) by A100, RFUNCT_3:def_10
.= max (((f | (divset (D,j))) . x),0) by RFUNCT_3:def_1
.= 0 by A87, A101, XXREAL_0:def_10 ;
hence r <= 0 ; ::_thesis: verum
end;
for s being real number st 0 < s holds
ex r being real number st
( r in rng ((max+ f) | (divset (D,j))) & 0 - s < r )
proof
let s be real number ; ::_thesis: ( 0 < s implies ex r being real number st
( r in rng ((max+ f) | (divset (D,j))) & 0 - s < r ) )
assume A102: s > 0 ; ::_thesis: ex r being real number st
( r in rng ((max+ f) | (divset (D,j))) & 0 - s < r )
consider r being Real such that
A103: r in rng ((max+ f) | (divset (D,j))) by A27, SUBSET_1:4;
consider x being Element of A such that
x in dom ((max+ f) | (divset (D,j))) and
A104: r = ((max+ f) | (divset (D,j))) . x by A103, PARTFUN1:3;
r = (max+ (f | (divset (D,j)))) . x by A104, RFUNCT_3:44;
then r >= 0 by RFUNCT_3:37;
hence ex r being real number st
( r in rng ((max+ f) | (divset (D,j))) & 0 - s < r ) by A102, A103; ::_thesis: verum
end;
then upper_bound (rng ((max+ f) | (divset (D,j)))) = 0 by A27, A30, A97, SEQ_4:def_1;
hence (upper_bound (rng (f | (divset (D,j))))) - (lower_bound (rng (f | (divset (D,j))))) >= (upper_bound (rng ((max+ f) | (divset (D,j))))) - (lower_bound (rng ((max+ f) | (divset (D,j))))) by A19, A96, SEQ_4:11, XREAL_1:48; ::_thesis: verum
end;
end;
end;
hence (upper_bound (rng (f | (divset (D,j))))) - (lower_bound (rng (f | (divset (D,j))))) >= (upper_bound (rng ((max+ f) | (divset (D,j))))) - (lower_bound (rng ((max+ f) | (divset (D,j))))) ; ::_thesis: verum
end;
A105: LV . j = (lower_bound (rng (f | (divset (D,j))))) * (vol (divset (D,j))) by A17, INTEGRA1:def_7;
UV . j = (upper_bound (rng (f | (divset (D,j))))) * (vol (divset (D,j))) by A17, INTEGRA1:def_6;
then A106: (UV - LV) . j = ((upper_bound (rng (f | (divset (D,j))))) * (vol (divset (D,j)))) - ((lower_bound (rng (f | (divset (D,j))))) * (vol (divset (D,j)))) by A105, RVSUM_1:27
.= ((upper_bound (rng (f | (divset (D,j))))) - (lower_bound (rng (f | (divset (D,j)))))) * (vol (divset (D,j))) ;
UV1 . j = (upper_bound (rng ((max+ f) | (divset (D,j))))) * (vol (divset (D,j))) by A17, INTEGRA1:def_6;
then A107: (UV1 - LV1) . j = ((upper_bound (rng ((max+ f) | (divset (D,j))))) * (vol (divset (D,j)))) - ((lower_bound (rng ((max+ f) | (divset (D,j))))) * (vol (divset (D,j)))) by A18, RVSUM_1:27
.= ((upper_bound (rng ((max+ f) | (divset (D,j))))) - (lower_bound (rng ((max+ f) | (divset (D,j)))))) * (vol (divset (D,j))) ;
vol (divset (D,j)) >= 0 by INTEGRA1:9;
hence (UV1 - LV1) . j <= (UV - LV) . j by A107, A106, A22, XREAL_1:64; ::_thesis: verum
end;
assume n <= m ; ::_thesis: abs ((osc1 . m) - 0) < a
then A108: abs ((osc . m) - 0) < a by A13;
for j being Nat st j in dom F holds
0 <= F . j
proof
let j be Nat; ::_thesis: ( j in dom F implies 0 <= F . j )
set r = F . j;
(max+ f) | A is bounded_below by Th15;
then A109: rng (max+ f) is bounded_below by INTEGRA1:11;
assume A110: j in dom F ; ::_thesis: 0 <= F . j
j in Seg (len F) by A110, FINSEQ_1:def_3;
then A111: j in Seg (len D) by CARD_1:def_7;
then A112: j in dom D by FINSEQ_1:def_3;
then A113: LV1 . j = (lower_bound (rng ((max+ f) | (divset (D,j))))) * (vol (divset (D,j))) by INTEGRA1:def_7;
A114: ex r being Real st r in rng ((max+ f) | (divset (D,j)))
proof
consider r being Real such that
A115: r in divset (D,j) by SUBSET_1:4;
j in dom D by A111, FINSEQ_1:def_3;
then divset (D,j) c= A by INTEGRA1:8;
then r in A by A115;
then r in dom f by FUNCT_2:def_1;
then r in (dom f) /\ (divset (D,j)) by A115, XBOOLE_0:def_4;
then r in dom (f | (divset (D,j))) by RELAT_1:61;
then r in dom (max+ (f | (divset (D,j)))) by RFUNCT_3:def_10;
then r in dom ((max+ f) | (divset (D,j))) by RFUNCT_3:44;
then ((max+ f) | (divset (D,j))) . r in rng ((max+ f) | (divset (D,j))) by FUNCT_1:def_3;
hence ex r being Real st r in rng ((max+ f) | (divset (D,j))) ; ::_thesis: verum
end;
(max+ f) | A is bounded_above by A1, Th14;
then rng (max+ f) is bounded_above by INTEGRA1:13;
then rng ((max+ f) | (divset (D,j))) is real-bounded by A109, RELAT_1:70, XXREAL_2:45;
then A116: (upper_bound (rng ((max+ f) | (divset (D,j))))) - (lower_bound (rng ((max+ f) | (divset (D,j))))) >= 0 by A114, SEQ_4:11, XREAL_1:48;
UV1 . j = (upper_bound (rng ((max+ f) | (divset (D,j))))) * (vol (divset (D,j))) by A112, INTEGRA1:def_6;
then A117: F . j = ((upper_bound (rng ((max+ f) | (divset (D,j))))) * (vol (divset (D,j)))) - ((lower_bound (rng ((max+ f) | (divset (D,j))))) * (vol (divset (D,j)))) by A110, A113, VALUED_1:13
.= ((upper_bound (rng ((max+ f) | (divset (D,j))))) - (lower_bound (rng ((max+ f) | (divset (D,j)))))) * (vol (divset (D,j))) ;
vol (divset (D,j)) >= 0 by INTEGRA1:9;
hence 0 <= F . j by A117, A116; ::_thesis: verum
end;
then A118: osc1 . m >= 0 by A14, RVSUM_1:84;
then A119: abs ((osc1 . m) - 0) = osc1 . m by ABSVALUE:def_1;
osc . m = ((upper_sum (f,T)) . m) + ((- (lower_sum (f,T))) . m) by SEQ_1:7
.= ((upper_sum (f,T)) . m) + (- ((lower_sum (f,T)) . m)) by SEQ_1:10
.= ((upper_sum (f,T)) . m) - ((lower_sum (f,T)) . m)
.= (upper_sum (f,(T . m))) - ((lower_sum (f,T)) . m) by INTEGRA2:def_2
.= (upper_sum (f,(T . m))) - (lower_sum (f,(T . m))) by INTEGRA2:def_3
.= (Sum (upper_volume (f,D))) - (lower_sum (f,(T . m))) by INTEGRA1:def_8
.= (Sum (upper_volume (f,D))) - (Sum (lower_volume (f,D))) by INTEGRA1:def_9 ;
then osc . m = Sum (UV - LV) by RVSUM_1:90;
then A120: osc1 . m <= osc . m by A14, A15, RVSUM_1:82;
then abs (osc . m) = osc . m by A118, ABSVALUE:def_1;
hence abs ((osc1 . m) - 0) < a by A108, A120, A119, XXREAL_0:2; ::_thesis: verum
end;
hence ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((osc1 . m) - 0) < a ; ::_thesis: verum
end;
then osc1 is convergent by SEQ_2:def_6;
then A121: lim ((upper_sum ((max+ f),T)) - (lower_sum ((max+ f),T))) = 0 by A12, SEQ_2:def_7;
A122: lower_sum ((max+ f),T) is convergent by A3, A5, A4, A6, A7, Th8;
upper_sum ((max+ f),T) is convergent by A3, A5, A4, A6, A7, Th9;
hence (lim (upper_sum ((max+ f),T))) - (lim (lower_sum ((max+ f),T))) = 0 by A122, A121, SEQ_2:12; ::_thesis: verum
end;
hence max+ f is integrable by A3, A5, A4, Th12; ::_thesis: verum
end;
theorem Th21: :: INTEGRA4:21
for C being non empty set
for f being PartFunc of C,REAL holds max- f = max+ (- f)
proof
let C be non empty set ; ::_thesis: for f being PartFunc of C,REAL holds max- f = max+ (- f)
let f be PartFunc of C,REAL; ::_thesis: max- f = max+ (- f)
dom (max+ (- f)) = dom (- f) by RFUNCT_3:def_10;
then A1: dom (max+ (- f)) = dom f by VALUED_1:8;
A2: dom (max- f) = dom f by RFUNCT_3:def_11;
for x1 being Element of C st x1 in dom f holds
(max- f) . x1 = (max+ (- f)) . x1
proof
let x1 be Element of C; ::_thesis: ( x1 in dom f implies (max- f) . x1 = (max+ (- f)) . x1 )
assume A3: x1 in dom f ; ::_thesis: (max- f) . x1 = (max+ (- f)) . x1
then A4: (max+ (- f)) . x1 = max+ ((- f) . x1) by A1, RFUNCT_3:def_10
.= max (((- f) . x1),0) by RFUNCT_3:def_1
.= max ((- (f . x1)),0) by VALUED_1:8 ;
(max- f) . x1 = max- (f . x1) by A2, A3, RFUNCT_3:def_11
.= max ((- (f . x1)),0) by RFUNCT_3:def_2 ;
hence (max- f) . x1 = (max+ (- f)) . x1 by A4; ::_thesis: verum
end;
hence max- f = max+ (- f) by A2, A1, PARTFUN1:5; ::_thesis: verum
end;
theorem Th22: :: INTEGRA4:22
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL st f | A is bounded & f is integrable holds
max- f is integrable
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL st f | A is bounded & f is integrable holds
max- f is integrable
let f be Function of A,REAL; ::_thesis: ( f | A is bounded & f is integrable implies max- f is integrable )
assume that
A1: f | A is bounded and
A2: f is integrable ; ::_thesis: max- f is integrable
A3: (- f) | A is bounded by A1, RFUNCT_1:82;
(- 1) (#) f is integrable by A1, A2, INTEGRA2:31;
then max+ (- f) is integrable by A3, Th20;
hence max- f is integrable by Th21; ::_thesis: verum
end;
theorem :: INTEGRA4:23
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL st f | A is bounded & f is integrable holds
( abs f is integrable & abs (integral f) <= integral (abs f) )
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL st f | A is bounded & f is integrable holds
( abs f is integrable & abs (integral f) <= integral (abs f) )
let f be Function of A,REAL; ::_thesis: ( f | A is bounded & f is integrable implies ( abs f is integrable & abs (integral f) <= integral (abs f) ) )
assume that
A1: f | A is bounded and
A2: f is integrable ; ::_thesis: ( abs f is integrable & abs (integral f) <= integral (abs f) )
A3: max- f is integrable by A1, A2, Th22;
A4: (max+ f) | A is bounded_above by A1, Th14;
A5: (max- f) | A is bounded_above by A1, Th16;
A6: max+ f is total by Th13;
A7: (max- f) | A is bounded_below by Th17;
A8: (max+ f) | A is bounded_below by Th15;
A9: max- f is total by Th13;
A10: max+ f is integrable by A1, A2, Th20;
then (max+ f) + (max- f) is integrable by A6, A9, A4, A8, A5, A7, A3, INTEGRA1:57;
hence abs f is integrable by RFUNCT_3:34; ::_thesis: abs (integral f) <= integral (abs f)
A11: (integral (max+ f)) - (integral (max- f)) = integral ((max+ f) - (max- f)) by A6, A9, A4, A8, A5, A7, A10, A3, INTEGRA2:33
.= integral f by RFUNCT_3:34 ;
A12: (integral (max+ f)) + (integral (max- f)) = integral ((max+ f) + (max- f)) by A6, A9, A4, A8, A5, A7, A10, A3, INTEGRA1:57
.= integral (abs f) by RFUNCT_3:34 ;
then A13: (integral (abs f)) - (integral f) = 2 * (integral (max- f)) by A11;
for x being Real st x in A holds
(max- f) . x >= 0 by RFUNCT_3:40;
then integral (max- f) >= 0 by A9, A5, A7, INTEGRA2:32;
then A14: integral (abs f) >= integral f by A13, XREAL_1:49;
A15: (integral (abs f)) + (integral f) = 2 * (integral (max+ f)) by A12, A11;
for x being Real st x in A holds
(max+ f) . x >= 0 by RFUNCT_3:37;
then integral (max+ f) >= 0 by A6, A4, A8, INTEGRA2:32;
then - (integral (abs f)) <= integral f by A15, XREAL_1:61;
hence abs (integral f) <= integral (abs f) by A14, ABSVALUE:5; ::_thesis: verum
end;
theorem Th24: :: INTEGRA4:24
for a being Real
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL st ( for x, y being Real st x in A & y in A holds
abs ((f . x) - (f . y)) <= a ) holds
(upper_bound (rng f)) - (lower_bound (rng f)) <= a
proof
let a be Real; ::_thesis: for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL st ( for x, y being Real st x in A & y in A holds
abs ((f . x) - (f . y)) <= a ) holds
(upper_bound (rng f)) - (lower_bound (rng f)) <= a
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL st ( for x, y being Real st x in A & y in A holds
abs ((f . x) - (f . y)) <= a ) holds
(upper_bound (rng f)) - (lower_bound (rng f)) <= a
let f be Function of A,REAL; ::_thesis: ( ( for x, y being Real st x in A & y in A holds
abs ((f . x) - (f . y)) <= a ) implies (upper_bound (rng f)) - (lower_bound (rng f)) <= a )
assume A1: for x, y being Real st x in A & y in A holds
abs ((f . x) - (f . y)) <= a ; ::_thesis: (upper_bound (rng f)) - (lower_bound (rng f)) <= a
A2: for y being real number st y in A holds
(upper_bound (rng f)) - a <= f . y
proof
let y be real number ; ::_thesis: ( y in A implies (upper_bound (rng f)) - a <= f . y )
assume A3: y in A ; ::_thesis: (upper_bound (rng f)) - a <= f . y
for b being real number st b in rng f holds
b <= a + (f . y)
proof
let b be real number ; ::_thesis: ( b in rng f implies b <= a + (f . y) )
assume b in rng f ; ::_thesis: b <= a + (f . y)
then consider x being Element of A such that
x in dom f and
A4: b = f . x by PARTFUN1:3;
abs ((f . x) - (f . y)) <= a by A1, A3;
then (f . x) - (f . y) <= a by ABSVALUE:5;
hence b <= a + (f . y) by A4, XREAL_1:20; ::_thesis: verum
end;
then upper_bound (rng f) <= a + (f . y) by SEQ_4:45;
hence (upper_bound (rng f)) - a <= f . y by XREAL_1:20; ::_thesis: verum
end;
for b being real number st b in rng f holds
(upper_bound (rng f)) - a <= b
proof
let b be real number ; ::_thesis: ( b in rng f implies (upper_bound (rng f)) - a <= b )
assume b in rng f ; ::_thesis: (upper_bound (rng f)) - a <= b
then ex x being Element of A st
( x in dom f & b = f . x ) by PARTFUN1:3;
hence (upper_bound (rng f)) - a <= b by A2; ::_thesis: verum
end;
then (upper_bound (rng f)) - a <= lower_bound (rng f) by SEQ_4:43;
then upper_bound (rng f) <= a + (lower_bound (rng f)) by XREAL_1:20;
hence (upper_bound (rng f)) - (lower_bound (rng f)) <= a by XREAL_1:20; ::_thesis: verum
end;
theorem Th25: :: INTEGRA4:25
for a being Real
for A being non empty closed_interval Subset of REAL
for f, g being Function of A,REAL st f | A is bounded & a >= 0 & ( for x, y being Real st x in A & y in A holds
abs ((g . x) - (g . y)) <= a * (abs ((f . x) - (f . y))) ) holds
(upper_bound (rng g)) - (lower_bound (rng g)) <= a * ((upper_bound (rng f)) - (lower_bound (rng f)))
proof
let a be Real; ::_thesis: for A being non empty closed_interval Subset of REAL
for f, g being Function of A,REAL st f | A is bounded & a >= 0 & ( for x, y being Real st x in A & y in A holds
abs ((g . x) - (g . y)) <= a * (abs ((f . x) - (f . y))) ) holds
(upper_bound (rng g)) - (lower_bound (rng g)) <= a * ((upper_bound (rng f)) - (lower_bound (rng f)))
let A be non empty closed_interval Subset of REAL; ::_thesis: for f, g being Function of A,REAL st f | A is bounded & a >= 0 & ( for x, y being Real st x in A & y in A holds
abs ((g . x) - (g . y)) <= a * (abs ((f . x) - (f . y))) ) holds
(upper_bound (rng g)) - (lower_bound (rng g)) <= a * ((upper_bound (rng f)) - (lower_bound (rng f)))
let f, g be Function of A,REAL; ::_thesis: ( f | A is bounded & a >= 0 & ( for x, y being Real st x in A & y in A holds
abs ((g . x) - (g . y)) <= a * (abs ((f . x) - (f . y))) ) implies (upper_bound (rng g)) - (lower_bound (rng g)) <= a * ((upper_bound (rng f)) - (lower_bound (rng f))) )
assume that
A1: f | A is bounded and
A2: a >= 0 and
A3: for x, y being Real st x in A & y in A holds
abs ((g . x) - (g . y)) <= a * (abs ((f . x) - (f . y))) ; ::_thesis: (upper_bound (rng g)) - (lower_bound (rng g)) <= a * ((upper_bound (rng f)) - (lower_bound (rng f)))
A4: rng f is bounded_above by A1, INTEGRA1:13;
A5: dom f = A by FUNCT_2:def_1;
A6: rng f is bounded_below by A1, INTEGRA1:11;
A7: for x, y being Real st x in A & y in A holds
abs ((f . x) - (f . y)) <= (upper_bound (rng f)) - (lower_bound (rng f))
proof
let x, y be Real; ::_thesis: ( x in A & y in A implies abs ((f . x) - (f . y)) <= (upper_bound (rng f)) - (lower_bound (rng f)) )
assume that
A8: x in A and
A9: y in A ; ::_thesis: abs ((f . x) - (f . y)) <= (upper_bound (rng f)) - (lower_bound (rng f))
now__::_thesis:_abs_((f_._x)_-_(f_._y))_<=_(upper_bound_(rng_f))_-_(lower_bound_(rng_f))
percases ( f . x >= f . y or f . x < f . y ) ;
suppose f . x >= f . y ; ::_thesis: abs ((f . x) - (f . y)) <= (upper_bound (rng f)) - (lower_bound (rng f))
then (f . x) - (f . y) >= 0 by XREAL_1:48;
then abs ((f . x) - (f . y)) = (f . x) - (f . y) by ABSVALUE:def_1;
then A10: (abs ((f . x) - (f . y))) + (f . y) = f . x ;
f . y in rng f by A5, A9, FUNCT_1:def_3;
then A11: lower_bound (rng f) <= f . y by A6, SEQ_4:def_2;
f . x in rng f by A5, A8, FUNCT_1:def_3;
then f . x <= upper_bound (rng f) by A4, SEQ_4:def_1;
then f . y <= (upper_bound (rng f)) - (abs ((f . x) - (f . y))) by A10, XREAL_1:19;
then lower_bound (rng f) <= (upper_bound (rng f)) - (abs ((f . x) - (f . y))) by A11, XXREAL_0:2;
then (lower_bound (rng f)) + (abs ((f . x) - (f . y))) <= upper_bound (rng f) by XREAL_1:19;
hence abs ((f . x) - (f . y)) <= (upper_bound (rng f)) - (lower_bound (rng f)) by XREAL_1:19; ::_thesis: verum
end;
suppose f . x < f . y ; ::_thesis: abs ((f . x) - (f . y)) <= (upper_bound (rng f)) - (lower_bound (rng f))
then (f . x) - (f . y) < 0 by XREAL_1:49;
then abs ((f . x) - (f . y)) = - ((f . x) - (f . y)) by ABSVALUE:def_1
.= (f . y) - (f . x) ;
then A12: (abs ((f . x) - (f . y))) + (f . x) = f . y ;
f . x in rng f by A5, A8, FUNCT_1:def_3;
then A13: lower_bound (rng f) <= f . x by A6, SEQ_4:def_2;
f . y in rng f by A5, A9, FUNCT_1:def_3;
then f . y <= upper_bound (rng f) by A4, SEQ_4:def_1;
then f . x <= (upper_bound (rng f)) - (abs ((f . x) - (f . y))) by A12, XREAL_1:19;
then lower_bound (rng f) <= (upper_bound (rng f)) - (abs ((f . x) - (f . y))) by A13, XXREAL_0:2;
then (lower_bound (rng f)) + (abs ((f . x) - (f . y))) <= upper_bound (rng f) by XREAL_1:19;
hence abs ((f . x) - (f . y)) <= (upper_bound (rng f)) - (lower_bound (rng f)) by XREAL_1:19; ::_thesis: verum
end;
end;
end;
hence abs ((f . x) - (f . y)) <= (upper_bound (rng f)) - (lower_bound (rng f)) ; ::_thesis: verum
end;
for x, y being Real st x in A & y in A holds
abs ((g . x) - (g . y)) <= a * ((upper_bound (rng f)) - (lower_bound (rng f)))
proof
let x, y be Real; ::_thesis: ( x in A & y in A implies abs ((g . x) - (g . y)) <= a * ((upper_bound (rng f)) - (lower_bound (rng f))) )
assume that
A14: x in A and
A15: y in A ; ::_thesis: abs ((g . x) - (g . y)) <= a * ((upper_bound (rng f)) - (lower_bound (rng f)))
A16: abs ((g . x) - (g . y)) <= a * (abs ((f . x) - (f . y))) by A3, A14, A15;
a * (abs ((f . x) - (f . y))) <= a * ((upper_bound (rng f)) - (lower_bound (rng f))) by A2, A7, A14, A15, XREAL_1:64;
hence abs ((g . x) - (g . y)) <= a * ((upper_bound (rng f)) - (lower_bound (rng f))) by A16, XXREAL_0:2; ::_thesis: verum
end;
hence (upper_bound (rng g)) - (lower_bound (rng g)) <= a * ((upper_bound (rng f)) - (lower_bound (rng f))) by Th24; ::_thesis: verum
end;
theorem Th26: :: INTEGRA4:26
for a being Real
for A being non empty closed_interval Subset of REAL
for f, g, h being Function of A,REAL st f | A is bounded & g | A is bounded & a >= 0 & ( for x, y being Real st x in A & y in A holds
abs ((h . x) - (h . y)) <= a * ((abs ((f . x) - (f . y))) + (abs ((g . x) - (g . y)))) ) holds
(upper_bound (rng h)) - (lower_bound (rng h)) <= a * (((upper_bound (rng f)) - (lower_bound (rng f))) + ((upper_bound (rng g)) - (lower_bound (rng g))))
proof
let a be Real; ::_thesis: for A being non empty closed_interval Subset of REAL
for f, g, h being Function of A,REAL st f | A is bounded & g | A is bounded & a >= 0 & ( for x, y being Real st x in A & y in A holds
abs ((h . x) - (h . y)) <= a * ((abs ((f . x) - (f . y))) + (abs ((g . x) - (g . y)))) ) holds
(upper_bound (rng h)) - (lower_bound (rng h)) <= a * (((upper_bound (rng f)) - (lower_bound (rng f))) + ((upper_bound (rng g)) - (lower_bound (rng g))))
let A be non empty closed_interval Subset of REAL; ::_thesis: for f, g, h being Function of A,REAL st f | A is bounded & g | A is bounded & a >= 0 & ( for x, y being Real st x in A & y in A holds
abs ((h . x) - (h . y)) <= a * ((abs ((f . x) - (f . y))) + (abs ((g . x) - (g . y)))) ) holds
(upper_bound (rng h)) - (lower_bound (rng h)) <= a * (((upper_bound (rng f)) - (lower_bound (rng f))) + ((upper_bound (rng g)) - (lower_bound (rng g))))
let f, g, h be Function of A,REAL; ::_thesis: ( f | A is bounded & g | A is bounded & a >= 0 & ( for x, y being Real st x in A & y in A holds
abs ((h . x) - (h . y)) <= a * ((abs ((f . x) - (f . y))) + (abs ((g . x) - (g . y)))) ) implies (upper_bound (rng h)) - (lower_bound (rng h)) <= a * (((upper_bound (rng f)) - (lower_bound (rng f))) + ((upper_bound (rng g)) - (lower_bound (rng g)))) )
assume that
A1: f | A is bounded and
A2: g | A is bounded and
A3: a >= 0 and
A4: for x, y being Real st x in A & y in A holds
abs ((h . x) - (h . y)) <= a * ((abs ((f . x) - (f . y))) + (abs ((g . x) - (g . y)))) ; ::_thesis: (upper_bound (rng h)) - (lower_bound (rng h)) <= a * (((upper_bound (rng f)) - (lower_bound (rng f))) + ((upper_bound (rng g)) - (lower_bound (rng g))))
A5: rng g is bounded_above by A2, INTEGRA1:13;
A6: rng f is bounded_above by A1, INTEGRA1:13;
A7: dom g = A by FUNCT_2:def_1;
A8: rng g is bounded_below by A2, INTEGRA1:11;
A9: for x, y being Real st x in A & y in A holds
abs ((g . x) - (g . y)) <= (upper_bound (rng g)) - (lower_bound (rng g))
proof
let x, y be Real; ::_thesis: ( x in A & y in A implies abs ((g . x) - (g . y)) <= (upper_bound (rng g)) - (lower_bound (rng g)) )
assume that
A10: x in A and
A11: y in A ; ::_thesis: abs ((g . x) - (g . y)) <= (upper_bound (rng g)) - (lower_bound (rng g))
now__::_thesis:_abs_((g_._x)_-_(g_._y))_<=_(upper_bound_(rng_g))_-_(lower_bound_(rng_g))
percases ( g . x >= g . y or g . x < g . y ) ;
suppose g . x >= g . y ; ::_thesis: abs ((g . x) - (g . y)) <= (upper_bound (rng g)) - (lower_bound (rng g))
then (g . x) - (g . y) >= 0 by XREAL_1:48;
then abs ((g . x) - (g . y)) = (g . x) - (g . y) by ABSVALUE:def_1;
then A12: (abs ((g . x) - (g . y))) + (g . y) = g . x ;
g . y in rng g by A7, A11, FUNCT_1:def_3;
then A13: lower_bound (rng g) <= g . y by A8, SEQ_4:def_2;
g . x in rng g by A7, A10, FUNCT_1:def_3;
then g . x <= upper_bound (rng g) by A5, SEQ_4:def_1;
then g . y <= (upper_bound (rng g)) - (abs ((g . x) - (g . y))) by A12, XREAL_1:19;
then lower_bound (rng g) <= (upper_bound (rng g)) - (abs ((g . x) - (g . y))) by A13, XXREAL_0:2;
then (lower_bound (rng g)) + (abs ((g . x) - (g . y))) <= upper_bound (rng g) by XREAL_1:19;
hence abs ((g . x) - (g . y)) <= (upper_bound (rng g)) - (lower_bound (rng g)) by XREAL_1:19; ::_thesis: verum
end;
suppose g . x < g . y ; ::_thesis: abs ((g . x) - (g . y)) <= (upper_bound (rng g)) - (lower_bound (rng g))
then (g . x) - (g . y) < 0 by XREAL_1:49;
then abs ((g . x) - (g . y)) = - ((g . x) - (g . y)) by ABSVALUE:def_1
.= (g . y) - (g . x) ;
then A14: (abs ((g . x) - (g . y))) + (g . x) = g . y ;
g . x in rng g by A7, A10, FUNCT_1:def_3;
then A15: lower_bound (rng g) <= g . x by A8, SEQ_4:def_2;
g . y in rng g by A7, A11, FUNCT_1:def_3;
then g . y <= upper_bound (rng g) by A5, SEQ_4:def_1;
then g . x <= (upper_bound (rng g)) - (abs ((g . x) - (g . y))) by A14, XREAL_1:19;
then lower_bound (rng g) <= (upper_bound (rng g)) - (abs ((g . x) - (g . y))) by A15, XXREAL_0:2;
then (lower_bound (rng g)) + (abs ((g . x) - (g . y))) <= upper_bound (rng g) by XREAL_1:19;
hence abs ((g . x) - (g . y)) <= (upper_bound (rng g)) - (lower_bound (rng g)) by XREAL_1:19; ::_thesis: verum
end;
end;
end;
hence abs ((g . x) - (g . y)) <= (upper_bound (rng g)) - (lower_bound (rng g)) ; ::_thesis: verum
end;
A16: dom f = A by FUNCT_2:def_1;
A17: rng f is bounded_below by A1, INTEGRA1:11;
A18: for x, y being Real st x in A & y in A holds
abs ((f . x) - (f . y)) <= (upper_bound (rng f)) - (lower_bound (rng f))
proof
let x, y be Real; ::_thesis: ( x in A & y in A implies abs ((f . x) - (f . y)) <= (upper_bound (rng f)) - (lower_bound (rng f)) )
assume that
A19: x in A and
A20: y in A ; ::_thesis: abs ((f . x) - (f . y)) <= (upper_bound (rng f)) - (lower_bound (rng f))
now__::_thesis:_abs_((f_._x)_-_(f_._y))_<=_(upper_bound_(rng_f))_-_(lower_bound_(rng_f))
percases ( f . x >= f . y or f . x < f . y ) ;
suppose f . x >= f . y ; ::_thesis: abs ((f . x) - (f . y)) <= (upper_bound (rng f)) - (lower_bound (rng f))
then (f . x) - (f . y) >= 0 by XREAL_1:48;
then abs ((f . x) - (f . y)) = (f . x) - (f . y) by ABSVALUE:def_1;
then A21: (abs ((f . x) - (f . y))) + (f . y) = f . x ;
f . y in rng f by A16, A20, FUNCT_1:def_3;
then A22: lower_bound (rng f) <= f . y by A17, SEQ_4:def_2;
f . x in rng f by A16, A19, FUNCT_1:def_3;
then f . x <= upper_bound (rng f) by A6, SEQ_4:def_1;
then f . y <= (upper_bound (rng f)) - (abs ((f . x) - (f . y))) by A21, XREAL_1:19;
then lower_bound (rng f) <= (upper_bound (rng f)) - (abs ((f . x) - (f . y))) by A22, XXREAL_0:2;
then (lower_bound (rng f)) + (abs ((f . x) - (f . y))) <= upper_bound (rng f) by XREAL_1:19;
hence abs ((f . x) - (f . y)) <= (upper_bound (rng f)) - (lower_bound (rng f)) by XREAL_1:19; ::_thesis: verum
end;
suppose f . x < f . y ; ::_thesis: abs ((f . x) - (f . y)) <= (upper_bound (rng f)) - (lower_bound (rng f))
then (f . x) - (f . y) < 0 by XREAL_1:49;
then abs ((f . x) - (f . y)) = - ((f . x) - (f . y)) by ABSVALUE:def_1
.= (f . y) - (f . x) ;
then A23: (abs ((f . x) - (f . y))) + (f . x) = f . y ;
f . x in rng f by A16, A19, FUNCT_1:def_3;
then A24: lower_bound (rng f) <= f . x by A17, SEQ_4:def_2;
f . y in rng f by A16, A20, FUNCT_1:def_3;
then f . y <= upper_bound (rng f) by A6, SEQ_4:def_1;
then f . x <= (upper_bound (rng f)) - (abs ((f . x) - (f . y))) by A23, XREAL_1:19;
then lower_bound (rng f) <= (upper_bound (rng f)) - (abs ((f . x) - (f . y))) by A24, XXREAL_0:2;
then (lower_bound (rng f)) + (abs ((f . x) - (f . y))) <= upper_bound (rng f) by XREAL_1:19;
hence abs ((f . x) - (f . y)) <= (upper_bound (rng f)) - (lower_bound (rng f)) by XREAL_1:19; ::_thesis: verum
end;
end;
end;
hence abs ((f . x) - (f . y)) <= (upper_bound (rng f)) - (lower_bound (rng f)) ; ::_thesis: verum
end;
for x, y being Real st x in A & y in A holds
abs ((h . x) - (h . y)) <= a * (((upper_bound (rng f)) - (lower_bound (rng f))) + ((upper_bound (rng g)) - (lower_bound (rng g))))
proof
let x, y be Real; ::_thesis: ( x in A & y in A implies abs ((h . x) - (h . y)) <= a * (((upper_bound (rng f)) - (lower_bound (rng f))) + ((upper_bound (rng g)) - (lower_bound (rng g)))) )
assume that
A25: x in A and
A26: y in A ; ::_thesis: abs ((h . x) - (h . y)) <= a * (((upper_bound (rng f)) - (lower_bound (rng f))) + ((upper_bound (rng g)) - (lower_bound (rng g))))
A27: a * (abs ((g . x) - (g . y))) <= a * ((upper_bound (rng g)) - (lower_bound (rng g))) by A3, A9, A25, A26, XREAL_1:64;
a * (abs ((f . x) - (f . y))) <= a * ((upper_bound (rng f)) - (lower_bound (rng f))) by A3, A18, A25, A26, XREAL_1:64;
then A28: (a * (abs ((f . x) - (f . y)))) + (a * (abs ((g . x) - (g . y)))) <= (a * ((upper_bound (rng f)) - (lower_bound (rng f)))) + (a * ((upper_bound (rng g)) - (lower_bound (rng g)))) by A27, XREAL_1:7;
abs ((h . x) - (h . y)) <= a * ((abs ((f . x) - (f . y))) + (abs ((g . x) - (g . y)))) by A4, A25, A26;
hence abs ((h . x) - (h . y)) <= a * (((upper_bound (rng f)) - (lower_bound (rng f))) + ((upper_bound (rng g)) - (lower_bound (rng g)))) by A28, XXREAL_0:2; ::_thesis: verum
end;
hence (upper_bound (rng h)) - (lower_bound (rng h)) <= a * (((upper_bound (rng f)) - (lower_bound (rng f))) + ((upper_bound (rng g)) - (lower_bound (rng g)))) by Th24; ::_thesis: verum
end;
theorem Th27: :: INTEGRA4:27
for a being Real
for A being non empty closed_interval Subset of REAL
for f, g being Function of A,REAL st f | A is bounded & f is integrable & g | A is bounded & a > 0 & ( for x, y being Real st x in A & y in A holds
abs ((g . x) - (g . y)) <= a * (abs ((f . x) - (f . y))) ) holds
g is integrable
proof
let a be Real; ::_thesis: for A being non empty closed_interval Subset of REAL
for f, g being Function of A,REAL st f | A is bounded & f is integrable & g | A is bounded & a > 0 & ( for x, y being Real st x in A & y in A holds
abs ((g . x) - (g . y)) <= a * (abs ((f . x) - (f . y))) ) holds
g is integrable
let A be non empty closed_interval Subset of REAL; ::_thesis: for f, g being Function of A,REAL st f | A is bounded & f is integrable & g | A is bounded & a > 0 & ( for x, y being Real st x in A & y in A holds
abs ((g . x) - (g . y)) <= a * (abs ((f . x) - (f . y))) ) holds
g is integrable
let f, g be Function of A,REAL; ::_thesis: ( f | A is bounded & f is integrable & g | A is bounded & a > 0 & ( for x, y being Real st x in A & y in A holds
abs ((g . x) - (g . y)) <= a * (abs ((f . x) - (f . y))) ) implies g is integrable )
assume that
A1: f | A is bounded and
A2: f is integrable and
A3: g | A is bounded and
A4: a > 0 and
A5: for x, y being Real st x in A & y in A holds
abs ((g . x) - (g . y)) <= a * (abs ((f . x) - (f . y))) ; ::_thesis: g is integrable
for T being DivSequence of A st delta T is convergent & lim (delta T) = 0 holds
(lim (upper_sum (g,T))) - (lim (lower_sum (g,T))) = 0
proof
let T be DivSequence of A; ::_thesis: ( delta T is convergent & lim (delta T) = 0 implies (lim (upper_sum (g,T))) - (lim (lower_sum (g,T))) = 0 )
assume that
A6: delta T is convergent and
A7: lim (delta T) = 0 ; ::_thesis: (lim (upper_sum (g,T))) - (lim (lower_sum (g,T))) = 0
A8: lower_sum (f,T) is convergent by A1, A6, A7, Th8;
A9: upper_sum (f,T) is convergent by A1, A6, A7, Th9;
then A10: (upper_sum (f,T)) - (lower_sum (f,T)) is convergent by A8;
reconsider osc1 = (upper_sum (g,T)) - (lower_sum (g,T)) as Real_Sequence ;
reconsider osc = (upper_sum (f,T)) - (lower_sum (f,T)) as Real_Sequence ;
(lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = 0 by A1, A2, A6, A7, Th12;
then A11: lim ((upper_sum (f,T)) - (lower_sum (f,T))) = 0 by A9, A8, SEQ_2:12;
A12: for b being real number st 0 < b holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((osc1 . m) - 0) < b
proof
let b be real number ; ::_thesis: ( 0 < b implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((osc1 . m) - 0) < b )
assume b > 0 ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((osc1 . m) - 0) < b
then b / a > 0 by A4, XREAL_1:139;
then consider n being Element of NAT such that
A13: for m being Element of NAT st n <= m holds
abs ((osc . m) - 0) < b / a by A10, A11, SEQ_2:def_7;
for m being Element of NAT st n <= m holds
abs ((osc1 . m) - 0) < b
proof
let m be Element of NAT ; ::_thesis: ( n <= m implies abs ((osc1 . m) - 0) < b )
reconsider D = T . m as Division of A ;
len (upper_volume (f,D)) = len D by INTEGRA1:def_6;
then reconsider UV = upper_volume (f,D) as Element of (len D) -tuples_on REAL by FINSEQ_2:133;
len (lower_volume (f,D)) = len D by INTEGRA1:def_7;
then reconsider LV = lower_volume (f,D) as Element of (len D) -tuples_on REAL by FINSEQ_2:133;
osc . m = ((upper_sum (f,T)) . m) + ((- (lower_sum (f,T))) . m) by SEQ_1:7
.= ((upper_sum (f,T)) . m) + (- ((lower_sum (f,T)) . m)) by SEQ_1:10
.= ((upper_sum (f,T)) . m) - ((lower_sum (f,T)) . m)
.= (upper_sum (f,(T . m))) - ((lower_sum (f,T)) . m) by INTEGRA2:def_2
.= (upper_sum (f,(T . m))) - (lower_sum (f,(T . m))) by INTEGRA2:def_3
.= (Sum (upper_volume (f,D))) - (lower_sum (f,(T . m))) by INTEGRA1:def_8
.= (Sum (upper_volume (f,D))) - (Sum (lower_volume (f,D))) by INTEGRA1:def_9 ;
then A14: osc . m = Sum (UV - LV) by RVSUM_1:90;
assume n <= m ; ::_thesis: abs ((osc1 . m) - 0) < b
then A15: abs ((osc . m) - 0) < b / a by A13;
len (lower_volume (g,D)) = len D by INTEGRA1:def_7;
then reconsider LV1 = lower_volume (g,D) as Element of (len D) -tuples_on REAL by FINSEQ_2:133;
len (upper_volume (g,D)) = len D by INTEGRA1:def_6;
then reconsider UV1 = upper_volume (g,D) as Element of (len D) -tuples_on REAL by FINSEQ_2:133;
reconsider F = UV1 - LV1 as FinSequence of REAL ;
osc1 . m = ((upper_sum (g,T)) . m) + ((- (lower_sum (g,T))) . m) by SEQ_1:7
.= ((upper_sum (g,T)) . m) + (- ((lower_sum (g,T)) . m)) by SEQ_1:10
.= ((upper_sum (g,T)) . m) - ((lower_sum (g,T)) . m)
.= (upper_sum (g,(T . m))) - ((lower_sum (g,T)) . m) by INTEGRA2:def_2
.= (upper_sum (g,(T . m))) - (lower_sum (g,(T . m))) by INTEGRA2:def_3
.= (Sum (upper_volume (g,D))) - (lower_sum (g,(T . m))) by INTEGRA1:def_8
.= (Sum (upper_volume (g,D))) - (Sum (lower_volume (g,D))) by INTEGRA1:def_9 ;
then A16: osc1 . m = Sum (UV1 - LV1) by RVSUM_1:90;
for j being Nat st j in dom F holds
0 <= F . j
proof
let j be Nat; ::_thesis: ( j in dom F implies 0 <= F . j )
set r = F . j;
A17: rng g is bounded_below by A3, INTEGRA1:11;
assume A18: j in dom F ; ::_thesis: 0 <= F . j
j in Seg (len F) by A18, FINSEQ_1:def_3;
then A19: j in Seg (len D) by CARD_1:def_7;
then A20: j in dom D by FINSEQ_1:def_3;
then A21: LV1 . j = (lower_bound (rng (g | (divset (D,j))))) * (vol (divset (D,j))) by INTEGRA1:def_7;
A22: ex r being Real st r in rng (g | (divset (D,j)))
proof
consider r being Real such that
A23: r in divset (D,j) by SUBSET_1:4;
j in dom D by A19, FINSEQ_1:def_3;
then divset (D,j) c= A by INTEGRA1:8;
then r in A by A23;
then r in dom g by FUNCT_2:def_1;
then r in (dom g) /\ (divset (D,j)) by A23, XBOOLE_0:def_4;
then r in dom (g | (divset (D,j))) by RELAT_1:61;
then (g | (divset (D,j))) . r in rng (g | (divset (D,j))) by FUNCT_1:def_3;
hence ex r being Real st r in rng (g | (divset (D,j))) ; ::_thesis: verum
end;
rng g is bounded_above by A3, INTEGRA1:13;
then rng (g | (divset (D,j))) is real-bounded by A17, RELAT_1:70, XXREAL_2:45;
then A24: (upper_bound (rng (g | (divset (D,j))))) - (lower_bound (rng (g | (divset (D,j))))) >= 0 by A22, SEQ_4:11, XREAL_1:48;
UV1 . j = (upper_bound (rng (g | (divset (D,j))))) * (vol (divset (D,j))) by A20, INTEGRA1:def_6;
then A25: F . j = ((upper_bound (rng (g | (divset (D,j))))) * (vol (divset (D,j)))) - ((lower_bound (rng (g | (divset (D,j))))) * (vol (divset (D,j)))) by A18, A21, VALUED_1:13
.= ((upper_bound (rng (g | (divset (D,j))))) - (lower_bound (rng (g | (divset (D,j)))))) * (vol (divset (D,j))) ;
vol (divset (D,j)) >= 0 by INTEGRA1:9;
hence 0 <= F . j by A25, A24; ::_thesis: verum
end;
then A26: osc1 . m >= 0 by A16, RVSUM_1:84;
then A27: abs (osc1 . m) = osc1 . m by ABSVALUE:def_1;
for j being Nat st j in Seg (len D) holds
(UV1 - LV1) . j <= (a * (UV - LV)) . j
proof
let j be Nat; ::_thesis: ( j in Seg (len D) implies (UV1 - LV1) . j <= (a * (UV - LV)) . j )
set x = (UV1 - LV1) . j;
set y = (a * (UV - LV)) . j;
A28: (a * (UV - LV)) . j = a * ((UV - LV) . j) by RVSUM_1:45;
assume A29: j in Seg (len D) ; ::_thesis: (UV1 - LV1) . j <= (a * (UV - LV)) . j
then A30: j in dom D by FINSEQ_1:def_3;
then A31: LV1 . j = (lower_bound (rng (g | (divset (D,j))))) * (vol (divset (D,j))) by INTEGRA1:def_7;
A32: a * ((upper_bound (rng (f | (divset (D,j))))) - (lower_bound (rng (f | (divset (D,j)))))) >= (upper_bound (rng (g | (divset (D,j))))) - (lower_bound (rng (g | (divset (D,j)))))
proof
A33: j in dom D by A29, FINSEQ_1:def_3;
then A34: (f | (divset (D,j))) | (divset (D,j)) is bounded_below by A1, INTEGRA1:8, INTEGRA2:6;
A35: dom (g | (divset (D,j))) = (dom g) /\ (divset (D,j)) by RELAT_1:61
.= A /\ (divset (D,j)) by FUNCT_2:def_1
.= divset (D,j) by A33, INTEGRA1:8, XBOOLE_1:28 ;
then reconsider g1 = g | (divset (D,j)) as PartFunc of (divset (D,j)),REAL by RELSET_1:5;
A36: dom (f | (divset (D,j))) = (dom f) /\ (divset (D,j)) by RELAT_1:61
.= A /\ (divset (D,j)) by FUNCT_2:def_1
.= divset (D,j) by A33, INTEGRA1:8, XBOOLE_1:28 ;
then reconsider f1 = f | (divset (D,j)) as PartFunc of (divset (D,j)),REAL by RELSET_1:5;
reconsider g1 = g1 as Function of (divset (D,j)),REAL by A35, FUNCT_2:def_1;
reconsider f1 = f1 as Function of (divset (D,j)),REAL by A36, FUNCT_2:def_1;
A37: divset (D,j) c= A by A33, INTEGRA1:8;
A38: for x, y being Real st x in divset (D,j) & y in divset (D,j) holds
abs ((g1 . x) - (g1 . y)) <= a * (abs ((f1 . x) - (f1 . y)))
proof
let x, y be Real; ::_thesis: ( x in divset (D,j) & y in divset (D,j) implies abs ((g1 . x) - (g1 . y)) <= a * (abs ((f1 . x) - (f1 . y))) )
assume that
A39: x in divset (D,j) and
A40: y in divset (D,j) ; ::_thesis: abs ((g1 . x) - (g1 . y)) <= a * (abs ((f1 . x) - (f1 . y)))
A41: g . y = g1 . y by A35, A40, FUNCT_1:47;
A42: f . y = f1 . y by A36, A40, FUNCT_1:47;
A43: f . x = f1 . x by A36, A39, FUNCT_1:47;
g . x = g1 . x by A35, A39, FUNCT_1:47;
hence abs ((g1 . x) - (g1 . y)) <= a * (abs ((f1 . x) - (f1 . y))) by A5, A37, A39, A40, A41, A43, A42; ::_thesis: verum
end;
(f | (divset (D,j))) | (divset (D,j)) is bounded_above by A1, A33, INTEGRA1:8, INTEGRA2:5;
then f1 | (divset (D,j)) is bounded by A34;
hence a * ((upper_bound (rng (f | (divset (D,j))))) - (lower_bound (rng (f | (divset (D,j)))))) >= (upper_bound (rng (g | (divset (D,j))))) - (lower_bound (rng (g | (divset (D,j))))) by A4, A38, Th25; ::_thesis: verum
end;
vol (divset (D,j)) >= 0 by INTEGRA1:9;
then A44: (a * ((upper_bound (rng (f | (divset (D,j))))) - (lower_bound (rng (f | (divset (D,j))))))) * (vol (divset (D,j))) >= ((upper_bound (rng (g | (divset (D,j))))) - (lower_bound (rng (g | (divset (D,j)))))) * (vol (divset (D,j))) by A32, XREAL_1:64;
UV1 . j = (upper_bound (rng (g | (divset (D,j))))) * (vol (divset (D,j))) by A30, INTEGRA1:def_6;
then A45: (UV1 - LV1) . j = ((upper_bound (rng (g | (divset (D,j))))) * (vol (divset (D,j)))) - ((lower_bound (rng (g | (divset (D,j))))) * (vol (divset (D,j)))) by A31, RVSUM_1:27
.= ((upper_bound (rng (g | (divset (D,j))))) - (lower_bound (rng (g | (divset (D,j)))))) * (vol (divset (D,j))) ;
A46: LV . j = (lower_bound (rng (f | (divset (D,j))))) * (vol (divset (D,j))) by A30, INTEGRA1:def_7;
UV . j = (upper_bound (rng (f | (divset (D,j))))) * (vol (divset (D,j))) by A30, INTEGRA1:def_6;
then (a * (UV - LV)) . j = a * (((upper_bound (rng (f | (divset (D,j))))) * (vol (divset (D,j)))) - ((lower_bound (rng (f | (divset (D,j))))) * (vol (divset (D,j))))) by A46, A28, RVSUM_1:27
.= a * (((upper_bound (rng (f | (divset (D,j))))) - (lower_bound (rng (f | (divset (D,j)))))) * (vol (divset (D,j)))) ;
hence (UV1 - LV1) . j <= (a * (UV - LV)) . j by A45, A44; ::_thesis: verum
end;
then osc1 . m <= Sum (a * (UV - LV)) by A16, RVSUM_1:82;
then A47: osc1 . m <= a * (osc . m) by A14, RVSUM_1:87;
then osc . m >= 0 / a by A4, A26, XREAL_1:79;
then abs (osc . m) = osc . m by ABSVALUE:def_1;
then a * (osc . m) < a * (b / a) by A4, A15, XREAL_1:68;
then a * (osc . m) < b by A4, XCMPLX_1:87;
hence abs ((osc1 . m) - 0) < b by A47, A27, XXREAL_0:2; ::_thesis: verum
end;
hence ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((osc1 . m) - 0) < b ; ::_thesis: verum
end;
then osc1 is convergent by SEQ_2:def_6;
then A48: lim ((upper_sum (g,T)) - (lower_sum (g,T))) = 0 by A12, SEQ_2:def_7;
A49: lower_sum (g,T) is convergent by A3, A6, A7, Th8;
upper_sum (g,T) is convergent by A3, A6, A7, Th9;
hence (lim (upper_sum (g,T))) - (lim (lower_sum (g,T))) = 0 by A49, A48, SEQ_2:12; ::_thesis: verum
end;
hence g is integrable by A3, Th12; ::_thesis: verum
end;
theorem Th28: :: INTEGRA4:28
for a being Real
for A being non empty closed_interval Subset of REAL
for f, g, h being Function of A,REAL st f | A is bounded & f is integrable & g | A is bounded & g is integrable & h | A is bounded & a > 0 & ( for x, y being Real st x in A & y in A holds
abs ((h . x) - (h . y)) <= a * ((abs ((f . x) - (f . y))) + (abs ((g . x) - (g . y)))) ) holds
h is integrable
proof
let a be Real; ::_thesis: for A being non empty closed_interval Subset of REAL
for f, g, h being Function of A,REAL st f | A is bounded & f is integrable & g | A is bounded & g is integrable & h | A is bounded & a > 0 & ( for x, y being Real st x in A & y in A holds
abs ((h . x) - (h . y)) <= a * ((abs ((f . x) - (f . y))) + (abs ((g . x) - (g . y)))) ) holds
h is integrable
let A be non empty closed_interval Subset of REAL; ::_thesis: for f, g, h being Function of A,REAL st f | A is bounded & f is integrable & g | A is bounded & g is integrable & h | A is bounded & a > 0 & ( for x, y being Real st x in A & y in A holds
abs ((h . x) - (h . y)) <= a * ((abs ((f . x) - (f . y))) + (abs ((g . x) - (g . y)))) ) holds
h is integrable
let f, g, h be Function of A,REAL; ::_thesis: ( f | A is bounded & f is integrable & g | A is bounded & g is integrable & h | A is bounded & a > 0 & ( for x, y being Real st x in A & y in A holds
abs ((h . x) - (h . y)) <= a * ((abs ((f . x) - (f . y))) + (abs ((g . x) - (g . y)))) ) implies h is integrable )
assume that
A1: f | A is bounded and
A2: f is integrable and
A3: g | A is bounded and
A4: g is integrable and
A5: h | A is bounded and
A6: a > 0 and
A7: for x, y being Real st x in A & y in A holds
abs ((h . x) - (h . y)) <= a * ((abs ((f . x) - (f . y))) + (abs ((g . x) - (g . y)))) ; ::_thesis: h is integrable
for T being DivSequence of A st delta T is convergent & lim (delta T) = 0 holds
(lim (upper_sum (h,T))) - (lim (lower_sum (h,T))) = 0
proof
let T be DivSequence of A; ::_thesis: ( delta T is convergent & lim (delta T) = 0 implies (lim (upper_sum (h,T))) - (lim (lower_sum (h,T))) = 0 )
assume that
A8: delta T is convergent and
A9: lim (delta T) = 0 ; ::_thesis: (lim (upper_sum (h,T))) - (lim (lower_sum (h,T))) = 0
A10: lower_sum (g,T) is convergent by A3, A8, A9, Th8;
A11: upper_sum (g,T) is convergent by A3, A8, A9, Th9;
then A12: (upper_sum (g,T)) - (lower_sum (g,T)) is convergent by A10;
(lim (upper_sum (g,T))) - (lim (lower_sum (g,T))) = 0 by A3, A4, A8, A9, Th12;
then A13: lim ((upper_sum (g,T)) - (lower_sum (g,T))) = 0 by A11, A10, SEQ_2:12;
A14: lower_sum (f,T) is convergent by A1, A8, A9, Th8;
reconsider osc2 = (upper_sum (h,T)) - (lower_sum (h,T)) as Real_Sequence ;
reconsider osc1 = (upper_sum (g,T)) - (lower_sum (g,T)) as Real_Sequence ;
reconsider osc = (upper_sum (f,T)) - (lower_sum (f,T)) as Real_Sequence ;
A15: upper_sum (f,T) is convergent by A1, A8, A9, Th9;
(lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = 0 by A1, A2, A8, A9, Th12;
then A16: lim ((upper_sum (f,T)) - (lower_sum (f,T))) = 0 by A15, A14, SEQ_2:12;
A17: (upper_sum (f,T)) - (lower_sum (f,T)) is convergent by A15, A14;
A18: for b being real number st 0 < b holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((osc2 . m) - 0) < b
proof
let b be real number ; ::_thesis: ( 0 < b implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((osc2 . m) - 0) < b )
assume b > 0 ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((osc2 . m) - 0) < b
then b / a > 0 by A6, XREAL_1:139;
then A19: (b / a) / 2 > 0 by XREAL_1:139;
then consider n1 being Element of NAT such that
A20: for m being Element of NAT st n1 <= m holds
abs ((osc . m) - 0) < (b / a) / 2 by A17, A16, SEQ_2:def_7;
consider n2 being Element of NAT such that
A21: for m being Element of NAT st n2 <= m holds
abs ((osc1 . m) - 0) < (b / a) / 2 by A12, A13, A19, SEQ_2:def_7;
ex n being Element of NAT st
( n1 <= n & n2 <= n )
proof
take n = max (n1,n2); ::_thesis: ( n is Element of REAL & n is Element of NAT & n1 <= n & n2 <= n )
reconsider n = n as Element of NAT by XXREAL_0:16;
n1 <= n by XXREAL_0:25;
hence ( n is Element of REAL & n is Element of NAT & n1 <= n & n2 <= n ) by XXREAL_0:25; ::_thesis: verum
end;
then consider n being Element of NAT such that
A22: n1 <= n and
A23: n2 <= n ;
for m being Element of NAT st n <= m holds
abs ((osc2 . m) - 0) < b
proof
let m be Element of NAT ; ::_thesis: ( n <= m implies abs ((osc2 . m) - 0) < b )
reconsider D = T . m as Division of A ;
len (upper_volume (f,D)) = len D by INTEGRA1:def_6;
then reconsider UV = upper_volume (f,D) as Element of (len D) -tuples_on REAL by FINSEQ_2:133;
len (lower_volume (f,D)) = len D by INTEGRA1:def_7;
then reconsider LV = lower_volume (f,D) as Element of (len D) -tuples_on REAL by FINSEQ_2:133;
osc . m = ((upper_sum (f,T)) . m) + ((- (lower_sum (f,T))) . m) by SEQ_1:7
.= ((upper_sum (f,T)) . m) + (- ((lower_sum (f,T)) . m)) by SEQ_1:10
.= ((upper_sum (f,T)) . m) - ((lower_sum (f,T)) . m)
.= (upper_sum (f,(T . m))) - ((lower_sum (f,T)) . m) by INTEGRA2:def_2
.= (upper_sum (f,(T . m))) - (lower_sum (f,(T . m))) by INTEGRA2:def_3
.= (Sum (upper_volume (f,D))) - (lower_sum (f,(T . m))) by INTEGRA1:def_8
.= (Sum (upper_volume (f,D))) - (Sum (lower_volume (f,D))) by INTEGRA1:def_9 ;
then A24: osc . m = Sum (UV - LV) by RVSUM_1:90;
len (lower_volume (h,D)) = len D by INTEGRA1:def_7;
then reconsider LV2 = lower_volume (h,D) as Element of (len D) -tuples_on REAL by FINSEQ_2:133;
len (upper_volume (h,D)) = len D by INTEGRA1:def_6;
then reconsider UV2 = upper_volume (h,D) as Element of (len D) -tuples_on REAL by FINSEQ_2:133;
len (lower_volume (g,D)) = len D by INTEGRA1:def_7;
then reconsider LV1 = lower_volume (g,D) as Element of (len D) -tuples_on REAL by FINSEQ_2:133;
len (upper_volume (g,D)) = len D by INTEGRA1:def_6;
then reconsider UV1 = upper_volume (g,D) as Element of (len D) -tuples_on REAL by FINSEQ_2:133;
reconsider H = UV - LV as FinSequence of REAL ;
reconsider G = UV1 - LV1 as FinSequence of REAL ;
reconsider F = UV2 - LV2 as FinSequence of REAL ;
osc1 . m = ((upper_sum (g,T)) . m) + ((- (lower_sum (g,T))) . m) by SEQ_1:7
.= ((upper_sum (g,T)) . m) + (- ((lower_sum (g,T)) . m)) by SEQ_1:10
.= ((upper_sum (g,T)) . m) - ((lower_sum (g,T)) . m)
.= (upper_sum (g,(T . m))) - ((lower_sum (g,T)) . m) by INTEGRA2:def_2
.= (upper_sum (g,(T . m))) - (lower_sum (g,(T . m))) by INTEGRA2:def_3
.= (Sum (upper_volume (g,D))) - (lower_sum (g,(T . m))) by INTEGRA1:def_8
.= (Sum (upper_volume (g,D))) - (Sum (lower_volume (g,D))) by INTEGRA1:def_9 ;
then A25: osc1 . m = Sum (UV1 - LV1) by RVSUM_1:90;
for j being Nat st j in dom G holds
0 <= G . j
proof
let j be Nat; ::_thesis: ( j in dom G implies 0 <= G . j )
set r = G . j;
A26: rng g is bounded_below by A3, INTEGRA1:11;
assume A27: j in dom G ; ::_thesis: 0 <= G . j
j in Seg (len G) by A27, FINSEQ_1:def_3;
then A28: j in Seg (len D) by CARD_1:def_7;
then A29: j in dom D by FINSEQ_1:def_3;
then A30: LV1 . j = (lower_bound (rng (g | (divset (D,j))))) * (vol (divset (D,j))) by INTEGRA1:def_7;
A31: ex r being Real st r in rng (g | (divset (D,j)))
proof
consider r being Real such that
A32: r in divset (D,j) by SUBSET_1:4;
j in dom D by A28, FINSEQ_1:def_3;
then divset (D,j) c= A by INTEGRA1:8;
then r in A by A32;
then r in dom g by FUNCT_2:def_1;
then r in (dom g) /\ (divset (D,j)) by A32, XBOOLE_0:def_4;
then r in dom (g | (divset (D,j))) by RELAT_1:61;
then (g | (divset (D,j))) . r in rng (g | (divset (D,j))) by FUNCT_1:def_3;
hence ex r being Real st r in rng (g | (divset (D,j))) ; ::_thesis: verum
end;
rng g is bounded_above by A3, INTEGRA1:13;
then rng (g | (divset (D,j))) is real-bounded by A26, RELAT_1:70, XXREAL_2:45;
then A33: (upper_bound (rng (g | (divset (D,j))))) - (lower_bound (rng (g | (divset (D,j))))) >= 0 by A31, SEQ_4:11, XREAL_1:48;
UV1 . j = (upper_bound (rng (g | (divset (D,j))))) * (vol (divset (D,j))) by A29, INTEGRA1:def_6;
then A34: G . j = ((upper_bound (rng (g | (divset (D,j))))) * (vol (divset (D,j)))) - ((lower_bound (rng (g | (divset (D,j))))) * (vol (divset (D,j)))) by A27, A30, VALUED_1:13
.= ((upper_bound (rng (g | (divset (D,j))))) - (lower_bound (rng (g | (divset (D,j)))))) * (vol (divset (D,j))) ;
vol (divset (D,j)) >= 0 by INTEGRA1:9;
hence 0 <= G . j by A34, A33; ::_thesis: verum
end;
then A35: osc1 . m >= 0 by A25, RVSUM_1:84;
assume A36: n <= m ; ::_thesis: abs ((osc2 . m) - 0) < b
then n1 <= m by A22, XXREAL_0:2;
then A37: abs ((osc . m) - 0) < (b / a) / 2 by A20;
n2 <= m by A23, A36, XXREAL_0:2;
then A38: abs ((osc1 . m) - 0) < (b / a) / 2 by A21;
for j being Nat st j in dom H holds
0 <= H . j
proof
let j be Nat; ::_thesis: ( j in dom H implies 0 <= H . j )
set r = H . j;
A39: rng f is bounded_below by A1, INTEGRA1:11;
assume A40: j in dom H ; ::_thesis: 0 <= H . j
j in Seg (len H) by A40, FINSEQ_1:def_3;
then A41: j in Seg (len D) by CARD_1:def_7;
then A42: j in dom D by FINSEQ_1:def_3;
then A43: LV . j = (lower_bound (rng (f | (divset (D,j))))) * (vol (divset (D,j))) by INTEGRA1:def_7;
A44: ex r being Real st r in rng (f | (divset (D,j)))
proof
consider r being Real such that
A45: r in divset (D,j) by SUBSET_1:4;
j in dom D by A41, FINSEQ_1:def_3;
then divset (D,j) c= A by INTEGRA1:8;
then r in A by A45;
then r in dom f by FUNCT_2:def_1;
then r in (dom f) /\ (divset (D,j)) by A45, XBOOLE_0:def_4;
then r in dom (f | (divset (D,j))) by RELAT_1:61;
then (f | (divset (D,j))) . r in rng (f | (divset (D,j))) by FUNCT_1:def_3;
hence ex r being Real st r in rng (f | (divset (D,j))) ; ::_thesis: verum
end;
rng f is bounded_above by A1, INTEGRA1:13;
then rng (f | (divset (D,j))) is real-bounded by A39, RELAT_1:70, XXREAL_2:45;
then A46: (upper_bound (rng (f | (divset (D,j))))) - (lower_bound (rng (f | (divset (D,j))))) >= 0 by A44, SEQ_4:11, XREAL_1:48;
UV . j = (upper_bound (rng (f | (divset (D,j))))) * (vol (divset (D,j))) by A42, INTEGRA1:def_6;
then A47: H . j = ((upper_bound (rng (f | (divset (D,j))))) * (vol (divset (D,j)))) - ((lower_bound (rng (f | (divset (D,j))))) * (vol (divset (D,j)))) by A40, A43, VALUED_1:13
.= ((upper_bound (rng (f | (divset (D,j))))) - (lower_bound (rng (f | (divset (D,j)))))) * (vol (divset (D,j))) ;
vol (divset (D,j)) >= 0 by INTEGRA1:9;
hence 0 <= H . j by A47, A46; ::_thesis: verum
end;
then A48: osc . m >= 0 by A24, RVSUM_1:84;
then (osc . m) * (osc1 . m) >= 0 by A35;
then (abs (osc . m)) + (abs (osc1 . m)) = abs ((osc . m) + (osc1 . m)) by ABSVALUE:11;
then (abs ((osc . m) - 0)) + (abs (osc1 . m)) = (osc . m) + (osc1 . m) by A48, A35, ABSVALUE:def_1;
then (osc . m) + (osc1 . m) < ((b / a) / 2) + ((b / a) / 2) by A37, A38, XREAL_1:8;
then a * ((osc . m) + (osc1 . m)) < a * (b / a) by A6, XREAL_1:68;
then A49: a * ((osc . m) + (osc1 . m)) < b by A6, XCMPLX_1:87;
osc2 . m = ((upper_sum (h,T)) . m) + ((- (lower_sum (h,T))) . m) by SEQ_1:7
.= ((upper_sum (h,T)) . m) + (- ((lower_sum (h,T)) . m)) by SEQ_1:10
.= ((upper_sum (h,T)) . m) - ((lower_sum (h,T)) . m)
.= (upper_sum (h,(T . m))) - ((lower_sum (h,T)) . m) by INTEGRA2:def_2
.= (upper_sum (h,(T . m))) - (lower_sum (h,(T . m))) by INTEGRA2:def_3
.= (Sum (upper_volume (h,D))) - (lower_sum (h,(T . m))) by INTEGRA1:def_8
.= (Sum (upper_volume (h,D))) - (Sum (lower_volume (h,D))) by INTEGRA1:def_9 ;
then A50: osc2 . m = Sum (UV2 - LV2) by RVSUM_1:90;
for j being Nat st j in dom F holds
0 <= F . j
proof
let j be Nat; ::_thesis: ( j in dom F implies 0 <= F . j )
set r = F . j;
A51: rng h is bounded_below by A5, INTEGRA1:11;
assume A52: j in dom F ; ::_thesis: 0 <= F . j
j in Seg (len F) by A52, FINSEQ_1:def_3;
then A53: j in Seg (len D) by CARD_1:def_7;
then A54: j in dom D by FINSEQ_1:def_3;
then A55: LV2 . j = (lower_bound (rng (h | (divset (D,j))))) * (vol (divset (D,j))) by INTEGRA1:def_7;
A56: ex r being Real st r in rng (h | (divset (D,j)))
proof
consider r being Real such that
A57: r in divset (D,j) by SUBSET_1:4;
j in dom D by A53, FINSEQ_1:def_3;
then divset (D,j) c= A by INTEGRA1:8;
then r in A by A57;
then r in dom h by FUNCT_2:def_1;
then r in (dom h) /\ (divset (D,j)) by A57, XBOOLE_0:def_4;
then r in dom (h | (divset (D,j))) by RELAT_1:61;
then (h | (divset (D,j))) . r in rng (h | (divset (D,j))) by FUNCT_1:def_3;
hence ex r being Real st r in rng (h | (divset (D,j))) ; ::_thesis: verum
end;
rng h is bounded_above by A5, INTEGRA1:13;
then rng (h | (divset (D,j))) is real-bounded by A51, RELAT_1:70, XXREAL_2:45;
then A58: (upper_bound (rng (h | (divset (D,j))))) - (lower_bound (rng (h | (divset (D,j))))) >= 0 by A56, SEQ_4:11, XREAL_1:48;
UV2 . j = (upper_bound (rng (h | (divset (D,j))))) * (vol (divset (D,j))) by A54, INTEGRA1:def_6;
then A59: F . j = ((upper_bound (rng (h | (divset (D,j))))) * (vol (divset (D,j)))) - ((lower_bound (rng (h | (divset (D,j))))) * (vol (divset (D,j)))) by A52, A55, VALUED_1:13
.= ((upper_bound (rng (h | (divset (D,j))))) - (lower_bound (rng (h | (divset (D,j)))))) * (vol (divset (D,j))) ;
vol (divset (D,j)) >= 0 by INTEGRA1:9;
hence 0 <= F . j by A59, A58; ::_thesis: verum
end;
then osc2 . m >= 0 by A50, RVSUM_1:84;
then A60: abs (osc2 . m) = osc2 . m by ABSVALUE:def_1;
for j being Nat st j in Seg (len D) holds
(UV2 - LV2) . j <= (a * ((UV - LV) + (UV1 - LV1))) . j
proof
let j be Nat; ::_thesis: ( j in Seg (len D) implies (UV2 - LV2) . j <= (a * ((UV - LV) + (UV1 - LV1))) . j )
set x = (UV2 - LV2) . j;
set y = (a * ((UV - LV) + (UV1 - LV1))) . j;
A61: (a * ((UV - LV) + (UV1 - LV1))) . j = a * (((UV - LV) + (UV1 - LV1)) . j) by RVSUM_1:45
.= a * (((UV - LV) . j) + ((UV1 - LV1) . j)) by RVSUM_1:11
.= a * (((UV . j) - (LV . j)) + ((UV1 - LV1) . j)) by RVSUM_1:27
.= a * (((UV . j) - (LV . j)) + ((UV1 . j) - (LV1 . j))) by RVSUM_1:27 ;
A62: vol (divset (D,j)) >= 0 by INTEGRA1:9;
assume A63: j in Seg (len D) ; ::_thesis: (UV2 - LV2) . j <= (a * ((UV - LV) + (UV1 - LV1))) . j
then A64: j in dom D by FINSEQ_1:def_3;
then A65: LV2 . j = (lower_bound (rng (h | (divset (D,j))))) * (vol (divset (D,j))) by INTEGRA1:def_7;
UV2 . j = (upper_bound (rng (h | (divset (D,j))))) * (vol (divset (D,j))) by A64, INTEGRA1:def_6;
then A66: (UV2 - LV2) . j = ((upper_bound (rng (h | (divset (D,j))))) * (vol (divset (D,j)))) - ((lower_bound (rng (h | (divset (D,j))))) * (vol (divset (D,j)))) by A65, RVSUM_1:27
.= ((upper_bound (rng (h | (divset (D,j))))) - (lower_bound (rng (h | (divset (D,j)))))) * (vol (divset (D,j))) ;
A67: LV1 . j = (lower_bound (rng (g | (divset (D,j))))) * (vol (divset (D,j))) by A64, INTEGRA1:def_7;
A68: UV1 . j = (upper_bound (rng (g | (divset (D,j))))) * (vol (divset (D,j))) by A64, INTEGRA1:def_6;
A69: a * (((upper_bound (rng (f | (divset (D,j))))) - (lower_bound (rng (f | (divset (D,j)))))) + ((upper_bound (rng (g | (divset (D,j))))) - (lower_bound (rng (g | (divset (D,j))))))) >= (upper_bound (rng (h | (divset (D,j))))) - (lower_bound (rng (h | (divset (D,j)))))
proof
A70: j in dom D by A63, FINSEQ_1:def_3;
A71: dom (g | (divset (D,j))) = (dom g) /\ (divset (D,j)) by RELAT_1:61
.= A /\ (divset (D,j)) by FUNCT_2:def_1
.= divset (D,j) by A70, INTEGRA1:8, XBOOLE_1:28 ;
then reconsider g1 = g | (divset (D,j)) as PartFunc of (divset (D,j)),REAL by RELSET_1:5;
reconsider g1 = g1 as Function of (divset (D,j)),REAL by A71, FUNCT_2:def_1;
A72: (g | (divset (D,j))) | (divset (D,j)) is bounded_below by A3, A71, INTEGRA2:6;
A73: dom (h | (divset (D,j))) = (dom h) /\ (divset (D,j)) by RELAT_1:61
.= A /\ (divset (D,j)) by FUNCT_2:def_1
.= divset (D,j) by A70, INTEGRA1:8, XBOOLE_1:28 ;
then reconsider h1 = h | (divset (D,j)) as PartFunc of (divset (D,j)),REAL by RELSET_1:5;
reconsider h1 = h1 as Function of (divset (D,j)),REAL by A73, FUNCT_2:def_1;
A74: dom (f | (divset (D,j))) = (dom f) /\ (divset (D,j)) by RELAT_1:61
.= A /\ (divset (D,j)) by FUNCT_2:def_1
.= divset (D,j) by A70, INTEGRA1:8, XBOOLE_1:28 ;
then reconsider f1 = f | (divset (D,j)) as PartFunc of (divset (D,j)),REAL by RELSET_1:5;
A75: (f | (divset (D,j))) | (divset (D,j)) is bounded_below by A1, A74, INTEGRA2:6;
A76: for x, y being Real st x in divset (D,j) & y in divset (D,j) holds
abs ((h1 . x) - (h1 . y)) <= a * ((abs ((f1 . x) - (f1 . y))) + (abs ((g1 . x) - (g1 . y))))
proof
let x, y be Real; ::_thesis: ( x in divset (D,j) & y in divset (D,j) implies abs ((h1 . x) - (h1 . y)) <= a * ((abs ((f1 . x) - (f1 . y))) + (abs ((g1 . x) - (g1 . y)))) )
assume that
A77: x in divset (D,j) and
A78: y in divset (D,j) ; ::_thesis: abs ((h1 . x) - (h1 . y)) <= a * ((abs ((f1 . x) - (f1 . y))) + (abs ((g1 . x) - (g1 . y))))
A79: g . y = g1 . y by A71, A78, FUNCT_1:47;
A80: h . y = h1 . y by A73, A78, FUNCT_1:47;
A81: h . x = h1 . x by A73, A77, FUNCT_1:47;
A82: f . y = f1 . y by A74, A78, FUNCT_1:47;
A83: f . x = f1 . x by A74, A77, FUNCT_1:47;
g . x = g1 . x by A71, A77, FUNCT_1:47;
hence abs ((h1 . x) - (h1 . y)) <= a * ((abs ((f1 . x) - (f1 . y))) + (abs ((g1 . x) - (g1 . y)))) by A7, A74, A77, A78, A79, A83, A82, A81, A80; ::_thesis: verum
end;
(g | (divset (D,j))) | (divset (D,j)) is bounded_above by A3, A71, INTEGRA2:5;
then A84: g1 | (divset (D,j)) is bounded by A72;
(f | (divset (D,j))) | (divset (D,j)) is bounded_above by A1, A74, INTEGRA2:5;
then A85: f1 | (divset (D,j)) is bounded by A75;
f1 is total by A74, PARTFUN1:def_2;
hence a * (((upper_bound (rng (f | (divset (D,j))))) - (lower_bound (rng (f | (divset (D,j)))))) + ((upper_bound (rng (g | (divset (D,j))))) - (lower_bound (rng (g | (divset (D,j))))))) >= (upper_bound (rng (h | (divset (D,j))))) - (lower_bound (rng (h | (divset (D,j))))) by A6, A85, A84, A76, Th26; ::_thesis: verum
end;
LV . j = (lower_bound (rng (f | (divset (D,j))))) * (vol (divset (D,j))) by A64, INTEGRA1:def_7;
then (a * ((UV - LV) + (UV1 - LV1))) . j = a * ((((upper_bound (rng (f | (divset (D,j))))) * (vol (divset (D,j)))) - ((lower_bound (rng (f | (divset (D,j))))) * (vol (divset (D,j))))) + (((upper_bound (rng (g | (divset (D,j))))) * (vol (divset (D,j)))) - ((lower_bound (rng (g | (divset (D,j))))) * (vol (divset (D,j)))))) by A64, A68, A67, A61, INTEGRA1:def_6
.= (a * (((upper_bound (rng (f | (divset (D,j))))) - (lower_bound (rng (f | (divset (D,j)))))) + ((upper_bound (rng (g | (divset (D,j))))) - (lower_bound (rng (g | (divset (D,j)))))))) * (vol (divset (D,j))) ;
hence (UV2 - LV2) . j <= (a * ((UV - LV) + (UV1 - LV1))) . j by A66, A69, A62, XREAL_1:64; ::_thesis: verum
end;
then osc2 . m <= Sum (a * ((UV - LV) + (UV1 - LV1))) by A50, RVSUM_1:82;
then osc2 . m <= a * (Sum ((UV - LV) + (UV1 - LV1))) by RVSUM_1:87;
then osc2 . m <= a * ((osc . m) + (osc1 . m)) by A24, A25, RVSUM_1:89;
hence abs ((osc2 . m) - 0) < b by A60, A49, XXREAL_0:2; ::_thesis: verum
end;
hence ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((osc2 . m) - 0) < b ; ::_thesis: verum
end;
then osc2 is convergent by SEQ_2:def_6;
then A86: lim ((upper_sum (h,T)) - (lower_sum (h,T))) = 0 by A18, SEQ_2:def_7;
A87: lower_sum (h,T) is convergent by A5, A8, A9, Th8;
upper_sum (h,T) is convergent by A5, A8, A9, Th9;
hence (lim (upper_sum (h,T))) - (lim (lower_sum (h,T))) = 0 by A87, A86, SEQ_2:12; ::_thesis: verum
end;
hence h is integrable by A5, Th12; ::_thesis: verum
end;
theorem :: INTEGRA4:29
for A being non empty closed_interval Subset of REAL
for f, g being Function of A,REAL st f | A is bounded & f is integrable & g | A is bounded & g is integrable holds
f (#) g is integrable
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f, g being Function of A,REAL st f | A is bounded & f is integrable & g | A is bounded & g is integrable holds
f (#) g is integrable
let f, g be Function of A,REAL; ::_thesis: ( f | A is bounded & f is integrable & g | A is bounded & g is integrable implies f (#) g is integrable )
assume that
A1: f | A is bounded and
A2: f is integrable and
A3: g | A is bounded and
A4: g is integrable ; ::_thesis: f (#) g is integrable
A5: (f (#) g) | (A /\ A) is bounded by A1, A3, RFUNCT_1:84;
consider r2 being real number such that
A6: for x being set st x in A /\ (dom g) holds
abs (g . x) <= r2 by A3, RFUNCT_1:73;
A7: A /\ (dom g) = A /\ A by FUNCT_2:def_1
.= A ;
A8: A /\ (dom f) = A /\ A by FUNCT_2:def_1
.= A ;
then consider a being Element of REAL such that
A9: a in A /\ (dom f) by SUBSET_1:4;
reconsider a = a as Element of A by A9;
A10: abs (f . a) >= 0 by COMPLEX1:46;
consider r1 being real number such that
A11: for x being set st x in A /\ (dom f) holds
abs (f . x) <= r1 by A1, RFUNCT_1:73;
reconsider r = max (r1,r2) as Real by XREAL_0:def_1;
A12: r2 <= r by XXREAL_0:25;
A13: r1 <= r by XXREAL_0:25;
A14: for x, y being Real st x in A & y in A holds
abs (((f (#) g) . x) - ((f (#) g) . y)) <= r * ((abs ((g . x) - (g . y))) + (abs ((f . x) - (f . y))))
proof
let x, y be Real; ::_thesis: ( x in A & y in A implies abs (((f (#) g) . x) - ((f (#) g) . y)) <= r * ((abs ((g . x) - (g . y))) + (abs ((f . x) - (f . y)))) )
assume that
A15: x in A and
A16: y in A ; ::_thesis: abs (((f (#) g) . x) - ((f (#) g) . y)) <= r * ((abs ((g . x) - (g . y))) + (abs ((f . x) - (f . y))))
A17: (f (#) g) . y = (f . y) * (g . y) by VALUED_1:5;
abs (g . y) <= r2 by A6, A7, A16;
then A18: abs (g . y) <= r by A12, XXREAL_0:2;
A19: abs ((f . x) - (f . y)) >= 0 by COMPLEX1:46;
abs (((f . x) - (f . y)) * (g . y)) = (abs ((f . x) - (f . y))) * (abs (g . y)) by COMPLEX1:65;
then A20: abs (((f . x) - (f . y)) * (g . y)) <= r * (abs ((f . x) - (f . y))) by A19, A18, XREAL_1:64;
(f (#) g) . x = (f . x) * (g . x) by VALUED_1:5;
then abs (((f (#) g) . x) - ((f (#) g) . y)) = abs (((f . x) * ((g . x) - (g . y))) + (((f . x) - (f . y)) * (g . y))) by A17;
then A21: abs (((f (#) g) . x) - ((f (#) g) . y)) <= (abs ((f . x) * ((g . x) - (g . y)))) + (abs (((f . x) - (f . y)) * (g . y))) by COMPLEX1:56;
abs (f . x) <= r1 by A11, A8, A15;
then A22: abs (f . x) <= r by A13, XXREAL_0:2;
A23: abs ((g . x) - (g . y)) >= 0 by COMPLEX1:46;
abs ((f . x) * ((g . x) - (g . y))) = (abs (f . x)) * (abs ((g . x) - (g . y))) by COMPLEX1:65;
then abs ((f . x) * ((g . x) - (g . y))) <= r * (abs ((g . x) - (g . y))) by A23, A22, XREAL_1:64;
then (abs ((f . x) * ((g . x) - (g . y)))) + (abs (((f . x) - (f . y)) * (g . y))) <= (r * (abs ((g . x) - (g . y)))) + (r * (abs ((f . x) - (f . y)))) by A20, XREAL_1:7;
hence abs (((f (#) g) . x) - ((f (#) g) . y)) <= r * ((abs ((g . x) - (g . y))) + (abs ((f . x) - (f . y)))) by A21, XXREAL_0:2; ::_thesis: verum
end;
A24: abs (f . a) <= r1 by A11, A9;
now__::_thesis:_f_(#)_g_is_integrable
percases ( r = 0 or r > 0 ) by A24, A10, XXREAL_0:25;
supposeA25: r = 0 ; ::_thesis: f (#) g is integrable
for x, y being Real st x in A & y in A holds
abs (((f (#) g) . x) - ((f (#) g) . y)) <= 1 * (abs ((f . x) - (f . y)))
proof
let x, y be Real; ::_thesis: ( x in A & y in A implies abs (((f (#) g) . x) - ((f (#) g) . y)) <= 1 * (abs ((f . x) - (f . y))) )
assume that
A26: x in A and
A27: y in A ; ::_thesis: abs (((f (#) g) . x) - ((f (#) g) . y)) <= 1 * (abs ((f . x) - (f . y)))
abs (((f (#) g) . x) - ((f (#) g) . y)) <= r * ((abs ((g . x) - (g . y))) + (abs ((f . x) - (f . y)))) by A14, A26, A27;
hence abs (((f (#) g) . x) - ((f (#) g) . y)) <= 1 * (abs ((f . x) - (f . y))) by A25, COMPLEX1:46; ::_thesis: verum
end;
hence f (#) g is integrable by A1, A2, A5, Th27; ::_thesis: verum
end;
suppose r > 0 ; ::_thesis: f (#) g is integrable
hence f (#) g is integrable by A1, A2, A3, A4, A5, A14, Th28; ::_thesis: verum
end;
end;
end;
hence f (#) g is integrable ; ::_thesis: verum
end;
theorem :: INTEGRA4:30
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL st f | A is bounded & f is integrable & not 0 in rng f & (f ^) | A is bounded holds
f ^ is integrable
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL st f | A is bounded & f is integrable & not 0 in rng f & (f ^) | A is bounded holds
f ^ is integrable
let f be Function of A,REAL; ::_thesis: ( f | A is bounded & f is integrable & not 0 in rng f & (f ^) | A is bounded implies f ^ is integrable )
assume that
A1: f | A is bounded and
A2: f is integrable and
A3: not 0 in rng f and
A4: (f ^) | A is bounded ; ::_thesis: f ^ is integrable
consider r being real number such that
A5: for x being set st x in A /\ (dom (f ^)) holds
abs ((f ^) . x) <= r by A4, RFUNCT_1:73;
reconsider r = r as Real by XREAL_0:def_1;
f " {0} = {} by A3, FUNCT_1:72;
then A6: f ^ is total by RFUNCT_1:54;
A7: for x, y being Real st x in A & y in A holds
abs (((f ^) . x) - ((f ^) . y)) <= (r ^2) * (abs ((f . x) - (f . y)))
proof
let x, y be Real; ::_thesis: ( x in A & y in A implies abs (((f ^) . x) - ((f ^) . y)) <= (r ^2) * (abs ((f . x) - (f . y))) )
assume that
A8: x in A and
A9: y in A ; ::_thesis: abs (((f ^) . x) - ((f ^) . y)) <= (r ^2) * (abs ((f . x) - (f . y)))
A10: x in dom (f ^) by A6, A8, PARTFUN1:def_2;
then A11: f . x <> 0 by RFUNCT_1:3;
A12: y in dom (f ^) by A6, A9, PARTFUN1:def_2;
then A13: f . y <> 0 by RFUNCT_1:3;
( 0 <= 1 / (abs (f . x)) & 0 <= 1 / (abs (f . y)) & 1 / (abs (f . x)) <= r & 1 / (abs (f . y)) <= r )
proof
A14: abs (f . y) > 0 by A13, COMPLEX1:47;
abs (f . x) > 0 by A11, COMPLEX1:47;
hence ( 0 <= 1 / (abs (f . x)) & 0 <= 1 / (abs (f . y)) ) by A14; ::_thesis: ( 1 / (abs (f . x)) <= r & 1 / (abs (f . y)) <= r )
reconsider x = x, y = y as Element of A by A8, A9;
y in A /\ (dom (f ^)) by A12, XBOOLE_0:def_4;
then abs ((f ^) . y) <= r by A5;
then abs (1 * ((f . y) ")) <= r by A12, RFUNCT_1:def_2;
then A15: abs (1 / (f . y)) <= r by XCMPLX_0:def_9;
x in A /\ (dom (f ^)) by A10, XBOOLE_0:def_4;
then abs ((f ^) . x) <= r by A5;
then abs (1 * ((f . x) ")) <= r by A10, RFUNCT_1:def_2;
then abs (1 / (f . x)) <= r by XCMPLX_0:def_9;
hence ( 1 / (abs (f . x)) <= r & 1 / (abs (f . y)) <= r ) by A15, ABSVALUE:7; ::_thesis: verum
end;
then A16: (1 / (abs (f . x))) * (1 / (abs (f . y))) <= r * r by XREAL_1:66;
abs ((f . x) - (f . y)) >= 0 by COMPLEX1:46;
then A17: (abs ((f . x) - (f . y))) * ((1 / (abs (f . x))) * (1 / (abs (f . y)))) <= (abs ((f . x) - (f . y))) * (r ^2) by A16, XREAL_1:64;
((f ^) . x) - ((f ^) . y) = ((f . x) ") - ((f ^) . y) by A10, RFUNCT_1:def_2
.= ((f . x) ") - ((f . y) ") by A12, RFUNCT_1:def_2 ;
then abs (((f ^) . x) - ((f ^) . y)) = (abs ((f . x) - (f . y))) / ((abs (f . x)) * (abs (f . y))) by A13, A11, SEQ_2:2
.= ((abs ((f . x) - (f . y))) / (abs (f . x))) * (1 / (abs (f . y))) by XCMPLX_1:103
.= ((abs ((f . x) - (f . y))) * (1 / (abs (f . x)))) * (1 / (abs (f . y))) by XCMPLX_1:99 ;
hence abs (((f ^) . x) - ((f ^) . y)) <= (r ^2) * (abs ((f . x) - (f . y))) by A17; ::_thesis: verum
end;
percases ( r ^2 = 0 or r ^2 > 0 ) by XREAL_1:63;
supposeA18: r ^2 = 0 ; ::_thesis: f ^ is integrable
for x, y being Real st x in A & y in A holds
abs (((f ^) . x) - ((f ^) . y)) <= 1 * (abs ((f . x) - (f . y)))
proof
let x, y be Real; ::_thesis: ( x in A & y in A implies abs (((f ^) . x) - ((f ^) . y)) <= 1 * (abs ((f . x) - (f . y))) )
assume that
A19: x in A and
A20: y in A ; ::_thesis: abs (((f ^) . x) - ((f ^) . y)) <= 1 * (abs ((f . x) - (f . y)))
abs (((f ^) . x) - ((f ^) . y)) <= 0 * (abs ((f . x) - (f . y))) by A7, A18, A19, A20;
hence abs (((f ^) . x) - ((f ^) . y)) <= 1 * (abs ((f . x) - (f . y))) by COMPLEX1:46; ::_thesis: verum
end;
hence f ^ is integrable by A1, A2, A4, A6, Th27; ::_thesis: verum
end;
suppose r ^2 > 0 ; ::_thesis: f ^ is integrable
hence f ^ is integrable by A1, A2, A4, A6, A7, Th27; ::_thesis: verum
end;
end;
end;