let A be non empty closed_interval Subset of REAL; for f, g being Function of REAL,REAL st f is_integrable_on A & f | A is bounded & g is_integrable_on A & g | A is bounded holds
( min (f,g) is_integrable_on A & (min (f,g)) | A is bounded & integral ((min (f,g)),A) = (1 / 2) * (((integral (f,A)) + (integral (g,A))) - (integral ((abs (f - g)),A))) )
let f, g be Function of REAL,REAL; ( f is_integrable_on A & f | A is bounded & g is_integrable_on A & g | A is bounded implies ( min (f,g) is_integrable_on A & (min (f,g)) | A is bounded & integral ((min (f,g)),A) = (1 / 2) * (((integral (f,A)) + (integral (g,A))) - (integral ((abs (f - g)),A))) ) )
assume that
A1A:
( f is_integrable_on A & f | A is bounded )
and
A2A:
( g is_integrable_on A & g | A is bounded )
; ( min (f,g) is_integrable_on A & (min (f,g)) | A is bounded & integral ((min (f,g)),A) = (1 / 2) * (((integral (f,A)) + (integral (g,A))) - (integral ((abs (f - g)),A))) )
reconsider fm = min (f,g) as PartFunc of REAL,REAL ;
reconsider f = f as PartFunc of REAL,REAL ;
reconsider g = g as PartFunc of REAL,REAL ;
A1:
( f is_integrable_on A & f | A is bounded )
by A1A;
A2:
( g is_integrable_on A & g | A is bounded )
by A2A;
Df:
REAL = dom f
by FUNCT_2:def 1;
Dg:
REAL = dom g
by FUNCT_2:def 1;
Dm:
REAL = dom (f - g)
by FUNCT_2:def 1;
Dp:
REAL = dom (f + g)
by FUNCT_2:def 1;
Da:
REAL = dom (abs (f - g))
by FUNCT_2:def 1;
DD:
REAL = dom ((f + g) - (abs (f - g)))
by FUNCT_2:def 1;
i1:
f + g is_integrable_on A
by A1, A2, INTEGRA6:11, Df, Dg;
B1:
(f + g) | (A /\ A) is bounded
by A1A, A2A, RFUNCT_1:83;
B2:
(f - g) | (A /\ A) is bounded
by A1A, A2A, RFUNCT_1:84;
f - g is_integrable_on A
by A1, A2, INTEGRA6:11, Dg, Df;
then i3:
abs (f - g) is_integrable_on A
by B2, INTEGRA6:7, Dm;
B3:
(abs (f - g)) | (A /\ A) is bounded
by B2, RFUNCT_1:82;
i4:
(f + g) - (abs (f - g)) is_integrable_on A
by i1, i3, B1, B3, INTEGRA6:11, Dp, Da;
B4:
((f + g) - (abs (f - g))) | (A /\ A) is bounded
by B1, B3, RFUNCT_1:84;
i5:
(1 / 2) (#) ((f + g) - (abs (f - g))) is_integrable_on A
by i4, B4, INTEGRA6:9, DD;
B5:
((1 / 2) (#) ((f + g) - (abs (f - g)))) | (A /\ A) is bounded
by B4, RFUNCT_1:80;
integral (fm,A) =
integral (((1 / 2) (#) ((f + g) - (abs (f - g)))),A)
by Th13
.=
(1 / 2) * (integral (((f + g) - (abs (f - g))),A))
by INTEGRA6:9, i4, B4, DD
.=
(1 / 2) * ((integral ((f + g),A)) - (integral ((abs (f - g)),A)))
by INTEGRA6:11, i1, B1, i3, B3, Da, Dp
;
hence
( min (f,g) is_integrable_on A & (min (f,g)) | A is bounded & integral ((min (f,g)),A) = (1 / 2) * (((integral (f,A)) + (integral (g,A))) - (integral ((abs (f - g)),A))) )
by Th13, i5, B5, INTEGRA6:11, A1, A2, Df, Dg; verum