:: Definition of Centroid Method as Defuzzification
:: by Takashi Mitsuishi
::
:: Received July 23, 2022
:: Copyright (c) 2022-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XBOOLE_0, SUBSET_1, XXREAL_1, CARD_1, RELAT_1, TARSKI,
FUNCT_1, XXREAL_0, PARTFUN1, ARYTM_1, ARYTM_3, COMPLEX1, FUZZY_1,
MEASURE5, FUZNUM_1, REAL_1, ORDINAL2, XXREAL_2, JGRAPH_2, FUNCT_4,
FCONT_1, SQUARE_1, VALUED_1, FDIFF_1, INTEGRA1, INTEGRA5, SEQ_4, NAT_1,
PREPOWER, NEWTON, RFUNCT_3, CARD_3, MEASURE7, FINSEQ_1, POLYEQ_3,
FUZZY_6;
notations TARSKI, XBOOLE_0, SUBSET_1, NEWTON, RELAT_1, ORDINAL1, NUMBERS,
SQUARE_1, XCMPLX_0, XXREAL_0, COMPLEX1, XREAL_0, FUNCT_1, RELSET_1,
MEASURE5, PARTFUN1, FUNCT_2, FUNCT_3, INTEGRA1, RFUNCT_3, VALUED_1,
FUNCT_4, COMSEQ_2, FDIFF_1, FINSEQ_1, SEQ_4, PREPOWER, FCONT_1, POLYEQ_3,
RVSUM_1, RCOMP_1, TAYLOR_1, INTEGRA5, COUSIN2, FUZZY_1, FUZNUM_1;
constructors SEQ_4, RELSET_1, FCONT_1, FUNCT_4, TAYLOR_1, FDIFF_1, COMSEQ_2,
PREPOWER, NEWTON, RFUNCT_3, INTEGRA5, COUSIN2, SEQ_2, RVSUM_1, POLYEQ_3;
registrations RELSET_1, NUMBERS, XXREAL_0, MEMBERED, XBOOLE_0, VALUED_0,
VALUED_1, PDIFFEQ1, FUNCT_2, XREAL_0, ORDINAL1, FCONT_1, RELAT_1,
FUNCT_1, XCMPLX_0, NAT_1, FUZNUM_1, SQUARE_1, INT_1, INTEGRA1, POLYDIFF,
PREPOWER, NEWTON;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
equalities RCOMP_1, SQUARE_1;
expansions TARSKI, FCONT_1;
theorems XBOOLE_0, TARSKI, FUNCT_1, ABSVALUE, PARTFUN1, TAYLOR_1, COMPLEX1,
XREAL_1, XXREAL_0, XXREAL_1, FUNCT_2, RELAT_1, XREAL_0, FCONT_1,
XCMPLX_1, FUZZY_2, FUNCT_4, SUBSET_1, FDIFF_1, VALUED_1, INTEGRA1,
INTEGRA5, PREPOWER, NEWTON, INTEGRA6, SEQ_4, RFUNCT_3, INTEGRA2,
INTEGRA9, COMSEQ_2, COUSIN2, RFUNCT_1, FINSEQ_3, POLYEQ_3;
begin
reserve A for non empty closed_interval Subset of REAL;
definition
let A be non empty closed_interval Subset of REAL;
let f be Function of REAL,REAL;
::: assume that
::: f is_integrable_on A and
::: f | A is bounded;
func centroid (f,A) -> Real equals
integral((id REAL)(#)f,A)/integral(f,A);
coherence;
end;
theorem
for a,b,c be Real st a < b & c > 0
holds centroid (AffineMap (0,c),['a,b']) = (a+b)/2
proof
let a,b,c be Real;
assume A1: a < b;
assume A2: c > 0;
R1: [#]REAL = REAL by SUBSET_1:def 3;
R2: ['a,b'] c= REAL;then
B1: ['a,b'] c= [#]REAL by SUBSET_1:def 3;
set f = AffineMap (c,0);
LU1: ['a,b'] = [.(lower_bound ['a,b']),(upper_bound ['a,b']).]
& ['a,b'] =[.a,b.] by A1,INTEGRA5:def 3,INTEGRA1:4;
set F = ((c/2) (#) ( #Z 2 ));
D3: dom ((id REAL) (#) AffineMap (0,c)) = REAL by FUNCT_2:def 1;
D5A: dom ((c/2) (#) ( #Z 2 )) = REAL by FUNCT_2:def 1;
D6A: dom ( #Z 2 ) = REAL by FUNCT_2:def 1;
for x being Real st x in [#]REAL holds ( #Z 2 ) is_differentiable_in x
by TAYLOR_1:2; then
C4A: ( #Z 2 ) is_differentiable_on [#]REAL by FDIFF_1:9,D6A; then
C4: F is_differentiable_on [#]REAL by FDIFF_1:20,D5A; then
E7: dom (F`|[#]REAL) = [#]REAL by FDIFF_1:def 7;
C1A:for x being Element of REAL st x in dom (F`|[#]REAL) holds
(F`|[#]REAL) . x = ((id REAL) (#) AffineMap (0,c)) . x
proof
let x be Element of REAL;
assume E4: x in dom (F`|[#]REAL);
E3: x in [#]REAL by E4,C4,FDIFF_1:def 7;
E2: ( #Z 2 ) is_differentiable_in x by TAYLOR_1:2;
E5: (F`|[#]REAL).x = diff(((c/2) (#) ( #Z 2 )),x) by FDIFF_1:def 7,C4,E3
.=(c/2) * diff(( #Z 2 ),x) by FDIFF_1:15,E2
.= (c/2) * (2 * (x #Z (2 - 1)) ) by TAYLOR_1:2
.= (c/2) * (2 * x) by PREPOWER:35
.= c*x;
((id REAL) (#) AffineMap (0,c)) . x
= ((id REAL).x) * (AffineMap (0,c). x) by VALUED_1:5
.= x * ((0 * x) + c) by FCONT_1:def 4
.=c*x;
hence thesis by E5;
end;
set F2 = (id REAL) (#) AffineMap (0,c);
reconsider F2 as PartFunc of REAL,REAL;
(F2 | ['a,b']) is continuous; then
(id REAL) (#) AffineMap (0,c) is_integrable_on ['a,b'] &
(F2 | ['a,b']) is bounded
by INTEGRA5:10,INTEGRA5:11,D3; then
C2: F `| [#]REAL is_integrable_on ['a,b'] &
(F `| [#]REAL) | ['a,b'] is bounded
by PARTFUN1:5,SUBSET_1:def 3,D3,E7,C1A;
C3: integral ((id REAL) (#) AffineMap(0,c),['a,b'])
= integral ((F `| [#]REAL),['a,b'])
by PARTFUN1:5,SUBSET_1:def 3,D3,E7,C1A
.= F . (upper_bound ['a,b']) - F . (lower_bound ['a,b'])
by INTEGRA5:13,B1,C2,C4A,FDIFF_1:20,D5A
.=F.b - F . (lower_bound ['a,b']) by LU1,INTEGRA1:5
.=((c/2) (#) ( #Z 2 )).b - F.a by LU1,INTEGRA1:5
.=(c/2) * ( #Z 2 ).b - F.a by VALUED_1:6
.=(c/2) * ( #Z 2 ).b - (c/2) * ( #Z 2 ).a by VALUED_1:6
.=(c/2) * b #Z 2 - (c/2) * ( #Z 2 ).a by TAYLOR_1:def 1
.=(c/2) * b #Z 2 - (c/2) * a #Z 2 by TAYLOR_1:def 1
.=(c/2) * b |^ 2 - (c/2) * a #Z 2 by PREPOWER:36
.=(c/2) * b |^ 2 - (c/2) * a |^ 2 by PREPOWER:36
.=(c/2) * b ^2 - (c/2) * a |^ 2 by NEWTON:81
.=(c/2) * b ^2 - (c/2) * a ^2 by NEWTON:81
.=((b+a)/2)*(c*(b-a));
A4: [#] REAL c= dom f by R1,FUNCT_2:def 1;
A5: for x being Real st x in [#] REAL holds
(AffineMap (c,0)) . x = (c * x) + 0 by FCONT_1:def 4; then
B6: AffineMap (c,0) is_differentiable_on [#] REAL by A4, FDIFF_1:23;
D4: dom (AffineMap (c,0) `| [#]REAL) = [#]REAL by B6,FDIFF_1:def 7;
then
dom (AffineMap (c,0) `| [#]REAL) = REAL by SUBSET_1:def 3; then
B5: dom (AffineMap (c,0) `| [#]REAL) = dom AffineMap(0,c)
by FUNCT_2:def 1;
B3A: for x being Element of REAL st
x in dom (AffineMap (c,0) `| [#]REAL) holds
(AffineMap (c,0) `| [#]REAL) . x = AffineMap(0,c) . x
proof
let x be Element of REAL;
assume x in dom (AffineMap (c,0) `| [#]REAL); then
(AffineMap (c,0) `| [#]REAL) . x
= (0*x) + c by D4,A5,A4, FDIFF_1:23
.= AffineMap(0,c) . x by FCONT_1:def 4;
hence thesis;
end;
B21: ['a,b'] c= dom (AffineMap(0,c)) by FUNCT_2:def 1,R2;
set F3 = AffineMap (0,c);
reconsider F3 as PartFunc of REAL,REAL;
(F3 | ['a,b']) is continuous; then
AffineMap(0,c) is_integrable_on ['a,b'] &
AffineMap(0,c) | ['a,b'] is bounded
by INTEGRA5:10,INTEGRA5:11,B21; then
B2: f `| [#]REAL is_integrable_on ['a,b'] &
(f `| [#]REAL) | ['a,b'] is bounded by B5,PARTFUN1:5,B3A;
B4: integral (AffineMap(0,c),['a,b'])
= integral ((f `| [#]REAL),['a,b']) by B5,PARTFUN1:5,B3A
.= f . (upper_bound ['a,b']) - f . (lower_bound ['a,b'])
by INTEGRA5:13,B1,B2,A5,A4,FDIFF_1:23
.= f . b - AffineMap(c,0) . (lower_bound ['a,b']) by LU1,INTEGRA1:5
.= f . b - AffineMap(c,0) . a by LU1,INTEGRA1:5
.= (c*b) + 0 - AffineMap(c,0) . a by FCONT_1:def 4
.= (c*b) - (c*a+0) by FCONT_1:def 4
.= c*(b-a);
a-a < b-a by A1,XREAL_1:9;
hence centroid (AffineMap (0,c),['a,b'])
= (a+b)/2 by XCMPLX_1:89,A2,B4,C3;
end;
theorem
for a,b be Real holds
(id REAL) is_integrable_on ['a,b'] & (id REAL) | ['a,b'] is bounded
proof
let a,b be Real;
reconsider iR = (id REAL) as PartFunc of REAL,REAL;
B1: iR | ['a,b'] is continuous;
['a,b'] c= dom iR;
hence thesis by INTEGRA5:11,INTEGRA5:10,B1;
end;
theorem Lm2:
(id REAL) is_integrable_on A & (id REAL) | A is bounded
proof
reconsider iR = id REAL as PartFunc of REAL,REAL;
B1: iR | A is continuous;
A c= dom iR;
hence thesis by INTEGRA5:11,INTEGRA5:10,B1;
end;
theorem Lm5:
for e being Real
for f being PartFunc of REAL,REAL st
A c= dom f & ( for x being Real st x in A holds f . x = e ) holds
( f is_integrable_on A & f | A is bounded &
integral (f,(lower_bound A),(upper_bound A))
= e * ((upper_bound A) - (lower_bound A)) )
proof
let e be Real;
let f be PartFunc of REAL,REAL;
assume that
A1: A c= dom f and
A2: for x being Real st x in A holds f . x = e;
B2: (lower_bound A)<=(upper_bound A) by SEQ_4:11;
A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4
.= ['(lower_bound A),(upper_bound A)'] by INTEGRA5:def 3,SEQ_4:11;
hence thesis by INTEGRA6:26,B2,A1,A2;
end;
theorem
for f be Function of REAL,REAL st
(for x be Real st x in A holds f.x = 0) holds
integral(f,A) = 0
proof
let f be Function of REAL,REAL;
assume A1: (for x be Real st x in A holds f.x = 0);
reconsider f as PartFunc of REAL,REAL;
B1x: dom f = REAL by FUNCT_2:def 1;
A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4
.= ['(lower_bound A),(upper_bound A)'] by INTEGRA5:def 3,SEQ_4:11;
then integral(f,A)
=integral (f,(lower_bound A),(upper_bound A)) by INTEGRA5:def 4,SEQ_4:11
.= 0 * ((upper_bound A) - (lower_bound A)) by Lm5,B1x,A1
.=0;
hence thesis;
end;
Lm4:
for f be PartFunc of REAL,REAL st A c= dom f &
(for x be Real st x in A holds f.x = 0) holds
integral(f,A) = 0
proof
let f be PartFunc of REAL,REAL;
assume that
B1: A c= dom f and
A1: (for x be Real st x in A holds f.x = 0);
A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4
.= ['(lower_bound A),(upper_bound A)'] by INTEGRA5:def 3,SEQ_4:11;
then
integral(f,A)
=integral (f,(lower_bound A),(upper_bound A)) by INTEGRA5:def 4,SEQ_4:11
.= 0 * ((upper_bound A) - (lower_bound A)) by Lm5,B1,A1
.=0;
hence thesis;
end;
theorem Lm3:
for f be Function of REAL,REAL st
f is_integrable_on A & f | A is bounded
holds
(id REAL) (#) f is_integrable_on A &
((id REAL) (#) f) | A is bounded
proof
let f be Function of REAL,REAL;
assume A1: f is_integrable_on A & f | A is bounded;
A4: dom f = REAL by FUNCT_2:def 1;
reconsider f as PartFunc of REAL,REAL;
A2: f is_integrable_on A & f | A is bounded by A1;
reconsider iR = (id REAL) as PartFunc of REAL,REAL;
A3: A c= dom iR;
B1: iR is_integrable_on A by Lm2;
iR | A is bounded by Lm2;
hence thesis by INTEGRA6:14,A2,A4,B1,A3,INTEGRA6:13;
end;
theorem
for a,b,c be Real st a < b holds
['a,b'] c= [#]REAL & lower_bound ['a,b'] = a & upper_bound ['a,b'] = b
proof
let a,b,c be Real;
assume A1: a < b;
R1: [#]REAL = REAL by SUBSET_1:def 3;
['a,b'] = [.(lower_bound ['a,b']),(upper_bound ['a,b']).]
& ['a,b'] =[.a,b.] by A1,INTEGRA5:def 3,INTEGRA1:4;
hence thesis by INTEGRA1:5,R1;
end;
theorem
for a,b,c be Real, f be Function of REAL,REAL st
a < b & b <= c &
f is_integrable_on ['a,c'] & f | ['a,c'] is bounded &
for x be Real st x in ['b,c'] holds f.x = 0
holds
centroid(f,['a,c']) = centroid(f,['a,b'])
proof
let a,b,c be Real;
let f be Function of REAL,REAL;
assume that
A1: a < b and
A2: b <= c and
A4: f is_integrable_on ['a,c'] and
A5: f | ['a,c'] is bounded and
A6: for x be Real st x in ['b,c'] holds f.x = 0;
B1: a <= c by A1,A2,XXREAL_0:2;
reconsider F=f as PartFunc of REAL,REAL;
B2: dom f = dom F & dom f = REAL by FUNCT_2:def 1;
B5: F | ['a,c'] is bounded by A5;
b in [.a,c.] by A1,A2; then
B3: b in ['a,c'] by INTEGRA5:def 3,A1,A2,XXREAL_0:2;
C1A: integral (F,a,c) = (integral (F,a,b)) + (integral (F,b,c))
by INTEGRA6:17,B1,A4,B5,B2,B3;
Q2: integral (f,['b,c']) = 0 by Lm4,B2,A6;
D2A: integral (f,['a,c'])
= integral (f,a,c) by INTEGRA5:def 4,A1,A2,XXREAL_0:2
.= (integral (f,a,b)) + 0 by C1A,INTEGRA5:def 4, A2,Q2
.= (integral (f,['a,b'])) by INTEGRA5:def 4,A1;
reconsider xf = (id REAL)(#)F as PartFunc of REAL,REAL;
E2: dom xf = REAL by FUNCT_2:def 1;
H1: REAL = dom (id REAL);
reconsider
iF = (id REAL) as PartFunc of REAL,REAL;
H2: iF is_integrable_on ['a,c'] by Lm2;
H3: iF | ['a,c'] is bounded by Lm2;
E4: iF (#) F is_integrable_on ['a,c'] by B2,A4,B5,H1,H2,H3,INTEGRA6:14;
E5: ((id REAL)(#)F) | ['a,c'] is bounded by B5,INTEGRA6:13,H3;
D1: xf is_integrable_on ['a,b'] & xf is_integrable_on ['b,c'] &
integral (xf,a,c) = (integral (xf,a,b)) + (integral (xf,b,c))
by INTEGRA6:17,B1,E4,E5,E2,B3;
A7: dom ((id REAL)(#)f) = REAL by FUNCT_2:52;
for x being Real st x in ['b,c'] holds xf.x = 0
proof
let x be Real;
assume R1: x in ['b,c'];
thus xf.x = ((id REAL).x) * (f.x) by VALUED_1:5
.= ((id REAL).x) * 0 by R1,A6
.= 0;
end; then
Q1: integral (xf,['b,c']) = 0 by A7,Lm4;
D3A: integral (xf,['a,c'])
= integral (xf,a,c) by INTEGRA5:def 4,A1,A2,XXREAL_0:2
.=integral (xf,a,b) + 0 by Q1,D1,INTEGRA5:def 4,A2
.= (integral (xf,['a,b'])) by A1,INTEGRA5:def 4;
centroid(f,['a,c'])
= integral((id REAL)(#)f,['a,c'])/(integral (f,['a,b'])) by D2A;
hence thesis by D3A;
end;
theorem
for a,b,c be Real, f be Function of REAL,REAL st
a <= b & b < c & f is_integrable_on ['a,c'] & f | ['a,c'] is bounded &
for x be Real st x in ['a,b'] holds f.x = 0
holds
centroid(f,['a,c']) = centroid(f,['b,c'])
proof
let a,b,c be Real;
let f be Function of REAL,REAL;
assume that
A1: a <= b and
A2: b < c and
A4: f is_integrable_on ['a,c'] and
A5: f | ['a,c'] is bounded and
A6: for x be Real st x in ['a,b'] holds f.x = 0;
B1: a <= c by A1,A2,XXREAL_0:2;
reconsider F=f as PartFunc of REAL,REAL;
B2A: dom f = REAL by FUNCT_2:def 1;
B5: F | ['a,c'] is bounded by A5;
b in [.a,c.] by A1,A2; then
B3: b in ['a,c'] by INTEGRA5:def 3,A1,A2,XXREAL_0:2;
integral (f,['a,b']) = 0 by Lm4,B2A,A6; then
Q2A: integral (f,a,b) = 0 by INTEGRA5:def 4, A1;
D2: integral (f,['a,c'])
= integral (f,a,c) by INTEGRA5:def 4,A1,A2,XXREAL_0:2
.= 0+(integral (f,b,c)) by INTEGRA6:17,A4,B5,B2A,B3,B1,Q2A
.= integral (f,['b,c']) by INTEGRA5:def 4,A2;
reconsider xf = (id REAL)(#)F as PartFunc of REAL,REAL;
E2: dom xf = REAL by FUNCT_2:def 1;
H1:REAL = dom (id REAL);
reconsider iF = id REAL as PartFunc of REAL,REAL;
H2: iF is_integrable_on ['a,c'] by Lm2;
H3: iF | ['a,c'] is bounded by Lm2; then
E4: iF (#) F is_integrable_on ['a,c'] by B2A,A4,B5,H1,H2,INTEGRA6:14;
E5: ((id REAL)(#)F) | ['a,c'] is bounded by H3,B5,INTEGRA6:13;
D1: xf is_integrable_on ['a,b'] & xf is_integrable_on ['b,c'] &
integral (xf,a,c) = (integral (xf,a,b)) + (integral (xf,b,c))
by INTEGRA6:17,E4,E5,E2,B3,B1;
A7: dom ((id REAL)(#)f) = REAL by FUNCT_2:52;
for x being Real st x in ['a,b'] holds xf.x = 0
proof
let x be Real;
assume R1: x in ['a,b'];
thus xf.x = ((id REAL).x) * (f.x) by VALUED_1:5
.= ((id REAL).x) * 0 by R1,A6
.= 0;
end; then
Q1: integral (xf,['a,b']) = 0 by A7,Lm4;
D3:integral (xf,['a,c'])
= integral (xf,a,c) by INTEGRA5:def 4,A1,A2,XXREAL_0:2
.= 0 + (integral (xf,b,c)) by Q1,D1,INTEGRA5:def 4,A1
.= (integral (xf,['b,c'])) by A2,INTEGRA5:def 4;
centroid(f,['a,c'])
= integral((id REAL)(#)f,['a,c'])/(integral (f,['b,c'])) by D2;
hence thesis by D3;
end;
theorem
for f being Function of REAL,REAL st
f is_integrable_on A & f | A is bounded & integral(f,A) > 0
holds
ex c being Real st c in A & f.c > 0
proof
let f be Function of REAL,REAL;
assume B1: f is_integrable_on A & f | A is bounded;
assume A1: integral(f,A) > 0;
assume A2: not ex c being Real st c in A & f.c > 0;
set g = (-1)(#)f;
ex r being Real st for y being set st y in dom (g | A) holds
|.(g | A).y.| < r
proof
consider r being Real such that
C1: for y being set st y in dom (f | A) holds |.(f | A).y.| < r
by COMSEQ_2:def 3,B1;
take r;
for y being set st y in dom (g | A) holds |.(g | A).y.| < r
proof
let y be set;
assume C4: y in dom (g|A);
C7: dom (f|A) = A & dom (g|A) = A by FUNCT_2:def 1;
|.(g | A).y.| = |.((-1)(#)f).y.| by FUNCT_1:49,C4
.= |.(-1)*(f.y).| by VALUED_1:6
.= |.-(f.y).|
.= |. f.y .| by COMPLEX1:52
.= |.(f | A).y.| by FUNCT_1:49,C4;
hence thesis by C1,C4,C7;
end;
hence thesis;
end; then
A4: (g | A) | A is bounded by COMSEQ_2:def 3;
for x be Real st x in A holds 0 <= g|A.x
proof
let x be Real;
assume C2: x in A;
C3: f.x <= 0 by A2,C2;
g|A.x = ((-1)(#)f).x by FUNCT_1:49,C2
.=(-1)*(f.x) by VALUED_1:6;
hence thesis by C3;
end; then
A6: 0 <= integral(g|A) by A4,INTEGRA2:32;
reconsider f as PartFunc of REAL,REAL;
dom f = REAL by FUNCT_2:def 1; then
A c= dom f & f is_integrable_on A & f | A is bounded by B1;
then
integral (((-1)(#)f),A) = (-1) * (integral (f,A)) by INTEGRA6:9;
hence contradiction by A1,A6,INTEGRA5:def 2;
end;
theorem
for r be Real, f be FuzzySet of REAL, F be Function of REAL,REAL st
r > 0 & f is_integrable_on A & f | A is bounded &
for x being Real holds F.x = min(r, f.x)
holds
integral(F,A) >= 0
proof
let r be Real;
let f be FuzzySet of REAL;
let F be Function of REAL,REAL;
assume that
A1: r > 0 and
A2: f is_integrable_on A & f | A is bounded and
A4: for x being Real holds F.x = min(r, f.x);
ex r being Real st for y being set st y in dom (F | A) holds
|.(F | A).y.| < r
proof
consider e being Real such that
C1: for y being set st y in dom (f | A) holds |.(f | A).y.| < e
by COMSEQ_2:def 3,A2;
take max(r,e)+1;
M1: max(r,e)+0 < max(r,e)+1 by XREAL_1:8;
for y being set st y in dom (F | A) holds |.(F | A).y.| < max(r,e)+1
proof
let x be set;
assume B1: x in dom (F | A);
B3a: dom (f|A) = A by FUNCT_2:def 1;
reconsider x as Real by B1;
per cases by XXREAL_0:15;
suppose D1: min(r, f.x) = r;
|.F|A.x.| = |.F.x .|by FUNCT_1:49,B1
.= |. r .| by D1,A4
.= r by A1,ABSVALUE:def 1;then
|.F|A.x.| <= max(r,e) by XXREAL_0:25;
hence thesis by M1,XXREAL_0:2;
end;
suppose D2: min(r, f.x) = f.x;
B44: |.F|A.x.| = |.F.x .| by FUNCT_1:49,B1
.= |. f.x .| by D2,A4
.= |. f|A.x .| by FUNCT_1:49,B1;
e <= max(r,e) by XXREAL_0:25; then
|.F|A.x.| < max(r,e) by XXREAL_0:2,C1,B3a,B1,B44;
hence thesis by XXREAL_0:2,M1;
end;
end;
hence thesis;
end; then
A5: ((F|A) | A) is bounded by COMSEQ_2:def 3;
for x be Real st x in A holds 0 <= F|A.x
proof
let x be Real;
assume C2: x in A;
per cases by XXREAL_0:15;
suppose D3: min(r, f.x) = r;
F|A.x = F.x by FUNCT_1:49,C2
.= r by D3,A4;
hence thesis by A1;
end;
suppose D4: min(r, f.x) = f.x;
reconsider x as Element of REAL by C2;
F|A.x = F.x by FUNCT_1:49,C2
.= f.x by D4,A4;
hence thesis by FUZZY_2:1;
end;
end;
then 0 <= integral(F|A) by A5,INTEGRA2:32;
hence 0 <= integral (F,A) by INTEGRA5:def 2;
end;
theorem Th13:
for f,g be Function of REAL,REAL holds
min(f,g) = (1/2) (#) ((f + g) - abs(f - g))
proof
let f,g be Function of REAL,REAL;
D1: REAL = dom ((1/2) (#) ((f + g)-abs(f - g))) by FUNCT_2:52;
for x being object st x in dom min(f,g) holds
min(f,g) . x = ((1/2) (#) ((f + g)-abs(f - g))) . x
proof
let x be object;
assume A0: x in dom min(f,g); then
A1: x in REAL; then
A2: x in dom ((f + g)-abs(f - g)) by FUNCT_2:52;
A3: x in dom(f-g) by A1,FUNCT_2:52;
A4: x in dom(f+g) by A1,FUNCT_2:52;
reconsider x as Element of REAL by A0;
((1/2) (#) ((f + g)-abs(f - g))) . x = (1/2)*(((f + g)-abs(f - g)) . x )
by VALUED_1:6
.= (1/2)*((f + g).x - abs(f - g).x ) by VALUED_1:13,A2
.= (1/2)*((f + g).x - |. (f - g).x .| ) by VALUED_1:18
.= (1/2)*((f + g).x - |. f.x - g.x .| ) by VALUED_1:13,A3
.= (1/2)*((f.x + g.x) - |. f.x - g.x .| ) by VALUED_1:def 1,A4
.= ((f.x + g.x) - |. f.x - g.x .| ) / 2
.= min(f.x,g.x) by COMPLEX1:73;
hence thesis by COUSIN2:def 1;
end;
hence thesis by FUNCT_1:2,D1,FUNCT_2:52;
end;
theorem Th12:
for f,g be 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) )
proof
let f,g be Function of REAL,REAL;
assume that
A1A: f is_integrable_on A & f | A is bounded and
A2A: g is_integrable_on A & g | A is bounded;
reconsider fm = min(f,g) as PartFunc of REAL,REAL;
reconsider f as PartFunc of REAL,REAL;
reconsider 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 thesis by Th13,i5,B5,INTEGRA6:11,A1,A2,Df,Dg;
end;
theorem Th15:
for f,g be Function of REAL,REAL holds
max(f,g) = (1/2) (#) (f + g + abs(f - g))
proof
let f,g be Function of REAL,REAL;
D1: REAL = dom ((1/2) (#) ((f + g)+abs(f - g))) by FUNCT_2:52;
for x being object st x in dom max(f,g) holds
max(f,g) . x = ((1/2) (#) ((f + g)+abs(f - g))) . x
proof
let x be object;
assume A0: x in dom max(f,g); then
A1: x in REAL; then
A2: x in dom ((f + g)+abs(f - g)) by FUNCT_2:52;
A3: x in dom(f-g) by A1,FUNCT_2:52;
A4: x in dom(f+g) by A1,FUNCT_2:52;
reconsider x as Element of REAL by A0;
((1/2) (#) ((f + g)+abs(f - g))) . x
= (1/2)*(((f + g)+abs(f - g)) . x ) by VALUED_1:6
.= (1/2)*((f + g).x + abs(f - g).x ) by VALUED_1:def 1,A2
.= (1/2)*((f + g).x + |. (f - g).x .| ) by VALUED_1:18
.= (1/2)*((f + g).x + |. f.x - g.x .| ) by VALUED_1:13,A3
.= (1/2)*((f.x + g.x) + |. f.x - g.x .| ) by VALUED_1:def 1,A4
.= ((f.x + g.x) + |. f.x - g.x .| ) / 2
.= max(f.x,g.x) by COMPLEX1:74;
hence thesis by COUSIN2:def 2;
end;
hence thesis by FUNCT_1:2,D1,FUNCT_2:52;
end;
theorem
for f,g be Function of REAL,REAL st
f is_integrable_on A & f | A is bounded &
g is_integrable_on A & g | A is bounded
holds
max(f,g) is_integrable_on A & max(f,g) | A is bounded &
integral(max(f,g),A)
= (1/2)*( integral(f,A) + integral(g,A) + integral(abs(f-g),A) )
proof
let f,g be Function of REAL,REAL;
assume that
A1A: f is_integrable_on A & f | A is bounded and
A2A: g is_integrable_on A & g | A is bounded;
reconsider fm = max(f,g) as PartFunc of REAL,REAL;
reconsider f,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;
i2: (f-g) is_integrable_on A by A1,A2,INTEGRA6:11,Dg,Df;
B2: (f-g) | (A /\ A) is bounded by A1A,A2A,RFUNCT_1:84; then
i3: (abs(f-g)) is_integrable_on A by i2,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:83;
then
i5: (1/2)(#)((f+g) + abs(f-g)) is_integrable_on A
by i4,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 Th15
.= (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 thesis by Th15,i5,B5,INTEGRA6:11,A1,A2,Df,Dg;
end;
theorem Th16X:
for r1,r2 be Real, f be Function of REAL,REAL st
f is_integrable_on A & f | A is bounded
holds
min(AffineMap(0,r1),(r2 (#) f)) is_integrable_on A &
min(AffineMap(0,r1),(r2 (#) f)) | A is bounded
proof
let r1,r2 be Real, f be Function of REAL,REAL;
assume that
A2: f is_integrable_on A and
A3: f | A is bounded;
A c= REAL; then
Df: A c= dom f by FUNCT_2:def 1;
A c= REAL; then
B21: A c= dom (AffineMap(0,r1)) by FUNCT_2:def 1;
set F3 = AffineMap (0,r1);
reconsider f,F3 as PartFunc of REAL,REAL;
C1: (F3 | A) is continuous;
A23: f is_integrable_on A & f | A is bounded by A2,A3;
reconsider f,F3 as Function of REAL,REAL;
F3 is_integrable_on A & F3 | A is bounded
& (r2 (#) f) is_integrable_on A & (r2 (#) f) | A is bounded
by INTEGRA6:9,Df,A23,RFUNCT_1:80,C1,INTEGRA5:10,INTEGRA5:11,B21;
hence thesis by Th12;
end;
theorem
for r1,r2 be Real, f,F be Function of REAL,REAL st
f is_integrable_on A & f | A is bounded &
for x being Real holds F.x = min(r1, r2*(f.x))
holds
F is_integrable_on A & F | A is bounded
proof
let r1,r2 be Real;
let f,F be Function of REAL,REAL;
assume that
A2: f is_integrable_on A & f | A is bounded and
A4: for x being Real holds F.x = min(r1, r2*(f.x));
DD: REAL = dom F
& REAL = dom min(AffineMap(0,r1),(r2 (#) f)) by FUNCT_2:52;
for x being object st x in dom F holds
F . x = min(AffineMap(0,r1),(r2 (#) f)) . x
proof
let x be object;
assume A0: x in dom F;
reconsider x as Element of REAL by A0;
min(AffineMap(0,r1),(r2 (#) f)) . x
= min(AffineMap(0,r1).x,(r2 (#) f).x) by COUSIN2:def 1
.= min(0*x+r1,(r2 (#) f).x) by FCONT_1:def 4
.= min(r1,r2 * (f.x)) by VALUED_1:6;
hence thesis by A4;
end; then
F = min(AffineMap(0,r1),(r2 (#) f)) by FUNCT_1:2,DD;
hence thesis by A2,Th16X;
end;
theorem Th19:
for s be Real, f,g being Function of REAL,REAL holds
( f | ].-infty,s.[ ) +* ( g | [.s,+infty.[ )
is Function of REAL,REAL
proof
let s be Real;
let f,g being Function of REAL,REAL;
set F = (f | ].-infty,s.[) +* (g | [.s,+infty.[);
set g1= f| (].-infty,s.[);
set g2= g| ([.s,+infty.[);
D3: -infty < s & s < +infty by XXREAL_0:9,XXREAL_0:12,XREAL_0:def 1;
Dg: dom F = (dom g1) \/ (dom g2) by FUNCT_4:def 1
.= (].-infty,s.[) \/ (dom g2) by FUNCT_2:def 1
.=(].-infty,s.[) \/ ([.s,+infty.[) by FUNCT_2:def 1
.=REAL by XXREAL_1:224,XXREAL_1:173,D3;
for x being object st x in REAL holds F . x in REAL
by XREAL_0:def 1;
hence thesis by FUNCT_2:3,Dg;
end;
theorem
for a,b,c being Real, f,g,F be Function of REAL,REAL st
a <= b & b <= c &
F = f | [.a,b.] +* g | [.b,c.]
holds
F is Function of ['a,c'],REAL
proof
let a,b,c be Real;
let f,g,F be Function of REAL,REAL;
set g1 = f | [.a,b.];
set g2 = g | [.b,c.];
assume that
A1: a <= b & b <= c and
A2: F = f | [.a,b.] +* g | [.b,c.];
Dg: dom F = (dom g1) \/ (dom g2) by FUNCT_4:def 1,A2
.= ([.a,b.]) \/ (dom g2) by FUNCT_2:def 1
.=([.a,b.]) \/ ( [.b,c.]) by FUNCT_2:def 1
.=([. a,c .]) by XXREAL_1:165,A1
.= ['a,c'] by INTEGRA5:def 3,XXREAL_0:2,A1;
for x being object st x in ['a,c'] holds F . x in REAL
by XREAL_0:def 1;
hence thesis by FUNCT_2:3,Dg;
end;
theorem Th25:
for a,b,c being Real, f,g,F be Function of REAL,REAL st
a <= b & b <= c & F = f | [.a,b.] +* g | [.b,c.]
holds
F = F | [. a,c .]
proof
let a,b,c be Real;
let f,g,F be Function of REAL,REAL;
set g1 = f | [.a,b.];
set g2 = g | [.b,c.];
assume that
A1: a <= b & b <= c and
A2: F = f | [.a,b.] +* g | [.b,c.];
dom F = (dom g1) \/ (dom g2) by FUNCT_4:def 1,A2
.= ([.a,b.]) \/ (dom g2) by FUNCT_2:def 1
.=([.a,b.]) \/ ( [.b,c.]) by FUNCT_2:def 1
.=[. a,c .] by XXREAL_1:165,A1;
hence thesis;
end;
theorem
for a,b,c being Real, f,g,h be Function of REAL,REAL st
a <= b & b <= c &
f | ['a,c'] is bounded & g | ['a,c'] is bounded &
h = (f| [.a,b.]) +* (g | [.b,c.]) & f.b = g.b
holds
h | ['a,c'] is bounded
proof
let a,b,c be Real, f,g,h be Function of REAL,REAL;
assume that
A1: a <= b & b <= c and
A2: f | ['a,c'] is bounded and
A3: g | ['a,c'] is bounded and
A4: h = (f| [.a,b.]) +* (g | [.b,c.]) and
A5: f.b = g.b;
B10: (f| [.a,b.]) tolerates (g | [.b,c.])
proof
for x being object st x in (dom (f| [.a,b.])) /\ (dom (g | [.b,c.]))
holds (f| [.a,b.]) . x = (g | [.b,c.]) . x
proof
let x be object;
assume T1: x in (dom (f| [.a,b.])) /\ (dom (g | [.b,c.]));
T2: (dom (f| [.a,b.])) /\ (dom (g | [.b,c.]))
= [.a,b.] /\ (dom (g | [.b,c.])) by FUNCT_2:def 1
.= [.a,b.] /\ [.b,c.] by FUNCT_2:def 1
.= {b} by XXREAL_1:418,A1; then
(f| [.a,b.]) . x = (f| [.a,b.]) . b by TARSKI:def 1,T1
.= g.b by A5,FUNCT_1:49,XXREAL_1:1,A1
.= (g | [.b,c.]) . b by FUNCT_1:49,XXREAL_1:1,A1;
hence thesis by TARSKI:def 1,T1,T2;
end;
hence thesis by PARTFUN1:def 4;
end;
ex r being Real st for y being set st y in dom (h | ['a,c']) holds
|.(h | ['a,c']).y.| < r
proof
consider r being Real such that
C1: for y being set st y in dom (f | ['a,c']) holds |.(f | ['a,c']).y.| < r
by COMSEQ_2:def 3,A2;
consider r1 being Real such that
C2: for y being set st y in dom (g | ['a,c']) holds |.(g | ['a,c']).y.| < r1
by COMSEQ_2:def 3,A3;
take max(r,r1);
for x being set st x in dom (h | ['a,c']) holds
|. (h | ['a,c']).x .| < max(r,r1)
proof
let x be set;
assume
B1: x in dom (h | ['a,c']);
D1: ['a,c'] = dom (f | ['a,c']) by FUNCT_2:def 1;
D2: ['a,c'] = dom (g | ['a,c']) by FUNCT_2:def 1;
B2: x in ['a,c'] by B1;
reconsider x as Real by B1;
x in [.a,c.] by INTEGRA5:def 3,A1,XXREAL_0:2,B2; then
BB2: a <= x & x <= c by XXREAL_1:1;
per cases;
suppose S1: x < b; then
x in [.a,b.] by BB2; then
B4: x in dom (f| [.a,b.]) by FUNCT_2:def 1;
E1: |. (h | ['a,c']).x .|
= |.((f| [.a,b.]) +* (g | [.b,c.])).x.| by A4,FUNCT_1:49,B1
.= |. (f| [.a,b.]).x .| by FUNCT_4:15,B4,B10
.= |. (f ).x .| by FUNCT_1:49,XXREAL_1:1,BB2,S1
.= |. (f | ['a,c']).x .| by FUNCT_1:49,B1;
r <= max(r,r1) by XXREAL_0:25;
hence thesis by XXREAL_0:2,E1,C1,B1, D1;
end;
suppose S2: x >= b; then
x in [.b,c.] by BB2; then
D4: x in dom (g|[.b,c.]) by FUNCT_2:def 1;
E2: |. (h | ['a,c']).x .|
= |.((f| [.a,b.]) +* (g | [.b,c.])).x.| by A4,FUNCT_1:49,B1
.= |. (g|[.b,c.]).x .| by FUNCT_4:13,D4
.= |. g.x .| by FUNCT_1:49,BB2,XXREAL_1:1,S2
.= |. (g | ['a,c']).x .| by FUNCT_1:49,B1;
r1 <= max(r,r1) by XXREAL_0:25;
hence thesis by XXREAL_0:2,C2,B1, D2,E2;
end;
end;
hence thesis;
end;
hence thesis by COMSEQ_2:def 3;
end;
theorem Th18B:
for a,b,c being Real, f,g,h be Function of REAL,REAL st
a <= b & b <= c &
f | ['a,c'] is bounded & g | ['a,c'] is bounded &
h | [.a,c.] = (f| [.a,b.]) +* (g | [.b,c.]) & f.b = g.b
holds
h | ['a,c'] is bounded
proof
let a,b,c be Real, f,g,h be Function of REAL,REAL;
assume that
A1: a <= b & b <= c and
A2: f | ['a,c'] is bounded and
A3: g | ['a,c'] is bounded and
A4: h | [.a,c.] = (f| [.a,b.]) +* (g | [.b,c.]) and
A5: f.b = g.b;
B10: (f| [.a,b.]) tolerates (g | [.b,c.])
proof
for x being object st x in (dom (f| [.a,b.])) /\ (dom (g | [.b,c.]))
holds (f| [.a,b.]) . x = (g | [.b,c.]) . x
proof
let x be object;
assume T1: x in (dom (f| [.a,b.])) /\ (dom (g | [.b,c.]));
T2: (dom (f| [.a,b.])) /\ (dom (g | [.b,c.]))
= [.a,b.] /\ (dom (g | [.b,c.])) by FUNCT_2:def 1
.= [.a,b.] /\ [.b,c.] by FUNCT_2:def 1
.= {b} by XXREAL_1:418,A1; then
(f| [.a,b.]) . x = (f| [.a,b.]) . b by TARSKI:def 1,T1
.= g.b by A5,FUNCT_1:49,XXREAL_1:1,A1
.= (g | [.b,c.]) . b by FUNCT_1:49,XXREAL_1:1,A1;
hence thesis by TARSKI:def 1,T1,T2;
end;
hence thesis by PARTFUN1:def 4;
end;
ex r being Real st for y being set st y in dom (h | ['a,c']) holds
|.(h | ['a,c']).y.| < r
proof
consider r being Real such that
C1: for y being set st y in dom (f | ['a,c']) holds |.(f | ['a,c']).y.| < r
by COMSEQ_2:def 3,A2;
consider r1 being Real such that
C2: for y being set st y in dom (g | ['a,c']) holds |.(g | ['a,c']).y.| < r1
by COMSEQ_2:def 3,A3;
take max(r,r1);
for x being set st x in dom (h | ['a,c']) holds
|. (h | ['a,c']).x .| < max(r,r1)
proof
let x be set;
assume
B1: x in dom (h | ['a,c']);
D1: ['a,c'] = dom (f | ['a,c']) by FUNCT_2:def 1;
D2: ['a,c'] = dom (g | ['a,c']) by FUNCT_2:def 1;
B2: x in ['a,c'] by B1;
reconsider x as Real by B1;
x in [.a,c.] by INTEGRA5:def 3,A1,XXREAL_0:2,B2;
then
BB2: a <= x & x <= c by XXREAL_1:1;
per cases;
suppose S1: x < b; then
x in [.a,b.] by BB2; then
B4: x in dom (f| [.a,b.]) by FUNCT_2:def 1;
E1: |. (h | ['a,c']).x .|
= |.((f| [.a,b.]) +* (g | [.b,c.])).x.|
by A4,INTEGRA5:def 3,A1,XXREAL_0:2
.= |. (f| [.a,b.]).x .| by FUNCT_4:15,B4,B10
.= |. (f ).x .| by FUNCT_1:49,XXREAL_1:1,BB2,S1
.= |. (f | ['a,c']).x .| by FUNCT_1:49,B1;
r <= max(r,r1) by XXREAL_0:25;
hence thesis by XXREAL_0:2,E1,C1,B1, D1;
end;
suppose S2: x >= b; then
x in [.b,c.] by BB2; then
D4: x in dom (g|[.b,c.]) by FUNCT_2:def 1;
E2: |. (h | ['a,c']).x .|
= |.((f| [.a,b.]) +* (g | [.b,c.])).x.| by A4,INTEGRA5:def 3,A1,XXREAL_0:2
.= |. (g|[.b,c.]).x .| by FUNCT_4:13,D4
.= |. g.x .| by FUNCT_1:49,BB2,XXREAL_1:1,S2
.= |. (g | ['a,c']).x .| by FUNCT_1:49,B1;
r1 <= max(r,r1) by XXREAL_0:25;
hence thesis by XXREAL_0:2,C2,B1, D2,E2;
end;
end;
hence thesis;
end;
hence thesis by COMSEQ_2:def 3;
end;
theorem Th18X:
for c being Real, f,g be Function of REAL,REAL st
f | A is bounded & g | A is bounded
holds
( (f | ].-infty,c.[) +* (g | [.c,+infty.[) ) | A is bounded
proof
let c being Real;
let f,g be Function of REAL,REAL;
assume that
A2: f | A is bounded and
A4: g | A is bounded;
set F = ((f|].-infty,c.[) +* (g|[.c,+infty.[));
reconsider F as Function of REAL,REAL by Th19;
ex r being Real st for y being set st y in dom (F | A) holds
|.(F | A).y.| < r
proof
consider r being Real such that
C1: for y being set st y in dom (f | A) holds |.(f | A).y.| < r
by COMSEQ_2:def 3,A2;
consider r1 being Real such that
C2: for y being set st y in dom (g | A) holds |.(g | A).y.| < r1
by COMSEQ_2:def 3,A4;
take max(r,r1);
for x being set st x in dom (F | A) holds |. (F | A).x .| < max(r,r1)
proof
let x be set;
assume B1: x in dom (F | A);
D1: A = dom (f | A) by FUNCT_2:def 1;
D2: A = dom (g | A) by FUNCT_2:def 1;
reconsider x as Real by B1;
per cases;
suppose S1: x < c; then
B4: not ( x in dom (g|[.c,+infty.[)) by XXREAL_1:236;
E1: |. (F | A).x .| = |. F.x .| by FUNCT_1:49,B1
.= |. (f|].-infty,c.[).x .| by FUNCT_4:11,B4
.= |. (f ).x .| by FUNCT_1:49,XXREAL_1:233,S1
.= |. (f | A).x .| by FUNCT_1:49,B1;
r <= max(r,r1) by XXREAL_0:25;
hence thesis by XXREAL_0:2,E1,C1, B1, D1;
end;
suppose S2: x >= c; then
x in [.c,+infty.[ by XXREAL_1:236; then
D4: x in dom (g|[.c,+infty.[) by FUNCT_2:def 1;
E2: |. (F | A).x .| = |. F.x .| by FUNCT_1:49,B1
.= |. (g|[.c,+infty.[).x .| by FUNCT_4:13,D4
.= |. g.x .| by FUNCT_1:49,XXREAL_1:236,S2
.= |. (g | A).x .| by FUNCT_1:49,B1;
r1 <= max(r,r1) by XXREAL_0:25;
hence thesis by XXREAL_0:2,C2,B1, D2,E2;
end;
end;
hence thesis;
end;
hence thesis by COMSEQ_2:def 3;
end;
theorem Lm22b1:
for a,b,c be Real, f,g,h,F be Function of REAL,REAL st
a <= b & b <= c & f is continuous & g is continuous &
h | [.a,c.] = (f | [.a,b.]) +* (g | [.b,c.]) & f.b = g.b & F = h | [.a,c.]
holds
F is continuous
proof
let a,b,c be Real, f,g,h,F be Function of REAL,REAL;
assume that
A1: a <= b & b <= c and
A2: f is continuous & g is continuous and
A3: h | [.a,c.] = (f| [.a,b.]) +* (g | [.b,c.]) and
A4: f.b = g.b and
A99: F = h | [.a,c.];
A6: dom f = REAL & dom g = REAL by FUNCT_2:def 1;
A5a: dom h = REAL by FUNCT_2:def 1;
DGG: dom (g | [.b,c.]) = [.b,c.] by FUNCT_2:def 1;
Bin: b in [.a,b.] & b in [.b,c.] by A1;
reconsider f as PartFunc of REAL,REAL;
reconsider g as PartFunc of REAL,REAL;
reconsider h as PartFunc of REAL,REAL;
A2a: f | [.a,b.] is continuous
& g | [.b,c.] is continuous by A2;
for x0, r being Real st x0 in [.a,c.] & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Real st x1 in [.a,c.] & |.(x1 - x0).| < s holds
|.((h . x1) - (h . x0)).| < r ) )
proof
let x0, r be Real;
assume P1a: x0 in [.a,c.];
assume P2: 0 < r;
P1: a <= x0 & x0 <= c by P1a,XXREAL_1:1;
ex s being Real st
( 0 < s & ( for x1 being Real st x1 in [.a,c.] & |.(x1 - x0).| < s holds
|.((h . x1) - (h . x0)).| < r ) )
proof
per cases;
suppose B1: x0 < b; then
B1a: x0 in [.a,b.] by P1; then
consider sf being Real such that
P3: 0 < sf and
P4: ( for x1 being Real st x1 in [.a,b.] & |.(x1 - x0).| < sf holds
|.((f . x1) - (f . x0)).| < r/2 ) by P2,FCONT_1:14,A2a,A6;
consider sg being Real such that
Q1: 0 < sg and
Q2: ( for x1 being Real st x1 in [.b,c.] & |.(x1 - b).| < sg holds
|.((g . x1) - (g . b)).| < r/2 ) by P2,Bin,FCONT_1:14,A2a,A6;
take min(sf,sg);
for x1 being Real st x1 in [.a,c.] & |.(x1 - x0).| < min(sf,sg) holds
|.((h . x1) - (h . x0)).| < r
proof
let x1 be Real;
assume that
P5: x1 in [.a,c.] and
P6: |.(x1 - x0).| < min(sf,sg);
RMin: min(sf,sg) <= sf & min(sf,sg) <= sg by XXREAL_0:17;
P5a: a <= x1 & x1 <= c by P5,XXREAL_1:1;
per cases;
suppose R1: x1 >= b; then
R2:x1 in [.b,c.] by P5a;
R1a: x1 -b >= b-b by XREAL_1:13,R1; then
x1 - x0 > 0 by B1,XREAL_1:15;
then
R4: x1 - b = |.(x1 - b).| & |.(x1 - x0).| = x1 - x0
by R1a,COMPLEX1:43; then
|.(x1 - b).| < |.(x1 - x0).| by B1,XREAL_1:15;
then
|.(x1 - b).| < min(sf,sg) by P6,XXREAL_0:2;then
|.(x1 - b).| < sg by RMin,XXREAL_0:2; then
R6: |.((g . x1) - (g . b)).| < r/2 by R2,Q2;
b - x0 > x0 - x0 by B1,XREAL_1:14;then
R7b: b-x0 = |. b-x0 .| by COMPLEX1:43;
|. b-x0 .| <= |.(x1 - x0).| by R1,XREAL_1:9,R7b,R4;
then |. b-x0 .| < min(sf,sg) by P6,XXREAL_0:2;then
|. b-x0 .| < sf by RMin,XXREAL_0:2; then
R7: |.((f . b) - (f . x0)).| < r/2 by Bin,P4;
G1i: x1 in dom (g | [.b,c.]) by R1,P5a,DGG;
G0n: not x0 in dom (g | [.b,c.]) by DGG,B1,XXREAL_1:1;
R8: |. (g . x1 - g . b) + (f.b - f . x0) .| <=
|. g . x1 - g . b .|+ |.f.b - f . x0.| by COMPLEX1:56;
R99: |. g . x1 - g . b .|+ |.f.b - f . x0.| < r/2+r/2
by R7,R6,XREAL_1:8;
|.((h . x1) - (h . x0)).|
= |. ((f| [.a,b.]) +* (g | [.b,c.])) . x1 - h . x0.| by A3,FUNCT_1:49,P5
.= |. (g | [.b,c.]) . x1 - h . x0.| by G1i,FUNCT_4:13
.= |. g . x1 - h . x0.| by FUNCT_1:49,R2
.= |. g . x1 - ((f| [.a,b.]) +* (g | [.b,c.])) . x0.|
by A3,FUNCT_1:49,P1a
.= |. g . x1 - (f| [.a,b.]) . x0.| by G0n,FUNCT_4:11
.= |. g . x1 - g . b + f.b - f . x0.| by A4,FUNCT_1:49,B1a;
hence thesis by R99,R8,XXREAL_0:2;
end;
suppose S1: x1 < b; then :: x1 in [.a,b.] & x0 in [.a,b.]
P7: not x1 in dom (g|[.b,c.]) by DGG,XXREAL_1:1;
P7a: not x0 in dom (g|[.b,c.]) by DGG,B1,XXREAL_1:1;
P8: x1 in [.a,b.] by P5a,S1;
P9a: r/2 +0 < r/2+ r/2 by P2,XREAL_1:8;
|.x1-x0.| < sf by P6,RMin,XXREAL_0:2; then
|.((f . x1) - (f . x0)).| < r/2 by P8,P4; then
P9: |.((f . x1) - (f . x0)).| < r by XXREAL_0:2,P9a;
|.((h . x1) - (h . x0)).|
= |. h | [.a,c.] . x1 - h . x0.| by FUNCT_1:49,P5
.= |. (f| [.a,b.]) . x1 - h . x0.| by P7,FUNCT_4:11,A3
.= |. (f) . x1 - h . x0.| by FUNCT_1:49,P8
.= |. (f) . x1 - ((f| [.a,b.]) +* (g | [.b,c.])) . x0.|
by A3,FUNCT_1:49,P1a
.= |. (f) . x1 - ((f| [.a,b.]) ) . x0.| by P7a,FUNCT_4:11;
hence thesis by P9,FUNCT_1:49,B1a;
end;
end;
hence thesis by P3,Q1,XXREAL_0:21;
end;
suppose B2: b <= x0; then
x0 in [.b,c.] by P1; then
consider sg being Real such that
S1a: 0 < sg and
S1: ( for x1 being Real st x1 in [.b,c.] & |. x1 - x0 .| < sg holds
|. g . x1 - g . x0 .| < r/2 ) by FCONT_1:14,A2a,A6,P2;
consider sf being Real such that
S2a: 0 < sf and
S2: ( for x1 being Real st x1 in [.a,b.] & |.(x1 - b).| < sf holds
|. f . x1 - f . b .| < r/2 ) by P2,FCONT_1:14,A2a,A6,Bin;
RMin: min(sf,sg) <= sf & min(sf,sg) <= sg by XXREAL_0:17;
take min(sf,sg);
for x1 being Real st x1 in [.a,c.] & |.(x1 - x0).| < min(sf,sg) holds
|.((h . x1) - (h . x0)).| < r
proof
let x1 be Real;
assume that
S3: x1 in [.a,c.] and
S4: |.(x1 - x0).| < min(sf,sg);
S3a: a <= x1 & x1 <= c by S3,XXREAL_1:1;
per cases;
suppose Q1: x1 < b; then :: x1 in [.a,b.] x0 in [.b,c.]
X11: not (x1 in dom(g | [.b,c.])) by DGG,XXREAL_1:1;
X12: x1 in [.a,b.] by S3a,Q1;
X03: x0 in dom(g | [.b,c.]) by B2,P1,DGG;
BB0: x0 -b >= b-b by XREAL_1:13,B2;then
x0 - x1 > 0 by Q1,XREAL_1:15; then
Xabs: x0 - b = |.(x0 - b).| & |.x0 - x1.| = x0 - x1
by BB0,COMPLEX1:43; then
|.(x0 - b).| < |.x0 - x1.| by Q1,XREAL_1:15; then
|.(x0 - b).| < |.-(x0 - x1).| by COMPLEX1:52; then
|.-(x0 - b).| < |.(x1 - x0).| by COMPLEX1:52; then
|.b-x0.| < min(sf,sg) by S4,XXREAL_0:2;then
|.b-x0.| < sg by RMin,XXREAL_0:2;then
S1a: |. g . b - g . x0 .| < r/2 by S1,Bin;
b - x1 > x1 - x1 by Q1,XREAL_1:14;then
R7b: b-x1 = |. b-x1 .| by COMPLEX1:43;
|. b-x1 .| <= |.(x0 - x1).| by B2,XREAL_1:9,R7b,Xabs;
then
|. b-x1 .| <= |.-(x0 - x1).| by COMPLEX1:52;then
|. b-x1 .| < min(sf,sg) by S4,XXREAL_0:2;then
|. b-x1 .| < sf by RMin,XXREAL_0:2;then
|. -(b-x1) .| < sf by COMPLEX1:52;then
|. x1 - b .| < sf;then
S2a: |. f . x1 - f . b .| < r/2 by S2,X12;
HH: |.((h . x1) - (h . x0)).|
= |. ((f| [.a,b.]) +* (g | [.b,c.])) . x1 - h . x0.|
by A3,FUNCT_1:49,S3
.= |. (f| [.a,b.]) . x1 - h . x0.| by X11,FUNCT_4:11
.= |. f . x1 - h . x0.| by FUNCT_1:49,S3a,Q1,XXREAL_1:1
.= |. f . x1 - ((f| [.a,b.]) +* (g | [.b,c.])) . x0.|
by A3,FUNCT_1:49,P1a
.= |. f . x1 - (g | [.b,c.]) . x0.| by X03,FUNCT_4:13
.= |. f . x1 - f . b + g.b - g . x0.|
by A4,FUNCT_1:49,B2,P1,XXREAL_1:1;
C156: |. (f . x1 - f . b) + (g.b - g . x0) .|
<= |. f . x1 - f . b .| + |. g.b - g . x0.| by COMPLEX1:56;
|. f . x1 - f . b .| + |. g.b - g . x0.| < r/2+r/2
by S1a,S2a,XREAL_1:8;
hence thesis by HH,C156,XXREAL_0:2;
end;
suppose b <= x1; then :: x1 in [.b,c.] x0 in [.b,c.]
QX1: x1 in [.b,c.] by S3a;
QX0: x0 in [.b,c.] by B2,P1;
P9a: r/2 +0 < r/2+ r/2 by P2,XREAL_1:8;
|.x1-x0.| < sg by S4,RMin,XXREAL_0:2; then
P9j: |.((g . x1) - (g . x0)).| < r/2 by S1,QX1;
|.((h . x1) - (h . x0)).|
= |. h | [.a,c.] . x1 - h . x0.| by FUNCT_1:49,S3
.= |. (g | [.b,c.]) . x1 - h . x0.| by FUNCT_4:13,DGG,QX1,A3
.= |. g . x1 - h . x0.| by FUNCT_1:49,QX1
.= |. g . x1 - (h | [.a,c.]) . x0.| by FUNCT_1:49,P1a
.= |. g . x1 - (g | [.b,c.]) . x0.| by DGG,QX0,FUNCT_4:13,A3
.= |.((g . x1) - (g . x0)).| by FUNCT_1:49,QX0;
hence |.((h . x1) - (h . x0)).| < r by P9j,P9a,XXREAL_0:2;
end;
end;
hence thesis by S1a,S2a,XXREAL_0:21;
end;
end;
hence thesis;
end;
hence thesis by A99,FCONT_1:14,A5a;
end;
Th24:
for a,b,c be Real, f,g be Function of REAL,REAL,
F be Function of REAL,REAL st
a <= b & b <= c & f is continuous & g is continuous &
F = (f | [.a,b.]) +* (g | [.b,c.]) & f.b = g.b
holds
F is continuous
proof
let a,b,c be Real, f,g,F be Function of REAL,REAL;
assume that
A1: a <= b & b <= c and
A2: f is continuous & g is continuous and
A3: F = (f| [.a,b.]) +* (g | [.b,c.]) and
A4: f.b = g.b;
F = F | [.a,c.] by Th25,A1,A3;
hence thesis by Lm22b1,A1,A2,A3,A4;
end;
theorem integra51011:
for A being non empty closed_interval Subset of REAL,
f be Function of REAL,REAL st
f is continuous holds f is_integrable_on A & f | A is bounded
proof
let A being non empty closed_interval Subset of REAL,
f be Function of REAL,REAL;
assume A1: f is continuous;
DD: REAL = dom f by FUNCT_2:def 1;
reconsider ff = f as PartFunc of REAL,REAL;
ff | A is continuous by A1;
hence f is_integrable_on A & f | A is bounded by INTEGRA5:11,INTEGRA5:10,DD;
end;
theorem Th20:
for c being Real, f,g,F be Function of REAL,REAL st
f is Lipschitzian & g is Lipschitzian &
f . c = g . c & F = (f | ].-infty,c.[) +* (g | [.c,+infty.[)
holds F is Lipschitzian
proof
let c being Real;
let f,g,F be Function of REAL,REAL;
assume that
A1: f is Lipschitzian and
A2: g is Lipschitzian and
A3: f . c = g . c and
A4: F = (f|].-infty,c.[) +* (g|[.c,+infty.[);
cR: c in REAL by XREAL_0:def 1; then
Dfc: c in dom f by FUNCT_2:def 1;
Dgc: c in dom g by FUNCT_2:def 1,cR;
consider rf being Real such that
RF: 0 < rf and
A5: for x1, x2 being Real st x1 in dom f & x2 in dom f holds
|.((f . x1) - (f . x2)).| <= rf * |.(x1 - x2).| by A1;
consider rg being Real such that
0 < rg and
A6: for x1, x2 being Real st x1 in dom g & x2 in dom g holds
|.((g . x1) - (g . x2)).| <= rg * |.(x1 - x2).| by A2;
ex r being Real st
( 0 < r &
( for x1, x2 being Real st x1 in dom F & x2 in dom F holds
|.(F . x1) - (F . x2).| <= r * |. x1 - x2 .| ) )
proof
take max(rf,rg);
A7: max(rf,rg) > 0 by RF,XXREAL_0:25;
for x1, x2 being Real st x1 in dom F & x2 in dom F holds
|.(F . x1) - (F . x2).| <= max(rf,rg) * |.x1 - x2.|
proof
let x1, x2 being Real;
assume that
x1 in dom F and
x2 in dom F;
x1 in REAL & x2 in REAL by XREAL_0:def 1;
then
Dx: x1 in dom f & x1 in dom g &
x2 in dom f & x2 in dom g by FUNCT_2:def 1;
per cases;
suppose B1: x1 < c; then
B7: not ( x1 in dom (g|[.c,+infty.[)) by XXREAL_1:236;
per cases;
suppose B2: x2 < c; then
B14: not ( x2 in dom (g|[.c,+infty.[)) by XXREAL_1:236;
B15: |.(F . x1) - (F . x2).|
= |.(f|].-infty,c.[) . x1
- (((f|].-infty,c.[) +* (g|[.c,+infty.[)) . x2).|
by FUNCT_4:11,B7,A4
.= |.(f|].-infty,c.[) . x1 - (f|].-infty,c.[) . x2.| by FUNCT_4:11,B14
.= |.f.x1 - (f|].-infty,c.[) . x2.| by FUNCT_1:49,XXREAL_1:233,B1;
0 <= |.x1 - x2.| by COMPLEX1:46; then
B17: rf * |.x1 - x2.| <= max(rf,rg) * |.x1 - x2.|
by XREAL_1:64,XXREAL_0:25;
|.(f . x1) - (f . x2).| <= rf * |.x1 - x2.| by A5,Dx; then
|.(f . x1) - (f . x2).| <= max(rf,rg) * |.x1 - x2.|
by XXREAL_0:2,B17;
hence thesis by B15,FUNCT_1:49,XXREAL_1:233,B2;
end;
suppose B3: x2 >= c; then
x2 in [.c,+infty.[ by XXREAL_1:236; then
B6: x2 in dom (g|[.c,+infty.[) by FUNCT_2:def 1;
B9: |.(F . x1) - (F . x2).| = |.(f|].-infty,c.[) . x1
- (((f|].-infty,c.[) +* (g|[.c,+infty.[)) . x2).|
by FUNCT_4:11,B7,A4
.= |.(f|].-infty,c.[) . x1 - (g|[.c,+infty.[) . x2.| by FUNCT_4:13,B6
.= |.f.x1 - (g|[.c,+infty.[) . x2.| by FUNCT_1:49,XXREAL_1:233,B1;
B8: |.f.x1 - f.c .| <= rf * |.x1 - c.| &
|. g.c - g.x2.| <= rg * |.c - x2.| by A5,A6,Dx,Dfc,Dgc;
|.x1 - c.| >= 0 & |.c - x2.| >= 0 by COMPLEX1:46; then
rf * |.x1 - c.| <= max(rf,rg)*|.x1 - c.| &
rg * |.c - x2.| <= max(rf,rg)*|.c - x2.| by XREAL_1:64,XXREAL_0:25;
then
|.f.x1 - f.c .| <= max(rf,rg) *|.x1 - c.| &
|. g.c - g.x2.| <= max(rf,rg) * |.c - x2.| by XXREAL_0:2, B8;
then
|.f.x1 - f.c .| <= max(rf,rg) * (-(x1 - c)) &
|. g.c - g.x2.| <= max(rf,rg) * (-(c - x2))
by COMPLEX1:70,B3,XREAL_1:47,B1;
then
B12X: |.f.x1 - f.c .| + |. g.c - g.x2.|
<= max(rf,rg) * (-(x1 - c)) + max(rf,rg) * (-(c - x2)) by XREAL_1:7;
B13: |.f.x1 - g.x2.| <= |.f.x1 - f.c .| + |. f.c - g.x2.| by COMPLEX1:63;
(x2 - x1) <= |. x2 -x1 .| by COMPLEX1:76; then
(x2 - x1) <= |. x1 -x2 .| by COMPLEX1:60; then
(x2 - x1)*max(rf,rg) <= |. x1 -x2 .|*max(rf,rg) by A7,XREAL_1:64;
then
|.f.x1 - f.c .| + |. g.c - g.x2.| <= max(rf,rg) * |. x1 -x2 .|
by XXREAL_0:2,B12X; then
|.f.x1 - g.x2.| <= max(rf,rg) * |. x1 -x2 .| by XXREAL_0:2,B13,A3;
hence |.(F . x1) - (F . x2).| <= max(rf,rg) * |. x1 -x2 .|
by B9,FUNCT_1:49,XXREAL_1:236,B3;
end;
end;
suppose C1: x1 >= c; then
x1 in [.c,+infty.[ by XXREAL_1:236; then
C5: x1 in dom (g|[.c,+infty.[) by FUNCT_2:def 1;
per cases;
suppose C2: x2 < c; then
C6: not ( x2 in dom (g|[.c,+infty.[)) by XXREAL_1:236;
C12: |.(F . x1) - (F . x2).| = |.(g|[.c,+infty.[) . x1
- (( (f|].-infty,c.[) +* (g|[.c,+infty.[) ). x2).|
by FUNCT_4:13,C5,A4
.= |.(g|[.c,+infty.[) . x1 - (f|].-infty,c.[) . x2.| by FUNCT_4:11,C6
.= |.g.x1 - (f|].-infty,c.[) . x2.| by FUNCT_1:49,XXREAL_1:236,C1;
C9: |.g.x1 - g.c .| <= rg * |.x1 - c.| &
|. f.c - f.x2.| <= rf * |.c - x2.| by A5,A6,Dx,Dfc,Dgc;
|.x1 - c.| >= 0 & |.c - x2.| >= 0 by COMPLEX1:46;
then
rg * |.x1 - c.| <= max(rf,rg)*|.x1 - c.| &
rf * |.c - x2.| <= max(rf,rg)*|.c - x2.| by XREAL_1:64,XXREAL_0:25;
then
|.g.x1 - g.c .| <= max(rf,rg) *|.x1 - c.| &
|. f.c - f.x2.| <= max(rf,rg) * |.c - x2.| by XXREAL_0:2, C9;
then
|.g.x1 - g.c .| <= max(rf,rg) * ((x1 - c)) &
|. f.c - f.x2.| <= max(rf,rg) * ((c - x2))
by COMPLEX1:43,C2,C1,XREAL_1:48;
then
C10: |. g.x1 - g.c .| + |. f.c - f.x2.|
<= max(rf,rg) * (x1 - c) + max(rf,rg) * (c - x2) by XREAL_1:7;
C11: |.g.x1 - f.x2.| <= |. g.x1 - g.c .| + |. g.c - f.x2.|
by COMPLEX1:63;
(x1 - x2)*max(rf,rg) <= |. x1 -x2 .|*max(rf,rg)
by A7,XREAL_1:64,COMPLEX1:76;
then
|. g.x1 - g.c .| + |. f.c - f.x2.| <= max(rf,rg) * |. x1 -x2 .|
by XXREAL_0:2,C10;
then
|.g.x1 - f.x2.| <= max(rf,rg) * |. x1 -x2 .| by XXREAL_0:2,C11,A3;
hence |.(F . x1) - (F . x2).| <= max(rf,rg) * |. x1 -x2 .|
by FUNCT_1:49,XXREAL_1:233,C2,C12;
end;
suppose C3: x2 >= c; then
x2 in [.c,+infty.[ by XXREAL_1:236; then
C8: x2 in dom (g|[.c,+infty.[) by FUNCT_2:def 1;
C13: |.(F . x1) - (F . x2).|
= |.(g|[.c,+infty.[) . x1
- (((f|].-infty,c.[) +* (g|[.c,+infty.[)) . x2).| by FUNCT_4:13,C5,A4
.= |.(g|[.c,+infty.[) . x1 - (g|[.c,+infty.[) . x2.| by FUNCT_4:13,C8
.= |.g.x1 - (g|[.c,+infty.[) . x2.| by FUNCT_1:49,XXREAL_1:236,C1;
0 <= |.x1 - x2.| by COMPLEX1:46; then
C14: rg * |.x1 - x2.| <= max(rf,rg) * |.x1 - x2.|
by XREAL_1:64,XXREAL_0:25;
|.(g . x1) - (g . x2).| <= rg * |.x1 - x2.| by A6,Dx;
then
|.(g . x1) - (g . x2).| <= max(rf,rg) * |.x1 - x2.|
by XXREAL_0:2,C14;
hence thesis by C13,FUNCT_1:49,XXREAL_1:236,C3;
end;
end;
end;
hence thesis by RF,XXREAL_0:25;
end;
hence thesis;
end;
theorem Th21:
for a,b being Real holds (AffineMap (a,b)) is Lipschitzian
proof
let a,b being Real;
set f = AffineMap (a,b);
ex r being Real st
( 0 < r & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds
|. (f . x1) - (f . x2) .| <= r * |. x1 - x2.| ) )
proof
take |. a .|+1;
|. a .| >= 0 by COMPLEX1:46;
hence |. a .|+1 > 0;
thus for x1, x2 being Real st x1 in dom f & x2 in dom f holds
|. (f . x1) - (f . x2) .| <= (|. a .|+1) * |. x1 - x2.|
proof
let x1, x2 be Real;
assume x1 in dom f & x2 in dom f;
B2: |. a .|+1 > |. a .|+0 by XREAL_1:8;
BB: |.(x1-x2).| >= 0 by COMPLEX1:46;
|. (f . x1) - (f . x2) .| =|. a*x1+b- (f . x2) .| by FCONT_1:def 4
.= |. a*x1+b- (a*x2+b) .| by FCONT_1:def 4
.= |.a*(x1-x2).|
.= |.a.|*|.(x1-x2).| by COMPLEX1:65;
hence thesis by XREAL_1:64,B2,BB;
end;
end;
hence thesis;
end;
theorem Th17L:
for a,b,p,q being Real, f be Function of REAL,REAL st a <> p &
f = ( AffineMap (a,b) | ].-infty,(q-b)/(a-p).[ )
+* ( AffineMap (p,q) | [.(q-b)/(a-p),+infty.[ )
holds f is Lipschitzian
proof
let a,b,p,q being Real, f be Function of REAL,REAL;
assume that
AP: a <> p and
AF: f = ( AffineMap (a,b) | ].-infty,(q-b)/(a-p).[ )
+* ( AffineMap (p,q) | [.(q-b)/(a-p),+infty.[ );
set fa = AffineMap (a,b);
set fp = AffineMap (p,q);
B1: a-p <> 0 by AP;
A1: fa is Lipschitzian by Th21;
A2: fp is Lipschitzian by Th21;
B2: fa.((q-b)/(a-p)) = a*((q-b)/(a-p))+b by FCONT_1:def 4
.= a*(q-b)/(a-p)+b by XCMPLX_1:74
.= (a*(q-b)+(a-p)*b)/(a-p) by XCMPLX_1:113,B1;
fp.((q-b)/(a-p)) = p*((q-b)/(a-p))+q by FCONT_1:def 4
.= p*(q-b)/(a-p)+q by XCMPLX_1:74
.= (p*(q-b)+(a-p)*q)/(a-p) by XCMPLX_1:113,B1;
hence thesis by Th20,AF,A1,A2,B2;
end;
theorem Th17X:
for a,b,p,q being Real, f be Function of REAL,REAL st a <> p &
f = ( AffineMap (a,b) | ].-infty,(q-b)/(a-p).[ )
+* ( AffineMap (p,q) | [.(q-b)/(a-p),+infty.[ )
holds
f is_integrable_on A & f | A is bounded
proof
let a,b,p,q being Real, f be Function of REAL,REAL;
assume that
A1: a <> p and
A2: f = ( AffineMap (a,b) | ].-infty,(q-b)/(a-p).[ )
+* ( AffineMap (p,q) | [.(q-b)/(a-p),+infty.[ );
reconsider f as PartFunc of REAL,REAL;
A3: REAL = dom f by FUNCT_2:def 1;
f is Lipschitzian by Th17L,A1,A2;
then
f | A is continuous;
hence thesis by INTEGRA5:10,INTEGRA5:11,A3;
end;
theorem Th17E:
for a,b,p,q being Real st a <> p holds
(AffineMap (a,b)) . ((q-b)/(a-p)) = (AffineMap (p,q)) . ((q-b)/(a-p))
proof
let a,b,p,q being Real;
assume a <> p;
then
B1: a-p <> 0;
B2: AffineMap (a,b).((q-b)/(a-p)) = a*((q-b)/(a-p))+b by FCONT_1:def 4
.= a*(q-b)/(a-p)+b by XCMPLX_1:74
.= (a*(q-b)+(a-p)*b)/(a-p) by XCMPLX_1:113,B1;
AffineMap (p,q).((q-b)/(a-p)) = p*((q-b)/(a-p))+q by FCONT_1:def 4
.= p*(q-b)/(a-p)+q by XCMPLX_1:74
.= (p*(q-b)+(a-p)*q)/(a-p) by XCMPLX_1:113,B1;
hence thesis by B2;
end;
theorem
for f be Membership_Func of REAL holds f is bounded
proof
let f be Membership_Func of REAL;
ex r being Real st for x being set st x in dom f holds
|. f.x .| < r
proof
take 1+1;
thus for x being set st x in dom f holds
|. f.x .| < 1+1
proof
let x be set;
assume x in dom f; then
reconsider x as Element of REAL;
f.x = |.f.x.| by FUZZY_2:1,COMPLEX1:43; then
|.f.x.|+0 < 1+1 by XREAL_1:8,FUZZY_2:1;
hence thesis;
end;
end;
hence thesis by COMSEQ_2:def 3;
end;
theorem
for r be Real, f be Function of REAL,REAL st
r <> 0 & f is_integrable_on A & f | A is bounded
holds
centroid((r (#) f),A) = centroid(f,A)
proof
let r be Real;
let f be Function of REAL,REAL;
assume that
A0: r <> 0 and
A1: f is_integrable_on A and
A2: f | A is bounded;
A3: f | A is integrable by A1,INTEGRA5:def 1;
A4: (f | A) | A is bounded by A2;
B4: integral((r (#) f),A)
= integral((r (#) f) | A) by INTEGRA5:def 2
.= integral(r (#) (f|A)) by RFUNCT_1:49
.= r * integral (f|A) by INTEGRA2:31,A3,A4
.= r * integral(f,A) by INTEGRA5:def 2;
B5: (((id REAL) (#) f) | A) is integrable &
(((id REAL) (#) f) | A) | A is bounded
by INTEGRA5:def 1,Lm3,A1,A2;
integral((id REAL) (#) (r (#) f),A)
= integral(r (#) ((id REAL) (#) f),A) by RFUNCT_1:13
.= integral((r (#) ((id REAL) (#) f)) |A) by INTEGRA5:def 2
.= integral((r (#) ((id REAL) (#) f) |A) ) by RFUNCT_1:49
.= r * integral( ((id REAL) (#) f) |A ) by INTEGRA2:31,B5
.= r * integral( (id REAL) (#) f,A ) by INTEGRA5:def 2;
hence centroid((r (#) f),A)
= centroid(f,A) by XCMPLX_1:91,A0,B4;
end;
theorem Th18Z:
for a,b,c being Real, f,g,h be Function of REAL,REAL st
a <= b & b <= c &
f is_integrable_on ['a,c'] & f | ['a,c'] is bounded &
g is_integrable_on ['a,c'] & g | ['a,c'] is bounded &
h | [.a,c.] = (f| [.a,b.]) +* (g | [.b,c.]) &
h is_integrable_on ['a,c'] & f.b = g.b
holds
integral(h,['a,c']) = integral(f,['a,b']) + integral(g,['b,c'])
proof
let a,b,c be Real, f,g,h be Function of REAL,REAL;
assume that
A1: a <= b & b <= c and
A2: f is_integrable_on ['a,c'] & f | ['a,c'] is bounded and
A3: g is_integrable_on ['a,c'] & g | ['a,c'] is bounded and
A4: h | [.a,c.] = (f| [.a,b.]) +* (g | [.b,c.]) and
A0: h is_integrable_on ['a,c'] and
A5: f.b = g.b;
B10: (f| [.a,b.]) tolerates (g | [.b,c.])
proof
for x being object st x in (dom (f| [.a,b.])) /\ (dom (g | [.b,c.])) holds
(f| [.a,b.]) . x = (g | [.b,c.]) . x
proof
let x being object;
assume T1: x in (dom (f| [.a,b.])) /\ (dom (g | [.b,c.]));
T2: (dom (f| [.a,b.])) /\ (dom (g | [.b,c.]))
= [.a,b.] /\ (dom (g | [.b,c.])) by FUNCT_2:def 1
.= [.a,b.] /\ [.b,c.] by FUNCT_2:def 1
.= {b} by XXREAL_1:418,A1;
(f| [.a,b.]) . x
= (f| [.a,b.]) . b by TARSKI:def 1,T1,T2
.= f.b by FUNCT_1:49,XXREAL_1:1,A1
.= (g | [.b,c.]) . b by FUNCT_1:49,XXREAL_1:1,A1,A5;
hence thesis by TARSKI:def 1,T1,T2;
end;
hence thesis by PARTFUN1:def 4;
end;
reconsider h1 = (h | ['a,b']) as PartFunc of ['a,b'],REAL;
reconsider f1 = (f | ['a,b']) as PartFunc of ['a,b'],REAL;
reconsider H = upper_sum_set h1 as Function of (divs ['a,b']),REAL;
reconsider F = upper_sum_set f1 as Function of (divs ['a,b']),REAL;
A6: H = F
proof
for D being object st D in (divs ['a,b']) holds
H . D = F . D
proof
let D be object;
assume D in (divs ['a,b']);then
reconsider D as Division of ['a,b'] by INTEGRA1:def 3;
set uvh1 = upper_volume (h1,D);
set uvf1 = upper_volume (f1,D);
len D = len uvh1 & len D = len uvf1 by INTEGRA1:def 6;then
A8: dom uvh1 = dom uvf1 by FINSEQ_3:29;
B4: uvh1 = uvf1
proof
for i being Element of NAT st i in dom uvh1 holds uvh1 . i = uvf1 . i
proof
let i be Element of NAT;
assume B1: i in dom (upper_volume (h1,D));
len D = len uvh1 by INTEGRA1:def 6;then
B2: i in dom D by FINSEQ_3:29,B1;
B5: (divset (D,i)) c= ['a,b'] by INTEGRA1:8,B2;
B7: h | (divset (D,i)) = f | (divset (D,i))
proof
for x being object st x in divset (D,i) holds
(h | (divset (D,i))) . x = (f | (divset (D,i))) . x
proof
let x be object;
assume
B8: x in divset (D,i); then
B9X: x in ['a,b'] by B5; then
B9: x in [.a,b.] by INTEGRA5:def 3,A1;
reconsider x as Real by B8;
a <= x & x <= b by XXREAL_1:1,B9; then
B9c: a <= x & x <= c by XXREAL_0:2,A1;
dom (f| [.a,b.]) = [.a,b.] by FUNCT_2:def 1; then
B11: x in dom (f| [.a,b.]) by B9X,INTEGRA5:def 3,A1;
(h | (divset (D,i))).x = h . x by B8,FUNCT_1:49
.= (h | [.a,c.]).x by FUNCT_1:49,B9c,XXREAL_1:1
.= (f| [.a,b.]) .x by B10,FUNCT_4:15,B11,A4
.= f.x by B9,FUNCT_1:49;
hence thesis by B8,FUNCT_1:49;
end;
hence thesis by FUNCT_2:12;
end;
B3: h1 | (divset (D,i)):: = (h | ['a,b']) | (divset (D,i))
= h | (divset (D,i)) by B5,FUNCT_1:51
.= f1 | (divset (D,i)) by B5,FUNCT_1:51,B7;
uvh1 . i
= (upper_bound (rng (f1 | (divset (D,i))))) * (vol (divset (D,i)))
by B3,INTEGRA1:def 6,B2;
hence thesis by INTEGRA1:def 6,B2;
end;
hence thesis by PARTFUN1:5,A8;
end;
H . D = upper_sum (h1,D) by INTEGRA1:def 10
.= Sum (upper_volume (f1,D)) by B4,INTEGRA1:def 8
.= upper_sum (f1,D) by INTEGRA1:def 8
.= F . D by INTEGRA1:def 10;
hence thesis;
end;
hence thesis by FUNCT_2:12;
end;
B6: integral (h,['a,b']) = integral h1 by INTEGRA5:def 2
.= upper_integral h1 by INTEGRA1:def 17
.= lower_bound (rng (upper_sum_set f1)) by A6,INTEGRA1:def 14
.= upper_integral f1 by INTEGRA1:def 14
.= integral f1 by INTEGRA1:def 17
.= integral (f,['a,b']) by INTEGRA5:def 2;
reconsider h2 = (h | ['b,c']) as PartFunc of ['b,c'],REAL;
reconsider g1 = (g | ['b,c']) as PartFunc of ['b,c'],REAL;
reconsider H1 = upper_sum_set h2 as Function of (divs ['b,c']),REAL;
reconsider G = upper_sum_set g1 as Function of (divs ['b,c']),REAL;
A66: H1 = G
proof
for D being object st D in (divs ['b,c']) holds
H1 . D = G . D
proof
let D be object;
assume D in (divs ['b,c']);then
reconsider D as Division of ['b,c'] by INTEGRA1:def 3;
set uvh2 = upper_volume (h2,D);
set uvg1 = upper_volume (g1,D);
len D = len uvh2 & len D = len uvg1 by INTEGRA1:def 6;then
A8: dom uvh2 = dom uvg1 by FINSEQ_3:29;
B4: uvh2 = uvg1
proof
for i being Element of NAT st i in dom uvh2 holds uvh2 . i = uvg1 . i
proof
let i be Element of NAT;
assume B1: i in dom (upper_volume (h2,D));
reconsider i as Nat;
len D = len uvh2 by INTEGRA1:def 6;then
B2: i in dom D by FINSEQ_3:29,B1;
B5: (divset (D,i)) c= ['b,c'] by INTEGRA1:8,B2;
B7: h | (divset (D,i)) = g | (divset (D,i))
proof
for x being object st x in divset (D,i) holds
(h | (divset (D,i))) . x = (g | (divset (D,i))) . x
proof
let x be object;
assume
B8: x in divset (D,i); then
B9X: x in ['b,c'] by B5; then
B9: x in [.b,c.] by INTEGRA5:def 3,A1;
reconsider x as Real by B8;
b <= x & x <= c by XXREAL_1:1,B9; then
B9c: a <= x & x <= c by XXREAL_0:2,A1;
dom (g| [.b,c.]) = [.b,c.] by FUNCT_2:def 1; then
B11: x in dom (g| [.b,c.]) by B9X,INTEGRA5:def 3,A1;
(h | (divset (D,i))).x = h . x by B8,FUNCT_1:49
.= ((f| [.a,b.]) +* (g| [.b,c.])).x
by A4,FUNCT_1:49,B9c,XXREAL_1:1
.= (g| [.b,c.]) .x by FUNCT_4:13,B11
.= g.x by B9,FUNCT_1:49;
hence thesis by B8,FUNCT_1:49;
end;
hence thesis by FUNCT_2:12;
end;
B3: h2 | (divset (D,i))
= g | (divset (D,i)) by B7,B5,FUNCT_1:51
.= g1 | (divset (D,i)) by B5,FUNCT_1:51;
uvh2 . i
= (upper_bound (rng (g1 | (divset (D,i))))) * (vol (divset (D,i)))
by B3,INTEGRA1:def 6,B2;
hence thesis by INTEGRA1:def 6,B2;
end;
hence thesis by PARTFUN1:5,A8;
end;
H1 . D = upper_sum (h2,D) by INTEGRA1:def 10
.= Sum (upper_volume (g1,D)) by B4,INTEGRA1:def 8
.= upper_sum (g1,D) by INTEGRA1:def 8
.= G . D by INTEGRA1:def 10;
hence thesis;
end;
hence thesis by FUNCT_2:12;
end;
C1: integral (h,['b,c'])
= integral h2 by INTEGRA5:def 2
.= upper_integral h2 by INTEGRA1:def 17
.= lower_bound (rng (upper_sum_set g1)) by A66,INTEGRA1:def 14
.= upper_integral g1 by INTEGRA1:def 14
.= integral g1 by INTEGRA1:def 17
.= integral (g,['b,c']) by INTEGRA5:def 2;
reconsider h,f,g as PartFunc of REAL,REAL;
A04: a <= c by A1,XXREAL_0:2;
A01: h | ['a,c'] is bounded by A1,A2,A3,A4,A5,Th18B;
A02: dom h = REAL by FUNCT_2:def 1;
b in [.a,c.] by A1; then
A03: b in ['a,c'] by INTEGRA5:def 3,A1,XXREAL_0:2;
integral (h,['a,c'])
= integral (h,a,c) by INTEGRA5:def 4,A1,XXREAL_0:2
.= integral (h,a,b) + integral (h,b,c)
by INTEGRA6:17,A04,A0,A01,A03,A02
.= integral (f,['a,b']) + integral (h,b,c) by B6,INTEGRA5:def 4,A1
.= integral (f,['a,b']) + integral (h,['b,c']) by INTEGRA5:def 4,A1;
hence thesis by C1;
end;
theorem
for a,b,c be Real, f,g,h be Function of REAL,REAL st
a <= b & b <= c & f is continuous & g is continuous &
h = (f| [.a,b.]) +* (g | [.b,c.]) & f.b = g.b
holds
integral((id REAL) (#) h,['a,c'])
= integral((id REAL) (#) f,['a,b']) + integral((id REAL) (#) g,['b,c'])
proof
let a,b,c be Real, f,g,h be Function of REAL,REAL;
assume that
A1: a <= b & b <= c and
A2: f is continuous & g is continuous and
A3: h = (f| [.a,b.]) +* (g | [.b,c.]) and
A4: f.b = g.b;
A55: dom f = REAL & dom g = REAL by FUNCT_2:def 1;
set A = ['a,c'];
reconsider ff = f as PartFunc of REAL,REAL;
reconsider gg = g as PartFunc of REAL,REAL;
A2a: ff | A is continuous & gg | A is continuous by A2;
f is_integrable_on ['a,c'] & f | ['a,c'] is bounded &
g is_integrable_on ['a,c'] & g | ['a,c'] is bounded
by INTEGRA5:11,INTEGRA5:10,A2a,A55; then
B12: (id REAL) (#) f is_integrable_on ['a,c'] &
((id REAL) (#) f) | ['a,c'] is bounded &
(id REAL) (#) g is_integrable_on ['a,c'] &
((id REAL) (#) g) | ['a,c'] is bounded by Lm3;
set
G = ((id REAL) (#) f)| [.a,b.] +* ((id REAL) (#) g )| [.b,c.];
B3a: dom G
= dom(((id REAL) (#) f)| [.a,b.])
\/ dom(((id REAL) (#) g )| [.b,c.]) by FUNCT_4:def 1
.= [.a,b.]
\/ dom(((id REAL) (#) g )| [.b,c.]) by FUNCT_2:def 1
.= [.a,b.] \/ [.b,c.] by FUNCT_2:def 1
.=[. a,c .] by XXREAL_1:165,A1;
AC: REAL /\ [.a,c.] c= [. a,c .] & [. a,c .] c= REAL /\ [.a,c.]
by XBOOLE_0:def 4;
B3b: [. a,c .]
= REAL /\ [.a,c.] by AC,XBOOLE_0:def 10
.= (dom (id REAL (#) h)) /\ [.a,c.] by FUNCT_2:def 1;
for x being object st x in dom G holds G . x = (id REAL (#) h) . x
proof
let x be object;
assume Gx: x in dom G; then
reconsider x as Real by B3a;
C1: a <= x & x <= c by XXREAL_1:1,Gx,B3a;
per cases;
suppose b <= x; then
CC: x in [.b,c.] by C1; then
CC1:x in dom (((id REAL) (#) g )| [.b,c.]) by FUNCT_2:def 1;
CC2:x in dom ( g | [.b,c.]) by CC,FUNCT_2:def 1;
G . x
= (((id REAL) (#) g )| [.b,c.]).x by FUNCT_4:13,CC1
.= ((id REAL) (#) g ).x by FUNCT_1:49,CC
.= (id REAL).x * g .x by VALUED_1:5
.= (id REAL).x * (g | [.b,c.]) . x by FUNCT_1:49,CC
.= (id REAL).x * (((f| [.a,b.]) +* (g | [.b,c.])) . x) by CC2,FUNCT_4:13
.= (id REAL (#) h) . x by A3,VALUED_1:5;
hence thesis;
end;
suppose DX: x < b; then
CCa: x in [.a,b.] by C1;
DD1: not x in dom (((id REAL) (#) g )| [.b,c.]) by XXREAL_1:1,DX;
DD2: not x in dom ( g | [.b,c.]) by XXREAL_1:1,DX;
G . x
= (((id REAL) (#) f )| [.a,b.]).x by FUNCT_4:11,DD1
.= ((id REAL) (#) f ).x by FUNCT_1:49,CCa
.= (id REAL).x * f .x by VALUED_1:5
.= (id REAL).x * (f | [.a,b.]) . x by FUNCT_1:49,CCa
.= (id REAL).x * (((f| [.a,b.]) +* (g | [.b,c.])) . x) by DD2,FUNCT_4:11
.= (id REAL (#) h) . x by A3,VALUED_1:5;
hence thesis;
end;
end;
then
B3: (id REAL (#) h) | [.a,c.]
= ((id REAL) (#) f)| [.a,b.] +* ((id REAL) (#) g )| [.b,c.]
by FUNCT_1:46,B3a,B3b;
B4: ((id REAL) (#) f).b
= (id REAL).b * g.b by A4,VALUED_1:5
.= ((id REAL) (#) g).b by VALUED_1:5;
h is continuous by Th24,A1,A2,A3,A4; then
(id REAL) (#) h is_integrable_on ['a,c'] by integra51011;
hence integral((id REAL) (#) h,['a,c'])
= integral((id REAL) (#) f,['a,b']) + integral((id REAL) (#) g,['b,c'])
by Th18Z,A1,B12,B3,B4;
end;
theorem Th18E:
for c being Real, f,g be Function of REAL,REAL
holds
f|].-infty,c.[ +* g|[.c,+infty.[ = (f|].-infty,c.]) +* (g|[.c,+infty.[)
proof
let c be Real;
let f,g be Function of REAL,REAL;
set f1 = (f|].-infty,c.[) +* (g|[.c,+infty.[);
set f2 = (f|].-infty,c.]) +* (g|[.c,+infty.[);
A4: -infty < c & c < +infty by XXREAL_0:12,XXREAL_0:9,XREAL_0:def 1;
A2: dom f1
= dom (f|].-infty,c.[) \/ dom (g|[.c,+infty.[) by FUNCT_4:def 1
.= ].-infty,c.[ \/ dom (g|[.c,+infty.[) by FUNCT_2:def 1
.= ].-infty,c.[ \/ [.c,+infty.[ by FUNCT_2:def 1
.= ].-infty,+infty.[ by XXREAL_1:173,A4
.= ].-infty,c.] \/ [.c,+infty.[ by XXREAL_1:172,A4
.= dom (f | ].-infty,c.]) \/ [.c,+infty.[ by FUNCT_2:def 1
.= dom (f | ].-infty,c.]) \/ dom (g | [.c,+infty.[) by FUNCT_2:def 1
.= dom f2 by FUNCT_4:def 1;
Dg: dom (g|[.c,+infty.[) = [.c,+infty.[ by FUNCT_2:def 1;
for x being object st x in dom f1 holds
f1 . x = f2 . x
proof
let x be object;
assume A3: x in dom f1;
dom f1
= dom (f|].-infty,c.[) \/ dom (g|[.c,+infty.[) by FUNCT_4:def 1
.= ].-infty,c.[ \/ dom (g|[.c,+infty.[) by FUNCT_2:def 1
.= ].-infty,c.[ \/ [.c,+infty.[ by FUNCT_2:def 1
.= REAL by XXREAL_1:224,XXREAL_1:173,A4;
then reconsider x as Real by A3;
per cases;
suppose C1: x >= c;
((f|].-infty,c.[) +* (g|[.c,+infty.[)).x
= (g|[.c,+infty.[).x by FUNCT_4:13,Dg,C1,XXREAL_1:236;
hence thesis by FUNCT_4:13,Dg,C1,XXREAL_1:236;
end;
suppose C2: x < c;
].-infty,c.[ c= ].-infty,c.] by XXREAL_1:21;
then
C6: x in ].-infty,c.] by XXREAL_1:233,C2;
C4: not (x in dom (g|[.c,+infty.[) ) by C2,XXREAL_1:236;
((f|].-infty,c.[) +* (g|[.c,+infty.[)).x
= (f|].-infty,c.[).x by FUNCT_4:11,C4
.= f .x by FUNCT_1:49,XXREAL_1:233,C2
.= (f|].-infty,c.]).x by FUNCT_1:49,C6;
hence thesis by FUNCT_4:11,C4;
end;
end;
hence thesis by FUNCT_1:2,A2;
end;
theorem
for c being Real, f,g be Function of REAL,REAL st
f | A is bounded & g | A is bounded
holds
( (f|].-infty,c.]) +* (g|[.c,+infty.[) ) | A is bounded
proof
let c be Real, f,g be Function of REAL,REAL;
assume f | A is bounded & g | A is bounded; then
( (f|].-infty,c.[) +* (g|[.c,+infty.[) ) | A is bounded by Th18X;
hence thesis by Th18E;
end;
theorem
for a,b,c being Real, f,g be Function of REAL,REAL st a <= c & c <= b
holds
f | [.a,c.[ +* g | [.c,b.] = f | [.a,c.] +* g | [.c,b.]
proof
let a,b,c be Real;
let f,g be Function of REAL,REAL;
assume
A4: a <= c & c <= b;
set
f1 = (f|[.a,c.[) +* (g|[.c,b.]);
set
f2 = (f|[.a,c.]) +* (g|[.c,b.]);
A2: dom f1
= dom (f|[.a,c.[) \/ dom (g|[.c,b.]) by FUNCT_4:def 1
.= [.a,c.[ \/ dom (g|[.c,b.]) by FUNCT_2:def 1
.= [.a,c.[ \/ [.c,b.] by FUNCT_2:def 1
.= [.a,b.] by XXREAL_1:166,A4
.= [.a,c.] \/ [.c,b.] by XXREAL_1:165,A4
.= dom (f | [.a,c.]) \/ [.c,b.] by FUNCT_2:def 1
.= dom (f | [.a,c.]) \/ dom (g | [.c,b.]) by FUNCT_2:def 1
.= dom f2 by FUNCT_4:def 1;
Dg: dom (g|[.c,b.]) = [.c,b.] by FUNCT_2:def 1;
for x being object st x in dom f1 holds
f1 . x = f2 . x
proof
let x be object;
assume A3: x in dom f1;
A5: dom f1
= dom (f|[.a,c.[) \/ dom (g|[.c,b.]) by FUNCT_4:def 1
.= [.a,c.[ \/ dom (g|[.c,b.]) by FUNCT_2:def 1
.= [.a,c.[ \/ [.c,b.] by FUNCT_2:def 1
.= [.a,b.] by XXREAL_1:166,A4;
then
reconsider x as Real by A3;::XREAL_0:def 1,
A6: a <= x & x <= b by A5,A3,XXREAL_1:1;
per cases;
suppose C1: x >= c;
((f|[.a,c.[) +* (g|[.c,b.])).x
= (g|[.c,b.]).x by FUNCT_4:13,Dg,C1,XXREAL_1:1,A6;
hence thesis by FUNCT_4:13,Dg,C1,XXREAL_1:1,A6;
end;
suppose C2: x < c;
C6: x in [.a,c.] by A6,C2;
C4: not (x in dom (g|[.c,b.]) ) by C2,XXREAL_1:1;
((f|[.a,c.[) +* (g|[.c,b.])).x
= (f|[.a,c.[).x by FUNCT_4:11,C4::C7,FUNCT_2:def 1
.= f .x by FUNCT_1:49,XXREAL_1:3,A6,C2
.= (f|[.a,c.]).x by FUNCT_1:49,C6;
hence thesis by FUNCT_4:11,C4;
end;
end;
hence thesis by FUNCT_1:2,A2;
end;
theorem
for a,b,c being Real, f,g,h be Function of REAL,REAL st
a <= c & h | [.a,c.] = (f| [.a,b.]) +* (g | [.b,c.]) & f.b = g.b
holds
( b <= a implies h | [.a,c.] = g | [.a,c.] ) &
( c <= b implies h | [.a,c.] = f | [.a,c.] )
proof
let a,b,c being Real, f,g,h be Function of REAL,REAL;
assume that
A1: a <= c and
A2: h | [.a,c.] = (f| [.a,b.]) +* (g | [.b,c.]) and
A3: f.b = g.b;
A4: b <= a implies h | [.a,c.] = g | [.a,c.]
proof
assume A5X: b <= a;then
A5: [.a,c.] c= [.b,c.] by XXREAL_1:34;
h | [.a,c.] = (h | [.b,c.] ) | [.a,c.] by XXREAL_1:34,A5X,RELAT_1:74;
then
reconsider H = (h | [.b,c.] ) | [.a,c.] as Function of [.a,c.],REAL;
(h | [.b,c.] ) | [.a,c.] = g | [.a,c.]
proof
A6: dom (H) = [.a,c.] by FUNCT_2:def 1
.= dom (g | [.a,c.]) by FUNCT_2:def 1;
for x being object st x in dom (g | [.a,c.]) holds
((h | [.b,c.] ) | [.a,c.]) . x = (g | [.a,c.]) . x
proof
let x being object;
assume Dg: x in dom (g | [.a,c.]);
A8: x in [.b,c.] by A5,Dg;
A9: x in dom (g | [.b,c.]) by FUNCT_2:def 1,A8;
((h | [.b,c.] ) | [.a,c.]) . x
= (h | [.b,c.] ).x by FUNCT_1:49,Dg
.= (h ).x by FUNCT_1:49,A5,Dg
.= ((f| [.a,b.]) +* (g | [.b,c.])).x by A2,FUNCT_1:49,Dg
.= (g | [.b,c.]).x by A9,FUNCT_4:13
.= g.x by FUNCT_1:49,A5,Dg;
hence thesis by FUNCT_1:49,Dg;
end;
hence thesis by FUNCT_1:2,A6;
end;
hence thesis by RELAT_1:74,A5X,XXREAL_1:34;
end;
c <= b implies h | [.a,c.] = f | [.a,c.]
proof
assume A10: c <= b;
then
A5: [.a,c.] c= [.a,b.] by XXREAL_1:34;
reconsider H1 = (h | [.a,c.] ) as Function of [.a,c.],REAL;
reconsider F1 = (f | [.a,c.] ) as Function of [.a,c.],REAL;
for x being object st x in [.a,c.] holds H1 . x = F1 . x
proof
let x be object;
assume B2: x in [.a,c.]; then
B3: x in [.a,b.] by A5;
per cases;
suppose B5: c = b;
B6: x in dom (f | [.a,b.]) by FUNCT_2:def 1,B3;
TO: for x being object st x in (dom (f| [.a,b.])) /\ (dom (g | [.b,c.]))
holds
(f| [.a,b.]).x = (g | [.b,c.]).x
proof
let x be object;
assume B8: x in (dom (f| [.a,b.])) /\ (dom (g | [.b,c.]));
DX: (dom (f| [.a,b.])) /\ (dom (g | [.b,c.]))
= (dom (f| [.a,b.])) /\ ([.b,c.]) by FUNCT_2:def 1
.= [.a,b.] /\ [.b,b.] by B5,FUNCT_2:def 1
.= {b} by XXREAL_1:418,B5,A1;
C1: x = b by TARSKI:def 1,DX,B8;
(f| [.a,b.]).x = g.x by A3,FUNCT_1:49,C1, XXREAL_1:1,B5,A1;
hence thesis by FUNCT_1:49,B8;
end;
(h | [.a,c.]).x
= (f | [.a,b.]).x by B6,FUNCT_4:15, PARTFUN1:def 4,TO,A2
.= f.x by FUNCT_1:49,B2,A5;
hence thesis by FUNCT_1:49,B2;
end;
suppose c <> b; then
c < b by A10,XXREAL_0:1; then
B4: {} = [.b,c.] by XXREAL_1:29
.= dom (g | [.b,c.]) by FUNCT_2:def 1;
(h | [.a,c.]).x
= (f | [.a,b.]).x by B4,FUNCT_4:11,A2
.= f.x by FUNCT_1:49,B2,A5;
hence thesis by FUNCT_1:49,B2;
end;
end;
hence thesis by FUNCT_2:12;
end;
hence thesis by A4;
end;
theorem Th17AX:
for b being Real, f,g,h be Function of REAL,REAL st
h = (f| ].-infty,b.[) +* (g | [.b,+infty.[) & f.b = g.b holds
( b <= lower_bound A implies h | A = g | A ) &
( upper_bound A <= b implies h | A = f | A )
proof
let b being Real, f,g,h be Function of REAL,REAL;
assume that
A1: h = (f| ].-infty,b.[) +* (g | [.b,+infty.[) and
A2: f.b = g.b;
XX: b <= lower_bound A implies h | A = g | A
proof
assume A3: b <= lower_bound A;
B3: dom (h | A) = A by FUNCT_2:def 1
.= dom (g | A) by FUNCT_2:def 1;
for x being object st x in dom (h | A) holds (h | A).x = (g | A).x
proof
let x be object;
assume A4: x in dom (h | A); then
reconsider x as Real;
x in A by A4; then
x in [.lower_bound A, upper_bound A .] by INTEGRA1:4;
then
lower_bound A <= x & x <= upper_bound A by XXREAL_1:1;
then
x in [.b,+infty.[ by XXREAL_1:236,XXREAL_0:2,A3; then
B5: x in dom (g | [.b,+infty.[) by FUNCT_2:def 1;
(h | A).x
= ((f| ].-infty,b.[) +* (g | [.b,+infty.[)).x by A1,FUNCT_1:47,A4
.= (g | [.b,+infty.[).x by B5,FUNCT_4:13
.= g.x by FUNCT_1:47,B5;
hence thesis by FUNCT_1:49,A4;
end;
hence thesis by B3,FUNCT_1:2;
end;
upper_bound A <= b implies h | A = f | A
proof
assume A3: upper_bound A <= b;
B3: dom (h | A) = A by FUNCT_2:def 1
.= dom (f | A) by FUNCT_2:def 1;
for x being object st x in dom (h | A) holds (h | A).x = (f | A).x
proof
let x be object;
assume A4: x in dom (h | A); then
reconsider x as Real;
x in A by A4; then
x in [.lower_bound A, upper_bound A .] by INTEGRA1:4;
then
lower_bound A <= x & x <= upper_bound A by XXREAL_1:1;
then
A10: x <= b by XXREAL_0:2,A3;
per cases;
suppose C1: x = b; then
x in [.b,+infty.[ by XXREAL_1:236;then
C3: x in dom (g | [.b,+infty.[ ) by FUNCT_2:def 1;
(h | A).x
= ((f| ].-infty,b.[) +* (g | [.b,+infty.[)).x by A1,FUNCT_1:47,A4
.= (g | [.b,+infty.[).x by FUNCT_4:13,C3
.= f.x by C1,A2,FUNCT_1:49,XXREAL_1:236;
hence thesis by FUNCT_1:49,A4;
end;
suppose x <> b; then
C4: x < b by A10,XXREAL_0:1; then
C5: not (x in dom (g | [.b,+infty.[)) by XXREAL_1:236;
(h | A).x
= ((f| ].-infty,b.[) +* (g | [.b,+infty.[)).x by A1,FUNCT_1:47,A4
.= (f| ].-infty,b.[).x by C5,FUNCT_4:11
.= f.x by FUNCT_1:49,C4,XXREAL_1:233;
hence thesis by FUNCT_1:49,A4;
end;
end;
hence thesis by B3,FUNCT_1:2;
end;
hence thesis by XX;
end;
theorem Th17C:
for a,b,p,q being Real, f be Function of REAL,REAL st
f = ( AffineMap (a,b) |].-infty,(q-b)/(a-p).[ )
+* ( AffineMap (p,q) |[.(q-b)/(a-p),+infty.[ ) & (q-b)/(a-p) in A
holds
f | A = ( AffineMap (a,b) |[.lower_bound A,(q-b)/(a-p).] )
+* ( AffineMap (p,q) |[.(q-b)/(a-p),upper_bound A.] )
proof
let a,b,p,q being Real, f be Function of REAL,REAL;
assume that
A2: f = ( AffineMap (a,b) |].-infty,(q-b)/(a-p).[ )
+* ( AffineMap (p,q) |[.(q-b)/(a-p),+infty.[ );
assume (q-b)/(a-p) in A; then
(q-b)/(a-p) in [.(lower_bound A),(upper_bound A).] by INTEGRA1:4;
then
A4: (lower_bound A) <= (q-b)/(a-p) & (q-b)/(a-p) <= (upper_bound A)
by XXREAL_1:1;
set F = ( AffineMap (a,b) |[.lower_bound A,(q-b)/(a-p).] )
+* ( AffineMap (p,q) |[.(q-b)/(a-p),upper_bound A.] );
A5: dom F = dom ( AffineMap (a,b) |[.lower_bound A,(q-b)/(a-p).] ) \/
dom ( AffineMap (p,q) |[.(q-b)/(a-p),upper_bound A.] ) by FUNCT_4:def 1
.= [.lower_bound A,(q-b)/(a-p).] \/
dom ( AffineMap (p,q) |[.(q-b)/(a-p),upper_bound A.] ) by FUNCT_2:def 1
.= [.lower_bound A,(q-b)/(a-p).] \/ [.(q-b)/(a-p),upper_bound A.]
by FUNCT_2:def 1
.= [.lower_bound A,upper_bound A.] by XXREAL_1:165,A4
.= A by INTEGRA1:4
.= dom (f | A) by FUNCT_2:def 1;
for x being object st x in dom F holds F . x = (f | A) . x
proof
let x be object;
assume A6: x in dom F; then
reconsider x as Real by A5;
x in A by A6,A5; then
x in [.(lower_bound A),(upper_bound A).] by INTEGRA1:4;
then
A8: (lower_bound A) <= x & x <= (upper_bound A) by XXREAL_1:1;
per cases;
suppose B1: x < (q-b)/(a-p); then
B3: not (x in dom ( AffineMap (p,q) |[.(q-b)/(a-p),upper_bound A.] ))
by XXREAL_1:1;
B6: not ( x in dom (AffineMap (p,q) |[.(q-b)/(a-p),+infty.[))
by XXREAL_1:236,B1;
B0: F.x = (AffineMap (a,b) |[.lower_bound A,(q-b)/(a-p).]) .x
by B3,FUNCT_4:11
.= AffineMap (a,b) .x by FUNCT_1:49,A8,B1,XXREAL_1:1
.= (AffineMap (a,b) | ].-infty,(q-b)/(a-p).[).x
by FUNCT_1:49,XXREAL_1:233,B1;
(f | A) . x = (( AffineMap (a,b) |].-infty,(q-b)/(a-p).[ )
+* ( AffineMap (p,q) |[.(q-b)/(a-p),+infty.[ )).x by A2,FUNCT_1:49,A6,A5;
hence thesis by B0, B6,FUNCT_4:11;
end;
suppose C1: x >= (q-b)/(a-p); then
x in [.(q-b)/(a-p),upper_bound A.] by A8; then
C2: x in dom ( AffineMap (p,q) |[.(q-b)/(a-p),upper_bound A.] )
by FUNCT_2:def 1;
x in [.(q-b)/(a-p),+infty.[ by XXREAL_1:236,C1;then
C3: x in dom (AffineMap (p,q) |[.(q-b)/(a-p),+infty.[)
by FUNCT_2:def 1;
F . x
= ( AffineMap (p,q) |[.(q-b)/(a-p),upper_bound A.] ).x by C2,FUNCT_4:13
.= AffineMap (p,q) .x by FUNCT_1:49,A8,C1,XXREAL_1:1
.= (AffineMap (p,q) |[.(q-b)/(a-p),+infty.[).x by FUNCT_1:49,XXREAL_1:236,C1
.= f.x by A2,FUNCT_4:13,C3;
hence thesis by FUNCT_1:49,A6,A5;
end;
end;
hence thesis by FUNCT_1:2,A5;
end;
theorem Th17B:
for a,b being Real holds
AffineMap (a,b) | A is bounded & AffineMap (a,b) is_integrable_on A
proof
let a,b be Real;
reconsider f = AffineMap (a,b) as PartFunc of REAL,REAL;
A c= REAL; then
A1: A c= dom f by FUNCT_2:def 1;
f | A is continuous;
hence thesis by INTEGRA5:11,INTEGRA5:10,A1;
end;
theorem Th17:
for a,b,p,q being Real, f be Function of REAL,REAL st a <> p &
f = ( AffineMap (a,b) |].-infty,(q-b)/(a-p).[ )
+* ( AffineMap (p,q) |[.(q-b)/(a-p),+infty.[ )
holds
( (q-b)/(a-p) in A implies
integral(f,A) = integral(AffineMap (a,b),['lower_bound A,(q-b)/(a-p)'])
+ integral(AffineMap (p,q),['(q-b)/(a-p),upper_bound A']) )
&
( (q-b)/(a-p) <= lower_bound A implies
integral(f,A) = integral(AffineMap (p,q),A) )
&
( (q-b)/(a-p) >= upper_bound A implies
integral(f,A) = integral(AffineMap (a,b),A) )
proof
let a,b,p,q be Real, f be Function of REAL,REAL;
assume that
A1: a <> p and
A2: f = ( AffineMap (a,b) | ].-infty,(q-b)/(a-p).[ )
+* ( AffineMap (p,q) | [.(q-b)/(a-p),+infty.[ );
B3: A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4
.= ['(lower_bound A),(upper_bound A)'] by INTEGRA5:def 3,SEQ_4:11;
A4: AffineMap (a,b) . ((q-b)/(a-p)) = AffineMap (p,q) . ((q-b)/(a-p))
by Th17E,A1;
A5: AffineMap (a,b) is_integrable_on ['lower_bound A,upper_bound A'] &
AffineMap (a,b) | ['lower_bound A,upper_bound A'] is bounded by Th17B;
A7: AffineMap (p,q) is_integrable_on ['lower_bound A,upper_bound A']
by Th17B;
A8: AffineMap (p,q) | ['lower_bound A,upper_bound A'] is bounded by Th17B;
A11: f is_integrable_on ['lower_bound A,upper_bound A'] by Th17X,A1,A2;
AA: ( (q-b)/(a-p) in A implies
integral(f,A) = integral(AffineMap (a,b),['lower_bound A,(q-b)/(a-p)'])
+ integral(AffineMap (p,q),['(q-b)/(a-p),upper_bound A']) )
proof
assume B1: (q-b)/(a-p) in A;
A10: f | [.lower_bound A,upper_bound A.]
= f | A by INTEGRA1:4
.= (AffineMap (a,b) | [.lower_bound A,(q-b)/(a-p).])
+* (AffineMap (p,q) | [.(q-b)/(a-p),upper_bound A.]) by Th17C,A2,B1;
(q-b)/(a-p) in [.lower_bound A,upper_bound A.] by INTEGRA1:4,B1;
then lower_bound A <= (q-b)/(a-p) &
(q-b)/(a-p) <= upper_bound A by XXREAL_1:1;
hence thesis by Th18Z,A11,A4,A5,A7,A8,A10,B3;
end;
BB: (q-b)/(a-p) <= lower_bound A implies
integral(f,A) = integral(AffineMap (p,q),A)
proof
assume C1: (q-b)/(a-p) <= lower_bound A;
reconsider LU = [.lower_bound A,upper_bound A.]
as non empty closed_interval Subset of REAL by INTEGRA1:4;
C4: LU = A by INTEGRA1:4;
C5: f | LU = f | A by INTEGRA1:4
.= AffineMap (p,q) | A by Th17AX,A2,A4,C1
.= AffineMap (p,q) | LU by INTEGRA1:4;
thus integral(f,A) = integral(f | LU) by C4,INTEGRA5:def 2
.= integral(AffineMap (p,q),LU) by INTEGRA5:def 2,C5
.= integral(AffineMap (p,q),A) by INTEGRA1:4;
end;
(q-b)/(a-p) >= upper_bound A implies
integral(f,A) = integral(AffineMap (a,b),A)
proof
assume E1: (q-b)/(a-p) >= upper_bound A;
reconsider LU = [.lower_bound A,upper_bound A.]
as non empty closed_interval Subset of REAL by INTEGRA1:4;
C4: LU = A by INTEGRA1:4;
C5: f | LU = f | A by INTEGRA1:4
.= AffineMap (a,b) | A by Th17AX,A2,A4,E1
.= AffineMap (a,b) | LU by INTEGRA1:4;
thus integral(f,A) = integral(f | LU) by C4,INTEGRA5:def 2
.= integral(AffineMap (a,b),LU) by INTEGRA5:def 2,C5
.= integral(AffineMap (a,b),A) by INTEGRA1:4;
end;
hence thesis by AA,BB;
end;
theorem Th23A:
for a,b,p,q being Real, f be 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
integral((id REAL) (#) 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'])
proof
let a,b,p,q being Real, f be Function of REAL,REAL;
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;
(q-b)/(a-p) in [.lower_bound A,upper_bound A.] by INTEGRA1:4,A3;
then
B1: lower_bound A <= (q-b)/(a-p) & (q-b)/(a-p) <= upper_bound A by XXREAL_1:1;
B6: ((id REAL) (#) AffineMap (a,b)) .((q-b)/(a-p))
= (id REAL).((q-b)/(a-p)) * AffineMap (a,b) .((q-b)/(a-p)) by VALUED_1:5
.= (id REAL).((q-b)/(a-p)) * AffineMap (p,q) .((q-b)/(a-p)) by Th17E,A1
.= ((id REAL) (#) AffineMap (p,q)) .((q-b)/(a-p)) by VALUED_1:5;
B2: ((id REAL) (#) f) | [.lower_bound A,upper_bound A.] =
((id REAL) (#) AffineMap (a,b)) | [.lower_bound A,(q-b)/(a-p).]
+* ((id REAL) (#) AffineMap (p,q)) | [.(q-b)/(a-p),upper_bound A.]
proof
A4: dom(((id REAL) (#) f) | [.lower_bound A,upper_bound A.])
= [.lower_bound A,upper_bound A.] by FUNCT_2:def 1
.= [.lower_bound A,(q-b)/(a-p).] \/ [.(q-b)/(a-p),upper_bound A.]
by XXREAL_1:165,B1
.= dom(((id REAL) (#) AffineMap (a,b)) | [.lower_bound A,(q-b)/(a-p).])
\/ [.(q-b)/(a-p),upper_bound A.] by FUNCT_2:def 1
.= dom(((id REAL) (#) AffineMap (a,b)) | [.lower_bound A,(q-b)/(a-p).])
\/ dom (((id REAL) (#) AffineMap (p,q)) | [.(q-b)/(a-p),upper_bound A.])
by FUNCT_2:def 1
.= dom(((id REAL) (#) AffineMap (a,b)) | [.lower_bound A,(q-b)/(a-p).]
+* ((id REAL) (#) AffineMap (p,q)) | [.(q-b)/(a-p),upper_bound A.])
by FUNCT_4:def 1;
for x be object st
x in dom(((id REAL) (#) f) | [.lower_bound A,upper_bound A.]) holds
(((id REAL) (#) f) | [.lower_bound A,upper_bound A.]).x =
( ((id REAL) (#) AffineMap (a,b)) | [.lower_bound A,(q-b)/(a-p).]
+* ((id REAL) (#) AffineMap (p,q)) | [.(q-b)/(a-p),upper_bound A.]).x
proof
let x be object;
assume G8: x in dom(((id REAL) (#) f) | [.lower_bound A,upper_bound A.]);
G1: x in [.lower_bound A,upper_bound A.] by G8;
reconsider x as Real by G8;
G3: lower_bound A <= x & x <= upper_bound A
by G8,XXREAL_1:1;
G9: x in A by INTEGRA1:4,G1;
per cases;
suppose G2: x < (q-b)/(a-p);
G5: not (x in dom (((id REAL) (#) AffineMap (p,q)) |
[.(q-b)/(a-p),upper_bound A.])) by G2,XXREAL_1:1;
G10: not (x in dom (AffineMap (p,q) |
[.(q-b)/(a-p),upper_bound A.]) ) by G2,XXREAL_1:1;
(((id REAL) (#) f) | [.lower_bound A,upper_bound A.]).x
= (((id REAL) (#) f)).x by FUNCT_1:49,G8
.= (id REAL).x * f.x by VALUED_1:5
.= (id REAL).x * ((AffineMap (a,b) | [.lower_bound A,(q-b)/(a-p).])
+* (AffineMap (p,q) | [.(q-b)/(a-p),upper_bound A.])).x
by A2,FUNCT_1:49,G9
.= (id REAL).x * (AffineMap (a,b) | [.lower_bound A,(q-b)/(a-p).]).x
by FUNCT_4:11,G10
.= (id REAL).x * AffineMap (a,b).x by FUNCT_1:49,G2,G3,XXREAL_1:1
.= ((id REAL) (#) AffineMap (a,b)).x by VALUED_1:5
.= (((id REAL) (#) AffineMap (a,b)) | [.lower_bound A,(q-b)/(a-p).]).x
by FUNCT_1:49,G2,G3,XXREAL_1:1;
hence thesis by FUNCT_4:11,G5;
end;
suppose P1: x >= (q-b)/(a-p);
P2: x in [.(q-b)/(a-p),upper_bound A.] by P1,G3; then
G10: x in dom (AffineMap (p,q) | [.(q-b)/(a-p),upper_bound A.])
by FUNCT_2:def 1;
G5: x in dom (((id REAL) (#) AffineMap (p,q)) |
[.(q-b)/(a-p),upper_bound A.]) by FUNCT_2:def 1,P2;
(((id REAL) (#) f) | [.lower_bound A,upper_bound A.]).x
= (((id REAL) (#) f)).x by FUNCT_1:49,G8
.= (id REAL).x * f.x by VALUED_1:5
.= (id REAL).x * ((AffineMap (a,b) | [.lower_bound A,(q-b)/(a-p).])
+* (AffineMap (p,q) | [.(q-b)/(a-p),upper_bound A.])).x
by A2,FUNCT_1:49,G9
.= (id REAL).x * (AffineMap (p,q) | [.(q-b)/(a-p),upper_bound A.]).x
by FUNCT_4:13,G10
.= (id REAL).x * AffineMap (p,q).x by FUNCT_1:49,P1,G3,XXREAL_1:1
.= ((id REAL) (#) AffineMap (p,q)).x by VALUED_1:5
.= (((id REAL) (#) AffineMap (p,q)) | [.(q-b)/(a-p),upper_bound A.]).x
by FUNCT_1:49,P1,G3,XXREAL_1:1;
hence thesis by FUNCT_4:13,G5;
end;
end;
hence thesis by FUNCT_1:2,A4;
end;
D3: dom ((id REAL) (#) AffineMap (a,b)) = REAL &
dom ((id REAL) (#) AffineMap (p,q)) = REAL by FUNCT_2:def 1;
reconsider Fa = (id REAL) (#) AffineMap (a,b) as PartFunc of REAL,REAL;
reconsider Fp = (id REAL) (#) AffineMap (p,q) as PartFunc of REAL,REAL;
Fa | ['lower_bound A,upper_bound A'] is continuous;then
B3: ((id REAL) (#) AffineMap (a,b))
is_integrable_on ['lower_bound A,upper_bound A'] &
((id REAL) (#) AffineMap (a,b)) | ['lower_bound A,upper_bound A'] is bounded
by INTEGRA5:10,INTEGRA5:11,D3;
Fp | ['lower_bound A,upper_bound A'] is continuous; then
B4: ((id REAL) (#) AffineMap (p,q))
is_integrable_on ['lower_bound A,upper_bound A'] &
((id REAL) (#) AffineMap (p,q)) | ['lower_bound A,upper_bound A'] is bounded
by INTEGRA5:10,INTEGRA5:11,D3;
set F = ( AffineMap (a,b) |].-infty,(q-b)/(a-p).[ )
+* ( AffineMap (p,q) |[.(q-b)/(a-p),+infty.[ );
reconsider F as Function of REAL,REAL by Th19;
AA: A = [.lower_bound A,upper_bound A.] by INTEGRA1:4
.= ['lower_bound A,upper_bound A'] by INTEGRA5:def 3,SEQ_4:11;
C4: F | ['lower_bound A,upper_bound A'] is integrable
by INTEGRA5:def 1,Th17X,A1;
C3: F | ['lower_bound A,upper_bound A']
= f | A by A2,A3,Th17C,AA
.= f | [.lower_bound A,upper_bound A.] by INTEGRA1:4
.= f | ['lower_bound A,upper_bound A'] by INTEGRA5:def 3,SEQ_4:11;
f is_integrable_on ['lower_bound A,upper_bound A'] &
f | ['lower_bound A,upper_bound A'] is bounded
by INTEGRA5:def 1,C4,C3,Th17X,A1; then
B5: ((id REAL) (#) f) is_integrable_on ['lower_bound A,upper_bound A'] by Lm3;
reconsider LU = [.lower_bound A,upper_bound A.]
as non empty closed_interval Subset of REAL by INTEGRA1:4;
thus integral((id REAL) (#) f,A)
=integral ((id REAL) (#) f,LU) by INTEGRA1:4
.= integral((id REAL) (#) f,['lower_bound A,upper_bound A'])
by INTEGRA5:def 3,SEQ_4:11
.= 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'])
by Th18Z,B1,B2,B3,B4,B5,B6;
end;
theorem Th23C:
for a,b being Real holds
(id REAL) (#) (AffineMap (a,b)) = (a (#) ( #Z 2)) + (b (#) ( #Z 1))
proof
let a,b be Real;
for x being object st x in REAL holds
((id REAL) (#) AffineMap (a,b)) . x
= ((a (#) ( #Z 2)) + (b (#) ( #Z 1))) . x
proof
let x be object;
assume x in REAL;then
reconsider x as Element of REAL;
((a (#) ( #Z 2)) + (b (#) ( #Z 1))) . x
= (a (#) ( #Z 2)).x + (b (#) ( #Z 1)) . x by VALUED_1:1
.= a * ( #Z 2).x + (b (#) ( #Z 1)) . x by VALUED_1:6
.= a * ( #Z 2).x + b * ( #Z 1) . x by VALUED_1:6
.= a * (x #Z 2) + b * ( #Z 1) . x by TAYLOR_1:def 1
.= a * (x #Z 2) + b * (x #Z 1) by TAYLOR_1:def 1
.= a * (x |^ 2) + b * (x #Z 1) by PREPOWER:36
.= a * (x |^ 2) + b * (x ) by PREPOWER:35
.= a * (x * x) + b * (x ) by NEWTON:81
.= x * (a * x + b)
.= ((id REAL).x) * (AffineMap(a,b).x) by FCONT_1:def 4;
hence thesis by VALUED_1:5;
end;
hence thesis by FUNCT_2:12;
end;
theorem Th23B:
for a,b,c,d being Real st c <= d holds
integral((id REAL) (#) (AffineMap (a,b)),c,d)
= 1/3*a*(d*d*d - c*c*c) + 1/2*b*(d*d - c*c)
proof
let a,b,c,d be Real;
assume A1: c <= d;
reconsider D = ['c,d'] as non empty closed_interval Subset of REAL;
reconsider F2 = ( ( #Z 2)) as PartFunc of REAL,REAL;
reconsider F1 = ( ( #Z 1)) as PartFunc of REAL,REAL;
DD: ['c,d'] c= REAL;
B2: ['c,d'] c= dom ( #Z 2) by FUNCT_2:def 1,DD;
B3: D c= dom (F1) by FUNCT_2:def 1,DD;
F1 | D is continuous;then
B4: F1 is_integrable_on D & F1 | ['c,d'] is bounded
by INTEGRA5:10,INTEGRA5:11,B3;
F2 | D is continuous;then
B5: F2 is_integrable_on ['c,d'] & F2 | ['c,d'] is bounded
by INTEGRA5:10,INTEGRA5:11,B2;
A2: ['c,d'] c= dom (a (#) ( F2)) by FUNCT_2:def 1,DD;
A3: ['c,d'] c= dom (b (#) ( F1)) by FUNCT_2:def 1,DD;
(a (#) ( F2)) | D is continuous & (b (#) F1) | D is continuous;then
A4: (b (#) F1) is_integrable_on ['c,d'] &
(a (#) F2) is_integrable_on ['c,d'] & (b (#) F1) | ['c,d'] is bounded
& (a (#) F2) | ['c,d'] is bounded by INTEGRA5:10,INTEGRA5:11,A2,A3;
[.(lower_bound ['c,d']),(upper_bound ['c,d']).] = ['c,d'] &
['c,d'] = [.c,d.] by A1,INTEGRA5:def 3,INTEGRA1:4; then
LM: lower_bound D = c & d = upper_bound D by INTEGRA1:5;
integral((id REAL) (#) (AffineMap (a,b)),c,d)
= integral((a (#) ( #Z 2)) + (b (#) ( #Z 1)),c,d) by Th23C
.= integral((a (#) F2),c,d) + integral((b (#) F1),c,d)
by INTEGRA6:12,A1,A2,A3,A4
.= a * integral(F2,c,d) + integral((b (#) F1),c,d) by INTEGRA6:10,A1,B2,B5
.= a * integral(F2,c,d) + b * integral(F1,c,d) by INTEGRA6:10,A1,B3,B4
.= a * integral(F2,D) + b * integral(F1,c,d) by INTEGRA5:def 4,A1
.= a * integral(F2,D) + b * integral(F1,D) by INTEGRA5:def 4,A1
.= a * (((1 / (2 + 1)) * ((upper_bound D) |^ (2 + 1)))
- ((1 / (2 + 1)) * ((lower_bound D) |^ (2 + 1))))
+ b * integral(F1,D) by INTEGRA9:19
.= a * (1 / 3 * (d |^ (2 + 1)) - (1 / 3 * (c |^ (2 + 1))))
+ b * ((1 / 2) * (d |^ (1 + 1)) - ((1 / 2) * (c |^ (1 + 1))))
by LM,INTEGRA9:19
.= a * (1 / 3) * ( d |^ (2 + 1) - c |^ (2 + 1) )
+ b * (1 / 2) * ( d |^ (1 + 1) - c |^ (1 + 1) )
.= a * (1 / 3) * ( (d |^ 2) * d - c |^ (2 + 1) )
+ b * (1 / 2) * ( d |^ (1 + 1) - c |^ (1 + 1) ) by NEWTON:6
.= a * (1 / 3) * ( (d |^ ( 1 + 1)) * d - (c |^ 2)*c )
+ b * (1 / 2) * ( d |^ (1 + 1) - c |^ (1 + 1) ) by NEWTON:6
.= a * (1 / 3) * ( (d |^ ( 1 + 1)) * d - (c |^ 2)*c )
+ b * (1 / 2) * ( d |^ 1 *d - c |^ (1 + 1) ) by NEWTON:6
.= a * (1 / 3) * ( (d |^ ( 1 + 1)) * d - (c |^ 2)*c )
+ b * (1 / 2) * ( d *d - c |^ 1 *c ) by NEWTON:6
.= a * (1 / 3) * ( (d |^ 1 *d ) * d - (c |^ (1+1))*c )
+ b * (1 / 2) * ( d *d - c *c ) by NEWTON:6
.= a * (1 / 3) * ( (d *d ) * d - (c |^ 1*c)*c )
+ b * (1 / 2) * ( d *d - c *c ) by NEWTON:6;
hence thesis;
end;
theorem Th23E:
for a,b being Real holds
AffineMap (a,b) = (a (#) ( #Z 1)) + (b (#) ( #Z 0))
proof
let a,b be Real;
for x being object st x in REAL holds
(AffineMap (a,b)) . x
= ((a (#) ( #Z 1)) + (b (#) ( #Z 0))) . x
proof
let x be object;
assume x in REAL; then
reconsider x as Element of REAL;
((a (#) ( #Z 1)) + (b (#) ( #Z 0))) . x
= (a (#) ( #Z 1)).x + (b (#) ( #Z 0)) . x by VALUED_1:1
.= a * ( #Z 1).x + (b (#) ( #Z 0)) . x by VALUED_1:6
.= a * ( #Z 1).x + b * ( #Z 0) . x by VALUED_1:6
.= a * (x #Z 1) + b * ( #Z 0) . x by TAYLOR_1:def 1
.= a * (x #Z 1) + b * (x #Z 0) by TAYLOR_1:def 1
.= a * (x |^ 1) + b * (x #Z 0) by PREPOWER:36
.= a * (x ) + b * (1 ) by PREPOWER:34
.= (AffineMap(a,b).x) by FCONT_1:def 4;
hence thesis;
end;
hence thesis by FUNCT_2:12;
end;
theorem Th23D:
for a,b,c,d being Real st c <= d holds
integral(AffineMap (a,b),c,d) = 1/2*a*(d*d - c*c) + b*(d - c)
proof
let a,b,c,d be Real;
assume A1: c <= d;
reconsider D = ['c,d'] as non empty closed_interval Subset of REAL;
reconsider F2 = ( ( #Z 1)) as PartFunc of REAL,REAL;
reconsider F1 = ( ( #Z 0)) as PartFunc of REAL,REAL;
DD: ['c,d'] c= REAL;
B2: ['c,d'] c= dom ( #Z 1) by FUNCT_2:def 1,DD;
B3: D c= dom (F1) by FUNCT_2:def 1,DD;
F1 | D is continuous;then
B4: F1 is_integrable_on D & F1 | ['c,d'] is bounded
by INTEGRA5:10,INTEGRA5:11,B3;
F2 | D is continuous;then
B5: F2 is_integrable_on ['c,d'] & F2 | ['c,d'] is bounded
by INTEGRA5:10,INTEGRA5:11,B2;
A2: ['c,d'] c= dom (a (#) ( F2)) by FUNCT_2:def 1,DD;
A3: ['c,d'] c= dom (b (#) ( F1)) by FUNCT_2:def 1,DD;
(a (#) ( F2)) | D is continuous & (b (#) F1) | D is continuous;then
A4: (b (#) F1) is_integrable_on ['c,d'] &
(a (#) F2) is_integrable_on ['c,d'] & (b (#) F1) | ['c,d'] is bounded
& (a (#) F2) | ['c,d'] is bounded by INTEGRA5:10,INTEGRA5:11,A2,A3;
[.(lower_bound ['c,d']),(upper_bound ['c,d']).] = ['c,d'] &
['c,d'] = [.c,d.] by A1,INTEGRA5:def 3,INTEGRA1:4; then
LM: lower_bound D = c & d = upper_bound D by INTEGRA1:5;
integral(AffineMap (a,b),c,d)
= integral((a (#) ( #Z 1)) + (b (#) ( #Z 0)),c,d) by Th23E
.= integral((a (#) F2),c,d) + integral((b (#) F1),c,d)
by INTEGRA6:12,A1,A2,A3,A4
.= a * integral(F2,c,d) + integral((b (#) F1),c,d) by INTEGRA6:10,A1,B2,B5
.= a * integral(F2,c,d) + b * integral(F1,c,d) by INTEGRA6:10,A1,B3,B4
.= a * integral(F2,D) + b * integral(F1,c,d) by INTEGRA5:def 4,A1
.= a * integral(F2,D) + b * integral(F1,D) by INTEGRA5:def 4,A1
.= a*(((1 / (1 + 1)) * ((upper_bound D) |^ (1 + 1)))
- ((1 / (1 + 1)) * ((lower_bound D) |^ (1 + 1))))
+ b * integral(F1,D) by INTEGRA9:19
.= a*(((1 / 2) * ((upper_bound D) |^ (1 + 1)))
- ((1 / 2) * ((lower_bound D) |^ (1 + 1))))
+ b*(((1 / (0 + 1)) * ((upper_bound D) |^ (0 + 1)))
- ((1 / (0 + 1)) * ((lower_bound D) |^ (0 + 1)))) by INTEGRA9:19
.= a*(1 / 2) * ( d |^ (1 + 1) - c |^ (1 + 1) ) +b*(d |^ 1 - c |^ 1) by LM
.= a*(1 / 2) * ( d |^ 1 *d - c |^ (1 + 1) ) +b*(d |^ 1 - c |^ 1) by NEWTON:6
.= a*(1 / 2) * ( d *d - c *c ) +b*(d - c ) by NEWTON:6;
hence thesis;
end;
theorem
for a,b,p,q,c,d,e being Real, f be 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)) )
proof
let a,b,p,q,c,d,e being Real, f be Function of REAL,REAL;
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;
set F = ( AffineMap (a,b) |].-infty,(q-b)/(a-p).[ )
+* ( AffineMap (p,q) |[.(q-b)/(a-p),+infty.[ );
reconsider F 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: c <= d & d <= e 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)),c,d)
+ 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)),c,d)
+ integral((id REAL) (#) (AffineMap (p,q)),d,e) ) /
(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)),c,d)
+ integral((id REAL) (#) (AffineMap (p,q)),d,e) ) /
(integral(AffineMap (a,b),c,d)
+ integral(AffineMap (p,q),['(q-b)/(a-p),upper_bound A']) )
by INTEGRA5:def 4,CD
.=(integral((id REAL) (#) (AffineMap (a,b)),c,d)
+ integral((id REAL) (#) (AffineMap (p,q)),d,e) ) /
(integral(AffineMap (a,b),c,d)+ integral(AffineMap (p,q),d,e) )
by INTEGRA5:def 4,CD
.=( (1/3*a*(d*d*d - c*c*c) + 1/2*b*(d*d - c*c))
+ integral((id REAL) (#) (AffineMap (p,q)),d,e) ) /
(integral(AffineMap (a,b),c,d)+ integral(AffineMap (p,q),d,e) )
by Th23B,CD
.=((1/3*a*(d*d*d - c*c*c) + 1/2*b*(d*d - c*c))
+ (1/3*p*(e*e*e - d*d*d) + 1/2*q*(e*e - d*d)) ) /
(integral(AffineMap (a,b),c,d)+ integral(AffineMap (p,q),d,e) )
by Th23B,CD
.=((1/3*a*(d*d*d - c*c*c) + 1/2*b*(d*d - c*c))
+ (1/3*p*(e*e*e - d*d*d) + 1/2*q*(e*e - d*d)) ) /
(1/2*a*(d*d - c*c) + b*(d - c) + integral(AffineMap (p,q),d,e) )
by Th23D,CD
.=((1/3*a*(d*d*d - c*c*c) + 1/2*b*(d*d - c*c))
+ (1/3*p*(e ^2*e - d*d*d) + 1/2*q*(e*e - d*d)) ) /
(1/2*a*(d*d - c ^2) + b*(d - c) + (1/2*p*(e*e - d*d) + q*(e - d)) )
by Th23D,CD
.=((1/3*a*(d^2*d - c^2*c) + 1/2*b*(d ^2 - c ^2))
+ (1/3*p*(e ^3 - d^2*d) + 1/2*q*(e ^2 - d ^2)) ) /
(1/2*a*(d ^2 - c ^2) + b*(d - c) + (1/2*p*(e ^2 - d ^2) + q*(e - d)) )
by POLYEQ_3:def 3
.=((1/3*a*(d^2*d - c^2*c) + 1/2*b*(d ^2 - c ^2))
+ (1/3*p*(e ^3 - d^3) + 1/2*q*(e ^2 - d ^2)) ) /
(1/2*a*(d ^2 - c ^2) + b*(d - c) + (1/2*p*(e ^2 - d ^2) + q*(e - d)) )
by POLYEQ_3:def 3
.= ((1/3*a*(d^3 - c^2*c) + 1/2*b*(d ^2 - c ^2))
+ (1/3*p*(e ^3 - d^3) + 1/2*q*(e ^2 - d ^2)) ) /
(1/2*a*(d ^2 - c ^2) + b*(d - c) + (1/2*p*(e ^2 - d ^2) + q*(e - d)) )
by POLYEQ_3:def 3
.= ((1/3*a*(d^3 - c^3) + 1/2*b*(d ^2 - c ^2))
+ (1/3*p*(e^3 - d^3) + 1/2*q*(e ^2 - d ^2)) ) /
(1/2*a*(d ^2 - c ^2) + b*(d - c) + (1/2*p*(e ^2 - d ^2) + q*(e - d)) )
by POLYEQ_3:def 3;
hence thesis;
end;
theorem
for f being Function of REAL,REAL holds
max+ f = max(AffineMap(0,0),f)
proof
let f be Function of REAL,REAL;
dom f = REAL by FUNCT_2:def 1; then
B7: dom (max+ f ) = REAL by RFUNCT_3:def 10;then
A2: dom (max+ f) = dom max(AffineMap(0,0),f) by FUNCT_2:def 1;
set F = max(AffineMap(0,0),f);
for x being object st x in dom F holds
F . x = (max+ f) . x
proof
let x be object;
assume x in dom F; then
reconsider x as Element of REAL;
(max+ f).x = max+ (f.x) by RFUNCT_3:def 10,B7
.= max(f.x, 0*x+0) by RFUNCT_3:def 1
.= max(f.x,AffineMap(0,0).x) by FCONT_1:def 4
.= (max(f,AffineMap(0,0))).x by COUSIN2:def 2;
hence thesis;
end;
hence F = (max+ f) by FUNCT_1:2,A2;
end;