let A be non empty closed_interval Subset of REAL; for a, b, p, q, c, d, e being Real
for f being Function of REAL,REAL st a <> p & f | A = ((AffineMap (a,b)) | [.(lower_bound A),((q - b) / (a - p)).]) +* ((AffineMap (p,q)) | [.((q - b) / (a - p)),(upper_bound A).]) & (q - b) / (a - p) in A holds
centroid (f,A) = ((((((1 / 3) * a) * ((((q - b) / (a - p)) ^3) - ((lower_bound A) ^3))) + (((1 / 2) * b) * ((((q - b) / (a - p)) ^2) - ((lower_bound A) ^2)))) + (((1 / 3) * p) * (((upper_bound A) ^3) - (((q - b) / (a - p)) ^3)))) + (((1 / 2) * q) * (((upper_bound A) ^2) - (((q - b) / (a - p)) ^2)))) / ((((((1 / 2) * a) * ((((q - b) / (a - p)) ^2) - ((lower_bound A) ^2))) + (b * (((q - b) / (a - p)) - (lower_bound A)))) + (((1 / 2) * p) * (((upper_bound A) ^2) - (((q - b) / (a - p)) ^2)))) + (q * ((upper_bound A) - ((q - b) / (a - p)))))
let a, b, p, q, c, d, e be Real; for f being Function of REAL,REAL st a <> p & f | A = ((AffineMap (a,b)) | [.(lower_bound A),((q - b) / (a - p)).]) +* ((AffineMap (p,q)) | [.((q - b) / (a - p)),(upper_bound A).]) & (q - b) / (a - p) in A holds
centroid (f,A) = ((((((1 / 3) * a) * ((((q - b) / (a - p)) ^3) - ((lower_bound A) ^3))) + (((1 / 2) * b) * ((((q - b) / (a - p)) ^2) - ((lower_bound A) ^2)))) + (((1 / 3) * p) * (((upper_bound A) ^3) - (((q - b) / (a - p)) ^3)))) + (((1 / 2) * q) * (((upper_bound A) ^2) - (((q - b) / (a - p)) ^2)))) / ((((((1 / 2) * a) * ((((q - b) / (a - p)) ^2) - ((lower_bound A) ^2))) + (b * (((q - b) / (a - p)) - (lower_bound A)))) + (((1 / 2) * p) * (((upper_bound A) ^2) - (((q - b) / (a - p)) ^2)))) + (q * ((upper_bound A) - ((q - b) / (a - p)))))
let f be Function of REAL,REAL; ( a <> p & f | A = ((AffineMap (a,b)) | [.(lower_bound A),((q - b) / (a - p)).]) +* ((AffineMap (p,q)) | [.((q - b) / (a - p)),(upper_bound A).]) & (q - b) / (a - p) in A implies centroid (f,A) = ((((((1 / 3) * a) * ((((q - b) / (a - p)) ^3) - ((lower_bound A) ^3))) + (((1 / 2) * b) * ((((q - b) / (a - p)) ^2) - ((lower_bound A) ^2)))) + (((1 / 3) * p) * (((upper_bound A) ^3) - (((q - b) / (a - p)) ^3)))) + (((1 / 2) * q) * (((upper_bound A) ^2) - (((q - b) / (a - p)) ^2)))) / ((((((1 / 2) * a) * ((((q - b) / (a - p)) ^2) - ((lower_bound A) ^2))) + (b * (((q - b) / (a - p)) - (lower_bound A)))) + (((1 / 2) * p) * (((upper_bound A) ^2) - (((q - b) / (a - p)) ^2)))) + (q * ((upper_bound A) - ((q - b) / (a - p))))) )
assume that
A1:
a <> p
and
A2:
f | A = ((AffineMap (a,b)) | [.(lower_bound A),((q - b) / (a - p)).]) +* ((AffineMap (p,q)) | [.((q - b) / (a - p)),(upper_bound A).])
and
A3:
(q - b) / (a - p) in A
; centroid (f,A) = ((((((1 / 3) * a) * ((((q - b) / (a - p)) ^3) - ((lower_bound A) ^3))) + (((1 / 2) * b) * ((((q - b) / (a - p)) ^2) - ((lower_bound A) ^2)))) + (((1 / 3) * p) * (((upper_bound A) ^3) - (((q - b) / (a - p)) ^3)))) + (((1 / 2) * q) * (((upper_bound A) ^2) - (((q - b) / (a - p)) ^2)))) / ((((((1 / 2) * a) * ((((q - b) / (a - p)) ^2) - ((lower_bound A) ^2))) + (b * (((q - b) / (a - p)) - (lower_bound A)))) + (((1 / 2) * p) * (((upper_bound A) ^2) - (((q - b) / (a - p)) ^2)))) + (q * ((upper_bound A) - ((q - b) / (a - p)))))
set F = ((AffineMap (a,b)) | ].-infty,((q - b) / (a - p)).[) +* ((AffineMap (p,q)) | [.((q - b) / (a - p)),+infty.[);
reconsider F = ((AffineMap (a,b)) | ].-infty,((q - b) / (a - p)).[) +* ((AffineMap (p,q)) | [.((q - b) / (a - p)),+infty.[) as Function of REAL,REAL by Th19;
A4:
F | A = f | A
by A2, Th17C, A3;
B1: integral (f,A) =
integral (F | A)
by A4, INTEGRA5:def 2
.=
integral (F,A)
by INTEGRA5:def 2
.=
(integral ((AffineMap (a,b)),['(lower_bound A),((q - b) / (a - p))'])) + (integral ((AffineMap (p,q)),['((q - b) / (a - p)),(upper_bound A)']))
by Th17, A1, A3
;
set c = lower_bound A;
set d = (q - b) / (a - p);
set e = upper_bound A;
(q - b) / (a - p) in [.(lower_bound A),(upper_bound A).]
by INTEGRA1:4, A3;
then CD:
( lower_bound A <= (q - b) / (a - p) & (q - b) / (a - p) <= upper_bound A )
by XXREAL_1:1;
centroid (f,A) =
((integral (((id REAL) (#) (AffineMap (a,b))),['(lower_bound A),((q - b) / (a - p))'])) + (integral (((id REAL) (#) (AffineMap (p,q))),['((q - b) / (a - p)),(upper_bound A)']))) / ((integral ((AffineMap (a,b)),['(lower_bound A),((q - b) / (a - p))'])) + (integral ((AffineMap (p,q)),['((q - b) / (a - p)),(upper_bound A)'])))
by B1, Th23A, A1, A2, A3
.=
((integral (((id REAL) (#) (AffineMap (a,b))),(lower_bound A),((q - b) / (a - p)))) + (integral (((id REAL) (#) (AffineMap (p,q))),['((q - b) / (a - p)),(upper_bound A)']))) / ((integral ((AffineMap (a,b)),['(lower_bound A),((q - b) / (a - p))'])) + (integral ((AffineMap (p,q)),['((q - b) / (a - p)),(upper_bound A)'])))
by INTEGRA5:def 4, CD
.=
((integral (((id REAL) (#) (AffineMap (a,b))),(lower_bound A),((q - b) / (a - p)))) + (integral (((id REAL) (#) (AffineMap (p,q))),((q - b) / (a - p)),(upper_bound A)))) / ((integral ((AffineMap (a,b)),['(lower_bound A),((q - b) / (a - p))'])) + (integral ((AffineMap (p,q)),['((q - b) / (a - p)),(upper_bound A)'])))
by INTEGRA5:def 4, CD
.=
((integral (((id REAL) (#) (AffineMap (a,b))),(lower_bound A),((q - b) / (a - p)))) + (integral (((id REAL) (#) (AffineMap (p,q))),((q - b) / (a - p)),(upper_bound A)))) / ((integral ((AffineMap (a,b)),(lower_bound A),((q - b) / (a - p)))) + (integral ((AffineMap (p,q)),['((q - b) / (a - p)),(upper_bound A)'])))
by INTEGRA5:def 4, CD
.=
((integral (((id REAL) (#) (AffineMap (a,b))),(lower_bound A),((q - b) / (a - p)))) + (integral (((id REAL) (#) (AffineMap (p,q))),((q - b) / (a - p)),(upper_bound A)))) / ((integral ((AffineMap (a,b)),(lower_bound A),((q - b) / (a - p)))) + (integral ((AffineMap (p,q)),((q - b) / (a - p)),(upper_bound A))))
by INTEGRA5:def 4, CD
.=
(((((1 / 3) * a) * (((((q - b) / (a - p)) * ((q - b) / (a - p))) * ((q - b) / (a - p))) - (((lower_bound A) * (lower_bound A)) * (lower_bound A)))) + (((1 / 2) * b) * ((((q - b) / (a - p)) * ((q - b) / (a - p))) - ((lower_bound A) * (lower_bound A))))) + (integral (((id REAL) (#) (AffineMap (p,q))),((q - b) / (a - p)),(upper_bound A)))) / ((integral ((AffineMap (a,b)),(lower_bound A),((q - b) / (a - p)))) + (integral ((AffineMap (p,q)),((q - b) / (a - p)),(upper_bound A))))
by Th23B, CD
.=
(((((1 / 3) * a) * (((((q - b) / (a - p)) * ((q - b) / (a - p))) * ((q - b) / (a - p))) - (((lower_bound A) * (lower_bound A)) * (lower_bound A)))) + (((1 / 2) * b) * ((((q - b) / (a - p)) * ((q - b) / (a - p))) - ((lower_bound A) * (lower_bound A))))) + ((((1 / 3) * p) * ((((upper_bound A) * (upper_bound A)) * (upper_bound A)) - ((((q - b) / (a - p)) * ((q - b) / (a - p))) * ((q - b) / (a - p))))) + (((1 / 2) * q) * (((upper_bound A) * (upper_bound A)) - (((q - b) / (a - p)) * ((q - b) / (a - p))))))) / ((integral ((AffineMap (a,b)),(lower_bound A),((q - b) / (a - p)))) + (integral ((AffineMap (p,q)),((q - b) / (a - p)),(upper_bound A))))
by Th23B, CD
.=
(((((1 / 3) * a) * (((((q - b) / (a - p)) * ((q - b) / (a - p))) * ((q - b) / (a - p))) - (((lower_bound A) * (lower_bound A)) * (lower_bound A)))) + (((1 / 2) * b) * ((((q - b) / (a - p)) * ((q - b) / (a - p))) - ((lower_bound A) * (lower_bound A))))) + ((((1 / 3) * p) * ((((upper_bound A) * (upper_bound A)) * (upper_bound A)) - ((((q - b) / (a - p)) * ((q - b) / (a - p))) * ((q - b) / (a - p))))) + (((1 / 2) * q) * (((upper_bound A) * (upper_bound A)) - (((q - b) / (a - p)) * ((q - b) / (a - p))))))) / (((((1 / 2) * a) * ((((q - b) / (a - p)) * ((q - b) / (a - p))) - ((lower_bound A) * (lower_bound A)))) + (b * (((q - b) / (a - p)) - (lower_bound A)))) + (integral ((AffineMap (p,q)),((q - b) / (a - p)),(upper_bound A))))
by Th23D, CD
.=
(((((1 / 3) * a) * (((((q - b) / (a - p)) * ((q - b) / (a - p))) * ((q - b) / (a - p))) - (((lower_bound A) * (lower_bound A)) * (lower_bound A)))) + (((1 / 2) * b) * ((((q - b) / (a - p)) * ((q - b) / (a - p))) - ((lower_bound A) * (lower_bound A))))) + ((((1 / 3) * p) * ((((upper_bound A) ^2) * (upper_bound A)) - ((((q - b) / (a - p)) * ((q - b) / (a - p))) * ((q - b) / (a - p))))) + (((1 / 2) * q) * (((upper_bound A) * (upper_bound A)) - (((q - b) / (a - p)) * ((q - b) / (a - p))))))) / (((((1 / 2) * a) * ((((q - b) / (a - p)) * ((q - b) / (a - p))) - ((lower_bound A) ^2))) + (b * (((q - b) / (a - p)) - (lower_bound A)))) + ((((1 / 2) * p) * (((upper_bound A) * (upper_bound A)) - (((q - b) / (a - p)) * ((q - b) / (a - p))))) + (q * ((upper_bound A) - ((q - b) / (a - p))))))
by Th23D, CD
.=
(((((1 / 3) * a) * (((((q - b) / (a - p)) ^2) * ((q - b) / (a - p))) - (((lower_bound A) ^2) * (lower_bound A)))) + (((1 / 2) * b) * ((((q - b) / (a - p)) ^2) - ((lower_bound A) ^2)))) + ((((1 / 3) * p) * (((upper_bound A) ^3) - ((((q - b) / (a - p)) ^2) * ((q - b) / (a - p))))) + (((1 / 2) * q) * (((upper_bound A) ^2) - (((q - b) / (a - p)) ^2))))) / (((((1 / 2) * a) * ((((q - b) / (a - p)) ^2) - ((lower_bound A) ^2))) + (b * (((q - b) / (a - p)) - (lower_bound A)))) + ((((1 / 2) * p) * (((upper_bound A) ^2) - (((q - b) / (a - p)) ^2))) + (q * ((upper_bound A) - ((q - b) / (a - p))))))
by POLYEQ_3:def 3
.=
(((((1 / 3) * a) * (((((q - b) / (a - p)) ^2) * ((q - b) / (a - p))) - (((lower_bound A) ^2) * (lower_bound A)))) + (((1 / 2) * b) * ((((q - b) / (a - p)) ^2) - ((lower_bound A) ^2)))) + ((((1 / 3) * p) * (((upper_bound A) ^3) - (((q - b) / (a - p)) ^3))) + (((1 / 2) * q) * (((upper_bound A) ^2) - (((q - b) / (a - p)) ^2))))) / (((((1 / 2) * a) * ((((q - b) / (a - p)) ^2) - ((lower_bound A) ^2))) + (b * (((q - b) / (a - p)) - (lower_bound A)))) + ((((1 / 2) * p) * (((upper_bound A) ^2) - (((q - b) / (a - p)) ^2))) + (q * ((upper_bound A) - ((q - b) / (a - p))))))
by POLYEQ_3:def 3
.=
(((((1 / 3) * a) * ((((q - b) / (a - p)) ^3) - (((lower_bound A) ^2) * (lower_bound A)))) + (((1 / 2) * b) * ((((q - b) / (a - p)) ^2) - ((lower_bound A) ^2)))) + ((((1 / 3) * p) * (((upper_bound A) ^3) - (((q - b) / (a - p)) ^3))) + (((1 / 2) * q) * (((upper_bound A) ^2) - (((q - b) / (a - p)) ^2))))) / (((((1 / 2) * a) * ((((q - b) / (a - p)) ^2) - ((lower_bound A) ^2))) + (b * (((q - b) / (a - p)) - (lower_bound A)))) + ((((1 / 2) * p) * (((upper_bound A) ^2) - (((q - b) / (a - p)) ^2))) + (q * ((upper_bound A) - ((q - b) / (a - p))))))
by POLYEQ_3:def 3
.=
(((((1 / 3) * a) * ((((q - b) / (a - p)) ^3) - ((lower_bound A) ^3))) + (((1 / 2) * b) * ((((q - b) / (a - p)) ^2) - ((lower_bound A) ^2)))) + ((((1 / 3) * p) * (((upper_bound A) ^3) - (((q - b) / (a - p)) ^3))) + (((1 / 2) * q) * (((upper_bound A) ^2) - (((q - b) / (a - p)) ^2))))) / (((((1 / 2) * a) * ((((q - b) / (a - p)) ^2) - ((lower_bound A) ^2))) + (b * (((q - b) / (a - p)) - (lower_bound A)))) + ((((1 / 2) * p) * (((upper_bound A) ^2) - (((q - b) / (a - p)) ^2))) + (q * ((upper_bound A) - ((q - b) / (a - p))))))
by POLYEQ_3:def 3
;
hence
centroid (f,A) = ((((((1 / 3) * a) * ((((q - b) / (a - p)) ^3) - ((lower_bound A) ^3))) + (((1 / 2) * b) * ((((q - b) / (a - p)) ^2) - ((lower_bound A) ^2)))) + (((1 / 3) * p) * (((upper_bound A) ^3) - (((q - b) / (a - p)) ^3)))) + (((1 / 2) * q) * (((upper_bound A) ^2) - (((q - b) / (a - p)) ^2)))) / ((((((1 / 2) * a) * ((((q - b) / (a - p)) ^2) - ((lower_bound A) ^2))) + (b * (((q - b) / (a - p)) - (lower_bound A)))) + (((1 / 2) * p) * (((upper_bound A) ^2) - (((q - b) / (a - p)) ^2)))) + (q * ((upper_bound A) - ((q - b) / (a - p)))))
; verum