:: Isosceles Triangular and Isosceles Trapezoidal Membership Functions Using
:: Centroid Method
:: by Takashi Mitsuishi
::
:: Received March 31, 2023
:: Copyright (c) 2023-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, MEASURE5,
FUZNUM_1, REAL_1, ORDINAL2, XXREAL_2, FUNCT_7, JGRAPH_2, FUNCT_4,
FCONT_1, SQUARE_1, VALUED_1, INTEGRA1, INTEGRA5, SEQ_4, POLYEQ_3, NEWTON,
MSALIMIT, NUMPOLY1, FUZZY_6;
notations TARSKI, XBOOLE_0, SUBSET_1, NEWTON, RELAT_1, NUMBERS, SQUARE_1,
XCMPLX_0, XXREAL_0, COMPLEX1, XREAL_0, RELSET_1, MEASURE5, PARTFUN1,
FUNCT_2, FUNCT_1, FCONT_1, FUNCT_3, INTEGRA1, VALUED_1, FUNCT_4,
COMSEQ_2, SEQ_4, POLYEQ_3, RCOMP_1, INTEGRA5, COUSIN2, FUZNUM_1, FUZZY_6;
constructors SEQ_4, RELSET_1, FCONT_1, FUNCT_4, FUZNUM_1, COMSEQ_2, NEWTON,
INTEGRA5, COUSIN2, POLYEQ_3, FUZZY_6;
registrations RELSET_1, NUMBERS, XXREAL_0, MEMBERED, XBOOLE_0, VALUED_0,
VALUED_1, FUNCT_2, XREAL_0, ORDINAL1, FCONT_1, RELAT_1, FUNCT_4, FUNCT_1,
XCMPLX_0, NAT_1, FUZNUM_1, SQUARE_1, INTEGRA1, NEWTON;
requirements NUMERALS, REAL, SUBSET, ARITHM;
definitions TARSKI;
equalities RCOMP_1, SQUARE_1;
expansions TARSKI, FUZNUM_1;
theorems TARSKI, XBOOLE_0, FUNCT_1, ABSVALUE, COMPLEX1, XREAL_1, XXREAL_0,
XXREAL_1, FUNCT_2, RELAT_1, XREAL_0, FCONT_1, XCMPLX_1, FUNCT_4,
VALUED_1, INTEGRA1, INTEGRA5, INTEGRA6, SEQ_4, COUSIN2, POLYEQ_3,
FUZZY_2, FUZZY_5, FUZZY_6, FUZNUM_1;
schemes FUNCT_2;
begin :: Preliminaries
Lm6:
for a,c be Real st c > 0 holds a in [' a-c,a+c ']
proof
let a,c be Real;
assume c > 0; then
A2: a-c <= a & a <= a+c by XREAL_1:43,XREAL_1:29; then
a in [. a-c,a+c .];
hence thesis by INTEGRA5:def 3,XXREAL_0:2,A2;
end;
theorem Th6:
for a,b,c,d be Real st a < b & b < c & c < d holds
['a,d'] \ ['b,c'] c= ['a,b'] \/ ['c,d']
proof
let a,b,c,d be Real;
assume A1: a < b & b < c & c < d; then
ADD: a < c by XXREAL_0:2;
let x be object;
assume A2: x in ['a,d'] \ ['b,c']; then
reconsider x as Real;
not x in ['b,c'] by XBOOLE_0:def 5,A2; then
A3: not (x in [. b,c .]) by INTEGRA5:def 3,A1;
x in ['a,d'] by XBOOLE_0:def 5,A2; then
x in [.a,d.] by INTEGRA5:def 3,ADD,XXREAL_0:2,A1; then
A4: a <= x & x <= d by XXREAL_1:1;
per cases by A3;
suppose x < b; then
x in [. a,b .] by A4; then
x in [' a,b '] by INTEGRA5:def 3,A1;
hence thesis by XBOOLE_0:def 3;
end;
suppose x > c; then
x in [. c,d .] by A4; then
x in [' c,d '] by INTEGRA5:def 3,A1;
hence thesis by XBOOLE_0:def 3;
end;
end;
theorem
for a,b,c,d be Real holds
[. a,d .] \ [. b,c .] c= [. a,b .[ \/ ]. c,d .]
proof
let a,b,c,d be Real;
let x be object;
assume A2: x in [. a,d .] \ [. b,c .]; then
reconsider x as Real;
A3: not x in [. b,c .] by XBOOLE_0:def 5,A2;
x in [.a,d.] by XBOOLE_0:def 5,A2; then
A4: a <= x & x <= d by XXREAL_1:1;
per cases by A3;
suppose x < b; then
x in [. a,b .[ by A4;
hence thesis by XBOOLE_0:def 3;
end;
suppose x > c; then
x in ]. c,d .] by A4;
hence thesis by XBOOLE_0:def 3;
end;
end;
theorem
for a,b,c,d be Real st a < b & b < c & c < d holds
[. a,d .] \ [. b,c .] c= [. a,b .] \/ [. c,d .]
proof
let a,b,c,d be Real;
assume A1: a < b & b < c & c < d; then
a < c by XXREAL_0:2; then
B1:[. a,d .] = [' a,d '] by INTEGRA5:def 3,XXREAL_0:2,A1;
B2:[. b,c .] = [' b,c '] by INTEGRA5:def 3,A1;
B3:[. a,b .] = [' a,b '] by INTEGRA5:def 3,A1;
[. c,d .] = [' c,d '] by INTEGRA5:def 3,A1;
hence thesis by B1,B2,B3,Th6,A1;
end;
Th8X:
for a,b,c,d be Real st a <= b & b < c & c <= d holds
[. a,b .[ \/ ]. c,d .] c= [. a,d .] \ [. b,c .]
proof
let a,b,c,d be Real;
assume a <= b & b < c & c <= d; then
a <= c & b <= d by XXREAL_0:2;
hence thesis by XXREAL_1:312;
end;
theorem
for p, q, r, s being Real st p < r & r <= s & s < q holds
[.r,s.] c< [.p,q.]
proof
let p, q, r, s be Real;
assume A1: p < r & r <= s & s < q; then
r <= q by XXREAL_0:2; then
A3: p <= q by XXREAL_0:2,A1;
ex x being object st x in [.p,q.] & not x in [.r,s.]
proof
take q;
thus thesis by XXREAL_1:1,A1,A3;
end;
hence thesis by XBOOLE_0:def 8,XXREAL_1:34,A1;
end;
Lm5:
for a,b,c be Real holds
for x be Real holds b - |. b*(x-a)/c .| <= b
proof
let a,b,c be Real;
let x be Real;
|. b*(x-a)/c .| >= 0 by COMPLEX1:46; then
- |. b*(x-a)/c .|+b <= 0+b by XREAL_1:6;
hence thesis;
end;
begin :: Continuous Functions
theorem
for f,g be Function of REAL,REAL st
f is continuous & g is continuous holds
max(f,g) is continuous
proof
let f,g be Function of REAL,REAL;
assume A1: f is continuous;
assume A2: g is continuous;
for x be Real holds max(f,g).x = max(f.x, g.x)
proof
let x be Real;
reconsider x as Element of REAL by XREAL_0:def 1;
max(f,g).x = max(f.x, g.x) by COUSIN2:def 2;
hence thesis;
end;
hence thesis by FUZZY_5:16,A1,A2;
end;
theorem
for f,g be Function of REAL,REAL st
f is continuous & g is continuous holds
min(f,g) is continuous
proof
let f,g be Function of REAL,REAL;
assume A1: f is continuous;
assume A2: g is continuous;
for x be Real holds min(f,g).x = min(f.x, g.x)
proof
let x be Real;
reconsider x as Element of REAL by XREAL_0:def 1;
min(f,g).x= min(f.x, g.x) by COUSIN2:def 1;
hence thesis;
end;
hence thesis by FUZZY_5:15,A1,A2;
end;
theorem
for A,B be non empty closed_interval Subset of REAL
st B c< A holds
lower_bound A < lower_bound B or
upper_bound B < upper_bound A
proof
let A,B be non empty closed_interval Subset of REAL;
assume B c< A; then
[. lower_bound B, upper_bound B .] c< A by INTEGRA1:4; then
A2:[. lower_bound B, upper_bound B .] c< [. lower_bound A, upper_bound A .]
by INTEGRA1:4;
lower_bound B <= upper_bound B by SEQ_4:11;
hence thesis by A2,XXREAL_1:82;
end;
theorem Th12:
for A,B be non empty closed_interval Subset of REAL st
B c= A holds
lower_bound A <= lower_bound B & upper_bound B <= upper_bound A
proof
let A,B be non empty closed_interval Subset of REAL;
assume B c= A; then
[. lower_bound B, upper_bound B .] c= A by INTEGRA1:4; then
A2: [. lower_bound B, upper_bound B .] c= [. lower_bound A, upper_bound A .]
by INTEGRA1:4;
lower_bound B <= upper_bound B by SEQ_4:11;
hence thesis by XXREAL_1:50,A2;
end;
theorem
for r be Real, f,g be Function of REAL,REAL holds
r (#) (f +* g) = (r (#) f) +* (r (#) g)
proof
let r be Real, f,g be Function of REAL,REAL;
set F1 = r (#) (f +* g);
set F2 = (r (#) f) +* (r (#) g);
D1:dom F1 = REAL & dom F2 = REAL 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 A1: x in dom F1; then
reconsider x as Real;
A2: x in REAL by A1;
per cases;
suppose B1: x in dom g;
B2: x in dom (r (#) g) by FUNCT_2:def 1,A2;
(r (#) (f +* g)).x = r * (f +* g).x by VALUED_1:6
.= r * ( g).x by FUNCT_4:13,B1
.= (r (#) g).x by VALUED_1:6
.= ((r (#) f) +* (r (#) g)).x by FUNCT_4:13,B2;
hence thesis;
end;
suppose C1: not x in dom g;
C2: dom g = REAL by FUNCT_2:def 1
.= dom (r (#) g) by FUNCT_2:def 1;
(r (#) (f +* g)).x = r * (f +* g).x by VALUED_1:6
.= r * f.x by FUNCT_4:11,C1
.= (r (#) f).x by VALUED_1:6
.= ((r (#) f) +* (r (#) g)).x by FUNCT_4:11,C2,C1;
hence thesis;
end;
end;
hence thesis by FUNCT_1:2,D1;
end;
reserve A for non empty Subset of REAL;
theorem Th27:
for r be Real, f be Function of REAL,REAL holds
(r (#) f) | A = r (#) (f | A)
proof
let r be Real, f be Function of REAL,REAL;
set F = (r (#) f) | A;
set g = r (#) (f | A);
A1: dom ((r (#) f) | A) = A by FUNCT_2:def 1;
A2: dom (r (#) (f | A)) = A by FUNCT_2:def 1;
for x being object st x in dom F holds F . x = g . x
proof
let x be object;
assume D1: x in dom F; then
reconsider x as Real;
F . x = (r (#) f).x by FUNCT_1:49,D1
.= r * (f).x by VALUED_1:6
.= r * (f | A).x by FUNCT_1:49,D1
.= g . x by VALUED_1:6;
hence thesis;
end;
hence thesis by FUNCT_1:2,A1,A2;
end;
theorem
for r be Real, f be PartFunc of REAL,REAL st A c= dom f
holds
(r (#) f) | A = r (#) (f | A)
proof
let r be Real, f be PartFunc of REAL,REAL;
assume AA: A c= dom f; then
A1: A c= dom (r (#) f) by VALUED_1:def 5;
set F = (r (#) f) | A;
set g = r (#) (f | A);
A2: dom (r (#) (f | A))
= dom ((f | A)) by VALUED_1:def 5 .= A by RELAT_1:62,AA;
for x being object st x in dom F holds F . x = g . x
proof
let x be object;
assume D1:x in dom F; then
reconsider x as Real;
F . x = (r (#) f).x by FUNCT_1:49,D1
.= r * (f).x by VALUED_1:6
.= r * (f | A).x by FUNCT_1:49,D1
.= g . x by VALUED_1:6;
hence thesis;
end;
hence thesis by FUNCT_1:2,A1,A2,RELAT_1:62;
end;
theorem
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, f,g be Function of REAL,REAL;
( f | ].-infty,s.] ) +* ( g | [.s,+infty.[ )
= f|].-infty,s.[ +* g|[.s,+infty.[ by FUZZY_6:35;
hence thesis by FUZZY_6:18;
end;
theorem Th28:
for a,b,r being Real holds
r (#) (AffineMap (a,b)) = AffineMap (r*a,r*b)
proof
let a,b,r be Real;
D1: dom(r (#) (AffineMap (a,b))) = REAL by FUNCT_2:def 1;
D2: REAL = dom( AffineMap (r*a,r*b)) by FUNCT_2:def 1;
for x being object st x in dom( AffineMap (r*a,r*b)) holds
(r (#) (AffineMap (a,b)) ).x = AffineMap (r*a,r*b).x
proof
let x be object;
assume x in dom( AffineMap (r*a,r*b)); then
reconsider x as Real;
(r (#) (AffineMap (a,b)) ).x
= r * (AffineMap (a,b)).x by VALUED_1:6
.= r * (a*x+b) by FCONT_1:def 4
.= (r * a)*x+(r*b)
.= AffineMap (r*a,r*b).x by FCONT_1:def 4;
hence thesis;
end;
hence thesis by FUNCT_1:2,D1,D2;
end;
theorem
for s be Real, f,g being Function of REAL,REAL holds
dom ( ( f | ].-infty,s.] ) +* ( g | [.s,+infty.[ ) ) = REAL &
dom ( ( f | ].-infty,s.[ ) +* ( g | [.s,+infty.[ ) ) = REAL
proof
let s be Real;
let f,g be 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;
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;
hence thesis by FUZZY_6:35;
end;
theorem Th1:
for a,b,c be Real st b > 0 & c > 0 holds
for x be Real holds
( AffineMap ( b/c,b-a*b/c) | ]. -infty,a .]
+* AffineMap (-b/c,b+a*b/c) | [. a,+infty .[ ).x =
b - |. b*(x-a)/c .|
proof
let a,b,c be Real;
assume A1: b > 0;
assume A2: c > 0;
for x being Real holds
( AffineMap ( b/c,b-a*b/c) | ]. -infty,a .]
+* AffineMap (-b/c,b+a*b/c) | [. a,+infty .[ ).x = b -|. b*(x-a)/c .|
proof
let x be Real;
D2: dom ( AffineMap (-b/c,b+a*b/c) | [. a,+infty .[)
= [. a,+infty .[ by FUNCT_2:def 1;
per cases;
suppose A3: x<a; then
A31: a-x >x-x by XREAL_1:9;
A32: ( AffineMap ( b/c,b-a*b/c) | ]. -infty,a .]
+* AffineMap (-b/c,b+a*b/c) | [. a,+infty .[ ).x
= ( AffineMap ( b/c,b-a*b/c) | ]. -infty,a .] ).x
by FUNCT_4:11,D2,XXREAL_1:236,A3
.= (AffineMap ( b/c,b-a*b/c)).x by FUNCT_1:49,A3,XXREAL_1:234
.= b/c*x + (b-a*b/c) by FCONT_1:def 4
.= x*b/c + (b-a*b/c) by XCMPLX_1:74;
b-|. b*(x-a)/c .| = b-|. b*(x-a) .|/|. c .| by COMPLEX1:67
.= b-|. b .|*|. (x-a) .|/|. c .| by COMPLEX1:65
.= b- b *|. (x-a) .|/|. c .| by COMPLEX1:43,A1
.= b- b *|. (x-a) .|/ c by COMPLEX1:43,A2
.= b- b *|. (a-x) .|/ c by COMPLEX1:60
.= b- b * (a-x) / c by COMPLEX1:43,A31
.= b - (b*a - b*x)/c
.= b - (b*a/c - b*x/c) by XCMPLX_1:120;
hence thesis by A32;
end;
suppose A4:x>=a; then
A41: x-a >=a-a by XREAL_1:9;
A42: ( AffineMap ( b/c,b-a*b/c) | ]. -infty,a .]
+* AffineMap (-b/c,b+a*b/c) | [. a,+infty .[ ).x
= ( AffineMap (-b/c,b+a*b/c) | [. a,+infty .[ ).x
by FUNCT_4:13,D2,XXREAL_1:236,A4
.= (AffineMap ( -b/c,b+a*b/c)).x by FUNCT_1:49,A4,XXREAL_1:236
.= (-b/c)*x + (b+a*b/c) by FCONT_1:def 4
.= -(b/c*x) + (b+a*b/c)
.= -(x*b/c) + (b+a*b/c) by XCMPLX_1:74;
b-|. b*(x-a)/c .| = b-|. b*(x-a) .|/|. c .| by COMPLEX1:67
.= b-|. b .|*|. (x-a) .|/|. c .| by COMPLEX1:65
.= b- b *|. (x-a) .|/|. c .| by COMPLEX1:43,A1
.= b- b *|. (x-a) .|/ c by COMPLEX1:43,A2
.= b- b * (x-a) / c by COMPLEX1:43,A41
.= b - (b*x - b*a)/c
.= b - (b*x/c - b*a/c) by XCMPLX_1:120;
hence thesis by A42;
end;
end;
hence thesis;
end;
theorem
for a,b,c be Real, f be Function of REAL,REAL st
b > 0 & c > 0 &
(for x be Real holds f.x = b-|. b*(x-a)/c .|) holds
f = AffineMap (b/c,b-a*b/c) | ]. -infty,a .]
+* AffineMap (-b/c,b+a*b/c) | [. a,+infty .[
proof
let a,b,c be Real;
let f be Function of REAL,REAL;
assume A1: b > 0;
assume A2: c > 0;
assume A3: for x be Real holds f.x = b-|. b*(x-a)/c .|;
INF: -infty < a & a < +infty by XXREAL_0:9,XXREAL_0:12,XREAL_0:def 1;
D1a: dom (AffineMap (b/c,b-a*b/c) | ]. -infty,a .]
+* AffineMap (-b/c,b+a*b/c) | [. a,+infty .[ )
= dom (AffineMap (b/c,b-a*b/c) | ]. -infty,a .])
\/ dom(AffineMap (-b/c,b+a*b/c) | [. a,+infty .[ ) by FUNCT_4:def 1
.= ].-infty,a.] \/ dom( AffineMap (-b/c,b+a*b/c) | [. a,+infty .[ )
by FUNCT_2:def 1
.= ].-infty,a.] \/ [.a,+infty.[ by FUNCT_2:def 1
.= ].-infty,+infty.[ by XXREAL_1:172,INF;
for x being object st x in dom f holds
f.x = (AffineMap (b/c,b-a*b/c) | ]. -infty,a .]
+* AffineMap (-b/c,b+a*b/c) | [. a,+infty .[).x
proof
let x be object;
assume x in dom f; then
reconsider x as Element of REAL;
f.x = b-|. b*(x-a)/c .| by A3;
hence thesis by Th1,A1,A2;
end;
hence thesis by FUNCT_1:2,D1a,XXREAL_1:224,FUNCT_2:52;
end;
theorem
for a,b being Real st a > 0 holds
|. AffineMap (a,b) .| = (- (AffineMap(a,b) | ].-infty,(-b)/a.[))
+* (AffineMap(a,b) | [.(-b)/a,+infty.[)
proof
let a,b be Real;
assume A1: a > 0;
INF: -infty < (-b)/a & (-b)/a < +infty
by XXREAL_0:9,XXREAL_0:12,XREAL_0:def 1;
D1a: dom ((- (AffineMap(a,b) | ].-infty,(-b)/a.[ ))
+* (AffineMap(a,b) | [.(-b)/a,+infty.[ ) )
= dom ((- (AffineMap(a,b) | ].-infty,(-b)/a.[ )))
\/ dom((AffineMap(a,b) | [.(-b)/a,+infty.[ ) ) by FUNCT_4:def 1
.= ].-infty,(-b)/a.[ \/ dom( AffineMap(a,b) | [.(-b)/a,+infty.[ )
by FUNCT_2:def 1
.= ].-infty,(-b)/a.[ \/ [.(-b)/a,+infty.[ by FUNCT_2:def 1
.= REAL by XXREAL_1:224,XXREAL_1:173,INF;
for x being object st x in dom (|. AffineMap (a,b) .|) holds
|. AffineMap (a,b) .| .x
=( (- (AffineMap(a,b) | ].-infty,(-b)/a.[ ))
+* (AffineMap(a,b) | [.(-b)/a,+infty.[ )) . x
proof
let x be object;
assume x in dom (|. AffineMap (a,b) .|); then
reconsider x as Real;
A5: |. AffineMap (a,b) .| .x = |. AffineMap (a,b) .x .| by VALUED_1:18
.= |. a * x + b .| by FCONT_1:def 4;
per cases;
suppose A6: x>=(-b)/a; then
x*a >= (-b)/a*a by A1,XREAL_1:64; then
x*a >= (-b) by A1,XCMPLX_1:87; then
A8: a*x+b >= -b+b by XREAL_1:6;
x in [.(-b)/a,+infty.[ by XXREAL_1:236,A6; then
x in dom (AffineMap(a,b) | [.(-b)/a,+infty.[ ) by FUNCT_2:def 1;
then
( (- (AffineMap(a,b) | ].-infty,(-b)/a.[ ))
+* (AffineMap(a,b) | [.(-b)/a,+infty.[ )) . x
= (AffineMap(a,b) | [.(-b)/a,+infty.[ ) . x by FUNCT_4:13
.= AffineMap(a,b).x by FUNCT_1:49,XXREAL_1:236,A6
.= a*x+b by FCONT_1:def 4;
hence thesis by A5,A8,COMPLEX1:43;
end;
suppose B6: x <(-b)/a; then
x*a < (-b)/a*a by A1,XREAL_1:68; then
x*a < (-b) by A1,XCMPLX_1:87; then
A8: a*x+b < -b+b by XREAL_1:6;
not (x in dom (AffineMap(a,b) | [.(-b)/a,+infty.[ )) by B6,XXREAL_1:236;
then
( (- (AffineMap(a,b) | ].-infty,(-b)/a.[ ))
+* (AffineMap(a,b) | [.(-b)/a,+infty.[ )) . x
= (- (AffineMap(a,b) | ].-infty,(-b)/a.[) ) . x by FUNCT_4:11
.= - ((AffineMap(a,b) | ].-infty,(-b)/a.[).x) by VALUED_1:8
.= -AffineMap(a,b).x by FUNCT_1:49,XXREAL_1:233,B6
.= -(a*x+b) by FCONT_1:def 4;
hence thesis by A5,A8,COMPLEX1:70;
end;
end;
hence thesis by FUNCT_1:2,D1a,FUNCT_2:52;
end;
theorem
for a,b being Real st a < 0 holds
|. AffineMap (a,b) .| = ( (AffineMap(a,b) | ].-infty,(-b)/a.[ ))
+* - (AffineMap(a,b) | [.(-b)/a,+infty.[ )
proof
let a,b be Real;
assume A2: a < 0;
set f = ( (AffineMap(a,b) | ].-infty,(-b)/a.[ ))
+* - (AffineMap(a,b) | [.(-b)/a,+infty.[ );
A1: dom(-(AffineMap(a,b) | [.(-b)/a,+infty.[) ) = [.(-b)/a,+infty.[ &
[.(-b)/a,+infty.[ = dom((- AffineMap(a,b)) | [.(-b)/a,+infty.[)
by FUNCT_2:def 1;
for x being object st x in dom ((- AffineMap(a,b)) | [.(-b)/a,+infty.[)
holds
(- (AffineMap(a,b) | [.(-b)/a,+infty.[)).x
= ((- AffineMap(a,b)) | [.(-b)/a,+infty.[).x
proof
let x be object;
assume
A3: x in dom ((- AffineMap(a,b)) | [.(-b)/a,+infty.[);
hence ((- AffineMap(a,b)) | [.(-b)/a,+infty.[).x
= (- AffineMap(a,b)).x by FUNCT_1:49
.=- (AffineMap(a,b).x) by VALUED_1:8
.=- (AffineMap(a,b) | [.(-b)/a,+infty.[.x) by FUNCT_1:49,A3
.=(- (AffineMap(a,b) | [.(-b)/a,+infty.[)).x by VALUED_1:8;
end; then
- (AffineMap(a,b) | [.(-b)/a,+infty.[)
= (- AffineMap(a,b)) | [.(-b)/a,+infty.[ by FUNCT_1:2,A1; then
reconsider f as Function of REAL,REAL by FUZZY_6:18;
for x being Element of REAL holds f . x = |. AffineMap (a,b) .| . x
proof
let x be Element of REAL;
per cases;
suppose A6: x>=(-b)/a; then
x*a <= (-b)/a*a by A2,XREAL_1:65; then
x*a <= (-b) by A2,XCMPLX_1:87; then
A8: a*x+b <= -b+b by XREAL_1:6;
x in [.(-b)/a,+infty.[ by XXREAL_1:236,A6; then
x in dom (-( AffineMap(a,b) | [.(-b)/a,+infty.[ ))
by FUNCT_2:def 1;
hence
f.x = ( -( AffineMap(a,b) | [.(-b)/a,+infty.[ ) ).x by FUNCT_4:13
.= ( -( AffineMap(a,b) | [.(-b)/a,+infty.[ ).x ) by VALUED_1:8
.= -( AffineMap(a,b).x ) by FUNCT_1:49,XXREAL_1:236,A6
.= -(a*x+b) by FCONT_1:def 4
.= |. a*x+b .| by COMPLEX1:70,A8
.= |. AffineMap (a,b) . x .| by FCONT_1:def 4
.= |. AffineMap (a,b) .| . x by VALUED_1:18;
end;
suppose B5: x<(-b)/a; then
x*a > (-b)/a*a by A2,XREAL_1:69; then
x*a > (-b) by A2,XCMPLX_1:87; then
B8: a*x+b > -b+b by XREAL_1:6;
not x in dom (-( AffineMap(a,b) | [.(-b)/a,+infty.[ ))
by B5,XXREAL_1:236;
hence f.x = (AffineMap(a,b) | ].-infty,(-b)/a.[ ).x by FUNCT_4:11
.= AffineMap(a,b).x by FUNCT_1:49,XXREAL_1:233,B5
.= a*x+b by FCONT_1:def 4
.= |. a*x+b .| by COMPLEX1:43,B8
.= |. AffineMap (a,b) . x .| by FCONT_1:def 4
.= |. AffineMap (a,b) .| . x by VALUED_1:18;
end;
end;
hence thesis by FUNCT_2:63;
end;
theorem Lm20A:
for a,b,c be Real, f be Function of REAL,REAL st
b > 0 & c > 0 &
(for x be Real holds f.x = max(0, b - |. b*(x-a)/c .|)) holds
for x be Real st not x in ['a-c,a+c'] holds f.x = 0
proof
let a,b,c be Real;
let f be Function of REAL,REAL;
assume A1: b > 0 & c > 0; then
B1: -c < 0;
assume A2: for x be Real holds f.x = max(0,b-|. b*(x-a)/c .|);
for x be Real st not x in ['a-c,a+c'] holds f.x = 0
proof
let x be Real;
assume A4: not x in ['a-c,a+c'];
a < a+c & a-c < a by XREAL_1:44, XREAL_1:29,A1; then
A3: not x in [. a-c,a+c .] by INTEGRA5:def 3,A4,XXREAL_0:2;
per cases by A3;
suppose x < a-c; then
B2: x-a < a-c-a by XREAL_1:9; then
b*(x-a) < b*(-c) by A1,XREAL_1:68; then
b*(x-a)/c < (-c*b)/c by A1,XREAL_1:74; then
b*(x-a)/c < (-c*b/c) by XCMPLX_1:187; then
b*(x-a)/c < -b by A1,XCMPLX_1:89; then
B4: b*(x-a)/c + b < -b+b by XREAL_1:6;
thus f.x = max(0, b - |. b*(x-a)/c .|) by A2
.= max(0, b - -(b*(x-a)/c)) by COMPLEX1:70,A1,B1,B2
.= 0 by B4,XXREAL_0:def 10;
end;
suppose a+c < x; then
C2: x-a > a+c-a by XREAL_1:9; then
b*(x-a) > b*c by A1,XREAL_1:68; then
b*(x-a)/c > b*c/c by A1,XREAL_1:74; then
b*(x-a)/c > b by A1,XCMPLX_1:89; then
C4: b*(x-a)/c - b*(x-a)/c > b - b*(x-a)/c by XREAL_1:9;
thus f.x = max(0, b - |. b*(x-a)/c .|) by A2
.= max(0, b - (b*(x-a)/c)) by COMPLEX1:43,A1,C2
.= 0 by C4,XXREAL_0:def 10;
end;
end;
hence thesis;
end;
theorem Th3:
for a,b,c be Real, f,g be Function of REAL,REAL st
a < b & b < c holds
(f | ]. -infty,b .] +* g | [. b,+infty .[ ) | [. a,c .]
= (f | [. a,b .]) +* (g | [. b,c .])
proof
let a,b,c be Real, f,g be Function of REAL,REAL;
assume A1: a < b & b < c;
set F = f | ]. -infty,b .] +* g | [. b,+infty .[;
F = f | ]. -infty,b .[ +* g | [. b,+infty .[ by FUZZY_6:35; then
reconsider F as Function of REAL,REAL by FUZZY_6:18;
A3: dom ((f | [. a,b .]) +* (g | [. b,c .]))
= dom (f | [. a,b .]) \/ dom (g | [. b,c .]) by FUNCT_4:def 1
.= [. a,b .] \/ dom (g | [. b,c .]) by FUNCT_2:def 1
.= [. a,b .] \/ [. b,c .] by FUNCT_2:def 1
.= [. a,c .] by XXREAL_1:165,A1;
A2: dom (F | [. a,c .]) = [. a,c .] by FUNCT_2:def 1;
A7: dom (g | [. b,+infty .[) = [. b,+infty .[ by FUNCT_2:def 1;
A8: dom (g | [. b,c .]) = [. b,c .] by FUNCT_2:def 1;
for x being object st
x in dom ((f | ]. -infty,b .] +* g | [. b,+infty .[ ) | [. a,c .]) holds
((f | ]. -infty,b .] +* g | [. b,+infty .[ ) | [. a,c .]).x
= ( (f | [. a,b .]) +* (g | [. b,c .])).x
proof
let x be object;
assume
A4a: x in dom ((f | ]. -infty,b .] +* g | [. b,+infty .[ ) | [. a,c .]);
then reconsider x as Real by A2;
A5: a <= x & x <= c by XXREAL_1:1,A4a,A2;
per cases;
suppose A6: x >= b;
((f | ]. -infty,b .] +* g | [. b,+infty .[ ) | [. a,c .]).x
= (f | ]. -infty,b .] +* g | [. b,+infty .[).x by FUNCT_1:49, A4a,A2
.= (g | [. b,+infty .[).x by FUNCT_4:13,A6,XXREAL_1:236,A7
.= g.x by FUNCT_1:49, A6,XXREAL_1:236
.= (g | [. b,c .]).x by FUNCT_1:49, A6,A5,XXREAL_1:1
.= ( (f | [. a,b .]) +* (g | [. b,c .])).x
by FUNCT_4:13,A6,A5,XXREAL_1:1,A8;
hence thesis;
end;
suppose B1: x < b;
].-infty, b.[ c= ].-infty,b.] by XXREAL_1:21; then
A10: x in ].-infty,b.] by XXREAL_1:233,B1;
A11: x in [.a,b.] by B1,A5;
A12: not x in [. b,c .] by B1,XXREAL_1:1;
((f | ]. -infty,b .] +* g | [. b,+infty .[ ) | [. a,c .]).x
= (f | ]. -infty,b .] +* g | [. b,+infty .[ ).x by FUNCT_1:49, A4a,A2
.= (f | ]. -infty,b .] ).x by FUNCT_4:11,A7,XXREAL_1:236,B1
.= f.x by FUNCT_1:49, A10
.= (f | [. a,b .]).x by FUNCT_1:49, A11
.= ( (f | [. a,b .]) +* (g | [. b,c .])).x by FUNCT_4:11,A8,A12;
hence thesis;
end;
end;
hence thesis by FUNCT_1:2,A2,A3;
end;
theorem Th4:
for a,b,c be Real, f be Function of REAL,REAL st
b > 0 & c > 0 holds
( AffineMap ( b/c,b-a*b/c) | ]. -infty,a .]
+* AffineMap (-b/c,b+a*b/c) | [. a,+infty .[ ) | [. a-c,a+c .]
= AffineMap ( b/c,b-a*b/c) | [. a-c,a .]
+* AffineMap (-b/c,b+a*b/c) | [. a,a+c .]
proof
let a,b,c be Real, f be Function of REAL,REAL;
assume b > 0 & c > 0; then
a-c < a & a < a+c by XREAL_1:29,XREAL_1:44;
hence thesis by Th3;
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
holds
f is_integrable_on ['a,b'] & f is_integrable_on ['b,c'] &
f | ['a,b'] is bounded & ['a,b'] c= dom f &
integral (f,a,c) = (integral (f,a,b)) + (integral (f,b,c))
proof
let a,b,c be Real;
let f be Function of REAL,REAL;
assume A1: a < b & b < c; then
AD: a <= c by XXREAL_0:2;
assume A2: f is_integrable_on ['a,c'] & f | ['a,c'] is bounded;
reconsider F = f as PartFunc of REAL,REAL;
A6:REAL = dom f by FUNCT_2:def 1;
b in [. a,c .] by A1; then
A9: b in ['a,c'] by A1,INTEGRA5:def 3,XXREAL_0:2;
F is_integrable_on ['a,c'] & F | ['a,c'] is bounded by A2;
hence thesis by A6,A9,INTEGRA6:17,INTEGRA6:18,AD,A1;
end;
Th11X:
for a,b,c,d be Real, f be Function of REAL,REAL st
a <= b & b < c & c <= d &
f is_integrable_on ['a,d'] & f | ['a,d'] is bounded &
for x be Real st x in ['a,b'] \/ ['c,d'] holds f.x = 0
holds
centroid(f,['a,d']) = centroid(f,['b,c'])
proof
let a,b,c,d be Real;
let f be Function of REAL,REAL;
assume A1: a <= b & b < c & c <= d; then
A4: a < c by XXREAL_0:2;
assume A2: f is_integrable_on ['a,d'] & f | ['a,d'] is bounded;
assume A3: for x be Real st x in ['a,b'] \/ ['c,d'] holds f.x = 0;
A5: for x be Real st x in [' c, d '] holds f.x = 0
proof
let x be Real;
assume x in [' c, d ']; then
x in ['a,b'] \/ ['c,d'] by XBOOLE_0:def 3;
hence thesis by A3;
end;
AA: a <= a & a <= c & c <= d by XXREAL_0:2,A1;
AD: a <= d by XXREAL_0:2,A1,A4;
reconsider F = f as PartFunc of REAL,REAL;
B2: F is_integrable_on ['a,d'] & F | ['a,d'] is bounded by A2;
A6:REAL = dom f by FUNCT_2:def 1;
a <= c & c <= d by XXREAL_0:2,A1; then
c in [. a,d .]; then
A9: c in ['a,d'] by XXREAL_0:2,A1,A4,INTEGRA5:def 3;
A8: for x be Real st x in [' a,b '] holds F.x = 0
proof
let x be Real;
assume x in [' a,b ']; then
x in ['a,b'] \/ ['c,d'] by XBOOLE_0:def 3;
hence thesis by A3;
end;
reconsider F as Function of REAL,REAL;
A7a: F is_integrable_on ['a,c'] by INTEGRA6:17,AD,A6,A9,B2;
A77a: F | ['a,c'] is bounded by INTEGRA6:18,AA,A6,B2;
thus centroid(f,['a,d'])
= centroid(F,[' a,c']) by A4,A5,A1,A2,FUZZY_6:8
.= centroid(f,['b,c']) by A8,A1,A7a,A77a,FUZZY_6:9;
end;
theorem
for a,b,c,d be Real, f be Function of REAL,REAL st
a < b & b < c & c < d &
f is_integrable_on ['a,d'] & f | ['a,d'] is bounded &
for x be Real st x in ['a,b'] \/ ['c,d'] holds f.x = 0
holds
centroid(f,['a,d']) = centroid(f,['b,c'])
proof
let a,b,c,d be Real;
let f be Function of REAL,REAL;
assume A1: a < b & b < c & c < d; then
A4: a < c by XXREAL_0:2;
assume A2: f is_integrable_on ['a,d'] & f | ['a,d'] is bounded;
assume A3: for x be Real st x in ['a,b'] \/ ['c,d'] holds f.x = 0;
A5: for x be Real st x in [' c, d '] holds f.x = 0
proof
let x be Real;
assume x in [' c, d ']; then
x in ['a,b'] \/ ['c,d'] by XBOOLE_0:def 3;
hence thesis by A3;
end;
AA: a <= a & a <= c & c <= d by XXREAL_0:2,A1;
AD: a <= d by XXREAL_0:2,A1,A4;
reconsider F = f as PartFunc of REAL,REAL;
B2: F is_integrable_on ['a,d'] & F | ['a,d'] is bounded by A2;
A6:REAL = dom f by FUNCT_2:def 1;
a <= c & c <= d by XXREAL_0:2,A1; then
c in [. a,d .]; then
A9: c in ['a,d'] by XXREAL_0:2,A1,A4,INTEGRA5:def 3;
A8: for x be Real st x in [' a,b '] holds F.x = 0
proof
let x be Real;
assume x in [' a,b ']; then
x in ['a,b'] \/ ['c,d'] by XBOOLE_0:def 3;
hence thesis by A3;
end;
reconsider F as Function of REAL,REAL;
A7a: F is_integrable_on ['a,c'] by INTEGRA6:17,AD,A6,A9,B2;
A77a: F | ['a,c'] is bounded by INTEGRA6:18,AA,A6,B2;
thus centroid(f,['a,d'])
= centroid(F,[' a,c']) by A4,A5,A1,A2,FUZZY_6:8
.= centroid(f,['b,c']) by A8,A1,A7a,A77a,FUZZY_6:9;
end;
theorem Th17:
for A,B be non empty closed_interval Subset of REAL,
f be Function of REAL,REAL st lower_bound B <> upper_bound B & B c= A &
f is_integrable_on A & f | A is bounded &
(for x be Real st x in (A \ B) holds f.x = 0) &
f.(lower_bound B) = 0 & f.(upper_bound B) = 0
holds
centroid (f,A) = centroid (f,B)
proof
let A,B be non empty closed_interval Subset of REAL,
f be Function of REAL,REAL;
assume that
A0: lower_bound B <> upper_bound B and
A1: B c= A and
A4: f is_integrable_on A & f | A is bounded and
A2: (for x be Real st x in (A \ B) holds f.x = 0) and
A3: f.(lower_bound B) = 0 & f.(upper_bound B) = 0;
AA: A = [.lower_bound A, upper_bound A .] by INTEGRA1:4
.= [' lower_bound A, upper_bound A '] by INTEGRA5:def 3,SEQ_4:11;
BB: B = [.lower_bound B, upper_bound B .] by INTEGRA1:4
.= [' lower_bound B, upper_bound B '] by INTEGRA5:def 3,SEQ_4:11;
lower_bound B <= upper_bound B by SEQ_4:11; then
A7: lower_bound B < upper_bound B by A0,XXREAL_0:1;
A8: lower_bound A <= lower_bound B &
upper_bound B <= upper_bound A by Th12,A1;
for x be Real st
x in ['lower_bound A,lower_bound B'] \/ ['upper_bound B,upper_bound A']
holds f.x = 0
proof
let x be Real;
assume
A9: x in ['lower_bound A,lower_bound B'] \/ ['upper_bound B,upper_bound A'];
per cases by A9,XBOOLE_0:def 3;
suppose x in ['lower_bound A,lower_bound B']; then
x in [. lower_bound A,lower_bound B .] by INTEGRA5:def 3,Th12,A1;
then
x in [. lower_bound A,lower_bound B .[ \/ {lower_bound B}
by XXREAL_1:129,Th12,A1; then
per cases by XBOOLE_0:def 3;
suppose x in [. lower_bound A,lower_bound B .[; then
X1: x in [. lower_bound A,lower_bound B .[
\/ ]. upper_bound B,upper_bound A .] by XBOOLE_0:def 3;
[. lower_bound A,lower_bound B .[ \/ ]. upper_bound B,upper_bound A .]
c= [. lower_bound A,upper_bound A .] \ [. lower_bound B,upper_bound B .]
by Th8X,A7,A8; then
x in [. lower_bound A,upper_bound A .] \
[. lower_bound B,upper_bound B .] by X1; then
x in A \ [. lower_bound B,upper_bound B .] by INTEGRA1:4;
then
x in (A \ B) by INTEGRA1:4;
hence thesis by A2;
end;
suppose x in {lower_bound B};
hence thesis by TARSKI:def 1,A3;
end;
end;
suppose x in ['upper_bound B,upper_bound A']; then
x in [. upper_bound B,upper_bound A .] by INTEGRA5:def 3,Th12,A1;
then
x in {upper_bound B} \/ ]. upper_bound B,upper_bound A .]
by XXREAL_1:130,Th12,A1; then
per cases by XBOOLE_0:def 3;
suppose x in ]. upper_bound B,upper_bound A .]; then
X1: x in [. lower_bound A,lower_bound B .[
\/ ]. upper_bound B,upper_bound A .] by XBOOLE_0:def 3;
[. lower_bound A,lower_bound B .[ \/ ]. upper_bound B,upper_bound A .]
c= [. lower_bound A,upper_bound A .] \ [. lower_bound B,upper_bound B .]
by Th8X,A8,A7; then
x in [. lower_bound A,upper_bound A .] \
[. lower_bound B,upper_bound B .] by X1; then
x in A \ [. lower_bound B,upper_bound B .] by INTEGRA1:4; then
x in (A \ B) by INTEGRA1:4;
hence thesis by A2;
end;
suppose x in {upper_bound B};
hence thesis by TARSKI:def 1,A3;
end;
end;
end;
hence centroid (f,A) = centroid (f,B) by BB,Th11X,A7,A8,AA,A4;
end;
begin :: Triangular and Trapezoidal Membership Functions
theorem
for a,c be Real, f be Function of REAL,REAL st
c > 0 & ( for x be Real holds f.x = max(0, 1 - |. (x-a)/c .|) )
holds
f is triangular FuzzySet of REAL
proof
let a,c be Real;
let f be Function of REAL,REAL;
assume B1: c > 0;
assume A1: for x be Real holds f.x = max(0, 1 - |. (x-a)/c .|);
deffunc H1(Element of REAL) = In(1 - |. ($1-a)/c .|,REAL);
consider h being Function of REAL,REAL such that
A3: for x being Element of REAL holds h.x = H1(x) from FUNCT_2:sch 4;
A5: for x be Real holds f.x = max(0, min(1, h.x))
proof
let x be Real;
reconsider x as Element of REAL by XREAL_0:def 1;
A4: h.x = In(1 - |. (x-a)/c .|,REAL) by A3; then
h.x <= 1 by XREAL_1:43,COMPLEX1:46; then
max(0, min(1, h.x))
= max(0, 1 - |. (x-a)/c .|) by A4,XXREAL_0:def 9
.= f.x by A1;
hence thesis;
end;
reconsider f as FuzzySet of REAL by FUZZY_5:25,A5;
thus thesis by FUZZY_5:25,A5,FUZZY_5:66,B1,A1;
end;
Lm1:
for a,b,c be Real, f be Function of REAL,REAL st
b > 1 &
( for x be Real holds f.x = min(1, max(0, b - |. b*(x-a)/c .|)) )
holds
f is normalized FuzzySet of REAL
proof
let a,b,c be Real;
let f be Function of REAL,REAL;
assume A2: b > 1;
assume
A1: for x be Real holds f.x = min(1, max(0, b - |. b*(x-a)/c .|));
deffunc H1(Element of REAL) = In(b - |. b*($1-a)/c .|,REAL);
consider h being Function of REAL,REAL such that
A3: for x being Element of REAL holds h.x = H1(x) from FUNCT_2:sch 4;
for x be Real holds f.x = min(1, max(0, h.x))
proof
let x be Real;
reconsider x as Element of REAL by XREAL_0:def 1;
min(1, max(0, h.x)) = min(1, max(0, H1(x))) by A3
.= f.x by A1;
hence thesis;
end; then
reconsider f as FuzzySet of REAL by FUZZY_5:26;
f is normalized
proof
ex x being Element of REAL st f . x = 1
proof
A6:a is Element of REAL by XREAL_0:def 1;
take a;
f.a = min(1, max(0, b - |. b*(a-a)/c .|)) by A1
.= min(1, max(0, b - 0)) by ABSVALUE:def 1
.= min(1, b) by XXREAL_0:def 10,A2
.= 1 by XXREAL_0:def 9,A2;
hence thesis by A6;
end;
hence thesis;
end;
hence thesis;
end;
Lm2:
for a,b,c be Real, f be Function of REAL,REAL st
b > 1 & c > 0 &
( for x be Real holds f.x = min(1, max(0, b - |. b*(x-a)/c .|)) )
holds
f is trapezoidal FuzzySet of REAL
proof
let a,b,c be Real;
let f be Function of REAL,REAL;
assume A1: b > 1;
assume A2: c > 0;
assume A3: for x be Real holds f.x = min(1, max(0, b - |. b*(x-a)/c .|));
reconsider f as FuzzySet of REAL by Lm1,A1,A3;
A4:(1-(b+a*b/c))/(-(b/c)) - (1-(b-a*b/c))/(b/c)
= (-(1-(b+a*b/c)))/(b/c) - (1-(b-a*b/c))/(b/c) by XCMPLX_1:192
.= (-(1-(b+a*b/c)) - (1-(b-a*b/c))) /(b/c) by XCMPLX_1:120
.= (2*b-2) /(b/c);
b-1 > 1-1 by A1,XREAL_1:9; then
2*(b-1) > 0; then
B2:0 + (1-(b-a*b/c))/(b/c) < (1-(b+a*b/c))/(-(b/c))
-(1-(b-a*b/c))/(b/c)+(1-(b-a*b/c))/(b/c) by XREAL_1:29,A4,A1,A2;
for x be Real holds
f.x= max(0,min(1,
( (AffineMap (b/c,b-a*b/c) |].-infty,((b+a*b/c)-(b-a*b/c))/((b/c)+(b/c)).[) +*
(AffineMap (-(b/c),b+a*b/c)|
[.((b+a*b/c)-(b-a*b/c))/((b/c)+(b/c)),+infty.[) ) .x ))
proof
let x be Real;
C2: ((b+a*b/c)-(b-a*b/c))/((b/c)+(b/c))
= (b+a*b/c-b+a*b/c)/((b/c)+(b/c))
.= (a*(b/c)+a*b/c)/((b/c)+(b/c)) by XCMPLX_1:74
.= (a*(b/c)+a*(b/c))/((b/c)+(b/c)) by XCMPLX_1:74
.= a*(b/c+b/c)/((b/c)+(b/c))
.= a by XCMPLX_1:89,A1,A2;
C1: ( (AffineMap (b/c,b-a*b/c) |
].-infty,((b+a*b/c)-(b-a*b/c))/((b/c)+(b/c)).[) +*
(AffineMap (-(b/c),b+a*b/c)|
[.((b+a*b/c)-(b-a*b/c))/((b/c)+(b/c)),+infty.[) ) .x
= ( (AffineMap (b/c,b-a*b/c) | ]. -infty,a .]) +*
(AffineMap (-(b/c),b+a*b/c) | [. a,+infty .[) ).x by FUZZY_6:35,C2
.= b-|. b*(x-a)/c .| by Th1,A1,A2;
set F
= AffineMap (b/c,b-a*b/c) |].-infty,((b+a*b/c)-(b-a*b/c))/((b/c)+(b/c)).[;
set G
= AffineMap (-(b/c),b+a*b/c)|[.((b+a*b/c)-(b-a*b/c))/((b/c)+(b/c)),+infty.[;
thus f.x = min(1, max(0, (F +* G).x)) by C1,A3
.= max(0, min(1, (F +* G).x)) by XXREAL_0:37;
end;
hence thesis by FUZZY_5:89,A1,A2,B2;
end;
theorem
for a,b,c be Real, f be Function of REAL,REAL st
b > 1 & c > 0 &
( for x be Real holds f.x = min(1, max(0, b - |. b*(x-a)/c .|)) )
holds
f is trapezoidal FuzzySet of REAL &
f is normalized FuzzySet of REAL by Lm1,Lm2;
theorem
for a,b,c be Real, f be Function of REAL,REAL st
b > 0 & c > 0 &
( for x be Real holds f.x = max(0, b - |. b*(x-a)/c .|) ) holds
f = b (#) (TriangularFS (a-c,a,a+c))
proof
let a,b,c be Real, f be Function of REAL,REAL;
assume that
A1: b > 0 and
A2: c > 0 and
A3: for x be Real holds f.x = max(0, b - |. b*(x-a)/c .|);
set g = b (#) (TriangularFS (a-c,a,a+c));
A4: dom f = REAL by FUNCT_2:def 1
.= dom (b (#) (TriangularFS (a-c,a,a+c))) by FUNCT_2:def 1;
for x being object st x in dom f holds f . x = g . x
proof
let x be object;
assume x in dom f; then
reconsider x as Real;
( b (#) (TriangularFS (a-c,a,a+c)) ) .x
= b * (TriangularFS (a-c,a,a+c)) .x by VALUED_1:6
.= b * max(0,1-|.(x-a)/c.|) by FUZZY_5:65,A2
.= max(b*0,b*(1-|.(x-a)/c.|)) by FUZZY_2:41,A1
.= max(0,(b - b*|.(x-a)/c.|))
.= max(0,(b - |.b.| * |.(x-a)/c.|)) by A1,ABSVALUE:def 1
.= max(0,(b - |.b*((x-a)/c).|)) by COMPLEX1:65
.= max(0,(b - |.b*(x-a)/c.|)) by XCMPLX_1:74
.= f.x by A3;
hence thesis;
end;
hence thesis by A4,FUNCT_1:def 11;
end;
theorem Th14:
for a,b,c be Real, f be Function of REAL,REAL st
b > 0 & c > 0 &
(for x be Real holds f.x = max(0,b-|. b*(x-a)/c .|)) holds
f is Lipschitzian
proof
let a,b,c be Real, f be Function of REAL,REAL;
assume that
A1: b > 0 and
A2: c > 0 and
A3: for x be Real holds f.x = max(0,b-|. b*(x-a)/c .|);
for x be Real holds f.x = max(0,min(b,b*(1-|. (x-a)/c .|)))
proof
let x be Real;
max(0,min(b,b*(1-|. (x-a)/c .|)))
= max(0, min(b, (b*1-b*|. (x-a)/c .|) ))
.= max(0, min(b, (b - |.b.| * |. (x-a)/c .|) )) by A1,ABSVALUE:def 1
.= max(0, min(b,(b - |.b*((x-a)/c).|))) by COMPLEX1:65
.= max(0,min(b,(b - |.b*(x-a)/c.|))) by XCMPLX_1:74
.= max(0,(b - |.b*(x-a)/c.|)) by XXREAL_0:def 9,Lm5;
hence thesis by A3;
end;
hence thesis by FUZZY_5:70,A2;
end;
theorem Th15:
for a,b,c be Real, f be Function of REAL,REAL st
b > 0 & c > 0 &
f | ['a-c,a+c'] =
( AffineMap ( b/c,b-a*b/c) |
[. lower_bound ['a-c,a+c'], ((b+a*b/c) - (b-a*b/c))/((b/c)-(-b/c)) .] )
+* ( AffineMap (-b/c,b+a*b/c) |
[. (b+a*b/c - (b-a*b/c))/((b/c)-(-b/c)), upper_bound ['a-c,a+c'] .] )
holds
centroid (f,['a-c,a+c']) = a
proof
let a,b,c be Real, f be Function of REAL,REAL;
assume that
A1: b > 0 and
A2: c > 0 and
A3: f | ['a-c,a+c'] = ( AffineMap ( b/c,b-a*b/c) |
[. lower_bound ['a-c,a+c'], ((b+a*b/c) - (b-a*b/c))/((b/c)-(-b/c)) .] )
+* ( AffineMap (-b/c,b+a*b/c) |
[. ((b+a*b/c) - (b-a*b/c))/((b/c)-(-b/c)), upper_bound ['a-c,a+c'] .] );
set s = b/c;
set d = b-a*b/c;
set p = -b/c;
set q = b+a*b/c;
set C = ['a-c,a+c'];
A7:(q-d)/(s-p) = (b+a*b/c - b+a*b/c)/((b/c)+b/c)
.= (a*b/c +a*(b/c))/(b/c+b/c) by XCMPLX_1:74
.= (a*(b/c) +a*(b/c))/(b/c+b/c) by XCMPLX_1:74
.= (a*(b/c + b/c))/(b/c+b/c)
.= a*((b/c + b/c)/(b/c+b/c)) by XCMPLX_1:74
.= a by XCMPLX_1:88,A1,A2;
A10: a-c <= a & a <= a+c by XREAL_1:43,XREAL_1:29,A2;
[.(lower_bound C),(upper_bound C).] = ['a-c,a+c'] &
['a-c,a+c'] = [.a-c,a+c.] by A10,INTEGRA5:def 3,INTEGRA1:4,XXREAL_0:2;
then
A8: lower_bound C = a-c & a+c = upper_bound C by INTEGRA1:5;
Dd: d = (b*c-a*b)/c by XCMPLX_1:127,A2
.= (c-a)*b/c
.= (b/c)*(c-a) by XCMPLX_1:74;
Qq: q = (a*b + b*c)/c by XCMPLX_1:113,A2
.= b*(a + c)/c
.=(b/c)*(a+c) by XCMPLX_1:74;
CE: centroid(f,C) = (1/3*s*((a)^3 - (lower_bound C)^3)
+ 1/2*d*((a)^2 - (lower_bound C)^2)
+ 1/3*p*((upper_bound C)^3 - a^3)
+ 1/2*q*((upper_bound C)^2 - a^2) ) /
( 1/2*s*((a)^2 -(lower_bound C)^2) + d*(a - lower_bound C)
+ 1/2*p*((upper_bound C)^2 -(a)^2) + q*(upper_bound C -a))
by FUZZY_6:48,A3,A7,Lm6,A2,A1
.= ( 1/3*s*(a^3 - (a-c)^3) + 1/2*d*((a-(a-c))*(a+(a-c)))
+ 1/3*p*((a+c)^3 - a^3) + 1/2*q*(((a+c)-a)*((a+c)+a)) ) /
( 1/2*s*((a-(a-c))*(a+(a-c))) + d*c
+ 1/2*p*(((a+c)-a)*((a+c)+a)) + q*c ) by A8;
B1: 1/3*s*(a^3 - (a-c)^3) + 1/2*d*(c*(a+a-c))
+ 1/3*p*((a+c)^3 - a^3) + 1/2*q*(c*(a+c+a))
= (1/3*s*(a^3 - (a-c) ^3) + 1/2*d*(c*(a+a-c))
+ 1/3*p*((a+c) |^ 3 - a^3) + 1/2*q*(c*(a+c+a)) ) by POLYEQ_3:27
.= (1/3*s*(a^3 - (a-c) |^3 ) + 1/2*d*(c*(a+a-c))
+ 1/3*p*((a+c) |^ 3 - a^3) + 1/2*q*(c*(a+c+a)) ) by POLYEQ_3:27
.= (1/3*s*(a^3 - (a-c)^2*(a-c) ) + 1/2*c*d*(a+a-c)
+ 1/3*p*((a+c) |^ 3 - a^3) + 1/2*c*q*(a+c+a) ) by POLYEQ_3:27
.= 1/3*(b/c)*(a^3 - (a-c)^2*(a-c) ) + 1/2*c*((b/c)*(c-a))*(a+a-c)
+ 1/3*(b/c)*(-1)*((a+c) |^ 3 - a^3) + 1/2*c*((b/c)*(a+c))*(a+c+a)
by Qq,Dd
.= (1/3*(b/c))* ( (a^3 - (a-c)^2*(a-c) ) +((-1)*((a+c) |^ 3 - a^3)))
+ 1/2*c*(b/c)*( (a+c)*(2*a+c) +(c-a)*(2*a-c) )
.= (1/3*(b/c))* ( (a^3 - (((a ^2) - ((2 * a) * c)) + (c ^2))*(a-c) )
+((-1)*((a+c)^2*(a+c) - a^3)))
+ 1/2*c*(b/c)*( (a*(2*a)+a*c+c*(2*a)+c*c) +(c*(2*a)-c*c-a*(2*a)+a*c) )
by POLYEQ_3:27
.= (1/3*(b/c))*(
a^3 - (a^2*a-a^2*c - 2*a*c*a+2*a*c*c + c^2*a-c^2*c)
+ (-1)*( (a^2*a+a^2*c + 2*a*c*a+2*a*c*c + c^2*a+c^2*c) - a^3 )
) + 1/2*(c*(b/c))*( 6*a*c )
.= (1/3*(b/c))*(
a^3 - (a^2*a-a^2*c - 2*a*c*a+2*a*c*c + c^2*a-c^2*c)
+ (-1)*( (a^2*a+a^2*c + 2*a*c*a+2*a*c*c + c^2*a+c^2*c) - a^3 )
) + 1/2*(c*b/c)*( 6*a*c ) by XCMPLX_1:74
.= (1/3*(b/c))*(
a^3 - a^2*a+a^2*c + 2*a*c*a - 2*a*c*c - c^2*a+c^2*c
+ ( (-1)*a^2*a+ (-1)*a^2*c + (-1)*2*a*c*a+(-1)*2*a*c*c +
(-1)*c^2*a+(-1)*c^2*c - (-1)*a^3 )
) + 1/2*(b)*( 6*a*c ) by XCMPLX_1:89,A2
.= (1/3*(b/c))*( a^3 - a^2*a + a*a*c - 4*a*c*c - c^2*a -a^2*a+ -a^2*c
-c^2*a+ - -a^3) + 1/2*6*b*a*c
.= (1/3*(b/c))*(
a^3 - a^2*a + a*a*c - 4*a*c*c - c^2*a -a^3+ -a^2*c
-c^2*a+ - -a^3) + 1/2*6*b*a*c by POLYEQ_3:def 3
.= (1/3*(b/c))*(-a^2*a +a*a*c -4*a*c*c -c^2*a -a^2*c -c^2*a +a^3
) + 3*b*a*c
.= (1/3*(b/c))*(-a^3 +a*a*c -4*a*c*c -c^2*a -a^2*c -c^2*a +a^3
) + 3*b*a*c by POLYEQ_3:def 3
.= (-6)*(1/3)*((b/c)*c)* a*c + 3*b*a*c
.= (-6)*(1/3)*((c*b/c))* a*c + 3*b*a*c by XCMPLX_1:74
.= (-6)*(1/3)*(b)* a*c + 3*b*a*c by XCMPLX_1:89,A2
.= a*(b*c);
1/2*s*((a-(a-c))*(a+(a-c))) + d*c + 1/2*p*(((a+c)-a)*((a+c)+a)) + q*c
= 1/2*((b/c)*c)*(2*a-c) - 1/2*((b/c)*c)*(2*a+c)
+ ((b/c)*c)*(c-a)+((b/c)*c)*(c+a) by Dd,Qq
.= 1/2*((b/c)*c)*(2*a-c) - 1/2*((b/c)*c)*(2*a+c)
+ ((b*c/c))*(c-a)+((b/c)*c)*(c+a) by XCMPLX_1:74
.= 1/2*((b/c)*c)*(2*a-c) - 1/2*((b/c)*c)*(2*a+c)
+ ((b))*(c-a)+((b/c)*c)*(c+a) by XCMPLX_1:89,A2
.= 1/2*((b*c/c))*(2*a-c) - 1/2*((b/c)*c)*(2*a+c)
+ b*(c-a)+((b/c)*c)*(c+a) by XCMPLX_1:74
.= 1/2*((b*c/c))*(2*a-c) - 1/2*((b*c/c))*(2*a+c)
+ b*(c-a)+((b/c)*c)*(c+a) by XCMPLX_1:74
.= 1/2*((b*c/c))*(2*a-c) - 1/2*((b*c/c))*(2*a+c)
+ b*(c-a)+((b*c/c))*(c+a) by XCMPLX_1:74
.= 1/2*((b*c/c))*(2*a-c) - 1/2*((b*c/c))*(2*a+c)
+ b*(c-a)+b*(c+a) by XCMPLX_1:89,A2
.= 1/2*((b*c/c))*(2*a-c) - 1/2*b*(2*a+c)
+ b*(c-a)+b*(c+a) by XCMPLX_1:89,A2
.= 1/2*b*(2*a-c) - 1/2*b*(2*a+c) + b*(c-a)+b*(c+a) by XCMPLX_1:89,A2
.= b*c;
hence centroid(f,C) = a by XCMPLX_1:89,A1,A2,CE,B1;
end;
Lm16:
for a,b,c be Real st
b > 0 & c > 0 holds
( for x be Real st x in ['a-c,a+c'] holds 0 <= b - |. b*(x-a)/c .|)
proof
let a,b,c be Real;
assume A1:b > 0 & c > 0;
let x be Real;
assume A2: x in ['a-c,a+c'];
A10a:a-c <= a & a <= a+c by XREAL_1:43,XREAL_1:29,A1;
x in [.a-c,a+c.] by INTEGRA5:def 3,XXREAL_0:2,A2,A10a; then
a-c <= x & x <= a+c by XXREAL_1:1; then
A3a: a-c+c <= x+c & x-x <= a+c-x by XREAL_1:13,XREAL_1:6; then
A3:c-(x-a) >= 0 & c+x-a >= a-a by XREAL_1:13;
per cases;
suppose 0 <= b*(x-a)/c; then
b - |. b*(x-a)/c .| = b - b*(x-a)/c by ABSVALUE:def 1
.= (b*c-b*(x-a))/c by XCMPLX_1:127,A1
.= b*(c-(x-a))/c;
hence thesis by A1,A3a;
end;
suppose b*(x-a)/c < 0; then
b - |. b*(x-a)/c .| = b - -b*(x-a)/c by ABSVALUE:def 1
.= b*(x-a)/c +b
.= (b*c+b*(x-a))/c by XCMPLX_1:113,A1
.= b*(c+x-a)/c;
hence thesis by A1,A3;
end;
end;
theorem Th16:
for a,b,c be Real, f be Function of REAL,REAL st
b > 0 & c > 0 &
( for x be Real holds f.x = max(0, b - |. b*(x-a)/c .|)) holds
f | ['a-c,a+c'] =
( AffineMap ( b/c,b-a*b/c) |
[. lower_bound ['a-c,a+c'], (b+a*b/c - (b-a*b/c))/((b/c)-(-b/c)) .] )
+* ( AffineMap (-b/c,b+a*b/c) |
[. (b+a*b/c - (b-a*b/c))/((b/c)-(-b/c)), upper_bound ['a-c,a+c'] .] )
proof
let a,b,c be Real, f be Function of REAL,REAL;
assume that
A1: b > 0 and
A2: c > 0 and
A3: for x be Real holds f.x = max(0, b - |. b*(x-a)/c .|);
set s = b/c;
set d = b-a*b/c;
set p = -b/c;
set q = b+a*b/c;
set C = ['a-c,a+c'];
A7:(q-d)/(s-p) = (b+a*b/c - b+a*b/c)/((b/c)+b/c)
.= (a*b/c +a*(b/c))/(b/c+b/c) by XCMPLX_1:74
.= (a*(b/c) +a*(b/c))/(b/c+b/c) by XCMPLX_1:74
.= (a*(b/c + b/c))/(b/c+b/c)
.= a*((b/c + b/c)/(b/c+b/c)) by XCMPLX_1:74
.= a by XCMPLX_1:88,A1,A2;
A10: a-c <= a & a <= a+c by XREAL_1:43,XREAL_1:29,A2;
A8: [.(lower_bound C),(upper_bound C).] = ['a-c,a+c'] &
['a-c,a+c'] = [.a-c,a+c.] by XXREAL_0:2,A10,INTEGRA5:def 3,INTEGRA1:4;
set G = AffineMap ( b/c,b-a*b/c) | ]. -infty,a .]
+* AffineMap (-b/c,b+a*b/c) | [. a,+infty .[;
G = AffineMap ( b/c,b-a*b/c) | ]. -infty,a .[
+* AffineMap (-b/c,b+a*b/c) | [. a,+infty .[ by FUZZY_6:35;
then reconsider G as Function of REAL,REAL by FUZZY_6:18;
set g = ( AffineMap ( b/c,b-a*b/c) |
[. lower_bound ['a-c,a+c'], ((b+a*b/c) - (b-a*b/c))/((b/c)-(-b/c)) .] )
+* ( AffineMap (-b/c,b+a*b/c) |
[. ((b+a*b/c) - (b-a*b/c))/((b/c)-(-b/c)), upper_bound ['a-c,a+c'] .] );
GI:g = ( AffineMap ( b/c,b-a*b/c) | [. lower_bound ['a-c,a+c'], a .] )
+* ( AffineMap (-b/c,b+a*b/c) | [. a, a+c .] ) by A8,INTEGRA1:5,A7
.= ( AffineMap ( b/c,b-a*b/c) | [.a-c, a .] )
+* ( AffineMap (-b/c,b+a*b/c) | [. a, a+c .] ) by A8,INTEGRA1:5
.= ( AffineMap ( b/c,b-a*b/c) | ]. -infty,a .]
+* AffineMap (-b/c,b+a*b/c) | [. a,+infty .[ ) | [. a-c,a+c .] by Th4,A1,A2;
B4: dom (f | ['a-c,a+c']) = ['a-c,a+c'] by FUNCT_2:def 1
.= [. a-c,a+c .] by XXREAL_0:2,A10,INTEGRA5:def 3
.= dom (G | [. a-c,a+c .]) by FUNCT_2:def 1
.= dom g by GI;
for x being object st x in dom (f | ['a-c,a+c']) holds
(f | ['a-c,a+c']) . x = g . x
proof
let x be object;
assume B1: x in dom (f | ['a-c,a+c']); then
C1: x in ['a-c,a+c'];
reconsider x as Real by B1;
C2: x in [.a-c,a+c.] by XXREAL_0:2,A10,INTEGRA5:def 3,C1;
C3: 0 <= b - |. b*(x-a)/c .| by Lm16,A1,A2,B1;
g . x = ( AffineMap ( b/c,b-a*b/c) | ]. -infty,a .]
+* AffineMap (-b/c,b+a*b/c) | [. a,+infty .[ ) .x by FUNCT_1:49,C2,GI
.= b - |. b*(x-a)/c .| by Th1,A1,A2
.= max(0, b - |. b*(x-a)/c .|) by C3,XXREAL_0:def 10
.= f.x by A3;
hence thesis by FUNCT_1:49,B1;
end;
hence f | ['a-c,a+c'] = ( AffineMap ( b/c,b-a*b/c) |
[. lower_bound ['a-c,a+c'], ((b+a*b/c) - (b-a*b/c))/((b/c)-(-b/c)) .] )
+* ( AffineMap (-b/c,b+a*b/c) |
[. ((b+a*b/c) - (b-a*b/c))/((b/c)-(-b/c)),
upper_bound ['a-c,a+c'] .] ) by B4,FUNCT_1:def 11;
end;
theorem Th19:
for a,b,c be Real, f be Function of REAL,REAL st b > 0 & c > 0 &
( for x be Real holds f.x = max(0,b-|. b*(x-a)/c .|) ) holds
centroid (f,['a-c,a+c']) = a
proof
let a,b,c be Real, f be Function of REAL,REAL;
assume that
A1: b > 0 and
A2: c > 0 and
A3: for x be Real holds f.x = max(0, b - |. b*(x-a)/c .|);
f | ['a-c,a+c'] = ( AffineMap ( b/c,b-a*b/c) |
[. lower_bound ['a-c,a+c'], (b+a*b/c - (b-a*b/c))/((b/c)-(-b/c)) .] )
+* ( AffineMap (-b/c,b+a*b/c) |
[. (b+a*b/c - (b-a*b/c))/((b/c)-(-b/c)), upper_bound ['a-c,a+c'] .] )
by Th16,A1,A2,A3;
hence thesis by Th15,A1,A2;
end;
reserve A for non empty closed_interval Subset of REAL;
theorem Lm20:
for a,b,c be Real, f be Function of REAL,REAL st
b > 0 & c > 0 &
(for x be Real holds f.x = max(0,b-|. b*(x-a)/c .|))
holds
f is_integrable_on A & f | A is bounded
proof
let a,b,c be Real, f be Function of REAL,REAL;
assume that
A1: b > 0 and
A2: c > 0 and
A3: for x be Real holds f.x = max(0, b - |. b*(x-a)/c .|);
reconsider f as PartFunc of REAL,REAL;
f is Lipschitzian by Th14,A3,A1,A2; then
A6: f | A is continuous;
dom f = REAL by FUNCT_2:def 1;
hence thesis by INTEGRA5:11,INTEGRA5:10,A6;
end;
theorem Lm20B:
for a,b,c be Real, f be Function of REAL,REAL st
b > 0 & c > 0 &
(for x be Real holds f.x = max(0,b-|. b*(x-a)/c .|))
holds
f.(lower_bound ['a-c,a+c']) = 0 & f.(a-c) = 0 &
f.(upper_bound ['a-c,a+c']) = 0 & f.(a+c) = 0
proof
let a,b,c be Real, f be Function of REAL,REAL;
assume that
A1: b > 0 and
A2: c > 0 and
A3: for x be Real holds f.x = max(0, b - |. b*(x-a)/c .|);
A5: a < a+c & a-c < a by XREAL_1:44, XREAL_1:29,A2;
A8: [.(lower_bound ['a-c,a+c']),(upper_bound ['a-c,a+c']).] = ['a-c,a+c']
& ['a-c,a+c'] = [.a-c,a+c.] by XXREAL_0:2,A5,INTEGRA5:def 3,INTEGRA1:4;
A6: f.(a-c) = max(0, b - |. b*((a-c)-a)/c .|) by A3
.= max(0, b - |. (-1)*(c*b)/c .|)
.= max(0, b - |. (-1)*(c*b/c) .|) by XCMPLX_1:74
.= max(0, b - |. (-c*b/c) .|)
.= max(0, b - |. -b .|) by A2,XCMPLX_1:89
.= max(0, b - -(- b)) by ABSVALUE:def 1,A1
.= 0;
f.(a+c) = max(0, b - |. b*((a+c)-a)/c .|) by A3
.= max(0, b - |. b .|) by A2,XCMPLX_1:89
.= max(0, b - b) by ABSVALUE:def 1,A1
.= 0;
hence thesis by A6,A8,INTEGRA1:5;
end;
theorem
for a,b,c be Real, f be Function of REAL,REAL st
b > 0 & c > 0 & ['a-c,a+c'] c= A &
(for x be Real holds f.x = max(0,b-|. b*(x-a)/c .|))
holds
centroid (f,A) = a
proof
let a,b,c be Real, f be Function of REAL,REAL;
assume that
A1: b > 0 and
A2: c > 0 and
A4: ['a-c,a+c'] c= A and
A3: for x be Real holds f.x = max(0, b - |. b*(x-a)/c .|);
A5: a < a+c & a-c < a by XREAL_1:44, XREAL_1:29,A2;
[.(lower_bound ['a-c,a+c']),(upper_bound ['a-c,a+c']).] = ['a-c,a+c']
& ['a-c,a+c'] = [.a-c,a+c.] by XXREAL_0:2,A5,INTEGRA5:def 3,INTEGRA1:4;
then
A8: lower_bound ['a-c,a+c'] = a-c &
a+c = upper_bound ['a-c,a+c'] by INTEGRA1:5;
A7: for x be Real st x in (A \ ['a-c,a+c']) holds f.x = 0
proof
let x be Real;
assume A71: x in (A \ ['a-c,a+c']);
not x in ['a-c,a+c'] by XBOOLE_0:def 5,A71;
hence thesis by Lm20A,A1,A2,A3;
end;
A9: f.(lower_bound ['a-c,a+c']) = 0 &
f.(upper_bound ['a-c,a+c']) = 0 by Lm20B,A1,A2,A3;
f is_integrable_on A & f | A is bounded by Lm20,A1,A2,A3; then
centroid (f,A) = centroid (f,['a-c,a+c']) by Th17,A4,A7,A9,A8,A5;
hence thesis by A1,A2,A3,Th19;
end;
theorem Lm21:
for a,b,c be Real st a < b & b < c & b-a = c-b holds
centroid (TriangularFS (a,b,c),['a,c']) = b
proof
let a,b,c be Real;
assume that
A1: a < b & b < c and
A2: b-a = c-b;
A4: b-a > a-a by A1, XREAL_1:9;
for x be Real holds TriangularFS (a,b,c).x = max(0,1-|.1*(x-b)/(b-a).|)
proof
let x be Real;
max(0,1-|.(x-b)/(b-a).|)
= TriangularFS (b-(b-a),b,b+(b-a)).x by FUZZY_5:65,A4;
hence thesis by A2;
end;
then
centroid (TriangularFS (a,b,c),['b - (b-a),b+(b-a)']) = b by Th19,A4;
hence thesis by A2;
end;
theorem Lm21L:
for a,b,c be Real st a < b & b < c holds
TriangularFS (a,b,c) is_integrable_on A &
TriangularFS (a,b,c) | A is bounded
proof
let a,b,c be Real;
assume A1: a < b & b < c;
reconsider f = TriangularFS (a,b,c) as PartFunc of REAL,REAL;
TriangularFS (a,b,c) is Lipschitzian by FUZZY_5:86,A1; then
A6:f | A is continuous;
dom f = REAL by FUNCT_2:def 1;
hence thesis by INTEGRA5:11,INTEGRA5:10,A6;
end;
theorem
for a,b,c,d be Real st a < b & b < c & b-a = c-b & d <> 0 holds
centroid (d (#) TriangularFS (a,b,c),['a,c']) = b
proof
let a,b,c,d be Real;
assume that
A1: a < b & b < c and
A2: b-a = c-b and
D1: d <> 0;
TriangularFS (a,b,c) is_integrable_on ['a,c'] &
TriangularFS (a,b,c) | ['a,c'] is bounded by Lm21L,A1; then
centroid((d (#) TriangularFS (a,b,c)),['a,c'])
= centroid(TriangularFS (a,b,c),['a,c']) by FUZZY_6:32,D1;
hence thesis by Lm21,A1,A2;
end;
theorem Lm22c:
for a,b,c,d be Real st a < b & b < c & c < d holds
TrapezoidalFS (a,b,c,d) is_integrable_on A &
TrapezoidalFS (a,b,c,d) | A is bounded
proof
let a,b,c,d be Real;
assume A1: a < b & b < c & c < d;
reconsider f = TrapezoidalFS (a,b,c,d) as PartFunc of REAL,REAL;
TrapezoidalFS (a,b,c,d) is Lipschitzian by FUZZY_5:87,A1; then
A6:f | A is continuous;
dom f = REAL by FUNCT_2:def 1;
hence thesis by INTEGRA5:11,INTEGRA5:10,A6;
end;
theorem Lm22d:
for a,b,c,d,r be Real st a < b & b < c & c < d holds
r (#) TrapezoidalFS (a,b,c,d) is_integrable_on A
proof
let a,b,c,d,r be Real;
assume A1: a < b & b < c & c < d;
reconsider f = TrapezoidalFS (a,b,c,d) as PartFunc of REAL,REAL;
A2: f is_integrable_on A & f | A is bounded by Lm22c,A1;
REAL = dom f by FUNCT_2:def 1;
hence thesis by A2,INTEGRA6:9;
end;
theorem
for a1,c,a2,d be Real, f be Function of REAL,REAL st
c > 0 & d > 0 & a1 < a2 &
f = ( d (#) TrapezoidalFS (a1-c,a1,a2,a2+c) ) | ['a1-c,a2+c']
holds f is_integrable_on ['a1-c,a2+c']
proof
let a1,c,a2,d be Real, f be Function of REAL,REAL;
assume that
A1: c > 0 & d > 0 & a1 < a2 and
A2: f = ( d (#) TrapezoidalFS (a1-c,a1,a2,a2+c) ) | ['a1-c,a2+c'];
a1-c < a1-0 & a2+0 < a2+c by A1,XREAL_1:15,XREAL_1:8; then
(( d (#) TrapezoidalFS (a1-c,a1,a2,a2+c) ) | ['a1-c,a2+c'])
| ['a1-c,a2+c'] is integrable by A1,Lm22d,INTEGRA5:def 1;
hence thesis by INTEGRA5:def 1,A2;
end;
theorem Lm22b1p:
for a,b,c be Real, f,g be Function of REAL,REAL,
h be PartFunc 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 & [.a,c.] c= dom h holds
h | [.a,c.] is continuous
proof
let a,b,c be Real, f,g be Function of REAL,REAL,
h be PartFunc 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
A5: [.a,c.] c= dom h;
A6: dom f = REAL & dom g = 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,g 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.]; then
P1: a <= x0 & x0 <= c by XXREAL_1:1;
assume P2: 0 < r;
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,A6,A2a;
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 ::::::::::::: x1 in [.b,c.] & x0 in [.a,b.]
R2:x1 in [.b,c.] by P5a;
R1a: x1 -b >= b-b by XREAL_1:13,R1; then
R4m: x1 - x0 > 0 by B1,XREAL_1:15; then
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;
R7a: b-x0 <= x1 - x0 by R1,XREAL_1:9;
b - x0 > x0 - x0 by B1,XREAL_1:14; then
b-x0 = |. b-x0 .| by COMPLEX1:43; then
|. b-x0 .| <= |.(x1 - x0).| by R7a,COMPLEX1:43,R4m; 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;
R9r: |. 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 R8,XXREAL_0:2,R9r;
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
P9r: |.((f . x1) - (f . x0)).| < r/2 by P8,P4;
|.((h . x1) - (h . x0)).|
= |. ((f| [.a,b.]) +* (g | [.b,c.])) . x1 - h . x0.|
by A3,FUNCT_1:49,P5
.= |. (f| [.a,b.]) . x1 - h . x0.| by P7,FUNCT_4:11
.= |. 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
.= |.((f . x1) - (f . x0)).| by FUNCT_1:49,B1a;
hence thesis by XXREAL_0:2,P9a,P9r;
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,Bin,FCONT_1:14,A6,A2a;
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;
R7X: b-x1 <= x0 - x1 by B2,XREAL_1:9;
b - x1 > x1 - x1 by Q1,XREAL_1:14; then
|. b-x1 .| <= |.(x0 - x1).| by R7X,COMPLEX1:43,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
P9e: |.((g . x1) - (g . x0)).| < r/2 by S1,QX1;
|.((h . x1) - (h . x0)).|
= |. ((f| [.a,b.]) +* (g | [.b,c.])) . x1 - h . x0.|
by A3,FUNCT_1:49,S3
.= |. (g | [.b,c.]) . x1 - h . x0.| by FUNCT_4:13,DGG,QX1
.= |. g . x1 - h . x0.| by FUNCT_1:49,QX1
.= |. g . x1 - ((f| [.a,b.]) +* (g | [.b,c.])) . x0.|
by A3,FUNCT_1:49,P1a
.= |. g . x1 - (g | [.b,c.]) . x0.| by DGG,QX0,FUNCT_4:13
.= |.((g . x1) - (g . x0)).| by FUNCT_1:49,QX0;
hence |.((h . x1) - (h . x0)).| < r by XXREAL_0:2,P9a,P9e;
end;
end;
hence thesis by S1a,S2a,XXREAL_0:21;
end;
end;
hence thesis;
end;
hence h | [.a,c.] is continuous by FCONT_1:14,A5;
end;
theorem
for a,b,p,q be 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 be Real, f be Function of REAL,REAL;
assume A1: a <> p &
f = (AffineMap (a,b)|].-infty,(q-b)/(a-p).]) +*
(AffineMap (p,q)|[.(q-b)/(a-p),+infty.[); then
f = (AffineMap (a,b)|].-infty,(q-b)/(a-p).[) +*
(AffineMap (p,q)|[.(q-b)/(a-p),+infty.[) by FUZZY_6:35;
hence thesis by FUZZY_6:28,A1;
end;
theorem Th26p:
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 | [.a,c.] = (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 | [.a,c.] = (f| [.a,b.]) +* (g | [.b,c.]) and
A4: f.b = g.b;
A5g: dom f = REAL & dom g = REAL by FUNCT_2:def 1;
set A = ['a,c'];
reconsider ff = f, 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,A5g,A2a; 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 FUZZY_6:6;
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;
XX: [. a,c .] c= REAL /\ [.a,c.] by XBOOLE_0:def 4;
AC: [. a,c .] = REAL /\ [.a,c.]
proof
REAL /\ [.a,c.] c= [. a,c .] by XBOOLE_0:def 4;
hence thesis by XX,XBOOLE_0:def 10;
end;
H1: dom (id REAL (#) (h| [.a,c.]))
= dom (id REAL) /\ dom( (h| [.a,c.])) by VALUED_1:def 4
.= [.a,c.] by AC,FUNCT_2:def 1;
H2: dom((id REAL (#) h) | [.a,c.]) = [.a,c.] by FUNCT_2:def 1;
H33: for x being object st x in dom ((id REAL (#) h) | [.a,c.]) holds
(id REAL (#) (h| [.a,c.])).x = ((id REAL (#) h) | [.a,c.]).x
proof
let x be object;
assume H4: x in dom ((id REAL (#) h) | [.a,c.]); then
reconsider x as Real;
(id REAL (#) (h| [.a,c.])).x
= (id REAL ).x * (h| [.a,c.]) .x by VALUED_1:5
.= (id REAL ).x * (h) .x by FUNCT_1:49,H4
.= (id REAL (#) h).x by VALUED_1:5
.= ((id REAL (#) h) | [.a,c.]).x by FUNCT_1:49,H4;
hence thesis;
end;
B3b: [. a,c .] = (dom (id REAL (#) (h| [.a,c.]))) /\ [.a,c.] by H1;
for x being object st x in dom G holds
G . x = (id REAL (#) (h| [.a,c.])) . x
proof
let x be object;
assume Xac: x in dom G; then
reconsider x as Real by B3a;
C1: a <= x & x <= c by Xac,B3a,XXREAL_1:1;
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| [.a,c.])) . 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 | [.a,c.])) . x by A3,VALUED_1:5;
hence thesis;
end;
end; then
B3z: (id REAL (#) (h| [.a,c.]))| [.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;
reconsider hh = h as PartFunc of REAL,REAL;
D1p: REAL = dom h by FUNCT_2:def 1; then
hh | [.a,c.] is continuous by Lm22b1p,A1,A2,A4,A3; then
hh | ['a,c'] is continuous by XXREAL_0:2,A1,INTEGRA5:def 3; then
h is_integrable_on ['a,c'] & h | ['a,c'] is bounded
by INTEGRA5:10,INTEGRA5:11,D1p; then
(id REAL) (#) h is_integrable_on ['a,c'] by FUZZY_6:6;
hence integral((id REAL) (#) h,['a,c'])
= integral((id REAL) (#) f,['a,b']) + integral((id REAL) (#) g,['b,c'])
by FUZZY_6:33,A1,B12,B4,FUNCT_1:2,H1,H2,H33,B3z;
end;
theorem LmSymTrape2:
for a, b, c, d, r be Real st
a < b & b < c & c < d holds
(((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +*
((AffineMap (0,1)) | [.b,c.]) +*
((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.])
= TrapezoidalFS (a,b,c,d) | [.a,d.]
proof
let a, b, c, d, r be Real;
assume that
Z1: a < b and
Z2: b < c and
Z3: c < d;
Z4: a < c by XXREAL_0:2,Z1,Z2;
set f1 = AffineMap ( 1/(b-a),-(a/(b-a)) ) | [.a,b.];
set f2 = AffineMap (0,1) | [.b,c.];
set f3 = AffineMap ( -(1/(d-c)),d/(d-c) ) | [.c,d.];
D2: dom ((AffineMap ( 1/(b-a),-(a/(b-a)) ) | [.a,b.]) +*
(AffineMap (0,1) | [.b,c.]) +*
(AffineMap ( -(1/(d-c)),d/(d-c) ) | [.c,d.]) )
= dom ((AffineMap ( 1/(b-a),-(a/(b-a)) ) | [.a,b.]) +*
(AffineMap (0,1) | [.b,c.]) ) \/
dom ((AffineMap ( -(1/(d-c)),d/(d-c) ) | [.c,d.]) ) by FUNCT_4:def 1
.= dom ((AffineMap ( 1/(b-a),-(a/(b-a)) ) | [.a,b.]) ) \/
dom( (AffineMap (0,1) | [.b,c.]) ) \/
dom ((AffineMap ( -(1/(d-c)),d/(d-c) ) | [.c,d.]) )
by FUNCT_4:def 1
.= [.a,b.] \/ dom( (AffineMap (0,1) | [.b,c.]) ) \/
dom ((AffineMap ( -(1/(d-c)),d/(d-c) ) | [.c,d.]) )
by FUNCT_2:def 1
.= [.a,b.] \/ [.b,c.] \/
dom ((AffineMap ( -(1/(d-c)),d/(d-c) ) | [.c,d.]) )
by FUNCT_2:def 1
.= [.a,b.] \/ [.b,c.] \/ [.c,d.] by FUNCT_2:def 1
.= [.a,c.] \/ [.c,d.] by XXREAL_1:165,Z1,Z2
.= [.a,d.] by XXREAL_1:165,Z4,Z3;
D1: dom (f1 +* f2 +* f3 )
= dom( TrapezoidalFS (a,b,c,d) | [.a,d.] ) by FUNCT_2:def 1,D2;
for x being object st x in dom (TrapezoidalFS (a,b,c,d) | [.a,d.]) holds
((((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +*
((AffineMap (0,1)) | [.b,c.]) +*
((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]) ).x
= ( TrapezoidalFS (a,b,c,d) | [.a,d.] ).x
proof
let x be object;
assume A1a: x in dom (TrapezoidalFS (a,b,c,d) | [.a,d.]); then
reconsider x as Real;
( TrapezoidalFS (a,b,c,d) | [.a,d.] ).x
= ( TrapezoidalFS (a,b,c,d) ).x by FUNCT_1:49,A1a
.= ( AffineMap (0,0)|(REAL \ ].a,d.[) +* f1 +* f2 +* f3).x
by FUZNUM_1:def 8,Z1,Z2,Z3
.= ( AffineMap (0,0)|(REAL \ ].a,d.[) +* f1 +* (f2 +* f3)).x
by FUNCT_4:14
.= ( AffineMap (0,0)|(REAL \ ].a,d.[) +* (f1 +* (f2 +* f3))).x
by FUNCT_4:14
.= ( AffineMap (0,0)|(REAL \ ].a,d.[) +* (f1 +* f2 +* f3) ).x
by FUNCT_4:14
.= (f1 +* f2 +* f3 ).x by FUNCT_4:13,A1a,D2;
hence thesis;
end;
hence thesis by FUNCT_1:2,D1;
end;
theorem
for a, b, c, d, r be Real st
a < b & b < c & c < d holds
TrapezoidalFS (a,b,c,d)
= (AffineMap (0,0) | (REAL \ ].a,d.[)) +*
TrapezoidalFS (a,b,c,d) | [.a,d.]
proof
let a, b, c, d, r be Real;
assume A1: a < b & b < c & c < d;
set f1 = (AffineMap (0,0)) | (REAL \ ].a,d.[);
set f2 = AffineMap ((1 / (b - a)),(- (a / (b - a)))) | [.a,b.];
set f3 = (AffineMap (0,1)) | [.b,c.];
set f4 = (AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.];
thus TrapezoidalFS (a,b,c,d)
= ((((AffineMap (0,0)) | (REAL \ ].a,d.[)) +*
((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +*
((AffineMap (0,1)) | [.b,c.])) +*
((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.])
by FUZNUM_1:def 8,A1
.= f1 +* (f2 +* f3) +* f4 by FUNCT_4:14
.= f1 +* ((f2 +* f3) +* f4) by FUNCT_4:14
.= (AffineMap (0,0) | (REAL \ ].a,d.[)) +* TrapezoidalFS (a,b,c,d) | [.a,d.]
by LmSymTrape2,A1;
end;
theorem LmSymTrape4:
for a, b, c, d, r be Real st
a < b & b < c & c < d holds
(r (#) AffineMap (1 / (b - a),- (a /(b-a)) ) ) | [.a,b.] +*
(r (#) AffineMap (0,1)) | [.b,c.] +*
(r (#) AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]
= ( r (#) TrapezoidalFS (a,b,c,d) ) | [.a,d.]
proof
let a, b, c, d, r be Real;
assume that
Z1: a < b and
Z2: b < c and
Z3: c < d;
Z4: a < c by XXREAL_0:2,Z1,Z2;
set f1 = AffineMap ( 1/(b-a),-(a/(b-a)) ) | [.a,b.];
set f2 = AffineMap (0,1) | [.b,c.];
set f3 = AffineMap ( -(1/(d-c)),d/(d-c) ) | [.c,d.];
A1: ( r (#) TrapezoidalFS (a,b,c,d) ) | [.a,d.]
= ( r (#) TrapezoidalFS (a,b,c,d) ) | ['a,d']
by INTEGRA5:def 3,XXREAL_0:2,Z3,Z4
.= r (#) (TrapezoidalFS (a,b,c,d) | ['a,d']) by Th27
.= r (#) (TrapezoidalFS (a,b,c,d) | [.a,d.] )
by INTEGRA5:def 3,XXREAL_0:2,Z3,Z4
.= r (#) ( ( (((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) +*
((AffineMap (0,1)) | [.b,c.])) +*
((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]) )
by LmSymTrape2,Z1,Z2,Z3;
set F1 = AffineMap ( 1/(b-a),-(a/(b-a)) );
set F2 = AffineMap (0,1);
set F3 = AffineMap ( -(1/(d-c)),d/(d-c) );
D2: [.a,d.] = dom(r (#) (f1 +* f2 +* f3)) by A1,FUNCT_2:def 1;
D1:dom ( (r (#) F1) | [.a,b.] +* (r (#) F2) | [.b,c.]
+* (r (#) F3) | [.c,d.])
=dom ( (r (#) F1) | ['a,b'] +* (r (#) F2) | [.b,c.]
+* (r (#) F3) | [.c,d.]) by INTEGRA5:def 3,Z1
.=dom ( (r (#) (F1 | ['a,b']) ) +* (r (#) F2) | [.b,c.]
+* (r (#) F3) | [.c,d.]) by Th27
.=dom ( (r (#) (F1 | ['a,b']) ) +* (r (#) F2) | ['b,c']
+* (r (#) F3) | [.c,d.]) by INTEGRA5:def 3,Z2
.=dom ( (r (#) (F1 | ['a,b']) ) +* (r (#) (F2 | ['b,c']))
+* (r (#) F3) | [.c,d.]) by Th27
.=dom ( (r (#) (F1 | ['a,b']) ) +* (r (#) (F2 | ['b,c']))
+* (r (#) F3) | ['c,d']) by INTEGRA5:def 3,Z3
.=dom ( (r (#) (F1 | ['a,b']) ) +* (r (#) (F2 | ['b,c']))
+* (r (#) (F3 | ['c,d']))) by Th27
.=dom ( (r (#) (F1 | [.a,b.]) ) +* (r (#) (F2 | ['b,c']))
+* (r (#) (F3 | ['c,d']))) by INTEGRA5:def 3,Z1
.=dom ( (r (#) (F1 | [.a,b.]) ) +* (r (#) (F2 | [.b,c.]))
+* (r (#) (F3 | ['c,d']))) by INTEGRA5:def 3,Z2
.=dom (
(r (#) AffineMap ( 1/(b-a),-(a/(b-a)) ) | [.a,b.]) +*
(r (#) AffineMap (0,1) | [.b,c.]) +*
(r (#) AffineMap ( -(1/(d-c)),d/(d-c) ) | [.c,d.])) by INTEGRA5:def 3,Z3
.= dom ((r (#) f1) +*
(r (#) AffineMap (0,1) | [.b,c.]) ) \/
dom ((r (#) AffineMap ( -(1/(d-c)),d/(d-c) ) | [.c,d.]) ) by FUNCT_4:def 1
.= dom (
(r (#) AffineMap ( 1/(b-a),-(a/(b-a)) ) | [.a,b.]) ) \/
dom( (r (#) AffineMap (0,1) | [.b,c.]) ) \/
dom ((r (#) AffineMap ( -(1/(d-c)),d/(d-c) ) | [.c,d.]) )
by FUNCT_4:def 1
.= [.a,b.] \/ dom( (r (#) AffineMap (0,1) | [.b,c.]) ) \/
dom ((r (#) AffineMap ( -(1/(d-c)),d/(d-c) ) | [.c,d.]) )
by FUNCT_2:def 1
.= [.a,b.] \/ [.b,c.] \/
dom ((r (#) AffineMap ( -(1/(d-c)),d/(d-c) ) | [.c,d.]) )
by FUNCT_2:def 1
.= [.a,b.] \/ [.b,c.] \/ [.c,d.] by FUNCT_2:def 1
.= [.a,c.] \/ [.c,d.] by XXREAL_1:165,Z1,Z2
.= [.a,d.] by XXREAL_1:165,Z4,Z3;
for x being object st x in dom (r (#) (f1 +* f2 +* f3)) holds
( ( r (#) F1 ) | [.a,b.] +*
( r (#) F2 ) | [.b,c.] +* ( r (#) F3 ) | [.c,d.] ).x=
(r (#) (f1 +* f2 +* f3)).x
proof
let x be object;
assume P0: x in dom (r (#) (f1 +* f2 +* f3)); then
reconsider x as Real by D2;
P1: a <= x & x <= d by XXREAL_1:1,P0,D2;
per cases;
suppose c <= x; then
P21: x in [.c,d.] by P1; then
P22: x in dom f3 by FUNCT_2:def 1;
P23: x in dom (( r (#) F3 ) | [.c,d.]) by FUNCT_2:def 1,P21;
( ( r (#) F1 ) | [.a,b.] +* ( r (#) F2 ) | [.b,c.] +*
( r (#) F3 ) | [.c,d.] ).x
= (( r (#) F3 ) | [.c,d.] ).x by FUNCT_4:13,P23
.= (( r (#) F3 ) | ['c,d'] ).x by INTEGRA5:def 3,Z3
.= ( r (#) (F3 | ['c,d']) ).x by Th27
.= ( r (#) f3 ).x by INTEGRA5:def 3,Z3
.= r * f3.x by VALUED_1:6
.= r * (f1 +* f2 +* f3).x by FUNCT_4:13,P22;
hence thesis by VALUED_1:6;
end;
suppose P3: x < c; then
P32: not x in dom f3 by XXREAL_1:1;
P33: not x in dom (( r (#) F3 ) | [.c,d.] ) by XXREAL_1:1,P3;
Q1:(r (#) (f1 +* f2 +* f3)).x = r * ((f1 +* f2 +* f3).x) by VALUED_1:6
.= r * (f1 +* f2).x by FUNCT_4:11,P32;
per cases;
suppose b <= x; then
R11: x in [.b,c.] by P3; then
R12: x in dom f2 by FUNCT_2:def 1;
R13: x in dom((r (#) F2) | [.b,c.]) by FUNCT_2:def 1,R11;
(r (#) (f1 +* f2 +* f3)).x = r * ( f2).x by FUNCT_4:13,R12,Q1
.= (r (#) f2).x by VALUED_1:6
.= (r (#) (F2 | ['b,c']) ).x by INTEGRA5:def 3,Z2
.= ((r (#) F2) | ['b,c'] ).x by Th27
.= ((r (#) F2) | [.b,c.] ).x by INTEGRA5:def 3,Z2
.= ( ( r (#) F1 ) | [.a,b.] +* ( r (#) F2 ) | [.b,c.] ).x
by FUNCT_4:13,R13;
hence thesis by FUNCT_4:11,P33;
end;
suppose R2: x < b; then
R22: not x in dom f2 by XXREAL_1:1;
R23: not x in dom (( r (#) F2 ) | [.b,c.]) by XXREAL_1:1,R2;
( ( r (#) F1 ) | [.a,b.] +* ( r (#) F2 ) | [.b,c.] +*
( r (#) F3 ) | [.c,d.] ).x =
( ( r (#) F1 ) | [.a,b.] +* ( r (#) F2 ) | [.b,c.] ).x
by FUNCT_4:11,P33
.= ( ( r (#) F1 ) | [.a,b.] ).x by FUNCT_4:11,R23
.= ( ( r (#) F1 ) | ['a,b'] ).x by INTEGRA5:def 3,Z1
.= ( r (#) (F1 | ['a,b']) ).x by Th27
.= (r (#) f1).x by INTEGRA5:def 3,Z1
.= r * (f1).x by VALUED_1:6
.= (r (#) (f1 +* f2 +* f3)).x by Q1,FUNCT_4:11,R22;
hence thesis;
end;
end;
end;
hence thesis by FUNCT_1:2,D1,D2,A1;
end;
theorem SymTrape:
for a1,c,a2,d be Real st
c > 0 & d > 0 & a1 < a2 holds
AffineMap(d/c,-(d/c)*(a1 - c)) | [.a1- c,a1.] +*
AffineMap(0,d) | [.a1,a2.] +*
AffineMap(-d/c, (d/c)*(a2 + c)) | [.a2,a2+c.]
= ( d (#) TrapezoidalFS (a1-c,a1,a2,a2+c) ) | ['a1-c,a2+c']
proof
let a1,c,a2,d be Real;
assume
A1: c > 0 & d > 0 & a1 < a2; then
AB: a1-c < a1-0 & a2+0 < a2+c by XREAL_1:15,XREAL_1:8; then
AC: a1-c < a2 by XXREAL_0:2,A1;
set dT = d (#) TrapezoidalFS (a1-c,a1,a2,a2+c);
set F = AffineMap(d/c,-(d/c)*(a1 - c)) | [.a1- c,a1.] +*
AffineMap(0,d) | [.a1,a2.] +*
AffineMap(-d/c, (d/c)*(a2 + c)) | [.a2,a2+c.];
A2:AffineMap(d/c,-(d/c)*(a1 - c)) | [.a1- c,a1.]
= AffineMap(d*(1/c),(-(d*1/c))*(a1 - c)) | [.a1- c,a1.] by XCMPLX_1:99
.= AffineMap(d*(1/c),(-d*(1/c))*(a1 - c)) | [.a1- c,a1.] by XCMPLX_1:99
.= AffineMap(d*(1/c),d*(-(1/c)*(a1 - c))) | [.a1- c,a1.]
.= (d (#) AffineMap((1/c),(-(1/c)*(a1 - c)))) | [.a1- c,a1.] by Th28
.= (d (#) AffineMap(1/(a1-(a1-c)),-((a1-c)/(a1-(a1-c))))) | [.a1-c,a1.]
by XCMPLX_1:99;
A3: AffineMap(-d/c, (d/c)*(a2 + c)) | [.a2,a2+c.]
= AffineMap(-d*(1/c), (d/c)*(a2 + c)) | [.a2,a2+c.] by XCMPLX_1:99
.= AffineMap(d*(-1/c), d*((a2 + c)/c)) | [.a2,a2+c.] by XCMPLX_1:75
.= (d (#) AffineMap(-1/((a2+c)-a2), ((a2+c)/((a2+c)-a2)))) | [.a2,a2+c.]
by Th28;
F = (d (#) AffineMap(1/(a1-(a1-c)),-((a1-c)/(a1-(a1-c))))) | [.a1-c,a1.] +*
(AffineMap(d*0,d*1) | [.a1,a2.]) +*
(d (#) AffineMap(-1/((a2+c)-a2), ((a2+c)/((a2+c)-a2)))) | [.a2,a2+c.] by A3,A2
.= (d (#) AffineMap(1/(a1-(a1-c)),-((a1-c)/(a1-(a1-c))))) | [.a1-c,a1.] +*
(d (#) AffineMap(0,1)) | [.a1,a2.] +*
(d (#) AffineMap(-1/((a2+c)-a2), ((a2+c)/((a2+c)-a2)))) | [.a2,a2+c.] by Th28
.= ( d (#) TrapezoidalFS (a1-c,a1,a2,a2+c) ) | [.a1-c,a2+c.]
by A1,AB,LmSymTrape4;
hence thesis by INTEGRA5:def 3,AC,XXREAL_0:2,AB;
end;
Lm29n1:
for a1,c,a2,d be Real st c > 0 & d > 0 & a1 < a2 holds
integral((id REAL) (#) AffineMap(d/c,-(d/c)*(a1 - c)), ['a1-c,a1']) +
integral((id REAL) (#) AffineMap(0,d), ['a1,a2']) +
integral((id REAL) (#) AffineMap(-d/c, (d/c)*(a2 + c)), ['a2,a2+c'])
= 1/2*d*(c+a2-a1)*(a1+a2)
proof
let a1,c,a2,d be Real;
assume
A1: c > 0 & d > 0 & a1 < a2;
set f = integral((id REAL) (#) AffineMap(d/c,-(d/c)*(a1 - c)), ['a1-c,a1']);
set g = integral((id REAL) (#) AffineMap(0,d), ['a1,a2']);
set h=integral((id REAL) (#) AffineMap(-d/c, (d/c)*(a2 + c)), ['a2,a2+c']);
B1: a1-c <= a2-0 & a2+0 <= a2 + c by A1,XREAL_1:13,XREAL_1:7;
B2: a1-c <= a1-0 & a1 <= a2 by A1,XREAL_1:13;
hence
f+g+h = integral((id REAL) (#) AffineMap(d/c,-(d/c)*(a1 - c)), a1-c,a1)
+g+h by INTEGRA5:def 4
.= integral((id REAL) (#) AffineMap(d/c,-(d/c)*(a1 - c)), a1-c,a1) +
integral((id REAL) (#) AffineMap(0,d),a1,a2) + h by INTEGRA5:def 4,A1
.= integral((id REAL) (#) AffineMap(d/c,-(d/c)*(a1 - c)), a1-c,a1) +
integral((id REAL) (#) AffineMap(0,d),a1,a2) +
integral((id REAL) (#) AffineMap(-d/c, (d/c)*(a2 + c)),a2,a2+c)
by INTEGRA5:def 4,B1
.= 1/3*(d/c)*(a1*a1*a1 - (a1-c)*(a1-c)*(a1-c))
+ 1/2*(-(d/c)*(a1 - c))*(a1*a1 - (a1-c)*(a1-c)) +
integral((id REAL) (#) AffineMap(0,d),a1,a2) +
integral((id REAL) (#) AffineMap(-d/c, (d/c)*(a2 + c)),a2,a2+c)
by FUZZY_6:45,B2
.= 1/3*(d/c)*(a1*a1*a1 - (a1-c)*(a1-c)*(a1-c))
+ 1/2*(-(d/c)*(a1 - c))*(a1*a1 - (a1-c)*(a1-c)) +
(1/3*0*(a2*a2*a2 - a1*a1*a1) + 1/2*d*(a2*a2 - a1*a1)) +
integral((id REAL) (#) AffineMap(-d/c, (d/c)*(a2 + c)),a2,a2+c)
by FUZZY_6:45,A1
.= 1/3*(d/c)*(a1*a1*a1 - (a1*a1-a1*c-c*a1+c*c)*(a1-c))
+ 1/2*(-(d/c)*(a1 - c))*(a1*a1 - (a1*a1-a1*c-c*a1+c*c))
+ 1/2*d*a2*a2 - 1/2*d*a1*a1+ (1/3*(-d/c)*((a2+c)*(a2+c)*(a2+c) - a2*a2*a2)
+ 1/2*((d/c)*(a2 + c))*((a2+c)*(a2+c) - a2*a2) ) by FUZZY_6:45,B1
.= -1/2*(-((d/c)*c))*a1*c + 1/2*(d/c*c)*a2*c+ 1/2*d*a2*a2 - 1/2*d*a1*a1
.= -1/2*(-(d))*a1*c + 1/2*(d/c*c)*a2*c+ 1/2*d*a2*a2 - 1/2*d*a1*a1
by XCMPLX_1:87,A1
.= 1/2*d*a1*c + 1/2*d*a2*c+ 1/2*d*a2*a2 - 1/2*d*a1*a1 by XCMPLX_1:87,A1
.= 1/2*d*(c+ a2-a1)*(a1 + a2);
end;
Lm29n:
for a1,c,a2,d be Real, f be Function of REAL,REAL st
c > 0 & d > 0 & a1 < a2 &
f | [.a1-c,a2+c.] = AffineMap(d/c,-(d/c)*(a1 - c)) | [.a1- c,a1.] +*
AffineMap(0,d) | [.a1,a2.] +*
AffineMap(-d/c, (d/c)*(a2 + c)) | [.a2,a2+c.]
holds
integral((id REAL) (#) f,['a1-c,a2+c']) =
integral((id REAL) (#) AffineMap(d/c,-(d/c)*(a1 - c)), ['a1-c,a1']) +
integral((id REAL) (#) AffineMap(0,d), ['a1,a2']) +
integral((id REAL) (#) AffineMap(-d/c, (d/c)*(a2 + c)), ['a2,a2+c'])
proof
let a1,c,a2,d be Real, f be Function of REAL,REAL;
assume that
A1: c > 0 & d > 0 & a1 < a2 and
A2: f | [.a1-c,a2+c.] = AffineMap(d/c,-(d/c)*(a1 - c)) | [.a1- c,a1.] +*
AffineMap(0,d) | [.a1,a2.] +*
AffineMap(-d/c, (d/c)*(a2 + c)) | [.a2,a2+c.];
set F1 = AffineMap(d/c,-(d/c)*(a1 - c));
set F2= AffineMap(0,d);
set F3 = AffineMap(-d/c, (d/c)*(a2 + c));
reconsider F =
AffineMap(d/c,-(d/c)*(a1 - c)) | ].-infty,a1.[ +*
AffineMap(0,d) | [.a1,+infty.[ as Function of REAL,REAL by FUZZY_6:18;
set ap = ((d)-(-(d/c)*(a1 - c)))/((d/c)-(0));
P2: (d- (-(d/c)*(a1 - c)))/(d/c-0)
= (d+(d/c)*(a1 - c))/(d/c)
.= d/(d/c)+ (a1 - c) by XCMPLX_1:113,A1
.= c + (a1 - c) by XCMPLX_1:54,A1
.= a1;
B1: a1-c <= a2-0 & a2+0 <= a2 + c by A1,XREAL_1:13,XREAL_1:7; then
P3f: [.(lower_bound ['a1 - c,a2']),(upper_bound ['a1 - c,a2']).]
= ['a1 - c,a2']
& ['a1 - c,a2'] = [.a1 - c,a2.] by INTEGRA5:def 3,INTEGRA1:4;
then
P3: upper_bound ['a1 - c,a2'] = a2
& lower_bound ['a1 - c,a2'] = a1-c by INTEGRA1:5;
a1-c <= a1-0 & a1 <= a2 by A1,XREAL_1:13; then
((d)-(-(d/c)*(a1 - c)))/((d/c)-(0)) in [.a1-c,a2.] by P2; then
P1: ((d)-(-(d/c)*(a1 - c)))/((d/c)-(0)) in ['a1-c,a2'] by INTEGRA5:def 3,B1;
F | ['a1-c,a2'] =
AffineMap(d/c,-(d/c)*(a1 - c)) | [.lower_bound ['a1-c,a2'],ap.] +*
AffineMap(0,d) | [.ap,upper_bound ['a1-c,a2'].] by FUZZY_6:40,P1,P2;
then
C1:integral((id REAL) (#) F, ['a1-c,a2'])
= integral((id REAL) (#) AffineMap(d/c,-(d/c)*(a1 - c)), ['a1-c,a1']) +
integral((id REAL) (#) AffineMap(0,d), ['a1,a2'])
by P2,P3,FUZZY_6:43,P1,A1;
a2 in [.a1,+infty.[ by XXREAL_1:236,A1; then
B4a: a2 in dom(AffineMap(0,d) | [.a1, +infty.[) by FUNCT_2:def 1;
B4: F3.a2 = (-d/c)*a2+(d/c)*(a2 + c) by FCONT_1:def 4
.= (-d/c)*a2+(d/c)*a2 + (d/c)*c
.= 0*a2 + d by A1,XCMPLX_1:87
.= F2.a2 by FCONT_1:def 4
.= (AffineMap(0,d) | [.a1,+infty.[).a2 by FUNCT_1:49,XXREAL_1:236,A1
.= F.a2 by FUNCT_4:13,B4a;
B2: F is Lipschitzian by FUZZY_6:28,P2,A1;
(F | [.a1-c,a2.]) +* ( F3|[.a2,a2+c.] )
= (F | ['a1-c,a2']) +* ( F3|[.a2,a2+c.] ) by INTEGRA5:def 3,B1
.= AffineMap(d/c,-(d/c)*(a1 - c)) | [.lower_bound ['a1-c,a2'],ap.] +*
AffineMap(0,d) | [.ap,upper_bound ['a1-c,a2'].] +* ( F3|[.a2,a2+c.] )
by FUZZY_6:40,P1,P2
.= AffineMap(d/c,-(d/c)*(a1 - c)) | [.a1-c,ap.] +*
AffineMap(0,d) | [.ap,upper_bound ['a1-c,a2'].] +* ( F3|[.a2,a2+c.] )
by P3f,INTEGRA1:5
.= f | [.a1-c,a2+c.] by A2,P2,P3f,INTEGRA1:5;
hence integral((id REAL) (#) f,['a1-c,a2+c'])
= integral((id REAL) (#) F1,['a1-c,a1'])
+ integral((id REAL) (#) F2,['a1,a2'])
+ integral((id REAL) (#) F3,['a2,a2+c']) by C1,Th26p,B1,B2,B4;
end;
theorem Lm29d1:
for a1,c,a2,d be Real st c > 0 & d > 0 & a1 < a2 holds
integral( AffineMap(d/c,-(d/c)*(a1 - c)), ['a1- c,a1']) +
integral( AffineMap(0,d), ['a1, a2']) +
integral( AffineMap(-d/c, (d/c)*(a2 + c)), ['a2,a2+c']) = d*(a2-a1+c)
proof
let a1,c,a2,d be Real;
assume
A1: c > 0 & d > 0 & a1 < a2;
set f = integral( AffineMap(d/c,-(d/c)*(a1 - c)), ['a1- c,a1']);
set g = integral( AffineMap(0,d), ['a1,a2']);
set h = integral( AffineMap(-d/c, (d/c)*(a2 + c)), ['a2,a2+c']);
B1: a1-c <= a2-0 & a2+0 <= a2 + c by A1,XREAL_1:13,XREAL_1:7;
B2: a1-c <= a1-0 & a1 <= a2 by A1,XREAL_1:13;
hence f+g+h = integral( AffineMap(d/c,-(d/c)*(a1 - c)), a1-c,a1)
+g+h by INTEGRA5:def 4
.= 1/2*(d/c)*(a1*a1 - (a1-c)*(a1-c)) + (-(d/c)*(a1 - c))*(a1 - (a1-c))
+ g + h by FUZZY_6:47,B2
.= 1/2*(d/c)*(a1*a1 - (a1-c)*(a1-c)) + (-(d/c)*(a1 - c))*(a1 - (a1-c))
+integral( AffineMap(0,d), a1,a2) +h by INTEGRA5:def 4,A1
.= 1/2*(d/c)*(a1*a1 - (a1-c)*(a1-c)) + (-(d/c)*(a1 - c))*(c)
+(1/2 * (0) * ( a2 * a2 - a1 * a1) + d * (a2 - a1)) +h by FUZZY_6:47,A1
.= 1/2*(d/c)*(a1*a1 - (a1-c)*(a1-c)) + (-(d/c)*(a1 - c))*(c) + d*(a2- a1) +
integral( AffineMap(-d/c, (d/c)*(a2 + c)), a2,a2+c) by INTEGRA5:def 4,B1
.= 1/2*(d/c)*(a1*a1 - (a1-c)*(a1-c)) + (-(d/c)*(a1 - c))*(c) + d*(a2- a1) +
(1/2*(-d/c)*((a2+c)*(a2+c) - a2*a2) + ((d/c)*(a2 + c))*((a2+c) - a2) )
by FUZZY_6:47,B1
.= 1/2*(d/c)*(a1*c+c*a1-c*c) + d*(a2- a1)
+ (-(d/c*c)*(a1 - c)) +
1/2*(-d/c)*(a2*c+c*a2+c*c) + (d/c*c)*(a2 + c)
.= 1/2*(d/c)*(a1*c+c*a1-c*c) + d*(a2-a1) + (-(d/c*c)*(a1 - c)) +
(-d/c)*1/2*(a2*c+c*a2+c*c) + d*(a2 + c) by XCMPLX_1:87,A1
.= 1/2*( d/c)*(a1*c+c*a1-c*c) + d*(a2- a1) + (-(d)*(a1 - c)) +
(-d/c)*1/2*(a2*c+c*a2+c*c) + d*(a2 + c) by XCMPLX_1:87,A1
.= d*(a2- a1) + d*c
+ ( d/c)*c*1/2*a1+1/2*( d/c)*c*a1 + (-d)*a1
- (-d)*c +(-(d/c*c))*1/2*c -1/2*( d/c*c)*c
+(-(d/c*c))*1/2*a2+(-(d/c*c))*1/2*a2 + d*a2
.= d*(a2- a1) + d*c
+ ( d/c)*c*1/2*a1+1/2*( d/c)*c*a1 + (-d)*a1
- (-d)*c +(-(d))*1/2*c -1/2*( d/c*c)*c
+(-(d/c*c))*1/2*a2+(-(d/c*c))*1/2*a2 + d*a2 by XCMPLX_1:87,A1
.= d*(a2- a1) + d*c
+ ( d/c*c)*1/2*a1+1/2*( d/c*c)*a1 + (-d)*a1
- (-d)*c +(-(d))*1/2*c -1/2*( d)*c
+(-(d/c*c))*1/2*a2+(-(d/c*c))*1/2*a2 + d*a2 by XCMPLX_1:87,A1
.= d*(a2- a1) + d*c + d*1/2*a1+1/2*( d/c*c)*a1 + (-d)*a1
- (-d)*c +(-(d))*1/2*c -1/2*( d)*c
+(-(d/c*c))*1/2*a2+(-(d/c*c))*1/2*a2 + d*a2 by XCMPLX_1:87,A1
.= d*(a2- a1) + d*c + d*1/2*a1+1/2*d*a1 + (-d)*a1
- (-d)*c +(-(d))*1/2*c -1/2*( d)*c
+(-(d/c*c))*1/2*a2+(-(d/c*c))*1/2*a2 + d*a2 by XCMPLX_1:87,A1
.= d*(a2- a1) + d*c + d*1/2*a1+1/2*d*a1 + (-d)*a1
- (-d)*c +(-(d))*1/2*c -1/2*( d)*c
+(-d)*1/2*a2+(-(d/c*c))*1/2*a2 + d*a2 by XCMPLX_1:87,A1
.= d*(a2- a1) + d*c + d*1/2*a1+1/2*d*a1 + (-d)*a1
- (-d)*c +(-(d))*1/2*c -1/2*( d)*c
+(-d)*1/2*a2+(-d)*1/2*a2 + d*a2 by XCMPLX_1:87,A1
.= d*(a2-a1+c);
end;
theorem Lm29d:
for a1,c,a2,d be Real, f be Function of REAL,REAL st
c > 0 & d > 0 & a1 < a2 &
f | [.a1-c,a2+c.] = AffineMap(d/c,-(d/c)*(a1 - c)) | [.a1-c,a1.] +*
AffineMap(0,d) | [.a1,a2.] +*
AffineMap(-d/c, (d/c)*(a2 + c)) | [.a2,a2+c.]
holds
integral( f,['a1-c,a2+c']) =
integral( AffineMap(d/c,-(d/c)*(a1 - c)), ['a1- c,a1']) +
integral( AffineMap(0,d), ['a1,a2']) +
integral( AffineMap(-d/c, (d/c)*(a2 + c)), ['a2,a2+c'])
proof
let a1,c,a2,d be Real, f be Function of REAL,REAL;
assume that
A1: c > 0 & d > 0 & a1 < a2 and
A2: f | [.a1-c,a2+c.] = AffineMap(d/c,-(d/c)*(a1 - c)) | [.a1- c,a1.] +*
AffineMap(0,d) | [.a1,a2.] +*
AffineMap(-d/c, (d/c)*(a2 + c)) | [.a2,a2+c.];
set g = AffineMap(-d/c, (d/c)*(a2 + c));
reconsider
F = AffineMap(d/c,-(d/c)*(a1 - c)) | ].-infty,a1.[ +*
AffineMap(0,d) | [.a1,+infty.[ as Function of REAL,REAL by FUZZY_5:74;
B4: (d- (-(d/c)*(a1 - c)))/(d/c-0)
= (d+(d/c)*(a1 - c))/(d/c)
.= d/(d/c)+ (a1 - c) by XCMPLX_1:113,A1
.= c + (a1 - c) by XCMPLX_1:54,A1
.= a1; then
C12: F is_integrable_on ['a1-c,a2+c'] & F | ['a1-c,a2+c'] is bounded
by FUZZY_6:29,A1;
B2: a1-c <= a1-0 & a1 <= a2 by A1,XREAL_1:13;
B1: a1-c <= a2-0 & a2+0 <= a2 + c by A1,XREAL_1:13,XREAL_1:7; then
[.(lower_bound ['a1 - c,a2']),(upper_bound ['a1 - c,a2']).]
= ['a1 - c,a2']
& ['a1 - c,a2'] = [.a1 - c,a2.] by INTEGRA5:def 3,INTEGRA1:4; then
D1: upper_bound ['a1 - c,a2'] = a2 & lower_bound ['a1 - c,a2'] = a1-c
by INTEGRA1:5;
a1 in [.a1 - c,a2.] by B2; then
CC: (d- (-(d/c)*(a1 - c)))/(d/c-0) in ['a1 - c,a2'] by B1,INTEGRA5:def 3,B4;
C2: F | [.a1 - c,a2.] = F | ['a1 - c,a2'] by INTEGRA5:def 3,B1
.= (AffineMap(d/c,-(d/c)*(a1 - c)) | [.a1 - c,a1.])
+* (AffineMap(0,d) | [.a1,a2.]) by D1,B4,FUZZY_6:40,CC;
reconsider tr = d (#) TrapezoidalFS (a1-c,a1,a2,a2+c)
as PartFunc of REAL,REAL;
reconsider f1 = f as PartFunc of REAL,REAL;
XX:tr | ['a1-c,a2+c'] = f1 | [.a1-c,a2+c.] by A2,SymTrape,A1;
a1-c < a1-0 & a2+0 < a2+c by A1,XREAL_1:15,XREAL_1:8; then
TrapezoidalFS (a1-c,a1,a2,a2+c) is continuous by FUZNUM_1:32,A1; then
X1: f1 | ['a1-c,a2+c'] is continuous by INTEGRA5:def 3,XX,B1,XXREAL_0:2;
REAL = dom f1 by FUNCT_2:def 1; then
C14: f is_integrable_on ['a1-c,a2+c'] by INTEGRA5:11,X1;
C13c: (-d/c)*a2 + (d/c)*(a2 + c) = (-d/c)*a2 + (d/c)*a2 + (d/c)*c
= d by XCMPLX_1:87,A1;
a2 in [.a1,+infty.[ by XXREAL_1:236,A1; then
a2 in dom (AffineMap(0,d) | [.a1, +infty.[) by FUNCT_2:def 1; then
C13:F.a2 = (AffineMap(0,d) | [.a1 ,+infty.[) .a2 by FUNCT_4:13
.= (AffineMap(0,d) ) .a2 by FUNCT_1:49,XXREAL_1:236,A1
.= (0*a2)+d by FCONT_1:def 4
.= AffineMap(-d/c, (d/c)*(a2 + c)).a2 by FCONT_1:def 4,C13c;
C11: g is_integrable_on ['a1-c,a2+c'] & g | ['a1-c,a2+c'] is bounded
by FUZZY_6:41;
C23: AffineMap(d/c,-(d/c)*(a1 - c)).a1
= (d/c)*a1 + -(d/c)*(a1 - c) by FCONT_1:def 4
.= (d/c)*a1 + -(d/c)*(a1) - -(d/c)*c
.=(0*a1)+d by XCMPLX_1:87,A1
.= AffineMap(0,d).a1 by FCONT_1:def 4;
C22:F is_integrable_on ['a1- c,a2'] by FUZZY_6:29,B4,A1;
C21:AffineMap(d/c,-(d/c)*(a1 - c)) is_integrable_on ['a1-c,a2'] &
AffineMap(d/c,-(d/c)*(a1 - c)) | ['a1-c,a2'] is bounded &
AffineMap(0,d) is_integrable_on ['a1-c,a2'] &
AffineMap(0,d) | ['a1-c,a2'] is bounded by FUZZY_6:41;
thus integral(f,['a1-c,a2+c'])
= integral(F,['a1- c,a2']) + integral(g,['a2,a2+c'])
by FUZZY_6:33,B1,C11,C12,C13,C14,A2,C2
.= (integral(AffineMap(d/c,-(d/c)*(a1 - c)), ['a1-c,a1'])
+ integral(AffineMap(0,d), ['a1,a2']))
+ integral(AffineMap(-d/c, (d/c)*(a2 + c)),['a2,a2+c'])
by FUZZY_6:33,B2,C21,C22,C2,C23;
end;
theorem
for a1,c,a2,d be Real st c > 0 & d > 0 & a1 < a2 holds
centroid ( d (#) TrapezoidalFS (a1-c,a1,a2,a2+c), ['a1-c,a2+c']) =
(a1+a2)/2
proof
let a1,c,a2,d be Real;
assume A1: c > 0 & d > 0 & a1 < a2;
set f = d (#) TrapezoidalFS (a1-c,a1,a2,a2+c);
DAa: a2 - a1 > a1-a1 by XREAL_1:14, A1;
a1-c <= a2-0 & a2+0 <= a2 + c by A1,XREAL_1:13,XREAL_1:7; then
A2: f | [.a1-c,a2+c.] = f | ['a1-c,a2+c'] by INTEGRA5:def 3,XXREAL_0:2
.= AffineMap(d/c,-(d/c)*(a1 - c)) | [.a1-c,a1.] +*
AffineMap(0,d) | [.a1,a2.] +*
AffineMap(-d/c, (d/c)*(a2 + c)) | [.a2,a2+c.] by SymTrape,A1;
thus centroid ( d (#) TrapezoidalFS (a1-c,a1,a2,a2+c), ['a1-c,a2+c'])
= integral((id REAL) (#) f,['a1-c,a2+c'])/integral( f,['a1-c,a2+c'])
by FUZZY_6:def 1
.= (integral((id REAL) (#) AffineMap(d/c,-(d/c)*(a1 - c)), ['a1-c,a1']) +
integral((id REAL) (#) AffineMap(0,d), ['a1,a2']) +
integral((id REAL) (#) AffineMap(-d/c, (d/c)*(a2 + c)), ['a2,a2+c']))
/integral( f,['a1-c,a2+c']) by Lm29n,A1,A2
.= (1/2*d*(c+a2-a1)*(a1+a2))/integral( f,['a1-c,a2+c']) by Lm29n1,A1
.= (1/2*d*(c+a2-a1)*(a1+a2))
/(integral( AffineMap(d/c,-(d/c)*(a1 - c)), ['a1- c,a1']) +
integral( AffineMap(0,d), ['a1,a2']) +
integral( AffineMap(-d/c, (d/c)*(a2 + c)), ['a2,a2+c'])) by Lm29d,A1,A2
.= (1/2*(a1+a2)*(d*(c+a2-a1)))/(d*(a2-a1+c)) by Lm29d1,A1
.=(a1+a2)/2 by XCMPLX_1:89,DAa,A1;
end;