let A be non empty closed_interval Subset of REAL; for f being PartFunc of REAL,REAL st f | A is monotone & A c= dom f holds
f is_integrable_on A
let f be PartFunc of REAL,REAL; ( f | A is monotone & A c= dom f implies f is_integrable_on A )
assume that
A1:
f | A is monotone
and
A2:
A c= dom f
; f is_integrable_on A
per cases
( f | A is non-decreasing or f | A is non-increasing )
by A1, RFUNCT_2:def 5;
suppose
f | A is
non-increasing
;
f is_integrable_on Athen A3:
((- 1) (#) f) | A is
non-decreasing
by RFUNCT_2:35;
A4:
(
(- f) || A is
total &
((- f) || A) | A is
bounded )
proof
consider x being
Element of
REAL such that A5:
x in A
by SUBSET_1:4;
A6:
dom ((- f) || A) =
(dom (- f)) /\ A
by RELAT_1:61
.=
(dom f) /\ A
by VALUED_1:8
.=
A
by A2, XBOOLE_1:28
;
hence
(- f) || A is
total
by PARTFUN1:def 2;
((- f) || A) | A is bounded
(
lower_bound A <= x &
x <= upper_bound A )
by A5, INTEGRA2:1;
then A7:
lower_bound A <= upper_bound A
by XXREAL_0:2;
for
x being
object st
x in A /\ (dom ((- f) || A)) holds
((- f) || A) . x >= ((- f) || A) . (lower_bound A)
proof
let x be
object ;
( x in A /\ (dom ((- f) || A)) implies ((- f) || A) . x >= ((- f) || A) . (lower_bound A) )
assume
x in A /\ (dom ((- f) || A))
;
((- f) || A) . x >= ((- f) || A) . (lower_bound A)
then reconsider x =
x as
Element of
A ;
A8:
(
x >= lower_bound A &
(- f) . x = ((- f) | A) . x )
by A6, FUNCT_1:47, INTEGRA2:1;
lower_bound A in A
by A7, INTEGRA2:1;
then A9:
(- f) . (lower_bound A) = ((- f) | A) . (lower_bound A)
by A6, FUNCT_1:47;
A10:
A =
A /\ (dom f)
by A2, XBOOLE_1:28
.=
A /\ (dom (- f))
by VALUED_1:8
;
then
lower_bound A in A /\ (dom (- f))
by A7, INTEGRA2:1;
hence
((- f) || A) . x >= ((- f) || A) . (lower_bound A)
by A3, A10, A8, A9, RFUNCT_2:24;
verum
end;
then A11:
((- f) || A) | A is
bounded_below
by RFUNCT_1:71;
for
x being
object st
x in A /\ (dom ((- f) || A)) holds
((- f) || A) . x <= ((- f) || A) . (upper_bound A)
proof
let x be
object ;
( x in A /\ (dom ((- f) || A)) implies ((- f) || A) . x <= ((- f) || A) . (upper_bound A) )
assume
x in A /\ (dom ((- f) || A))
;
((- f) || A) . x <= ((- f) || A) . (upper_bound A)
then reconsider x =
x as
Element of
A ;
A12:
(
x <= upper_bound A &
(- f) . x = ((- f) | A) . x )
by A6, FUNCT_1:47, INTEGRA2:1;
upper_bound A in A
by A7, INTEGRA2:1;
then A13:
(- f) . (upper_bound A) = ((- f) | A) . (upper_bound A)
by A6, FUNCT_1:47;
A14:
A =
A /\ (dom f)
by A2, XBOOLE_1:28
.=
A /\ (dom (- f))
by VALUED_1:8
;
then
upper_bound A in A /\ (dom (- f))
by A7, INTEGRA2:1;
hence
((- f) || A) . x <= ((- f) || A) . (upper_bound A)
by A3, A14, A12, A13, RFUNCT_2:24;
verum
end;
then
((- f) || A) | A is
bounded_above
by RFUNCT_1:70;
hence
((- f) || A) | A is
bounded
by A11;
verum
end;
dom f = dom (- f)
by VALUED_1:8;
then
- f is_integrable_on A
by A2, A3, Lm1;
then
(- f) || A is
integrable
;
then A15:
(- 1) (#) ((- f) || A) is
integrable
by A4, INTEGRA2:31;
A16:
dom ((- f) || A) =
(dom (- f)) /\ A
by RELAT_1:61
.=
(dom f) /\ A
by VALUED_1:8
.=
A
by A2, XBOOLE_1:28
;
then A17:
A = dom ((- 1) (#) ((- f) || A))
by VALUED_1:def 5;
A18:
dom (f || A) = (dom f) /\ A
by RELAT_1:61;
then A19:
dom (f || A) = A
by A2, XBOOLE_1:28;
A20:
dom ((- 1) (#) ((- f) || A)) = A
by A16, VALUED_1:def 5;
A21:
for
z being
Element of
A st
z in A holds
((- 1) (#) ((- f) || A)) . z = (f || A) . z
A = dom (f || A)
by A2, A18, XBOOLE_1:28;
then
(- 1) (#) ((- f) || A) = f || A
by A21, A17, PARTFUN1:5;
hence
f is_integrable_on A
by A15;
verum end;