:: Some Properties of Membership Functions Composed of Triangle Functions and
:: Piecewise Linear Functions
:: by Takashi Mitsuishi
::
:: Received June 30, 2021
:: Copyright (c) 2021-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,
MSALIMIT, FUZNUM_1, REAL_1, ORDINAL2, FCONT_1, SQUARE_1, FUNCT_3,
RCOMP_1, NUMPOLY1, JGRAPH_2, FUNCT_4, FUNCT_7, SIN_COS, FUNCT_9, INT_1,
VALUED_1, FDIFF_1, SIN_COS9, FUZZY_5;
notations TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, COMPLEX1, RELAT_1, SQUARE_1,
FUNCT_1, INT_1, XCMPLX_0, XXREAL_0, XREAL_0, VALUED_1, PARTFUN1, FUNCT_2,
FUNCT_3, FUNCT_4, FUNCT_9, FDIFF_1, SIN_COS, RCOMP_1, SIN_COS9, FCONT_1,
FUZZY_1, FUZNUM_1, LFUZZY_1;
constructors COMPLEX1, SEQ_4, RELSET_1, FCONT_1, FUNCT_4, FUZNUM_1, LFUZZY_1,
SIN_COS, SQUARE_1, POWER, FUNCT_9, FDIFF_1, SIN_COS9;
registrations RELSET_1, NUMBERS, XXREAL_0, MEMBERED, XBOOLE_0, VALUED_0,
VALUED_1, FUNCT_2, XREAL_0, ORDINAL1, FCONT_1, XCMPLX_0, RCOMP_1,
SIN_COS, SIN_COS6, SQUARE_1, INT_1, SIN_COS9;
requirements NUMERALS, REAL, SUBSET, ARITHM;
definitions TARSKI, FUZNUM_1;
equalities RCOMP_1, SQUARE_1;
expansions TARSKI, FCONT_1, FUZNUM_1, RELAT_1;
theorems TARSKI, FUNCT_1, ABSVALUE, XBOOLE_0, SIN_COS, COMPLEX1, XXREAL_1,
XREAL_0, FCONT_1, XCMPLX_1, RCOMP_1, FUZNUM_1, FUNCT_9, SIN_COS4, ROLLE,
FDIFF_1, VALUED_1, SIN_COS3, SQUARE_1, XXREAL_0, FUNCT_4, XREAL_1,
FUNCT_2, SIN_COS6, TOPREAL6, SIN_COS7;
schemes FUNCT_2;
begin :: Preliminaries
ABS1:
for x,y be Real st x >= 0 & x <= y holds |.x.| <= |.y.| by TOPREAL6:2;
theorem LeMM01:
for a,b,c,d being Real holds
|. max(c,min(d,a)) - max(c,min(d,b)) .| <= |. a-b .|
proof
let a,b,c,d be Real;
A1: |. max(c,min(d,a)) - max(c,min(d,b)) .|
= |. (c + min(d,a) + |. c - min(d,a).|) / 2 - max(c,min(d,b)) .|
by COMPLEX1:74
.= |. (c + min(d,a) + |. c - min(d,a).|) / 2
- (c + min(d,b) + |. c - min(d,b).|) / 2 .| by COMPLEX1:74
.= |. (min(d,a) - min(d,b)+ |. c - min(d,a).| - |. c - min(d,b).|) / 2 .|
.= |. (((d + a) - |.(d - a).|) / 2 - min(d,b)
+ |. c - min(d,a).| - |. c - min(d,b).|) / 2 .| by COMPLEX1:73
.= |. (((d + a) - |.(d - a).|) / 2 - ((d + b) - |.(d - b).|) / 2
+ |. c - min(d,a).| - |. c - min(d,b).|) / 2 .| by COMPLEX1:73
.= |. (a - b- |.(d - a).| + |.(d - b).|) / 2
+ |. c - min(d,a).| - |. c - min(d,b).| .| / |.2.| by COMPLEX1:67
.= |. ((a - b- |.(d - a).| + |.(d - b).|) / 2)
+ (|. c - min(d,a).| - |. c - min(d,b).|) .| / 2 by COMPLEX1:43;
A2a: |. ((a - b- |.(d - a).| + |.(d - b).|) / 2)
+ (|. c - min(d,a).| - |. c - min(d,b).|) .| / 2
<=(|. ((a - b- |.(d - a).| + |.(d - b).|) / 2).|
+ |.(|. c - min(d,a).| - |. c - min(d,b).|) .|)/ 2
by XREAL_1:72,COMPLEX1:56;
A4: |. ((a - b- |.(d - a).| + |.(d - b).|) / 2).|
=|. a - b- (|.(d - a).| - |.(d - b).|) .|/ |.2.| by COMPLEX1:67
.=|. a - b- (|.(d - a).| - |.(d - b).|) .|/ 2 by COMPLEX1:43;
A3: |. a - b - (|.(d - a).| - |.(d - b).|) .|
<=|. a - b.|+|. (|.(d - a).| - |.(d - b).|) .| by COMPLEX1:57;
|. (|.(d - a).| - |.(d - b).|) .|
<=|. (d - a) - (d - b) .| by COMPLEX1:64; then
|. (|.(d - a).| - |.(d - b).|) .| <= |.b-a .|; then
|. (|.(d - a).| - |.(d - b).|) .|<= |.a -b.| by COMPLEX1:60; then
|.a -b.|+|. (|.(d - a).| - |.(d - b).|) .| <= |.a -b.|+|.a -b.|
by XREAL_1:6; then
|. a - b- (|.(d - a).| - |.(d - b).|) .|
<= |.a -b.|+|.a -b.| by XXREAL_0:2,A3; then
|. ((a - b- |.(d - a).| + |.(d - b).|) / 2).|
<= (|.a -b.|+|.a -b.|)/2 by A4,XREAL_1:72; then
A5: |. ((a - b- |.(d - a).| + |.(d - b).|) / 2).|/2
<= |.a-b.|/2 by XREAL_1:72;
|.(|. c - min(d,a).| - |. c - min(d,b).|) .|
<= |. (c - min(d,a)) - ( c - min(d,b)) .| by COMPLEX1:64; then
|.(|. c - min(d,a).| - |. c - min(d,b).|) .|
<= |. min(d,b)- min(d,a) .|; then
A6a: |.(|. c - min(d,a).| - |. c - min(d,b).|) .|
<= |. min(d,a)- min(d,b) .| by COMPLEX1:60;
|. min(d,a)- min(d,b) .|/2
=|. ((d + a) - |.(d - a).|) / 2- min(d,b) .|/2 by COMPLEX1:73
.=|. ((d + a) - |.(d - a).|) / 2- ((d + b) - |.(d - b).|) / 2 .|/2
by COMPLEX1:73
.=|.( ((d + a) - |.(d - a).|) - ((d + b) - |.(d - b).|) )/ 2 .|/2
.=(|.( a - |.(d - a).| - b + |.(d - b).| ) .| / |.2.|)/2 by COMPLEX1:67
.=(|.( a - |.(d - a).| - b + |.(d - b).| ) .| / 2)/2 by COMPLEX1:43
.=|. a - b- (|.(d - a).| - |.(d - b).|) .| / 4; then
A8: |.(|. c - min(d,a).| - |. c - min(d,b).|) .|/2
<=|. a - b- (|.(d - a).| - |.(d - b).|) .| / 4 by A6a,XREAL_1:72;
A7: |. a - b- (|.(d - a).| - |.(d - b).|) .|
<=|. a - b .| + |.|.(d - a).| - |.(d - b).|.| by COMPLEX1:57;
|.|.(d - a).| - |.(d - b).|.|
<= |.(d - a) - (d - b).| by COMPLEX1:64; then
|.|.(d - a).| - |.(d - b).|.| <= |.b-a.|; then
|.|.(d - a).| - |.(d - b).|.| <= |. a-b .| by COMPLEX1:60; then
|. a - b .|+|.|.(d - a).| - |.(d - b).|.|
<= |. a - b .|+|. a-b .| by XREAL_1:6; then
|. a - b- (|.(d - a).| - |.(d - b).|) .|
<=|. a-b .|+|. a-b .| by XXREAL_0:2,A7; then
|. a - b- (|.(d - a).| - |.(d - b).|) .|/4
<=(|. a-b .|+|. a-b .|)/4 by XREAL_1:72; then
|.(|. c - min(d,a).| - |. c - min(d,b).|) .|/2
<=(|. a-b .|+|. a-b .|)/4 by A8,XXREAL_0:2; then
|. ((a - b- |.(d - a).| + |.(d - b).|) / 2).|/2
+|.(|. c - min(d,a).| - |. c - min(d,b).|) .|/2
<= |.a-b.|/2 +(|. a-b .|+|. a-b .|)/4 by XREAL_1:7,A5;
hence thesis by A2a,A1,XXREAL_0:2;
end;
theorem LmSin1:
for x being Real holds
|. sin x .| <= |.x.|
proof
let x be Real;
per cases;
suppose A1: x>0;
set X = [.0,(0 + x).];
reconsider X as set;
AA: (sin | X) is continuous PartFunc of REAL,REAL;
A4: sin is_differentiable_on ].0,(0 + x).[ by FDIFF_1:26,SIN_COS:68;
[.0,(0 + x).] c=REAL; then
[.0,(0 + x).] c= dom sin by FUNCT_2:def 1; then
consider s being Real such that 0 < s and s < 1 and
A2:sin . (0 + x) = (sin . 0) + (x * (diff (sin,(0 + (s * x)))))
by A1,ROLLE:4,AA,A4;
|. cos(s * x).|<=1 by SIN_COS:27; then
|. cos.(s * x).|<=1 & 0<=|. x .| by COMPLEX1:46,SIN_COS:def 19; then
A6: |. x .|*|. cos.(s * x).|<=|. x .|*1 by XREAL_1:64;
|.sin x.| = |. sin.x .| by SIN_COS:def 17
.=|. x * cos.(s * x).| by SIN_COS:64,SIN_COS:30,A2
.=|. x .|*|. cos.(s * x).| by COMPLEX1:65;
hence thesis by A6;
end;
suppose B1a:x<0;
set X1 = [.0,(0 + (-x)).];
reconsider X1 as set;
B3a: (sin | X1) is continuous PartFunc of REAL,REAL;
B4: sin is_differentiable_on ].0,(0 + (-x)).[ by FDIFF_1:26,SIN_COS:68;
[.0,(0 + (-x)).] c=REAL; then
[.0,(0 + (-x)).] c= dom sin by FUNCT_2:def 1; then
consider s being Real such that 0 < s and s < 1 and
B2:sin . (0 + (-x)) = (sin . 0) + ((-x) * (diff (sin,(0 + (s * (-x))))))
by B1a,ROLLE:4,B3a,B4;
|. cos(s * (-x)).|<=1 by SIN_COS:27; then
|. cos.(s * (-x)).|<=1 & 0<=|. (-x) .| by COMPLEX1:46,SIN_COS:def 19; then
BB: |. (-x) .|*|. cos.(s * (-x)).|<=|. (-x) .|*1 by XREAL_1:64;
|.sin x.| = |. sin.x .| by SIN_COS:def 17
.= |. -sin.x .| by COMPLEX1:52
.=|.0+ (-x) * (diff (sin,(0 + (s * (-x))))).| by SIN_COS:30,B2
.=|. (-x) * cos.(s * (-x)).| by SIN_COS:64
.=|. (-x) .|*|. cos.(s * (-x)).| by COMPLEX1:65;
hence thesis by BB,COMPLEX1:52;
end;
suppose Z1:x=0; then
|.sin x.| = |.0.| by SIN_COS:31;
hence thesis by Z1;
end;
end;
theorem LmSin2:
for x,y being Real holds |. sin x - sin y .| <= |.x-y.|
proof
let x,y be Real;
A2: |. sin x - sin y .| = |.2 * (cos ((x + y) / 2) * sin ((x - y) / 2)).|
by SIN_COS4:16
.= |.2.| * |.(cos ((x + y) / 2) * sin ((x - y) / 2)).|
by COMPLEX1:65
.=|. 2 .|* (|. (cos ((x + y) / 2)) .| * |.(sin ((x - y) / 2)).|)
by COMPLEX1:65
.=|. 2 .|* |. (cos ((x + y) / 2)) .| * |.(sin ((x - y) / 2)).|
.= 2 * |. (cos ((x + y) / 2)) .| * |.(sin ((x - y) / 2)).| by COMPLEX1:43;
0<=|. (cos ((x + y) / 2)) .| & |.cos ((x + y) / 2).| <= 1
& 0<=|.(x - y) / 2.|
& |.(sin ((x - y) / 2)).| <= |.(x - y) / 2.| by SIN_COS:27,LmSin1,COMPLEX1:46;
then
|.(sin ((x - y) / 2)).|*|. cos((x + y)/2) .|
<= |.(x - y) / 2.|*|. cos((x + y)/2) .|
& |. cos((x + y)/2) .|*|.(x - y) / 2.|<=1*|.(x - y) / 2.| by XREAL_1:64; then
|. (cos ((x + y) / 2)) .| * |.(sin ((x - y) / 2)).|<=1*|.(x - y) / 2.|
by XXREAL_0:2; then
AA: (|. (cos ((x + y) / 2)) .| * |.(sin ((x - y) / 2)).|)*2
<=(1*|.(x - y) / 2.|)*2 by XREAL_1:64;
(1*|.(x - y) / 2.|)*2 = (|.(x - y).|/|.2.|)*2 by COMPLEX1:67
.=(|.(x - y).|/2)*2 by COMPLEX1:43
.=|.(x - y).|;
hence thesis by AA,A2;
end;
EXpReq11:
for x be Real st exp_R x = 1 holds x = 0 by SIN_COS7:29;
theorem EXpReq12:
for x be Real st exp x = 1 holds x = 0
proof
let x be Real;
assume exp x = 1;
then
exp_R x = 1 by SIN_COS:49;
hence thesis by EXpReq11;
end;
theorem asymTT2:
for a,b,p,q be Real st
a > 0 & p > 0 & (-b)/a < q/p
holds (-b)/a < (q-b)/(a+p) & (q-b)/(a+p) < q/p & (a*q+b*p)/(a+p) > 0
proof
let a,b,p,q be Real;
assume A1:a > 0;
assume A2: p > 0;
assume (-b)/a < q/p; then
A4a: (-b)/a -(-b)/a < q/p -(-b)/a by XREAL_1:9;
q/p - (-b)/a = (q*a-(-b)*p)/(p*a) by A1,A2,XCMPLX_1:130
.=(q*a+b*p)/(p*a); then
A5: a*q+b*p>0 by A4a,A1,A2;
(q-b)/(a+p)-((-b)/a)=
(((q-b) * a) - ((-b) *(a+p))) / ((a+p) * a) by XCMPLX_1:130,A1,A2::A12,
.=(a*q+b*p)/((a+p)*a); then
A6: (q-b)/(a+p)-((-b)/a)+((-b)/a) > 0+((-b)/a) by XREAL_1:6,A2,A1,A5;
(q-b)/(a+p) - q/p
= (((q-b) * p) - (q *(a+p))) / ((a+p) * p) by A1,XCMPLX_1:130,A2
.=(-(a*q+b*p))/((a+p)*p);
then
(q-b)/(a+p)-q/p + q/p < 0+q/p by XREAL_1:6,A1,A2,A5;
hence thesis by A6,A5,A1,A2;
end;
theorem asymTT3:
for a,b,p,q,s be Real st
a > 0 & p > 0 & (s-b)/a = (s-q)/(-p)
holds (s-b)/a= (q-b)/(a+p) & (s-q)/(-p) = (q-b)/(a+p)
proof
let a,b,p,q,s be Real;
assume AA:a > 0;
assume PP: p > 0;
assume A4: (s-b)/a = (s-q)/(-p); then
(s-b)*(-p) = (s-q)/(-p)*a*(-p) by XCMPLX_1:87,AA; then
(s-b)*(-p) = (s-q)/(-p)*(-p)*a; then
(-p)*s-b*(-p) = (s-q)*a by XCMPLX_1:87,PP; then
(a*q + b*p)/(a+p) = s*(a+p)/(a+p); then
s-b = (a*q + b*p)/(a+p)-b by XCMPLX_1:89,AA,PP
.= (a*q + b*p)/(a+p)-b*((a+p)/(a+p)) by XCMPLX_1:88,AA,PP
.= (a*q + b*p)/(a+p)-b*(a+p)/(a+p) by XCMPLX_1:74
.= ( (a*q + b*p)-(b*a+b*p) )/(a+p) by XCMPLX_1:120
.= a*(q-b)/(a+p); then
(s-b)/a = a*((q-b)/(a+p))/a by XCMPLX_1:74
.=(q-b)/(a+p) by XCMPLX_1:89,AA;
hence thesis by A4;
end;
theorem asymTT4:
for a,b,p,q,s be Real st
a > 0 & p > 0 & (s-b)/a < (s-q)/(-p) holds
(s-b)/a < (q-b)/(a+p) & (q-b)/(a+p) < (s-q)/(-p)
proof
let a,b,p,q,s be Real;
assume AA: a > 0;
assume PP: p > 0;
assume (s-b)/a < (s-q)/(-p);then
(s-b)/a*a < (s-q)/(-p)*a by XREAL_1:68,AA; then
a/a*(s-b) < (s-q)/(-p)*a by XCMPLX_1:75; then
1*(s-b) < (s-q)/(-p)*a by XCMPLX_1:60,AA; then
(s-b)*(-p) > (s-q)/(-p)*a*(-p) by XREAL_1:69,PP; then
(s-b)*(-p) > (s-q)/(-p)*(-p)*a; then
(-p)*s-b*(-p) > (s-q)*a by XCMPLX_1:87,PP;then
(-p)*s-b*(-p)+p*s > s*a-q*a+p*s by XREAL_1:6;then
-b*(-p)+a*q > s*a-q*a+p*s +a*q by XREAL_1:6;then
(b*p+a*q)/(a+p) > s*(a+p)/(a+p) by XREAL_1:74,AA,PP; then
A3:(b*p+a*q)/(a+p) > s by XCMPLX_1:89,AA,PP;
(b*p+a*q)/(a+p)-b = ((b*p+a*q) - b*(a+p))/(a+p) by XCMPLX_1:126,AA,PP
.=(a*(q - b))/(a+p); then
(a*(q - b))/(a+p) > s-b by A3,XREAL_1:9; then
a*(q - b)/(a+p)/a > (s-b)/a by XREAL_1:74,AA; then
A4a:a*((q - b)/(a+p))/a > (s-b)/a by XCMPLX_1:74;
(b*p+a*q)/(a+p)-q= ((b*p+a*q) - q*(a+p))/(a+p) by XCMPLX_1:126,AA,PP
.=(-p)*(q-b)/(a+p); then
(-p)*(q-b)/(a+p) > s-q by XREAL_1:9,A3; then
(-p)*(q-b)/(a+p)/(-p) < (s-q)/(-p) by XREAL_1:75,PP;then
(-p)*((q-b)/(a+p))/(-p) < (s-q)/(-p) by XCMPLX_1:74;
hence thesis by PP,A4a,AA,XCMPLX_1:89;
end;
begin :: The set of membership functions
definition
let X be non empty set;
func Membership_Funcs (X) -> set means :Def1:
for f being object holds
f in it iff f is Membership_Func of X;
existence
proof
set S = the set of all f where f is Membership_Func of X;
take S;
thus for x being object holds
x in S iff x is Membership_Func of X
proof
let x be object;
hereby assume x in S; then
ex f be Membership_Func of X st x=f;
hence x is Membership_Func of X;
end;
assume x is Membership_Func of X;
hence x in S;
end;
end;
uniqueness
proof
let F1,F2 be set;
assume that
E1:for x being object holds
x in F1 iff x is Membership_Func of X and
E2:for x being object holds
x in F2 iff x is Membership_Func of X;
for x being object holds x in F1 iff x in F2
proof
let x be object;
x in F1 iff x is Membership_Func of X by E1;
hence x in F1 iff x in F2 by E2;
end;
hence F1=F2 by TARSKI:2;
end;
end;
theorem LM1:
for X be non empty set, x be object
st x in Membership_Funcs (X) holds
ex f be Membership_Func of X st x = f & dom f = X
proof
let X be non empty set,
x be object;
assume x in Membership_Funcs (X); then
reconsider f = x as Membership_Func of X by Def1;
take f;
thus x=f;
thus dom f = X by FUNCT_2:def 1;
end;
theorem
Membership_Funcs (REAL)
= {f where f is Function of REAL,REAL : f is FuzzySet of REAL}
proof
A1:Membership_Funcs (REAL)
c={f where f is Function of REAL,REAL : f is FuzzySet of REAL}
proof
let f be object;
assume f in Membership_Funcs (REAL);
then ex f0 being Membership_Func of REAL st f0=f & dom f0 =REAL by LM1;
hence thesis;
end;
{f where f is Function of REAL,REAL : f is FuzzySet of REAL}
c=Membership_Funcs (REAL)
proof
let f be object;
assume f in {f where f is Function of REAL,REAL : f is FuzzySet of REAL};
then
consider f1 being Function of REAL,REAL such that
B1:f=f1 and B2: f1 is FuzzySet of REAL;
thus thesis by B1,B2,Def1;
end;
hence thesis by XBOOLE_0:def 10,A1;
end;
:::: characteristic function (indicator function)
theorem
for A,X be non empty set holds
{chi (A,X)} c= Membership_Funcs (X)
proof
let A,X be non empty set;
let x be object;
assume x in {chi(A,X)};
then x=chi(A,X) by TARSKI:def 1;
hence thesis by Def1;
end;
theorem
{chi([.a,b.],REAL) where a,b is Real : a <= b}
c= Membership_Funcs (REAL)
proof
let x be object;
assume x in {chi([.a,b.],REAL) where a,b is Real : a <= b};
then ex a,b be Real st x=chi([.a,b.],REAL) & a <= b;
hence thesis by Def1;
end;
theorem
{chi(A,REAL) where A is Subset of REAL : A c= REAL}
c= Membership_Funcs (REAL)
proof
let x be object;
assume x in {chi(A,REAL) where A is Subset of REAL : A c= REAL};
then ex A be Subset of REAL st x=chi(A,REAL) & A c= REAL;
hence thesis by Def1;
end;
theorem
{f where f is FuzzySet of REAL : ex A be Subset of REAL st f=chi(A,REAL) }
c= Membership_Funcs (REAL)
proof
let x be object;
assume x in {f where f is FuzzySet of REAL :
ex A be Subset of REAL st f=chi(A,REAL)};
then consider f0 be FuzzySet of REAL such that
A1: x=f0 and ex A be Subset of REAL st f0=chi(A,REAL);
thus thesis by Def1,A1;
end;
:::: membership functions using min (max) operation
theorem MMcon1:
for f,g be Function of REAL,REAL, a being Real st
g is continuous & for x be Real holds f.x = min(a, g.x)
holds f is continuous
proof
let f,g be Function of REAL,REAL;
let a be Real;
assume A1a: g is continuous;
assume A0:for x be Real holds f.x= min(a, g.x);
reconsider f as PartFunc of REAL,REAL;
for x0 being Real st x0 in dom f holds f is_continuous_in x0
proof
let x0 be Real;
assume A2: x0 in dom f;
A3a: dom f = REAL & dom g = REAL by FUNCT_2:def 1;
for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Real st x1 in dom f & |.(x1 - x0).| < s holds
|.((f . x1) - (f . x0)).| < r ) )
proof
let r being Real;
assume A4:0 < r;
consider s being Real such that
S1: 0 < s and
S2: for x1 being Real st x1 in dom g & |.(x1 - x0).| < s holds
|.((g . x1) - (g . x0)).| < r by A3a,FCONT_1:3,A1a,A2,A4;
take s;
for x1 being Real st x1 in dom f & |.(x1 - x0).| < s holds
|.((f . x1) - (f . x0)).| < r
proof
let x1 be Real;
assume S6: x1 in dom f;
S8a:dom f = REAL & dom g = REAL by FUNCT_2:def 1;
assume S7: |.(x1 - x0).| < s;
S5: 2*|.((f . x1) - (f . x0)).|
=2*|.((f . x1) - min(a, g.x0)).| by A0
.=2*|.min(a, g.x1) - min(a, g.x0).| by A0
.=2*|.min(a, g.x1) - ((a + g.x0) - |.a - g.x0.|) / 2.| by COMPLEX1:73
.=2*|.((a + g.x1) - |.a - g.x1.|) / 2 - ((a + g.x0) - |.a - g.x0.|) / 2.|
by COMPLEX1:73
.=2*(|.(((a + g.x1) - |.a - g.x1.|) - ((a + g.x0) - |.a - g.x0.|)) / 2 .| )
.=2*(|.((a + g.x1) - |.a - g.x1.|)-((a + g.x0) - |.a - g.x0.|) .| / |.2.|)
by COMPLEX1:67
.=2*(|.((a + g.x1) - |.a - g.x1.|) - ((a + g.x0) - |.a - g.x0.|) .| / 2)
by COMPLEX1:43
.=|. g.x1 - g.x0 + (|.a - g.x0.|- |.a - g.x1.|) .|;
|.((g . x1) - (g . x0)).| < r by S2,S7,S8a,S6; then
S4: |.((g . x1) - (g . x0)).| +|.((g . x1) - (g . x0)).| < r+ r
by XREAL_1:8;
S3: |. g.x1 - g.x0 + (|.a - g.x0.|- |.a - g.x1.|) .|
<= (|. g.x1 - g.x0 .| + |. (|.a - g.x0.|- |.a - g.x1.|) .|)
by COMPLEX1:56;
|. (|.a - g.x0.|- |.a - g.x1.|) .| <= |. (a - g.x0)- (a - g.x1) .|
by COMPLEX1:64; then
(|. g.x1 - g.x0 .| + |. (|.a - g.x0.|- |.a - g.x1.|) .|)
<= |. g.x1 - g.x0 .| + |. - g.x0 + g.x1 .| by XREAL_1:7;
then
(|. g.x1 - g.x0 .| + |. (|.a - g.x0.|- |.a - g.x1.|) .|) < 2*r
by S4,XXREAL_0:2;
then
2*|.((f . x1) - (f . x0)).| < 2*r by S5,S3,XXREAL_0:2;
then
2*|.((f . x1) - (f . x0)).|/2 < 2*r/2 by XREAL_1:74;
hence |.((f . x1) - (f . x0)).| < r;
end;
hence thesis by S1;
end;
hence f is_continuous_in x0 by FCONT_1:3;
end;
hence thesis;
end;
theorem ::: TODO just: min (f,g) is continuous
for F,f,g be Function of REAL,REAL st
f is continuous & g is continuous &
for x be Real holds F.x = min(f.x, g.x)
holds
F is continuous
proof
let F,f,g be Function of REAL,REAL;
assume B1a: f is continuous;
assume A1a:g is continuous;
assume A0:for x be Real holds F.x= min(f.x, g.x);
reconsider F as PartFunc of REAL,REAL;
for x0 being Real st x0 in dom F holds F is_continuous_in x0
proof
let x0 be Real;
assume A2: x0 in dom F;
B0a: dom F = REAL & dom g = REAL & dom f = REAL by FUNCT_2:def 1;
for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Real st x1 in dom F & |.(x1 - x0).| < s holds
|.((F . x1) - (F . x0)).| < r ) )
proof
let r be Real;
assume A4a: 0 < r;
consider sg being Real such that
S1: 0 < sg and
S2: for x1 being Real st x1 in dom g & |.(x1 - x0).| < sg holds
|.((g . x1) - (g . x0)).| < r/2 by A4a,FCONT_1:3,A1a,A2,B0a;
consider sf being Real such that
P1: 0 < sf and
P2: for x1 being Real st x1 in dom f & |.(x1 - x0).| < sf holds
|.((f . x1) - (f . x0)).| < r/2 by FCONT_1:3,B0a,B1a,A2,A4a;
reconsider s = min(sf,sg) as Real;
P8: s <= sg & s <= sf by XXREAL_0:17;
take s;
for x1 being Real st x1 in dom F & |.(x1 - x0).| < s holds
|.((F . x1) - (F . x0)).| < r
proof
let x1 be Real;
assume S6: x1 in dom F;
S8a: dom F = REAL & dom g = REAL & dom f = REAL by FUNCT_2:def 1;
assume |.(x1 - x0).| < s; then
|.(x1 - x0).| < sg & |.(x1 - x0).| < sf by P8,XXREAL_0:2; then
|.((g . x1) - (g . x0)).| < r/2 & |.((f . x1) - (f . x0)).| < r/2
by S8a,S2,P2,S6; then
|.((g . x1) - (g . x0)).| + |.((f . x1) - (f . x0)).| < r/2+r/2
by XREAL_1:8; then
SS: (|.((g . x1) - (g . x0)).| + |.((f . x1) - (f . x0)).|)
+(|.((g . x1) - (g . x0)).| + |.((f . x1) - (f . x0)).|)
< (r/2+r/2)+(r/2+r/2) by XREAL_1:8;
T3: |.((F . x1) - (F . x0)).|
=|. min(f.x1, g.x1) - F.x0 .| by A0
.=|.min(f.x1, g.x1) - min(f.x0, g.x0).| by A0
.=|.min(f.x1, g.x1) - ((f.x0 + g.x0) - |.f.x0 - g.x0.|) / 2.|
by COMPLEX1:73
.=|.((f.x1 + g.x1) - |.f.x1 - g.x1.|) / 2
- ((f.x0 + g.x0) - |.f.x0 - g.x0.|) / 2.| by COMPLEX1:73
.=|.((f.x1 - f.x0) + (g.x1 - g.x0)
+ (|.f.x0 - g.x0.|- |.f.x1 - g.x1.|)) / 2.|
.=|.((f.x1 - f.x0) + (g.x1 - g.x0)
+ (|.f.x0 - g.x0.|- |.f.x1 - g.x1.|)).| / |.2.| by COMPLEX1:67
.=|.(f.x1 - f.x0) + (g.x1 - g.x0)
+ (|.f.x0 - g.x0.|- |.f.x1 - g.x1.|).| / 2 by COMPLEX1:43;
T1: |.(f.x1 - f.x0) + (g.x1 - g.x0)
+ (|.f.x0 - g.x0.|- |.f.x1 - g.x1.|).|
<= |.(f.x1 - f.x0) + (g.x1 - g.x0) .|
+ |. (|.f.x0 - g.x0.| - |.f.x1 - g.x1.|).| by COMPLEX1:56;
|.(f.x1 - f.x0) + (g.x1 - g.x0) .|
+ |. (|.f.x0 - g.x0.| - |.f.x1 - g.x1.|).|
<= |.(f.x1 - f.x0) .|+|. (g.x1 - g.x0) .|
+ |. (|.f.x0 - g.x0.| - |.f.x1 - g.x1.|).| by XREAL_1:6,COMPLEX1:56;
then
T2: |.(f.x1 - f.x0) + (g.x1 - g.x0)
+ (|.f.x0 - g.x0.|- |.f.x1 - g.x1.|).|
<= |.(f.x1 - f.x0) .|+|. (g.x1 - g.x0) .|
+ |. (|.f.x0 - g.x0.| - |.f.x1 - g.x1.|).| by XXREAL_0:2,T1;
|. (|.f.x0 - g.x0.| - |.f.x1 - g.x1.|).|
<=|. (f.x0 - g.x0) - (f.x1 - g.x1).| &
|. (f.x0 - g.x0) - (f.x1 - g.x1).|=|. (g.x1-g.x0) - (f.x1-f.x0).| &
|. ( g.x1- g.x0) - (f.x1 - f.x0).|
<= |. g.x1-g.x0 .|+|.(f.x1 - f.x0).| by COMPLEX1:57,COMPLEX1:64; then
|. (|.f.x0 - g.x0.| - |.f.x1 - g.x1.|).|
<=|.(f.x1 - f.x0).|+|. ( g.x1- g.x0) .| by XXREAL_0:2; then
|. (|.f.x0 - g.x0.| - |.f.x1 - g.x1.|).|+
(|.(f.x1 - f.x0) .|+|. (g.x1 - g.x0) .|)
<=|.(f.x1 - f.x0).|+|. ( g.x1- g.x0) .|+
(|.(f.x1 - f.x0) .|+|. (g.x1 - g.x0) .|) by XREAL_1:6; then
|.(f.x1 - f.x0) + (g.x1 - g.x0) + (|.f.x0 - g.x0.|- |.f.x1 -g.x1.|).|
<= (|.(f.x1 - f.x0) .|+|. (g.x1 - g.x0) .|)+
|.(f.x1 - f.x0).|+|. ( g.x1- g.x0) .| by XXREAL_0:2,T2; then
|.(f.x1 - f.x0) + (g.x1 - g.x0) + (|.f.x0 - g.x0.|- |.f.x1- g.x1.|).|
< (r/2+r/2)+(r/2+r/2) by XXREAL_0:2,SS; then
|.(f.x1 - f.x0) + (g.x1-g.x0) + (|.f.x0-g.x0.|-|.f.x1- g.x1.|).|/2
< (r/2+r/2+r/2+r/2)/2 by XREAL_1:74;
hence |.((F . x1) - (F . x0)).| < r by T3;
end;
hence thesis by XXREAL_0:21,S1,P1;
end;
hence F is_continuous_in x0 by FCONT_1:3;
end;
hence thesis;
end;
theorem MMcon2: ::: should be restated in terms of lambda operators
for F,f,g be Function of REAL,REAL st
f is continuous & g is continuous &
for x be Real holds F.x = max(f.x, g.x)
holds
F is continuous
proof
let F,f,g be Function of REAL,REAL;
assume B1a: f is continuous;
assume A1a:g is continuous;
assume A0:for x be Real holds F.x= max(f.x, g.x);
reconsider F as PartFunc of REAL,REAL;
for x0 being Real st x0 in dom F holds F is_continuous_in x0
proof
let x0 be Real;
assume A2: x0 in dom F;
B0a: dom F = REAL & dom g = REAL & dom f = REAL by FUNCT_2:def 1;
for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Real st x1 in dom F & |.(x1 - x0).| < s holds
|.((F . x1) - (F . x0)).| < r ) )
proof
let r be Real;
assume A4a: 0 < r;
consider sg being Real such that
S1: 0 < sg and
S2: for x1 being Real st x1 in dom g & |.(x1 - x0).| < sg holds
|.((g . x1) - (g . x0)).| < r/2 by FCONT_1:3,A1a,A2,B0a,A4a;
consider sf being Real such that
P1: 0 < sf and
P2: for x1 being Real st x1 in dom f & |.(x1 - x0).| < sf holds
|.((f . x1) - (f . x0)).| < r/2 by FCONT_1:3,B0a,B1a,A2,A4a;
reconsider s = min(sf,sg) as Real;
P8: s <= sg & s <= sf by XXREAL_0:17;
take s;
for x1 being Real st x1 in dom F & |.(x1 - x0).| < s holds
|.((F . x1) - (F . x0)).| < r
proof
let x1 being Real;
assume S6: x1 in dom F;
S8a: dom F = REAL & dom g = REAL & dom f = REAL by FUNCT_2:def 1;
assume |.(x1 - x0).| < s;
then
|.(x1 - x0).| < sg & |.(x1 - x0).| < sf by P8,XXREAL_0:2;
then
|.((g . x1) - (g . x0)).| < r/2 & |.((f . x1) - (f . x0)).| < r/2
by S2,P2,S8a,S6; then
|.((g . x1) - (g . x0)).| + |.((f . x1) - (f . x0)).| < r/2+r/2
by XREAL_1:8; then
SS: (|.((g . x1) - (g . x0)).| + |.((f . x1) - (f . x0)).|)
+(|.((g . x1) - (g . x0)).| + |.((f . x1) - (f . x0)).|)
< (r/2+r/2)+(r/2+r/2) by XREAL_1:8;
T3: |.((F . x1) - (F . x0)).|
=|. max(f.x1, g.x1) - F.x0 .| by A0
.=|.max(f.x1, g.x1) - max(f.x0, g.x0).| by A0
.=|.max(f.x1, g.x1) - ((f.x0 + g.x0) + |.f.x0 - g.x0.|) / 2.|
by COMPLEX1:74
.=|.((f.x1 + g.x1) + |.f.x1 - g.x1.|) / 2
- ((f.x0 + g.x0) + |.f.x0 - g.x0.|) / 2.| by COMPLEX1:74
.=|.((f.x1 - f.x0) + (g.x1 - g.x0)
- |.f.x0 - g.x0.|+ |.f.x1 - g.x1.|) / 2.|
.=|.(f.x1 - f.x0) + (g.x1 - g.x0)
- |.f.x0 - g.x0.|+ |.f.x1 - g.x1.|.| / |.2.| by COMPLEX1:67
.=|.(f.x1 - f.x0) + (g.x1 - g.x0)
- |.f.x0 - g.x0.|+ |.f.x1 - g.x1.| .| / 2 by COMPLEX1:43;
T1: |.(f.x1 - f.x0) + (g.x1 - g.x0)
+ (- |.f.x0 - g.x0.|+ |.f.x1 - g.x1.|).|
<= |.(f.x1 - f.x0) + (g.x1 - g.x0) .|
+ |. - |.f.x0 - g.x0.|+ |.f.x1 - g.x1.|.| by COMPLEX1:56;
|.(f.x1 - f.x0) + (g.x1 - g.x0) .|
+ |. (- |.f.x0 - g.x0.|+ |.f.x1 - g.x1.|).|
<= |.(f.x1 - f.x0) .|+|. (g.x1 - g.x0) .|
+ |. (- |.f.x0 - g.x0.|+ |.f.x1 - g.x1.|).| by XREAL_1:6,COMPLEX1:56;
then
T2: |.(f.x1 - f.x0) + (g.x1 - g.x0)
+ ((- |.f.x0 - g.x0.|+ |.f.x1 - g.x1.|)).|
<= |.(f.x1 - f.x0) .|+|. (g.x1 - g.x0) .|
+ |. (- |.f.x0 - g.x0.|+ |.f.x1 - g.x1.|).| by XXREAL_0:2,T1;
|.(|.f.x0 - g.x0.| - |.f.x1 - g.x1.|).|
=|. |.f.x1 - g.x1.|-|.f.x0 - g.x0.| .| &
|. (|.f.x0 - g.x0.| - |.f.x1 - g.x1.|).|
<=|. (f.x0 - g.x0) - (f.x1 - g.x1).| &
|. (f.x0 - g.x0) - (f.x1 - g.x1).|=|. (g.x1-g.x0) - (f.x1-f.x0).| &
|. ( g.x1- g.x0) - (f.x1 - f.x0).|
<= |. g.x1-g.x0 .|+|.(f.x1 - f.x0).|
by COMPLEX1:57,COMPLEX1:64,COMPLEX1:60; then
|. |.f.x1 - g.x1.|-|.f.x0 - g.x0.| .|
<=|.(f.x1 - f.x0).|+|. ( g.x1- g.x0) .| by XXREAL_0:2; then
|. |.f.x1 - g.x1.|-|.f.x0 - g.x0.| .|+
(|.(f.x1 - f.x0) .|+|. (g.x1 - g.x0) .|)
<=|.(f.x1 - f.x0).|+|. ( g.x1- g.x0) .|+
(|.(f.x1 - f.x0) .|+|. (g.x1 - g.x0) .|) by XREAL_1:6; then
|.(f.x1 - f.x0) + (g.x1 - g.x0) + (- |.f.x0 - g.x0.|+ |.f.x1 - g.x1.|).|
<= (|.(f.x1 - f.x0) .|+|. (g.x1 - g.x0) .|)+
|.(f.x1 - f.x0).|+|. ( g.x1- g.x0) .| by XXREAL_0:2,T2; then
|.(f.x1 - f.x0) + (g.x1 - g.x0) + (- |.f.x0 - g.x0.|+ |.f.x1 - g.x1.|).|
< (r/2+r/2)+(r/2+r/2) by XXREAL_0:2,SS; then
|.(f.x1 - f.x0) + (g.x1-g.x0) + (- |.f.x0 - g.x0.|+ |.f.x1 - g.x1.|).|/2
< (r/2+r/2+r/2+r/2)/2 by XREAL_1:74;
hence |.((F . x1) - (F . x0)).| < r by T3;
end;
hence thesis by XXREAL_0:21,S1,P1;
end;
hence F is_continuous_in x0 by FCONT_1:3;
end;
hence thesis;
end;
theorem MMcon3:
for f,g be Function of REAL,REAL,
a being Real st
g is continuous & for x be Real holds f.x= max(a, g.x)
holds f is continuous
proof
let f,g be Function of REAL,REAL;
let a be Real;
assume A3: g is continuous;
assume A0:for x be Real holds f.x= max(a, g.x);
consider h being Function of REAL,REAL such that
A2: h = AffineMap (0,a);
for x be Real holds f.x= max(h.x, g.x)
proof
let x be Real;
f.x=max(0*x+a, g.x) by A0
.=max(AffineMap (0,a).x, g.x) by FCONT_1:def 4;
hence thesis by A2;
end;
hence thesis by MMcon2,A3,A2;
end;
theorem MMcon4:
for f,g be Function of REAL,REAL, a,b being Real st
g is continuous & for x be Real holds f.x= max(a,min(b, g.x))
holds f is continuous
proof
let f,g be Function of REAL,REAL;
let a,b being Real;
assume A1: g is continuous;
assume A2: for x be Real holds f.x= max(a,min(b, g.x));
deffunc H1(Element of REAL) = In(min(b,g.$1),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 h.x= min(b, g.x)
proof
let x being Real;
reconsider x as Element of REAL by XREAL_0:def 1;
h.x = In(min(b,g.x),REAL) by A3
.= min(b, g.x);
hence thesis;
end;
then
A4: h is continuous by MMcon1,A1;
for x be Real holds f.x= max(a,h.x)
proof
let x be Real;
thus f.x= max(a,min(b, g.x)) by A2
.= max(a,h.x) by A5;
end;
hence thesis by MMcon3,A4;
end;
theorem
for f,g be Function of REAL,REAL st
g is continuous & for x be Real holds f.x= max(0,min(1, g.x))
holds f is continuous by MMcon4;
theorem LmSin3:
for f be Function of REAL,REAL, a,b be Real st
for th be Real holds f.th = 1/2*sin(a*th+b)+1/2
holds f is continuous
proof
let f be Function of REAL,REAL;
let a,b be Real;
assume A3: for th be Real holds f.th = 1/2*sin(a*th+b)+1/2;
reconsider f as PartFunc of REAL,REAL;
for x0 being Real st x0 in dom f holds f is_continuous_in x0
proof
let x0 be Real;
for N1 being Neighbourhood of f . x0
ex N being Neighbourhood of x0 st
for x1 being Real st x1 in dom f & x1 in N holds f . x1 in N1
proof
let N1 be Neighbourhood of f.x0;
consider g being Real such that
A1: 0 < g and
A2: N1 = ].(f.x0 - g),(f.x0 + g).[ by RCOMP_1:def 6;
ex N being Neighbourhood of x0 st
for x1 being Real st x1 in dom f & x1 in N holds f . x1 in N1
proof
per cases;
suppose B1:a=0; ::suppose1
ex N being Neighbourhood of x0 st
for x1 being Real st x1 in dom f & x1 in N holds f . x1 in N1
proof
take N=].(x0 - g),(x0 + g).[;
reconsider N as Neighbourhood of x0 by RCOMP_1:def 6,A1;
for x1 being Real st x1 in dom f & x1 in N holds f . x1 in N1
proof
let x1 be Real;
|. f.x1 - f.x0 .|
= |. f.x1 - (1/2*sin(a*x0+b)+1/2) .| by A3
.= |. 1/2*sin(0*x1+b)+1/2 - (1/2*sin(0*x0+b)+1/2) .| by B1,A3
.= 0 by ABSVALUE:def 1;
hence thesis by A2,RCOMP_1:1,A1;
end;
hence thesis;
end;
hence thesis;
end; ::suppose1
suppose B2: a<>0;::suppose2
AB: |.a.|>0 & |.a.|<>0 by COMPLEX1:47,B2;
ex N being Neighbourhood of x0 st
for x1 being Real st x1 in dom f & x1 in N holds f . x1 in N1
proof
take N=].(x0 - g*(1/|.a.|)*(1/(1/2))),(x0 + g*(1/|.a.|)*(1/(1/2))).[;
reconsider N as Neighbourhood of x0 by RCOMP_1:def 6,A1,AB;::B4,
for x1 being Real st x1 in dom f & x1 in N holds f . x1 in N1
proof
let x1 be Real;
assume x1 in dom f;
assume x1 in N; then
|.x1-x0.|*(1/2*|.a.|) < (g*(1/|.a.|)*(1/(1/2)))*(1/2*|.a.|)
by RCOMP_1:1,XREAL_1:68,AB; then
1/2*|.a.|*|.x1-x0.| < (g*(1/|.a.|)*(1/(1/2))*(1/2))*|.a.|; then
1/2*|.a.|*|.x1-x0.| < (g*(|.1/a.|)*(1/(1/2))*(1/2))*|.a.|
by ABSVALUE:7; then
1/2*|.a.|*|.x1-x0.| < g*((|.1/a.|)*|.a.| ); then
E1a: 1/2*|.a.|*|.x1-x0.| < g*1 by ABSVALUE:6,B2;
E3: |. f.x1 - f.x0 .| = |. f.x1 - (1/2*sin(a*x0+b)+1/2) .| by A3
.= |. 1/2*sin(a*x1+b)+1/2 - (1/2*sin(a*x0+b)+1/2) .| by A3
.= |. 1/2*(sin(a*x1+b) - sin(a*x0+b)) .|
.= |.1/2.| * |.sin(a*x1+b)-sin(a*x0+b).| by COMPLEX1:65
.=1/2*|.sin(a*x1+b)-sin(a*x0+b).| by COMPLEX1:43;
1/2*|.a*x1+b-(a*x0+b).| = 1/2*|.a*(x1-x0).|
.=1/2*(|.a.|*|.x1-x0.|) by COMPLEX1:65; then
|. f.x1 - f.x0 .| <= 1/2*|.a.|*|.x1-x0.| by E3,LmSin2,XREAL_1:64;
then
|. f.x1 - f.x0 .| < g by E1a,XXREAL_0:2;
hence thesis by A2,RCOMP_1:1;
end;
hence thesis;
end;
hence thesis;
end;
end;
hence thesis;
end;
hence thesis by FCONT_1:4;
end;
hence thesis;
end;
theorem
for f be Function of REAL,REAL, a,b be Real st
for x be Real holds f.x = 1/2*sin(a*x+b)+1/2
holds f is continuous by LmSin3;
theorem
for r,s be Real, f be Function of REAL,REAL st
for x be Real holds f.x = max(r,min(s,x))
holds
f is Lipschitzian
proof
let r,s be Real;
let f be Function of REAL,REAL;
assume A1:for x be Real holds f.x= max(r,min(s,x));
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 1;
for x1, x2 being Real st x1 in dom f & x2 in dom f holds
|.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).|
proof
let x1, x2 be Real;
|.((f . x1) - (f . x2)).| = |.(max(r,min(s,x1)) - (f . x2)).| by A1
.=|.max(r,min(s,x1)) - max(r,min(s,x2)).| by A1;
hence thesis by LeMM01;
end;
hence thesis;
end;
hence thesis;
end;
theorem MM3:
for g be Function of REAL,REAL holds
{f where f is Function of REAL,REAL :
for x be Real holds f.x= min(1,max(0, g.x))}
c= Membership_Funcs (REAL)
proof
let g be Function of REAL,REAL;
let f0 be object;
assume f0 in {f where f is Function of REAL,REAL :
for x be Real holds f.x= min(1,max(0, g.x))};
then consider f be Function of REAL,REAL such that
A1: f0=f and
A2: for x be Real holds f.x= min(1,max(0, g.x));
rng f c= [.0,1.]
proof
let y be object;
assume y in rng f;then
consider x be object such that
B2: x in REAL and B3: y = f.x by FUNCT_2:11;
reconsider x as Real by B2;
B4:y = min(1,max(0, g.x)) by A2,B3;
0<=max(0, g.x) by XXREAL_0:25; then
0<=min(1,max(0, g.x)) & min(1,max(0, g.x))<=1 by XXREAL_0:20,XXREAL_0:17;
hence thesis by B4;
end;
then f is [.0,1.] -valued;
hence thesis by Def1,A1;
end;
MM4:
for g be Function of REAL,REAL holds
{f where f is Function of REAL,REAL :
for x be Real holds f.x= max(0,min(1, g.x))}
c= Membership_Funcs (REAL)
proof
let g be Function of REAL,REAL;
let f0 be object;
assume f0 in {f where f is Function of REAL,REAL :
for x be Real holds f.x= max(0,min(1, g.x))};
then consider f be Function of REAL,REAL such that
A1: f0=f and
A2: for x be Real holds f.x= max(0,min(1, g.x));
rng f c= [.0,1.]
proof
let y be object;
assume y in rng f;then
consider x be object such that
B2: x in REAL and B3: y = f.x by FUNCT_2:11;
reconsider x as Real by B2;
B4:y = max(0,min(1, g.x)) by A2,B3;
min(1, g.x)<=1 by XXREAL_0:17; then
0<=max(0,min(1, g.x)) & max(0,min(1, g.x))<=1 by XXREAL_0:28,XXREAL_0:25;
hence thesis by B4;
end;
then f is [.0,1.] -valued;
hence thesis by Def1,A1;
end;
theorem MM41:
{f where f,g is Function of REAL,REAL :
for x be Real holds f.x= max(0,min(1, g.x))}
c= Membership_Funcs (REAL)
proof
let F be object;
assume F in {f where f,g is Function of REAL,REAL :
for x be Real holds f.x= max(0,min(1, g.x))};
then consider f,g being Function of REAL,REAL
such that
A1: F=f and A2: for x be Real holds f.x= max(0,min(1, g.x));
F in {f where f is Function of REAL,REAL :
for x be Real holds f.x= max(0,min(1, g.x))} by A1,A2;
hence thesis by MM4,TARSKI:def 3;
end;
theorem MM40:
for f,g be Function of REAL,REAL st
(for x be Real holds f.x= max(0,min(1, g.x)))
holds
f is FuzzySet of REAL
proof
let f,g be Function of REAL,REAL;
assume for x be Real holds f.x= max(0,min(1, g.x)); then
f in {f where f is Function of REAL,REAL :
for x be Real holds f.x= max(0,min(1, g.x))}; then
f in Membership_Funcs (REAL) by TARSKI:def 3,MM4;
hence thesis by Def1;
end;
theorem
for f,g be Function of REAL,REAL st
(for x be Real holds f.x= min(1,max(0, g.x)))
holds f is FuzzySet of REAL
proof
let f,g be Function of REAL,REAL;
assume for x be Real holds f.x= min(1,max(0, g.x)); then
f in {f where f is Function of REAL,REAL :
for x be Real holds f.x= min(1,max(0, g.x))}; then
f in Membership_Funcs (REAL) by TARSKI:def 3,MM3;
hence thesis by Def1;
end;
:::: fuzzy Set from trigonometric function
theorem
{f where f is Function of REAL,REAL :
ex a,b be Real st for th be Real holds f.th= 1/2*sin(a*th+b)+1/2}
c= Membership_Funcs (REAL)
proof
let x be object;
assume x in {f where f is Function of REAL,REAL :
ex a,b be Real st for th be Real holds f.th= 1/2*sin(a*th+b)+1/2};
then consider f be Function of REAL,REAL such that
A1: x=f and
A2: ex a,b be Real st for th be Real holds f.th= 1/2*sin(a*th+b)+1/2;
rng f c= [.0,1.]
proof
let y be object;
assume y in rng f;then
consider th be object such that
B2: th in REAL and B3: y = f . th by FUNCT_2:11;
reconsider th as Real by B2;
consider a,b be Real such that
B1:for th0 be Real holds f.th0= 1/2*sin(a*th0+b)+1/2 by A2;
|.sin(a*th+b) .| <= 1 by SIN_COS:27; then
-1 <= sin(a*th+b) & sin(a*th+b) <= 1 by ABSVALUE:5; then
1/2*(-1) <= 1/2*sin(a*th+b) & 1/2*sin(a*th+b) <= 1/2*1 by XREAL_1:64;
then
B4: -1/2+1/2 <= sin(a*th+b)*1/2+1/2 &
1/2*sin(a*th+b)+1/2 <= 1/2+1/2 by XREAL_1:7;
y = 1/2*sin(a*th+b)+1/2 by B1,B3;
hence thesis by B4;
end;
then f is [.0,1.] -valued;
hence thesis by Def1,A1;
end;
theorem TrF11:
{f where f is Function of REAL,REAL, a,b is Real:
for th be Real holds f.th= 1/2*sin(a*th+b)+1/2}
c=Membership_Funcs (REAL)
proof
let x be object;
assume x in {f where f is Function of REAL,REAL ,a,b is Real:
for th be Real holds f.th= 1/2*sin(a*th+b)+1/2};
then consider f be Function of REAL,REAL, a,b be Real such that
A1: x=f and
A2: for th be Real holds f.th= 1/2*sin(a*th+b)+1/2;
rng f c= [.0,1.]
proof
let y be object;
assume y in rng f;then
consider th be object such that
B2: th in REAL and B3: y = f . th by FUNCT_2:11;
reconsider th as Real by B2;
consider a,b be Real such that
B1:for th0 be Real holds f.th0= 1/2*sin(a*th0+b)+1/2 by A2;
|.sin(a*th+b) .| <= 1 by SIN_COS:27;
then
-1 <= sin(a*th+b) & sin(a*th+b) <= 1 by ABSVALUE:5; then
1/2*(-1) <= 1/2*sin(a*th+b) & 1/2*sin(a*th+b) <= 1/2*1 by XREAL_1:64;
then
B4: -1/2+1/2 <= sin(a*th+b)*1/2+1/2 &
1/2*sin(a*th+b)+1/2 <= 1/2+1/2 by XREAL_1:7;
y = 1/2*sin(a*th+b)+1/2 by B1,B3;
hence thesis by B4;
end;
then f is [.0,1.] -valued;
hence thesis by Def1,A1;
end;
theorem
for a,b be Real, f be Function of REAL,REAL st
(for th be Real holds f.th= 1/2*sin(a*th+b)+1/2)
holds f is FuzzySet of REAL
proof
let a,b be Real;
let f be Function of REAL,REAL;
assume for th be Real holds f.th= 1/2*sin(a*th+b)+1/2;
then
f in {f where f is Function of REAL,REAL, a,b is Real:
for th be Real holds f.th= 1/2*sin(a*th+b)+1/2};
hence thesis by Def1,TrF11;
end;
theorem TrF2:
{f where f is Function of REAL,REAL :
ex a,b be Real st for th be Real holds f.th= 1/2*cos(a*th+b)+1/2}
c= Membership_Funcs (REAL)
proof
let x be object;
assume x in {f where f is Function of REAL,REAL :
ex a,b be Real st for th be Real holds f.th= 1/2*cos(a*th+b)+1/2};
then consider f be Function of REAL,REAL such that
A1: x=f and
A2: ex a,b be Real st for th be Real holds f.th= 1/2*cos(a*th+b)+1/2;
rng f c= [.0,1.]
proof
let y be object;
assume y in rng f;then
consider th be object such that
B2: th in REAL and B3: y = f . th by FUNCT_2:11;
reconsider th as Real by B2;
consider a,b be Real such that
B1:for th0 be Real holds f.th0= 1/2*cos(a*th0+b)+1/2 by A2;
|.cos(a*th+b) .| <= 1 by SIN_COS:27; then
-1 <= cos(a*th+b) & cos(a*th+b) <= 1 by ABSVALUE:5; then
1/2*(-1) <= 1/2*cos(a*th+b) & 1/2*cos(a*th+b) <= 1/2*1 by XREAL_1:64;
then
B4: -1/2+1/2 <= cos(a*th+b)*1/2+1/2 &
1/2*cos(a*th+b)+1/2 <= 1/2+1/2 by XREAL_1:7;
y = 1/2*cos(a*th+b)+1/2 by B1,B3;
hence thesis by B4;
end;
then f is [.0,1.] -valued;
hence thesis by Def1,A1;
end;
theorem
for a,b be Real, f be Function of REAL,REAL st
(for th be Real holds f.th= 1/2*cos(a*th+b)+1/2)
holds f is FuzzySet of REAL
proof
let a,b be Real;
let f be Function of REAL,REAL;
assume for th be Real holds f.th= 1/2*cos(a*th+b)+1/2;
then
f in {f where f is Function of REAL,REAL :
ex a,b be Real st for th be Real holds f.th= 1/2*cos(a*th+b)+1/2};
hence thesis by Def1,TrF2;
end;
theorem
for a,b be Real, f be FuzzySet of REAL st
(a<>0 & for th be Real holds f.th= 1/2*sin(a*th+b)+1/2)
holds
f is normalized
proof
let a,b be Real, f be FuzzySet of REAL;
assume A1: a<>0;
assume A2:( for th be Real holds f.th= 1/2*sin(a*th+b)+1/2);
ex x being Element of REAL st f . x = 1
proof
take (PI/2-b)/a;
f.((PI/2-b)/a) = 1/2*sin(a*((PI/2-b)/a)+b)+1/2 by A2
.= 1/2*sin(a/a*(PI/2-b)+b)+1/2 by XCMPLX_1:75
.= 1/2*sin(1*(PI/2-b)+b)+1/2 by XCMPLX_1:60,A1
.= 1 by SIN_COS:77;
hence thesis by XREAL_0:def 1;
end;
hence thesis;
end;
theorem
for f be FuzzySet of REAL st
f in {f where f is Function of REAL,REAL :
ex a,b be Real st a<>0 & for th be Real holds f.th= 1/2*sin(a*th+b)+1/2}
holds
f is normalized
proof
let f be FuzzySet of REAL;
assume ::A2:
f in {f where f is Function of REAL,REAL :
ex a,b be Real st a<>0 & for th be Real holds f.th= 1/2*sin(a*th+b)+1/2};
then consider f2 be Function of REAL,REAL such that
A3:f=f2 and
A4: ex a,b be Real st a<>0 & for th be Real holds f2.th= 1/2*sin(a*th+b)+1/2;
consider a,b be Real such that
A7: a<>0 and
A5:for th be Real holds f2.th= 1/2*sin(a*th+b)+1/2 by A4;
reconsider a as Element of REAL by XREAL_0:def 1;
ex x being Element of REAL st f . x = 1
proof
take (PI/2-b)/a;
f.((PI/2-b)/a) = 1/2*sin(a*((PI/2-b)/a)+b)+1/2 by A5,A3
.= 1/2*sin(a/a*(PI/2-b)+b)+1/2 by XCMPLX_1:75
.= 1/2*sin(1*(PI/2-b)+b)+1/2 by XCMPLX_1:60,A7
.= 1 by SIN_COS:77;
hence thesis by XREAL_0:def 1;
end;
hence thesis;
end;
theorem TrF22:
for f be FuzzySet of REAL
for a,b be Real st a<>0 & for th be Real holds f.th= 1/2*cos(a*th+b)+1/2
holds
f is normalized
proof
let f be FuzzySet of REAL;
let a,b be Real;
assume A1:a<>0;
assume A2:for th be Real holds f.th= 1/2*cos(a*th+b)+1/2;
ex x being Element of REAL st f . x = 1
proof
take (-b)/a;
f.((-b)/a)=1/2*cos(a*((-b)/a)+b)+1/2 by A2
.= 1/2*cos(a/a*(-b)+b)+1/2 by XCMPLX_1:75
.= 1/2*cos(1*(-b)+b)+1/2 by XCMPLX_1:60,A1
.= 1 by SIN_COS:31;
hence thesis by XREAL_0:def 1;
end;
hence thesis;
end;
theorem
for f be FuzzySet of REAL st
f in {f where f is Function of REAL,REAL :
ex a,b be Real st a<>0 & for th be Real holds f.th= 1/2*cos(a*th+b)+1/2}
holds
f is normalized
proof
let f be FuzzySet of REAL;
assume f in {f where f is Function of REAL,REAL :
ex a,b be Real st a<>0 & for th be Real holds f.th= 1/2*cos(a*th+b)+1/2};
then
consider f1 being Function of REAL,REAL such that
A1:f1=f and
A2:(ex a,b be Real st a<>0 & for th be Real holds f1.th= 1/2*cos(a*th+b)+1/2);
thus thesis by A1,TrF22,A2;
end;
:::: periodicity of membership functions
theorem TrF160:
for F being Function of REAL,REAL, a,b,c,d being Real, i be Integer st
a<>0 & i<>0 & for x be Real holds F.x= max(0,min(1, c*sin(a*x+b)+d))
holds
F is (2 * PI)/a * i -periodic
proof
let F be Function of REAL,REAL;
let a,b,c,d be Real;
let i be Integer;
assume A0: a<>0 & i<>0;
assume A2: for x be Real holds F.x= max(0,min(1, c*sin(a*x+b)+d));
for x being Real st x in dom F holds
x + (2 * PI)/a * i in dom F & x - (2 * PI)/a * i in dom F
& F . x = F . (x + (2 * PI)/a * i)
proof
let x be Real;
assume x in dom F;
A3A: x + (2 * PI)/a * i in REAL
& x - (2 * PI)/a * i in REAL by XREAL_0:def 1;
S1:sin is (2 * PI) * i -periodic by FUNCT_9:21,A0;
SS: a*x+b in dom sin by SIN_COS:24, XREAL_0:def 1;
F . (x + (2 * PI)/a * i)
= max(0,min(1, c*sin(a*(x + (2 * PI)/a * i)+b)+d)) by A2
.= max(0,min(1, c*sin(a*x + a*((2 * PI)/a) * i+b)+d))
.= max(0,min(1, c*sin(a*x + a/a*(2 * PI) * i+b)+d)) by XCMPLX_1:75
.= max(0,min(1, c*sin(a*x + 1*(2 * PI) * i+b)+d)) by XCMPLX_1:60,A0
.= max(0,min(1, c*sin.((a*x + b) + (2 * PI) * i)+d)) by SIN_COS:def 17
.= max(0,min(1, c*sin.(a*x + b)+d)) by FUNCT_9:1,SS,S1
.= max(0,min(1, c*sin(a*x + b)+d)) by SIN_COS:def 17;
hence thesis by FUNCT_2:def 1,A3A,A2;
end;
hence thesis by FUNCT_9:1,A0;
end;
theorem
for F being Function of REAL,REAL, a,b,c,d being Real st
for x be Real holds F.x= max(0,min(1, c*sin(a*x+b)+d))
holds
F is periodic
proof
let F be Function of REAL,REAL;
let a,b,c,d be Real;
assume A0: for x be Real holds F.x= max(0,min(1, c*sin(a*x+b)+d));
ex t being Real st F is t -periodic
proof
per cases;
suppose A1:a<>0;
take (2 * PI)/a * 1;
thus thesis by TrF160,A0,A1;
end;
suppose A5:a=0;
take 1;
for x being Real st x in dom F holds
( x + 1 in dom F & x - 1 in dom F & F . x = F . (x + 1) )
proof
let x be Real;
assume x in dom F;
A4A: x + 1 in REAL & x - 1 in REAL by XREAL_0:def 1;
F . x = max(0,min(1, c*sin(a*x+b)+d)) by A0
.= max(0,min(1, c*sin(0*(x+1)+b)+d)) by A5;
hence thesis by A4A,FUNCT_2:def 1,A0,A5;
end;
hence F is 1 -periodic by FUNCT_9:1;
end;
end;
hence thesis by FUNCT_9:def 2;
end;
theorem MM1:
{f where f is Function of REAL,REAL :
ex a,b be Real st for th be Real holds f.th= max(0, sin(a*th+b))}
c= Membership_Funcs (REAL)
proof
let x be object;
assume x in {f where f is Function of REAL,REAL :
ex a,b be Real st for th be Real holds f.th= max(0, sin(a*th+b))};
then consider f be Function of REAL,REAL such that
A1: x=f and
A2: ex a,b be Real st for th be Real holds f.th= max(0, sin(a*th+b));
rng f c= [.0,1.]
proof
let y be object;
assume y in rng f;then
consider th be object such that
B2: th in REAL and B3: y = f . th by FUNCT_2:11;
reconsider th as Real by B2;
consider a,b be Real such that
B1:for th0 be Real holds f.th0= max(0, sin(a*th0+b)) by A2;
sin(a*th+b) <= 1 by SIN_COS6:4; then
B4: 0 <= max(0, sin(a*th+b)) &
max(0, sin(a*th+b)) <= 1 by XXREAL_0:25,XXREAL_0:28;
y = max(0, sin(a*th+b)) by B1,B3;
hence thesis by B4;
end;
then f is [.0,1.] -valued;
hence thesis by Def1,A1;
end;
theorem
for a,b be Real, f be Function of REAL,REAL st
(for x be Real holds f.x= max(0, sin(a*x+b)))
holds f is FuzzySet of REAL
proof
let a,b be Real;
let f be Function of REAL,REAL;
assume for th be Real holds f.th= max(0, sin(a*th+b));
then
f in {f where f is Function of REAL,REAL :
ex a,b be Real st for th be Real holds f.th= max(0, sin(a*th+b))};
hence thesis by Def1,MM1;
end;
theorem MM2:
{f where f is Function of REAL,REAL :
ex a,b be Real st for x be Real holds f.x= max(0, cos(a*x+b))}
c= Membership_Funcs (REAL)
proof
let x be object;
assume x in {f where f is Function of REAL,REAL :
ex a,b be Real st for th be Real holds f.th= max(0, cos(a*th+b))}; then
consider f be Function of REAL,REAL such that
A1: x=f and
A2: ex a,b be Real st for th be Real holds f.th= max(0, cos(a*th+b));
rng f c= [.0,1.]
proof
let y be object;
assume y in rng f;then
consider th be object such that
B2: th in REAL and B3: y = f . th by FUNCT_2:11;
reconsider th as Real by B2;
consider a,b be Real such that
B1:for th0 be Real holds f.th0= max(0, cos(a*th0+b)) by A2;
cos(a*th+b) <= 1 by SIN_COS6:6;
then
B4: 0 <= max(0, cos(a*th+b)) &
max(0, cos(a*th+b)) <= 1 by XXREAL_0:25,XXREAL_0:28;
y = max(0, cos(a*th+b)) by B1,B3;
hence thesis by B4;
end;
then f is [.0,1.] -valued;
hence thesis by Def1,A1;
end;
theorem
for a,b be Real, f be Function of REAL,REAL st
(for x be Real holds f.x = max(0, cos(a*x+b)))
holds f is FuzzySet of REAL
proof
let a,b be Real;
let f be Function of REAL,REAL;
assume for th be Real holds f.th= max(0, cos(a*th+b)); then
f in {f where f is Function of REAL,REAL :
ex a,b be Real st for th be Real holds f.th= max(0, cos(a*th+b))};
hence thesis by Def1,MM2;
end;
theorem
{f where f is Function of REAL,REAL, a,b,c,d is Real:
for x be Real holds f.x= max(0,min(1, c*sin(a*x+b)+d))}
c= {f where f,g is Function of REAL,REAL :
for x be Real holds f.x= max(0,min(1, g.x))}
proof
let g be object;
assume g in {f where f is Function of REAL,REAL, a,b,c,d is Real:
for x be Real holds f.x= max(0,min(1, c*sin(a*x+b)+d))};
then
consider f be Function of REAL,REAL, a,b,c,d be Real such that
A1:f=g and
A2:for x be Real holds f.x= max(0,min(1, c*sin(a*x+b)+d));
ex g being Function of REAL,REAL st
for x be Real holds g.x= c*sin(a*x+b)+d
proof
deffunc H1(Element of REAL) = In(c*sin(a*$1+b)+d,REAL);
ex f being Function of REAL,REAL st
for x being Element of REAL holds
f.x = H1(x) from FUNCT_2:sch 4;
then
consider f being Function of REAL,REAL such that
A1: for x being Element of REAL holds
f.x = H1(x);
take f;
for x be Real holds f.x= c*sin(a*x+b)+d
proof
let x be Real;
reconsider x as Element of REAL by XREAL_0:def 1;
f.x = H1(x) by A1;
hence thesis;
end;
hence thesis;
end; then
consider g being Function of REAL,REAL such that
A4:for x be Real holds g.x= c*sin(a*x+b)+d;
for x be Real holds f.x= max(0,min(1, g.x))
proof
let x be Real;
f.x = max(0,min(1, c*sin(a*x+b)+d)) by A2
.= max(0,min(1, g.x)) by A4;
hence thesis;
end;
hence thesis by A1;
end;
theorem MM5a:
{f where f is Function of REAL,REAL, a,b,c,d is Real:
for x be Real holds f.x= max(0,min(1, c*sin(a*x+b)+d))}
c= Membership_Funcs (REAL)
proof
let g be object;
assume g in {f where f is Function of REAL,REAL, a,b,c,d is Real:
for x be Real holds f.x= max(0,min(1, c*sin(a*x+b)+d))};
then
consider f be Function of REAL,REAL, a,b,c,d be Real such that
A1:f=g and
A2:for x be Real holds f.x= max(0,min(1, c*sin(a*x+b)+d));
f is FuzzySet of REAL
proof
rng f c= [.0,1.]
proof
let y be object;
assume y in rng f; then
consider x be object such that
B2: x in REAL and B3: y = f.x by FUNCT_2:11;
reconsider x as Real by B2;
B4:y = max(0,min(1, c*sin(a*x+b)+d)) by A2,B3;
min(1, c*sin(a*x+b)+d)<=1 by XXREAL_0:17; then
0<=max(0,min(1, c*sin(a*x+b)+d))
& max(0,min(1, c*sin(a*x+b)+d))<=1 by XXREAL_0:28,XXREAL_0:25;
hence thesis by B4;
end;
then
f is [.0,1.] -valued;
hence thesis;
end;
hence thesis by Def1,A1;
end;
theorem
for f being Function of REAL,REAL, a,b,c,d being Real st
for x be Real holds f.x= max(0,min(1, c*sin(a*x+b)+d))
holds f is FuzzySet of REAL
proof
let f be Function of REAL,REAL;
let a,b,c,d be Real;
assume for x be Real holds f.x= max(0,min(1, c*sin(a*x+b)+d)); then
f in {f where f is Function of REAL,REAL, a,b,c,d is Real :
for x be Real holds f.x= max(0,min(1, c*sin(a*x+b)+d))};
hence thesis by Def1,MM5a;
end;
theorem MM60:
{f where f is Function of REAL,REAL, a,b,c,d is Real:
for x be Real holds f.x= max(0,min(1, c*arctan(a*x+b)+d))}
c= {f where f,g is Function of REAL,REAL :
for x be Real holds f.x= max(0,min(1, g.x))}
proof
let g be object;
assume g in {f where f is Function of REAL,REAL, a,b,c,d is Real:
for x be Real holds f.x= max(0,min(1, c*arctan(a*x+b)+d))};
then
consider f be Function of REAL,REAL, a,b,c,d be Real such that
A1:f=g and
A2:for x be Real holds f.x= max(0,min(1, c*arctan(a*x+b)+d));
ex g being Function of REAL,REAL st
for x be Real holds g.x= c*arctan(a*x+b)+d
proof
deffunc H1(Element of REAL) = In(c*arctan(a*$1+b)+d,REAL);
ex f being Function of REAL,REAL st
for x being Element of REAL holds
f.x = H1(x) from FUNCT_2:sch 4;
then
consider f being Function of REAL,REAL such that
A1: for x being Element of REAL holds
f.x = H1(x);
take f;
for x be Real holds f.x= c*arctan(a*x+b)+d
proof
let x be Real;
reconsider x as Element of REAL by XREAL_0:def 1;
f.x = H1(x) by A1;
hence thesis;
end;
hence thesis;
end; then
consider g being Function of REAL,REAL such that
A4:for x be Real holds g.x= c*arctan(a*x+b)+d;
for x be Real holds f.x= max(0,min(1, g.x))
proof
let x be Real;
f.x = max(0,min(1, c*arctan(a*x+b)+d)) by A2
.= max(0,min(1, g.x)) by A4;
hence thesis;
end;
hence thesis by A1;
end;
theorem
{f where f is Function of REAL,REAL, a,b,c,d is Real:
for x be Real holds f.x= max(0,min(1, c*arctan(a*x+b)+d))}
c= Membership_Funcs (REAL) by MM60,MM41;
theorem
for f being Function of REAL,REAL, a,b,c,d being Real st
for x be Real holds f.x= max(0,min(1, c*arctan(a*x+b)+d))
holds f is FuzzySet of REAL
proof
let f be Function of REAL,REAL;
let a,b,c,d be Real;
assume for x be Real holds f.x= max(0,min(1, c*arctan(a*x+b)+d)); then
f in {f where f is Function of REAL,REAL, a,b,c,d is Real:
for x be Real holds f.x= max(0,min(1, c*arctan(a*x+b)+d))} ;
then
f in Membership_Funcs (REAL) by MM60,MM41;
hence thesis by Def1;
end;
theorem MMLip1:
for f be Function of REAL,REAL, a,b,c,d,r,s be Real st
for x be Real holds f.x= max(r,min(s, c*sin(a*x+b)+d))
holds f is Lipschitzian
proof
let f be Function of REAL,REAL;
let a,b,c,d,r,s be Real;
assume A1: for x be Real holds f.x= max(r,min(s, c*sin(a*x+b)+d));
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
per cases;
suppose C1: c = 0;
take 1;
for x1, x2 being Real st x1 in dom f & x2 in dom f holds
|.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).|
proof
let x1, x2 be Real;
assume x1 in dom f & x2 in dom f;
|.((f . x1) - (f . x2)).|
= |.max(r,min(s, c*sin(a*x1+b)+d))- f.x2.| by A1
.= |.max(r,min(s, 0*sin(a*x1+b)+d))- max(r,min(s, 0*sin(a*x2+b)+d)).|
by C1,A1
.=0 by COMPLEX1:44;
hence thesis by COMPLEX1:46;
end;
hence thesis;
end;
suppose A3: c <> 0;
per cases;
suppose A0: a = 0;
take 1;
for x1, x2 being Real st x1 in dom f & x2 in dom f holds
|.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).|
proof
let x1, x2 be Real;
|.((f . x1) - (f . x2)).|
= |.max(r,min(s, c*sin(a*x1+b)+d))- f.x2.| by A1
.= |.max(r,min(s, c*sin(0*x1+b)+d))- max(r,min(s, c*sin(0*x2+b)+d)).|
by A0,A1
.=0 by COMPLEX1:44;
hence thesis by COMPLEX1:46;
end;
hence thesis;
end;
suppose A2: a <> 0;
take |.a.|*|.c.|;
A5: |.c.|>0 & |.a.|>0 by A2,A3,COMPLEX1:47;
for x1, x2 being Real st x1 in dom f & x2 in dom f holds
|.((f . x1) - (f . x2)).| <= |.a.|*|.c.| * |.(x1 - x2).|
proof
let x1, x2 be Real;
assume x1 in dom f & x2 in dom f;
A9: |.((f . x1) - (f . x2)).|
= |.max(r,min(s, c*sin(a*x1+b)+d))- f.x2.| by A1
.= |.max(r,min(s, c*sin(a*x1+b)+d))- max(r,min(s, c*sin(a*x2+b)+d)).| by A1;
A7: |.max(r,min(s, c*sin(a*x1+b)+d))- max(r,min(s, c*sin(a*x2+b)+d)).|
<= |.c*sin(a*x1+b)+d-(c*sin(a*x2+b)+d).| by LeMM01;
A8: |.c.|*|.(a*x1+b)-(a*x2+b).| = |.c.|*|.a*(x1-x2).|
.= |.c.|*(|.a.|*|.(x1-x2).|) by COMPLEX1:65;
A6: |.c*(sin(a*x1+b)-sin(a*x2+b)).|=|.c.|*|.sin(a*x1+b)-sin(a*x2+b).| &
|.c*sin(a*x1+b)+d-(c*sin(a*x2+b)+d).|=|.c*(sin(a*x1+b)-sin(a*x2+b)).|
by COMPLEX1:65;
|.c*sin(a*x1+b)+d-(c*sin(a*x2+b)+d).| <= |.c.|*|.(a*x1+b)-(a*x2+b).|
by XREAL_1:64,A5,A6,LmSin2;
hence thesis by A9,A8,A7,XXREAL_0:2;
end;
hence thesis by A5;
end;
end;
end;
hence thesis;
end;
theorem
for f be Function of REAL,REAL, a,b,c,d be Real st
for x be Real holds f.x= max(0,min(1, c*sin(a*x+b)+d))
holds f is Lipschitzian by MMLip1;
:::: membership functions from Gaussian function
theorem GauF04:
for a,b be Real, f be Function of REAL,REAL st
(b <> 0 & for x be Real holds f.x= exp_R(-(x-a)^2/(2*b^2)))
holds
f is FuzzySet of REAL
proof
let a,b be Real;
let f be Function of REAL,REAL;
assume A1:b<>0;
assume A2: for x be Real holds f.x= exp_R(-(x-a)^2/(2*b^2));
rng f c= [.0,1.]
proof
let z be object;
assume z in rng f; then
consider x be object such that
B2: x in REAL and
B3: f . x = z by FUNCT_2:11;
reconsider x as Real by B2;
B4:z=exp_R(-(x-a)^2/(2*b^2)) by B3,A2;
B5:exp_R(-(x-a)^2/(2*b^2)) <= 1
proof
per cases;
suppose x=a; then
exp_R(-(x-a)^2/(2*b^2)) = 1 by SIN_COS:51;
hence thesis;
end;
suppose x<>a; then
(x-a)<>0; then
(x-a)^2>0 & b^2 >0 by SQUARE_1:12,A1; then
exp_R. (-(x-a)^2/(2*b^2)) <=1 by SIN_COS:53;
hence thesis by SIN_COS:def 23;
end;
end;
0 <= exp_R(-(x-a)^2/(2*b^2)) & exp_R(-(x-a)^2/(2*b^2)) <= 1
by B5,SIN_COS:55;
hence thesis by B4;
end; then
f is [.0,1.] -valued;
hence thesis;
end;
theorem GauF04complex:
for a,b be Real, f be Function of REAL,REAL st
(b <> 0 & for x be Real holds f.x= exp(-(x-a)^2/(2*b^2)))
holds
f is FuzzySet of REAL
proof
let a,b be Real;
let f be Function of REAL,REAL;
assume A1:b<>0;
assume A2: for x be Real holds f.x= exp(-(x-a)^2/(2*b^2));
for x be Real holds f.x= exp_R(-(x-a)^2/(2*b^2))
proof
let x be Real;
f.x=exp(-(x-a)^2/(2*b^2)) by A2
.=exp_R(-(x-a)^2/(2*b^2)) by SIN_COS:49;
hence thesis;
end;
hence thesis by GauF04,A1;
end;
theorem
for a,b be Real st b<>0 holds
{f where f is Function of REAL,REAL :
for x be Real holds f.x= exp(-(x-a)^2/(2*b^2))}
c= Membership_Funcs (REAL)
proof
let a,b be Real;
assume A0: b<>0;
let y be object;
assume y in {f where f is Function of REAL,REAL :
for x be Real holds f.x= exp(-(x-a)^2/(2*b^2))}; then
consider f be Function of REAL,REAL such that
A1: y=f and
A2: for x be Real holds f.x= exp(-(x-a)^2/(2*b^2));
f is FuzzySet of REAL by A0,A2,GauF04complex;
hence thesis by Def1,A1;
end;
theorem
for a,b be Real, f be FuzzySet of REAL st
(for x be Real holds f.x= exp(-(x-a)^2/(2*b^2)))
holds
f is normalized
proof
let a,b be Real, f be FuzzySet of REAL;
assume A2: for x be Real holds f.x= exp(-(x-a)^2/(2*b^2));
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 = exp(-(a-a)^2/(2*b^2)) by A2
.=1 by SIN_COS3:20;
hence thesis by A6;
end;
hence thesis;
end;
theorem:: GauF02:
for a,b be Real, f be FuzzySet of REAL st
(b<>0 & for x be Real holds f.x= exp(-(x-a)^2/(2*b^2)))
holds
f is strictly-normalized
proof
let a,b be Real;
let f be FuzzySet of REAL;
assume A1: b<>0;
assume A2: for x be Real holds f.x = exp(-(x-a)^2/(2*b^2));
ex x being Element of REAL st
( f . x = 1 & ( for y being Element of REAL st f . y = 1 holds y = x ) )
proof
A4:a is Element of REAL by XREAL_0:def 1;
take a;
A3: f.a= exp(-(a-a)^2/(2*b^2)) by A2
.=1 by SIN_COS3:20;
for y being Element of REAL st f . y = 1 holds y = a
proof
let y be Element of REAL;
assume f.y=1; then
exp(-(y-a)^2/(2*b^2)) =1 by A2; then
(y-a)=0 by A1,EXpReq12;
hence y=a;
end;
hence thesis by A4,A3;
end;
hence thesis;
end;
theorem GauF05:
for a,b be Real, f be Function of REAL,REAL st
(b<>0 & for x be Real holds f.x= exp_R(-(x-a)^2/(2*b^2)))
holds
f is continuous
proof
let a,b be Real;
let f be Function of REAL,REAL;
assume b<>0;
assume A1:for x be Real holds f.x= exp_R(-(x-a)^2/(2*b^2));
set h = AffineMap(1,-a);
set g = (-1)/(2*b^2) (#) h (#) h;
D1: dom(g) = REAL /\ REAL by FUNCT_2:def 1;
f=exp_R * ((-1)/(2*b^2) (#) h (#) h)
proof
dom (exp_R * g) = REAL by FUNCT_2:def 1; then
A21:dom f = dom (exp_R * ((-1)/(2*b^2) (#) h (#) h)) by FUNCT_2:def 1;
( for x being object st x in dom f holds
f . x = (exp_R * ((-1)/(2*b^2) (#) h (#) h)). x )
proof
let x be object;
assume S2a: x in dom f; then
x in REAL by FUNCT_2:def 1; then
reconsider x as Real;
S1:x in dom (g) by D1,FUNCT_2:def 1,S2a;
(exp_R * ((-1)/(2*b^2) (#) h (#) h)). x
= exp_R.(((-1)/(2*b^2) (#) h (#) h). x) by FUNCT_1:13,S1
.=exp_R.(((-1)/(2*b^2) (#) h).x * h. x ) by VALUED_1:5
.=exp_R.(((-1)/(2*b^2)) * h.x * h. x ) by VALUED_1:6
.=exp_R.(((-1)/(2*b^2)) * h.x * (1*x+(-a)) ) by FCONT_1:def 4
.=exp_R.(((-1)/(2*b^2)) * (1*x+(-a)) * (x-a) ) by FCONT_1:def 4
.=exp_R(((-1)/(2*b^2)) * ((x-a) * (x-a)) ) by SIN_COS:def 23
.=exp_R(((x-a) * (x-a)) /(2*b^2)*(-1) ) by XCMPLX_1:75
.= exp_R(-(x-a)^2/(2*b^2));
hence thesis by A1;
end;
hence thesis by FUNCT_1:2,A21;
end;
hence thesis;
end;
theorem GauF06:
for a,b,c,r,s be Real, f be Function of REAL,REAL st
( b<>0 & for x be Real holds f.x= max(r,min(s, exp_R(-(x-a)^2/(2*b^2))+c)) )
holds
f is continuous
proof
let a,b,c,r,s be Real;
let f be Function of REAL,REAL;
assume B0: b<>0;
assume A1:for x be Real holds f.x= max(r,min(s, exp_R(-(x-a)^2/(2*b^2))+c));
deffunc H1(Element of REAL) = In(exp_R(-($1-a)^2/(2*b^2)),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 x0 being Real st x0 in dom f holds
f is_continuous_in x0
proof
let x0 be Real;
assume x0 in dom f; then
x0 in REAL by FUNCT_2:def 1; then
B1: x0 in dom h by FUNCT_2:def 1;
for e being Real st 0 < e holds
ex d being Real st
( 0 < d & ( for x1 being Real st x1 in dom f & |.(x1 - x0).| < d holds
|.((f . x1) - (f . x0)).| < e ) )
proof
let e be Real;
assume
A2: 0 < e;
ex d being Real st
( 0 < d & ( for x1 being Real st x1 in dom f & |.(x1 - x0).| < d holds
|.((f . x1) - (f . x0)).| < e ) )
proof
for x being Real holds h.x = exp_R(-(x-a)^2/(2*b^2))
proof
let x be Real;
reconsider x as Element of REAL by XREAL_0:def 1;
h.x= H1(x) by A3
.=exp_R(-(x-a)^2/(2*b^2));
hence thesis;
end; then
h is continuous by GauF05,B0; then
consider d1 being Real such that
A4: d1 > 0 and
A7: ( for x1 being Real st x1 in dom h & |.(x1 - x0).| < d1 holds
|.(h . x1) - (h . x0).| < e ) by A2, FCONT_1:3,B1;
take d1;
for x1 being Real st x1 in dom f & |.(x1 - x0).| < d1 holds
|.((f . x1) - (f . x0)).| < e
proof
let x1 be Real;
assume x1 in dom f; then
x1 in REAL by FUNCT_2:def 1; then
A8: x1 in dom h by FUNCT_2:def 1;
assume A6: |.(x1 - x0).| < d1;
|.(f . x1) - (f . x0).|
=|.max(r,min(s, exp_R(-(x1-a)^2/(2*b^2))+c)) - (f . x0).| by A1
.=|.max(r,min(s, exp_R(-(x1-a)^2/(2*b^2))+c))
- max(r,min(s, exp_R(-(x0-a)^2/(2*b^2))+c)).| by A1; then
A9: |.(f . x1) - (f . x0).|
<=|.exp_R(-(x1-a)^2/(2*b^2))+c-(exp_R(-(x0-a)^2/(2*b^2))+c).| by LeMM01;
reconsider x1 as Element of REAL by XREAL_0:def 1;
reconsider x0 as Element of REAL by XREAL_0:def 1;
|.(h . x1) - (h . x0).| = |.H1(x1)-h.x0.| by A3
.=|.exp_R(-(x1-a)^2/(2*b^2))-H1(x0).| by A3; then
|.exp_R(-(x1-a)^2/(2*b^2))-exp_R(-(x0-a)^2/(2*b^2)).| < e by A8,A6,A7;
hence thesis by A9,XXREAL_0:2;
end;
hence thesis by A4;
end;
hence thesis;
end;
hence thesis by FCONT_1:3;
end;
hence thesis;
end;
theorem
for a,b,c be Real, f be Function of REAL,REAL st
( b<>0 & for x be Real holds f.x= max(0,min(1, exp_R(-(x-a)^2/(2*b^2))+c)) )
holds
f is continuous by GauF06;
theorem GauF07:
for a,b,c be Real, f be Function of REAL,REAL st
( b<>0 & for x be Real holds f.x= max(0,min(1, exp_R(-(x-a)^2/(2*b^2))+c)) )
holds
f is FuzzySet of REAL
proof
let a,b,c be Real;
let f be Function of REAL,REAL;
assume b <> 0;
assume A2: for x be Real holds f.x= max(0,min(1, exp_R(-(x-a)^2/(2*b^2))+c));
ex g being Function of REAL,REAL st
for x be Real holds g.x= exp_R(-(x-a)^2/(2*b^2))+c
proof
deffunc H1(Element of REAL) = In(exp_R(-($1-a)^2/(2*b^2))+c,REAL);
consider f being Function of REAL,REAL such that
A1: for x being Element of REAL holds f.x = H1(x) from FUNCT_2:sch 4;
take f;
for x be Real holds f.x= exp_R(-(x-a)^2/(2*b^2))+c
proof
let x be Real;
reconsider x as Element of REAL by XREAL_0:def 1;
f.x = H1(x) by A1;
hence thesis;
end;
hence thesis;
end; then
consider g being Function of REAL,REAL such that
A4:for x be Real holds g.x= exp_R(-(x-a)^2/(2*b^2))+c;
for x be Real holds f.x= max(0,min(1, g.x))
proof
let x be Real;
f.x = max(0,min(1, exp_R(-(x-a)^2/(2*b^2))+c)) by A2
.= max(0,min(1, g.x)) by A4;
hence thesis;
end;
hence thesis by MM40;
end;
theorem
{f where f is Function of REAL,REAL, a,b,c is Real:
b <> 0 & for x be Real holds f.x= max(0,min(1, exp_R(-(x-a)^2/(2*b^2))+c))}
c= Membership_Funcs (REAL)
proof
let g be object;
assume g in {f where f is Function of REAL,REAL, a,b,c is Real:
b <> 0 & for x be Real holds f.x= max(0,min(1, exp_R(-(x-a)^2/(2*b^2))+c))};
then consider f be Function of REAL,REAL, a,b,c be Real such that
A1: f=g and
A0: b <> 0 and
A2: for x be Real holds f.x= max(0,min(1, exp_R(-(x-a)^2/(2*b^2))+c));
g is FuzzySet of REAL by A0,A1,A2,GauF07;
hence thesis by Def1;
end;
:::: S or Z type Membership function
theorem MMLip3:
for f be Function of REAL,REAL, a,b,r,s be Real st
for x be Real holds f.x= max(r,min(s, AffineMap (a,b).x))
holds f is Lipschitzian
proof
let f be Function of REAL,REAL;
let a,b,r,s be Real;
assume A1: for x be Real holds f.x= max(r,min(s, AffineMap (a,b).x));
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
per cases;
suppose C0: a = 0;
take 1;
for x1, x2 being Real st x1 in dom f & x2 in dom f holds
|.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).|
proof
let x1, x2 being Real;
assume x1 in dom f & x2 in dom f;
|.((f . x1) - (f . x2)).|
= |.max(r,min(s, AffineMap (a,b).x1))-f.x2.| by A1
.= |.max(r,min(s, AffineMap (a,b).x1))-max(r,min(s, AffineMap (a,b).x2)).|
by A1
.= |.max(r,min(s, a*x1+b))-max(r,min(s, AffineMap (a,b).x2)).|
by FCONT_1:def 4
.= |.max(r,min(s, a*x1+b))-max(r,min(s, a*x2+b)).| by FCONT_1:def 4
.=0 by COMPLEX1:44,C0;
hence thesis by COMPLEX1:46;
end;
hence thesis;
end;
suppose A2: a <> 0;
take |.a.|;
for x1, x2 being Real st x1 in dom f & x2 in dom f holds
|.((f . x1) - (f . x2)).| <= |.a.| * |.(x1 - x2).|
proof
let x1, x2 being Real;
assume x1 in dom f & x2 in dom f;
|.((f . x1) - (f . x2)).|
= |.max(r,min(s, AffineMap (a,b).x1))-f.x2.| by A1
.= |.max(r,min(s, AffineMap (a,b).x1))-max(r,min(s, AffineMap (a,b).x2)).|
by A1
.= |.max(r,min(s, a*x1+b))-max(r,min(s, AffineMap (a,b).x2)).|
by FCONT_1:def 4
.= |.max(r,min(s, a*x1+b))-max(r,min(s, a*x2+b)).| by FCONT_1:def 4; then
|.((f . x1) - (f . x2)).| <= |.a*x1+b- (a*x2+b).| by LeMM01; then
|.((f . x1) - (f . x2)).| <= |.a*(x1- x2).|;
hence |.((f . x1) - (f . x2)).| <= |.a.|*|.x1-x2.| by COMPLEX1:65;
end;
hence thesis by A2,COMPLEX1:47;
end;
end;
hence thesis;
end;
theorem
for f be Function of REAL,REAL, a,b be Real st
for x be Real holds f.x= max(0,min(1, AffineMap (a,b).x))
holds f is Lipschitzian by MMLip3;
theorem:: MM70:
for f be Function of REAL,REAL, a,b be Real st
for x be Real holds f.x= max(0,min(1, AffineMap (a,b).x))
holds f is FuzzySet of REAL by MM40;
theorem
{f where f is Function of REAL,REAL, a,b is Real:
for x be Real holds f.x= max(0,min(1, AffineMap (a,b).x))}
c= Membership_Funcs (REAL)
proof
let g be object;
assume g in {f where f is Function of REAL,REAL, a,b is Real:
for x be Real holds f.x= max(0,min(1, AffineMap (a,b).x))};
then
consider f be Function of REAL,REAL, a,b be Real such that
A1: f=g and
A2: for x be Real holds f.x= max(0,min(1, AffineMap (a,b).x));
g is FuzzySet of REAL by A1,A2,MM40;::MM70;
hence thesis by Def1;
end;
:::: symmetrical Triangular or Trapezoidal Fuzzy Sets
theorem
for a,b be Real, f be Function of REAL,REAL st
(for x be Real holds f.x = max(0,1-|.(x-a)/b.|))
holds f is FuzzySet of REAL
proof
let a,b be Real, f be Function of REAL,REAL;
assume B2: for x be Real holds
f.x = max(0,1-|.(x-a)/b.|);
rng f c= [.0,1.]
proof
let y be object;
assume y in rng f; then
consider x be object such that
B1: x in REAL and B3: y = f . x by FUNCT_2:11;
reconsider x as Real by B1;
0 <= max(0,1-|.(x-a)/b.|) & max(0,1-|.(x-a)/b.|) <= 1
proof
0 <=|.(x-a)/b.| by COMPLEX1:46; then
1+0 <= 1+|.(x-a)/b.| by XREAL_1:7; then
1 - |.(x-a)/b.|<=1+|.(x-a)/b.|-|.(x-a)/b.| by XREAL_1:9;
hence thesis by XXREAL_0:28,XXREAL_0:25;
end;
then
0 <= f.x & f.x <= 1 by B2;
hence thesis by B3;
end; then
f is [.0,1.] -valued;
hence thesis;
end;
LmABS:
for a,x be Real st 0 <= a holds (x <= -a or a <= x) iff a <= |.x.|
proof
let a,x be Real;
assume AS:0 <= a;
hereby assume
A1: x <=-a or a <= x;
per cases;
suppose a = x or -a = x; then
|.a.| = |.x.| by COMPLEX1:52;
hence a <= |.x.| by AS,ABSVALUE:def 1;
end;
suppose not (a = x or -a = x );
then x < -a or a < x by A1,XXREAL_0:1;
hence a <= |.x.| by ABSVALUE:5;
end;
end;
assume A0: a <= |.x.|;
per cases;
suppose a = |.x.|; then
a=x or a=-x by ABSVALUE:1;
hence x <=-a or a <= x;
end;
suppose a <> |.x.|; then
a < |.x.| by A0,XXREAL_0:1;
hence x <=-a or a <= x by ABSVALUE:5;
end;
end;
theorem TR6:
for a,b be Real st b > 0 holds
for x be Real holds
TriangularFS (a-b,a,a+b).x = max(0,1-|.(x-a)/b.|)
proof
let a,b be Real;
assume A1: b>0;
let x be Real;
A2A: 0 + a < b + a by XREAL_1:29,A1; then
A2:a-b < a+b-b & a < a+b by XREAL_1:14;
set f1 = AffineMap (0,0) | (REAL \ ].(a-b),(a+b).[ );
set f2 = AffineMap (1 / (a - (a-b)),- (a-b)/(a-(a-b))) | [.(a-b),a.];
set f3 = AffineMap (- 1/(a+b - a),(a+b)/(a+b-a) ) | [.a,a+b.];
set F = f1 +* f2 +* f3;
P1: dom f1 = REAL \ ].(a-b),(a+b).[ by FUNCT_2:def 1;
P2: dom f2 = [.(a-b),a.] by FUNCT_2:def 1;
P3: dom f3 = [.a,a+b.] by FUNCT_2:def 1;
dom F = dom TriangularFS (a-b,a,a+b) by FUZNUM_1:def 7,A2
.= REAL by FUNCT_2:def 1; then
P66: x in dom (f1+*f2) or x in dom f3 by FUNCT_4:12,XREAL_0:def 1;
F.x = max(0,1-|.(x-a)/b.|)
proof
per cases by P66,FUNCT_4:12;
suppose P610: x in dom f1; then
x in REAL & not x in ].(a-b),(a+b).[ by XBOOLE_0:def 5,P1;
then
P613: x <= a-b or a+b <= x;
per cases;
suppose X0:x=a+b; then
X2B: a<=x by A1,XREAL_1:29;
X3: F.x = f3.x by FUNCT_4:13,P3,X2B,X0,XXREAL_1:1
.= AffineMap (- 1/(a+b - a),(a+b)/(a+b-a) ).x
by FUNCT_1:47,X2B,X0,XXREAL_1:1,P3
.= (- 1/(a+b - a))*x + (a+b)/(a+b-a) by FCONT_1:def 4
.= (- (a+b)*(1/(a+b - a)))+ (a+b)/(a+b-a) by X0
.= (- 1*(a+b)/(a+b - a))+ (a+b)/(a+b-a) by XCMPLX_1:74
.=0;
1-|.(x-a)/b.| = 1 - |.1.| by A1,XCMPLX_1:60,X0
.=1- 1 by ABSVALUE:def 1;
hence F.x = max(0,1-|.(x-a)/b.|) by X3;
end;
suppose X2:x <> a+b;
not (a<=x & x <= a+b) by A2,P613,XXREAL_0:1,XXREAL_0:2,X2; then
not x in dom f3 by P3,XXREAL_1:1; then
P614: F.x = (f1+*f2).x by FUNCT_4:11;
per cases;
suppose X0: x = a-b;
x in [.a-b,a.] by A2,X0; then
X2: x in dom f2 by FUNCT_2:def 1; then
X3: F.x = f2.x by P614,FUNCT_4:13
.= AffineMap (1 / (a - (a-b)),- (a-b)/(a-(a-b))) .x
by FUNCT_1:47,X2
.= ( 1/(a - (a-b)))*x +( - (a-b)/(a-(a-b))) by FCONT_1:def 4
.= ( 1/(a - (a-b)))*(a-b)- (a-b)/(a-(a-b)) by X0
.= ( (a-b)*1/(a - (a-b)))- (a-b)/(a-(a-b)) by XCMPLX_1:74
.=0;
1-|.(x-a)/b.| = 1-|.(-b)/b.| by X0
.= 1-|.-b/b.| by XCMPLX_1:187
.= 1 - |.-1.| by A1,XCMPLX_1:60
.= 1 - |.1.| by COMPLEX1:52
.=1- 1 by ABSVALUE:def 1;
hence
F.x = max(0,1-|.(x-a)/b.|) by X3;
end;
suppose x <> a-b; then
x < a-b or a < x by A2A,P613,XXREAL_0:2,XXREAL_0:1; then
not x in [.a-b,a.] by XXREAL_1:1; then
not x in dom f2 by FUNCT_2:def 1; then
P616:F.x = f1.x by P614,FUNCT_4:11
.=(AffineMap (0,0)) .x by FUNCT_1:47,P610
.=0*x+0 by FCONT_1:def 4
.=0;
x-a <= a-b-a or a+b-a <= x-a by P613,XREAL_1:13; then
P617: (x-a)/b <= (a-b-a)/b or (a+b-a)/b <= (x-a)/b by A1,XREAL_1:72;
(a-b-a)/b = (-b)/b
.=-b/b by XCMPLX_1:187
.=-1 by A1,XCMPLX_1:60; then
(x-a)/b <= -1 or 1 <= (x-a)/b by P617,A1,XCMPLX_1:60; then
1 <= |.(x-a)/b.| by LmABS;
hence F.x = max(0,1-|.(x-a)/b.|) by P616,XXREAL_0:def 10,XREAL_1:47;
end;
end;
end;
suppose P710: x in dom f2; then :::::: [.a-b,a.]
P711: a-b <= x & x <= a by P2,XXREAL_1:1;
per cases;
suppose P713:x=a;
a <= a+b by P713,P711,XREAL_1:20; then
P714:x in dom f3 by P713,P3;
P715: F.x = f3.x by FUNCT_4:13,P714
.= AffineMap (- 1/(a+b - a),(a+b)/(a+b-a) ).x
by FUNCT_1:47,P714
.= (- 1/(a+b - a))*x + (a+b)/(a+b-a) by FCONT_1:def 4
.=- (1/b*a) + (a+b)/b by P713
.=- (a*1/b) + (a+b)/b by XCMPLX_1:74
.=(a+b)/b- (a/b)
.= ((a+b)-a)/b by XCMPLX_1:120
.=1 by XCMPLX_1:60,A1;
1-|.(x-a)/b.| = 1- 0 by ABSVALUE:def 1,P713; then
max(0,1-|.(x-a)/b.|) = 1 by XXREAL_0:def 10;
hence F.x = max(0,1-|.(x-a)/b.|) by P715;
end;
suppose M1: x<>a; then
P716:x<a by P711,XXREAL_0:1;
x < a or a+b < x by M1,P711,XXREAL_0:1; then
not x in [.a,a+b.] by XXREAL_1:1; then
not x in dom f3 by FUNCT_2:def 1; then
P777:F.x = (f1+*f2).x by FUNCT_4:11
.= f2.x by P710,FUNCT_4:13
.= AffineMap (1 / (a - (a-b)),- (a-b)/(a-(a-b))).x
by FUNCT_1:49,P710,P2
.=1 / (a - (a-b))*x +(- (a-b)/(a-(a-b))) by FCONT_1:def 4
.=x*1 / (a - (a-b)) +(- (a-b)/(a-(a-b))) by XCMPLX_1:74
.=x*1 / (a - a+b) - (a-b)/(a-a+b)
.=(x-(a-b))/b by XCMPLX_1:120;
x-a<a-a by XREAL_1:9, P716; then
P77:1-|.(x-a)/b.| = 1--(x-a)/b by ABSVALUE:def 1,A1
.= 1+(x-a)/b
.=b/b+(x-a)/b by XCMPLX_1:60,A1
.=(b+(x-a))/b by XCMPLX_1:62
.=(x-(a-b))/b;
a-b <= x by P710,P2,XXREAL_1:1; then
(a-b)-(a-b)<=x-(a-b) by XREAL_1:9; then
max(0,1-|.(x-a)/b.|) = (x-(a-b))/b by XXREAL_0:def 10,P77,A1;
hence thesis by P777;
end;
end;::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
suppose P810: x in dom f3;
then
P811: a <= x & x <= a+b by XXREAL_1:1,P3;
P812:x in dom (f2+*f3) by FUNCT_4:12,P810;
P888:F.x = (f1 +* (f2+*f3)).x by FUNCT_4:14
.= (f2+*f3).x by FUNCT_4:13,P812
.= f3.x by FUNCT_4:13,P810
.= AffineMap (- 1/(a+b - a),(a+b)/(a+b-a) ).x
by FUNCT_1:49,P810,P3
.=(-1 /(a+b - a))*x + (a+b)/(a+b-a) by FCONT_1:def 4
.=-1 /(a+b - a)*x + (a+b)/(a+b-a)
.=-x*1 /(a+b - a) + (a+b)/(a+b-a) by XCMPLX_1:74
.=(a+b)/b -x/b
.=((a+b)-x)/b by XCMPLX_1:120;
x-a >= a-a by XREAL_1:9,P811; then
P88:1-|.(x-a)/b.| = 1-(x-a)/b by ABSVALUE:def 1,A1
.= b/b-(x-a)/b by XCMPLX_1:60,A1
.= (b-(x-a))/b by XCMPLX_1:120
.= (b-x+a)/b;
x-x <= a+b-x by XREAL_1:9,P811; then
max(0,1-|.(x-a)/b.|) = (b-x+a)/b by XXREAL_0:def 10,P88,A1;
hence thesis by P888;
end;
end;
hence thesis by FUZNUM_1:def 7,A2;
end;
theorem
for a,b be Real, f be FuzzySet of REAL st
b > 0 & (for x be Real holds f.x = max(0,1-|.(x-a)/b.|))
holds f is triangular
proof
let a,b be Real;
let f be FuzzySet of REAL;
assume A1: b>0;
assume A2: for x be Real holds f.x = max(0,1-|.(x-a)/b.|);
take a-b,a,a+b;
A4: dom TriangularFS (a-b,a,a+b) = REAL &
dom f = REAL by FUNCT_2:def 1;
for x being object st x in dom f holds
f . x = TriangularFS (a-b,a,a+b).x
proof
let x be object;
assume x in dom f; then
reconsider x as Real by A4;
f . x = max(0,1-|.(x-a)/b.|) by A2
.= TriangularFS (a-b,a,a+b).x by A1,TR6;
hence thesis;
end;
hence thesis by FUNCT_1:2,A4;
end;
theorem:: TR8:
for a,b be Real, f be FuzzySet of REAL st
b > 0 & (for x be Real holds f.x = max(0,1-|.(x-a)/b.|))
holds f is strictly-normalized
proof
let a,b be Real;
let f be FuzzySet of REAL;
assume A1: b>0;
assume A2: for x be Real holds f.x = max(0,1-|.(x-a)/b.|);
ex x being Element of REAL st
( f . x = 1 & ( for y being Element of REAL st f . y = 1 holds y = x ) )
proof
A4:a is Element of REAL by XREAL_0:def 1;
take a;
A3: f.a = max(0,1-|.(a-a)/b.|) by A2
.= max(0,1-0) by ABSVALUE:def 1
.= 1 by XXREAL_0:def 10;
for y being Element of REAL st f . y = 1 holds y = a
proof
let y be Element of REAL;
assume f.y=1; then
max(0,1-|.(y-a)/b.|)=1 by A2; then
1-|.(y-a)/b.|=1 by XXREAL_0:16; then
y-a=0 by A1,ABSVALUE:2;
hence y=a;
end;
hence thesis by A4,A3;
end;
hence thesis;
end;
theorem MM60:
for f be Function of REAL,REAL, a,b,c be Real st
(for x be Real holds f.x= max(0,min(1, c*(1-|.(x-a)/b.|))) )
holds f is FuzzySet of REAL
proof
let f be Function of REAL,REAL;
let a,b,c be Real;
assume A2: for x be Real holds f.x= max(0,min(1, c*(1-|.(x-a)/b.|)));
ex g being Function of REAL,REAL st
for x be Real holds g.x= c*(1-|.(x-a)/b.|)
proof
deffunc H1(Element of REAL) = In(c*(1-|.($1-a)/b.|),REAL);
consider f being Function of REAL,REAL such that
A1: for x being Element of REAL holds f.x = H1(x) from FUNCT_2:sch 4;
take f;
for x be Real holds f.x= c*(1-|.(x-a)/b.|)
proof
let x be Real;
reconsider x as Element of REAL by XREAL_0:def 1;
f.x = H1(x) by A1;
hence thesis;
end;
hence thesis;
end; then
consider g being Function of REAL,REAL such that
A4:for x be Real holds g.x= c*(1-|.(x-a)/b.|);
for x be Real holds f.x= max(0,min(1, g.x))
proof
let x be Real;
f.x = max(0,min(1, c*(1-|.(x-a)/b.|))) by A2
.= max(0,min(1, g.x)) by A4;
hence thesis;
end;
hence thesis by MM40;
end;
theorem
for f be Function of REAL,REAL, a,b be Real st
b>0 & for x be Real holds f.x = max(0,1-|.(x-a)/b.|)
holds f is continuous
proof
let f be Function of REAL,REAL, a,b be Real;
assume A2:b>0; then
A4:a-b<a & a<a+b by XREAL_1:44,XREAL_1:29;
assume A1: for x be Real holds f.x = max(0,1-|.(x-a)/b.|);
f=TriangularFS (a-b,a,a+b)
proof
A6:dom f = REAL & REAL=dom TriangularFS (a-b,a,a+b) by FUNCT_2:def 1;
for x being object st x in dom f holds
f . x = TriangularFS (a-b,a,a+b) . x
proof
let x be object;
assume x in dom f; then
x in REAL by FUNCT_2:def 1; then
reconsider x as Real;
f.x=max(0,1-|.(x-a)/b.|) by A1;
hence thesis by TR6,A2;
end;
hence thesis by FUNCT_1:2, A6;
end;
hence thesis by A4,FUZNUM_1:30;
end;
theorem MMLip2:
for f be Function of REAL,REAL, a,b,c,r,s be Real st
( b <> 0 & for x be Real holds f.x= max(r,min(s, c*(1-|.(x-a)/b.|))) )
holds f is Lipschitzian
proof
let f be Function of REAL,REAL;
let a,b,c,r,s be Real;
assume A3: b <> 0;
assume A1: for x be Real holds f.x= max(r,min(s, c*(1-|.(x-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
per cases;
suppose C0: c = 0;
take 1;
for x1, x2 being Real st x1 in dom f & x2 in dom f holds
|.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).|
proof
let x1, x2 be Real;
|.((f . x1) - (f . x2)).|
= |.max(r,min(s, c*(1-|.(x1-a)/b.|)))-f.x2.| by A1
.= |.max(r,min(s, 0*(1-|.(x1-a)/b.|)))-max(r,min(s, 0*(1-|.(x2-a)/b.|))).|
by C0,A1
.=0 by COMPLEX1:44;
hence thesis by COMPLEX1:46;
end;
hence thesis;
end;
suppose A2: c <> 0;
take 1/|.b.|*|.c.|;
A5: |.c.|>0 & |.b.|>0 by A2,A3,COMPLEX1:47;
for x1, x2 being Real st x1 in dom f & x2 in dom f holds
|.((f . x1) - (f . x2)).| <= (1/|.b.|*|.c.|) * |.(x1 - x2).|
proof
let x1, x2 be Real;
assume x1 in dom f & x2 in dom f;
|.((f . x1) - (f . x2)).|
= |.max(r,min(s, c*(1-|.(x1-a)/b.|)))-f.x2.| by A1
.= |.max(r,min(s, c*(1-|.(x1-a)/b.|)))-max(r,min(s, c*(1-|.(x2-a)/b.|))).|
by A1; then
A9: |.((f . x1) - (f . x2)).|
<= |.c*(1-|.(x1-a)/b.|)-c*(1-|.(x2-a)/b.|).| by LeMM01;
|.(x1-a)/b-(x2-a)/b.| = |.((x1-a)-(x2-a))/b.| by XCMPLX_1:120
.= |.(x1-x2).|/|.b.| by COMPLEX1:67; then
|.|.(x1-a)/b.|-|.(x2-a)/b.|.|*|.c.|<= |.(x1-x2).|/|.b.| * |.c.| by
XREAL_1:64,A5,COMPLEX1:64; then
|.c.|* |.|.(x2-a)/b.|-|.(x1-a)/b.|.|<= |.(x1-x2).|/|.b.| * |.c.|
by COMPLEX1:60; then
|.c*(-|.(x1-a)/b.|+|.(x2-a)/b.|).|<= |.(x1-x2).|/|.b.| * |.c.|
by COMPLEX1:65; then
|.c*(1-|.(x1-a)/b.|)-c*(1-|.(x2-a)/b.|).|<= (1/|.b.|* |.c.|)*|.(x1-x2).|
by XCMPLX_1:101;
hence thesis by XXREAL_0:2,A9;
end;
hence thesis by A5;
end;
end;
hence thesis;
end;
theorem
for f be Function of REAL,REAL, a,b,c be Real st
( b <> 0 & for x be Real holds f.x= max(0,min(1, c*(1-|.(x-a)/b.|))) )
holds f is Lipschitzian by MMLip2;
TR2XX:
{TriangularFS (a,b,c) where a,b,c is Real : a < b & b < c}
c= Membership_Funcs (REAL)
proof
let x be object;
assume x in{TriangularFS (a,b,c) where a,b,c is Real:a < b & b < c};
then
ex a,b,c be Real st x=TriangularFS (a,b,c) & a < b & b < c;
hence thesis by Def1;
end;
theorem
{f where f is Function of REAL,REAL, a,b is Real:
b > 0 & for x be Real holds f.x = max(0,1-|.(x-a)/b.|)}
c= Membership_Funcs (REAL)
proof
{f where f is Function of REAL,REAL, a,b is Real:
b > 0 & for x be Real holds f.x = max(0,1-|.(x-a)/b.|)}c=
{TriangularFS (a,b,c) where a,b,c is Real:a < b & b < c}
proof
let f be object;
assume f in {f where f is Function of REAL,REAL, a,b is Real:
b > 0 & for x be Real holds f.x = max(0,1-|.(x-a)/b.|)}; then
consider f0 be Function of REAL,REAL, a,b be Real such that
A1:f=f0 and A2:b>0 and
A3:for x be Real holds f0.x = max(0,1-|.(x-a)/b.|);
A4:a-b<a & a<a+b by XREAL_1:44,XREAL_1:29,A2;
f=TriangularFS (a-b,a,a+b)
proof
reconsider f as Function of REAL,REAL by A1;
A6:dom f = REAL & REAL=dom TriangularFS (a-b,a,a+b) by FUNCT_2:def 1;
for x being object st x in dom f holds
f . x = TriangularFS (a-b,a,a+b) . x
proof
let x be object;
assume x in dom f; then
x in REAL by FUNCT_2:def 1; then
reconsider x as Real;
f.x=max(0,1-|.(x-a)/b.|) by A1,A3;
hence thesis by TR6,A2;
end;
hence thesis by FUNCT_1:2, A6;
end;
hence thesis by A4;
end;
hence thesis by TR2XX;
end;
theorem
{f where f is Function of REAL,REAL, a,b,c,d is Real:
b <> 0 & for x be Real holds f.x= max(0,min(1, c*(1-|.(x-a)/b.|)))}
c= Membership_Funcs (REAL)
proof
let g be object;
assume g in {f where f is Function of REAL,REAL, a,b,c,d is Real:
b <> 0 & for x be Real holds f.x= max(0,min(1, c*(1-|.(x-a)/b.|)))}; then
consider f be Function of REAL,REAL, a,b,c,d be Real such that
A1: f=g and
b <> 0 and
A2: for x be Real holds f.x= max(0,min(1, c*(1-|.(x-a)/b.|)));
g is FuzzySet of REAL by A1,A2,MM60;
hence thesis by Def1;
end;
:::: asymmetry Trapezoidal or Triangular membership function
theorem asymTT10:
for a,b,p,q,s be Real holds
( AffineMap (a,b)|].-infty,s.[ ) +* ( AffineMap (p,q)|[.s,+infty.[ )
is Function of REAL,REAL
proof
let a,b,p,q,s be Real;
set g = ( ((AffineMap (a,b))|(].-infty,s.[)) +*
((AffineMap (p,q))|([.s,+infty.[)) );
set g1= ( (AffineMap (a,b))|(].-infty,s.[) );
set g2= ( (AffineMap (p,q))|([.s,+infty.[) );
D3: -infty < s & s < +infty by XXREAL_0:9,XXREAL_0:12,XREAL_0:def 1;
Dg: dom g = (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 g . x in REAL by XREAL_0:def 1;
hence thesis by FUNCT_2:3,Dg;
end;
theorem:: asymTT1:
for a,b,p,q be Real, f be Function of REAL,REAL st
for x be Real holds
f.x = max(0,min(1, ( ((AffineMap (a,b))|(].-infty,(q-b)/(a-p).[)) +*
((AffineMap (p,q))|([.(q-b)/(a-p),+infty.[)) ) .x ))
holds f is FuzzySet of REAL
proof
let a,b,p,q be Real;
let f be Function of REAL,REAL;
assume
A3: for x be Real holds
f.x = max(0,min(1, ( ((AffineMap (a,b))|(].-infty,(q-b)/(a-p).[)) +*
((AffineMap (p,q))|([.(q-b)/(a-p),+infty.[)) ) .x ));
set g = ( ((AffineMap (a,b))|(].-infty,(q-b)/(a-p).[)) +*
((AffineMap (p,q))|([.(q-b)/(a-p),+infty.[)) );
reconsider g as Function of REAL,REAL by asymTT10;
for x being Real holds f.x= max(0,min(1, g.x)) by A3;
hence thesis by MM40;
end;
theorem TrAng1:
for a,b,c be Real st a<b & b<c holds
TriangularFS (a,b,c). a = 0 &
TriangularFS (a,b,c). b = 1 &
TriangularFS (a,b,c). c = 0
proof
let a,b,c be Real;
assume A1: a<b & b<c; then
X1a: b-b < c -b by XREAL_1:9;
set f1=((AffineMap (0,0)) | (REAL \ ].a,c.[));
set f2= (AffineMap (1/(b - a),- (a / (b - a))) | [.a,b.]);
set f3=((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]);
P2: dom f2 = [.a,b.] by FUNCT_2:def 1;
P3: dom f3 = [.b,c.] by FUNCT_2:def 1; then
P8: not a in dom f3 by XXREAL_1:1,A1;
P9: a in dom f2 by P2,A1;
FA: TriangularFS (a,b,c).a = (f1+*f2+*f3).a by FUZNUM_1:def 7,A1
.= (f1+*f2).a by FUNCT_4:11,P8
.= f2.a by FUNCT_4:13,P9
.= (AffineMap (1/(b - a),- (a / (b - a)))).a by FUNCT_1:47,P9
.= (1/(b - a))*a + (- (a / (b - a))) by FCONT_1:def 4
.=(a*1)/(b - a) + (- (a / (b - a))) by XCMPLX_1:74
.=0;
B0: b in dom f3 by P3,A1;
FB: TriangularFS (a,b,c).b = (f1+*f2+*f3).b by FUZNUM_1:def 7,A1
.= f3.b by FUNCT_4:13,B0
.= (AffineMap ((- (1 / (c - b))),(c / (c - b)))).b by FUNCT_1:47,B0
.= (- (1 / (c - b)))*b + c / (c - b) by FCONT_1:def 4
.= (- b*(1 / (c - b))) + c / (c - b)
.= - ((b*1) / (c - b)) + c / (c - b) by XCMPLX_1:74
.= (-b) / (c - b) + c / (c - b) by XCMPLX_1:187
.= ( - b+c) / (c - b) by XCMPLX_1:62
.=1 by XCMPLX_1:60,X1a;
C0: c in dom f3 by P3,A1;
TriangularFS (a,b,c).c = (f1+*f2+*f3).c by FUZNUM_1:def 7,A1
.= f3.c by FUNCT_4:13,C0
.= (AffineMap ((- (1 / (c - b))),(c / (c - b)))).c by FUNCT_1:47,C0
.= (- (1 / (c - b)))*c + c / (c - b) by FCONT_1:def 4
.= (- c*(1 / (c - b))) + c / (c - b)
.= - (c*1) / (c - b) + c / (c - b) by XCMPLX_1:74
.=0;
hence thesis by FA,FB;
end;
theorem TrZoi1:
for a,b,c,d be Real st a < b & b < c & c < d holds
TrapezoidalFS (a,b,c,d). a = 0 &
TrapezoidalFS (a,b,c,d). b = 1 &
TrapezoidalFS (a,b,c,d). c = 1 &
TrapezoidalFS (a,b,c,d). d = 0
proof
let a,b,c,d be Real;
assume A1: a<b & b<c & c < d; then
AA1: a in [.a,b.];
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.]);
D2: dom f2 = [.a,b.] by FUNCT_2:def 1;
D3: dom f3 = [.b,c.] by FUNCT_2:def 1;
D4: dom f4 = [.c,d.] by FUNCT_2:def 1;
AA2: a in dom f2 by D2,A1;
AA4: dom (f3 +* f4)= (dom f3 \/ dom f4) by FUNCT_4:def 1
.= ([.b,c.] \/ dom f4) by FUNCT_2:def 1
.= ([.b,c.] \/ [.c,d.]) by FUNCT_2:def 1
.= [. b,d .] by XXREAL_1:165,A1;
AA3: not a in dom (f3+*f4) by AA4,XXREAL_1:1,A1;
AA: (f1+*f2+*f3+*f4).a = (f1 +* f2 +* (f3 +* f4)).a by FUNCT_4:14
.= (f1+*f2).a by FUNCT_4:11,AA3
.= f2.a by FUNCT_4:13,AA2
.=(AffineMap (1/(b - a),- (a / (b - a))) ).a by FUNCT_1:49,AA1
.=0 by FUZNUM_1:2;
B1: b in [.b,c.] by A1;
B0: b in dom f3 by D3,A1;
B2: not b in dom f4 by D4,XXREAL_1:1,A1;
BB: (f1+*f2+*f3+*f4).b = (f1+*f2+*f3).b by FUNCT_4:11,B2
.= f3.b by FUNCT_4:13,B0
.= (AffineMap (0,1)).b by FUNCT_1:49,B1
.= 0*b+1 by FCONT_1:def 4
.= 1;
A4: d-c <>0 by A1;
C2: c in [.c,d.] by A1;
C1: c in dom f4 by D4,A1;
CC: (f1+*f2+*f3+*f4).c =f4.c by FUNCT_4:13,C1
.= (AffineMap ((- (1 / (d - c))),(d / (d - c))) ).c by FUNCT_1:49,C2
.= 1 by FUZNUM_1:4,A4;
AD1: d in [.c,d.] by A1;
AD2: d in dom f4 by D4,A1;
(f1+*f2+*f3+*f4).d = f4.d by FUNCT_4:13,AD2
.= (AffineMap ((- (1 / (d - c))),(d / (d - c))) ).d by FUNCT_1:49,AD1
.=0 by FUZNUM_1:5;
hence thesis by AA,BB,CC,FUZNUM_1:def 8,A1;
end;
theorem asymTT6:
for a,b,p,q be Real st
a > 0 & p > 0 & (-b)/a < q/p & (1-b)/a = (1-q)/(-p) holds
for x be Real holds
(TriangularFS ((-b)/a,(1-b)/a,q/p)).x
= max(0,min(1, ((AffineMap (a,b) |].-infty,(q-b)/(a+p).[) +*
(AffineMap (-p,q)|[.(q-b)/(a+p),+infty.[)).x ))
proof
let a,b,p,q be Real;
assume A2: a > 0;
assume A3: p > 0;
assume A4:(-b)/a < q/p;
assume A5: (1-b)/a = (1-q)/(-p);
0+(-q) < 1+(-q) & -p < 0 by A3, XREAL_1:8; then
A6:(1-q)/(-p)< (-q)/(-p) by XREAL_1:75;
0+(-b) < 1+(-b) by XREAL_1:8; then
A0: (-b)/a < (1-b)/a & (1-b)/a < q/p by XREAL_1:74,A2,A5,A6,XCMPLX_1:191;
set f1 = ( AffineMap (0,0) | (REAL \ ].(-b)/a,q/p.[));
set f2 = ( AffineMap (1/((1-b)/a - (-b)/a),-(((-b)/a)/((1-b)/a-((-b)/a))) )
| ([.(-b)/a,(1-b)/a.]));
set f3 = ( AffineMap ( -(1/((q/p)-(1-b)/a)),(q/p)/((q/p)-(1-b)/a) )
| [.(1-b)/a,q/p.] );
set f4 = ( AffineMap (a,b)|(].-infty,(q-b)/(a+p).[) );
set f5 = ( AffineMap (-p,q)|([.(q-b)/(a+p),+infty.[) );
D2: dom f2 =[.(-b)/a,(1-b)/a.] by FUNCT_2:def 1;
D3: dom f3 =[.(1-b)/a,q/p.] by FUNCT_2:def 1;
D5: dom f5 =[.(q-b)/(a+p),+infty.[ by FUNCT_2:def 1;
for x be Real holds
(TriangularFS ((-b)/a,(1-b)/a,q/p)).x
= max(0,min(1, ( ((AffineMap (a,b))|(].-infty,(q-b)/(a+p).[)) +*
((AffineMap (-p,q))|([.(q-b)/(a+p),+infty.[)) ) .x ))
proof
let x be Real;
per cases;
suppose B1: x <= (-b)/a;
(-b)/a < (q-b)/(a+p) by asymTT2,A2,A3,A4; then
B15: x < (q-b)/(a+p) by B1,XXREAL_0:2;
per cases;
suppose N2: x= (-b)/a; then
N3: (TriangularFS ((-b)/a,(1-b)/a,q/p)).x = 0 by TrAng1,A0;
max(0,min(1, ( ((AffineMap (a,b))|(].-infty,(q-b)/(a+p).[)) +*
((AffineMap (-p,q))|([.(q-b)/(a+p),+infty.[)) ) .x))
=max(0,min(1, ( (AffineMap (a,b))|(].-infty,(q-b)/(a+p).[)).x))
by FUNCT_4:11,D5,XXREAL_1:236,B15
.=max(0,min(1, (AffineMap (a,b)).x)) by FUNCT_1:49,XXREAL_1:233,B15
.=max(0,min(1, (a*x+b))) by FCONT_1:def 4
.=max(0,min(1, (a/a*(-b)+b))) by XCMPLX_1:75,N2
.=max(0,min(1, (1*(-b)+b))) by XCMPLX_1:60,A2
.= 0 by XXREAL_0:36;
hence thesis by N3;
end;
suppose N1: x <> (-b)/a; ::::: x < -b/a
not x in ].(-b)/a,q/p.[ & x in REAL by B1,XREAL_0:def 1,XXREAL_1:4; then
B14: x in REAL \ ].(-b)/a,q/p.[ by XBOOLE_0:def 5;
B17: dom(f2 +* f3) = (dom f2) \/ (dom f3) by FUNCT_4:def 1
.= ([.(-b)/a,(1-b)/a.]) \/ (dom f3) by FUNCT_2:def 1
.=([.(-b)/a,(1-b)/a.]) \/ ([.(1-b)/a,q/p.]) by FUNCT_2:def 1
.=[.(-b)/a,q/p.] by XXREAL_1:165,A0;
B16: x < (-b)/a by B1,N1,XXREAL_0:1; then
B11: not x in dom(f2 +* f3) by XXREAL_1:1,B17;
x*a < (-b)/a*a by XREAL_1:68,A2,B16; then
x*a < a/a*(-b) by XCMPLX_1:75; then
x*a < 1*(-b) by XCMPLX_1:60,A2; then
B150a: x*a+b < -b+b by XREAL_1:6;
B10:(f1 +* f2 +* f3).x = (f1 +* (f2 +* f3)).x by FUNCT_4:14
.= f1.x by FUNCT_4:11,B11
.= AffineMap (0,0).x by FUNCT_1:49,B14
.= 0*x+0 by FCONT_1:def 4
.=0;
max(0,min(1, ( ((AffineMap (a,b))|(].-infty,(q-b)/(a+p).[)) +*
((AffineMap (-p,q))|([.(q-b)/(a+p),+infty.[)) ) .x))
=max(0,min(1, ( (AffineMap (a,b))|(].-infty,(q-b)/(a+p).[)).x))
by FUNCT_4:11,D5,XXREAL_1:236,B15
.=max(0,min(1, (AffineMap (a,b)).x)) by FUNCT_1:49,XXREAL_1:233,B15
.=max(0,min(1, (a*x+b))) by FCONT_1:def 4
.=max(0,(a*x+b)) by B150a,XXREAL_0:def 9
.= 0 by B150a,XXREAL_0:def 10;
hence thesis by B10,FUZNUM_1:def 7,A0;
end;
end; ::::::B1
suppose B2: (-b)/a < x; then
(-b)/a*a < x*a by XREAL_1:68,A2; then
a/a*(-b) < x*a by XCMPLX_1:75; then
1*(-b) < x*a by XCMPLX_1:60,A2; then
B2Xa: -b+b < x*a +b by XREAL_1:6;
per cases;
suppose B3: x < (1-b)/a; then
x*a < (1-b)/a*a by XREAL_1:68,A2; then
x*a < a/a*(1-b) by XCMPLX_1:75; then
x*a < 1*(1-b) by XCMPLX_1:60,A2; then
B3Xa: x*a+b < 1-b+b by XREAL_1:6;
B33: x in [.(-b)/a,(1-b)/a.] by B3,B2;
B32: x in dom f2 by D2,B3,B2;
B31: not x in dom f3 by D3,XXREAL_1:1,B3;
B34: (TriangularFS ((-b)/a,(1-b)/a,q/p)).x
=(f1 +* f2 +* f3).x by FUZNUM_1:def 7,A0
.= (f1+*f2).x by FUNCT_4:11,B31
.=f2.x by FUNCT_4:13,B32
.= AffineMap (1/((1-b)/a+-(-b)/a),-((-b)/a)/((1-b)/a+-(-b)/a) ).x
by FUNCT_1:49,B33
.= AffineMap (1/((1-b)/a+-(-b)/a),-((-b)/a)/((1-b)/a+b/a) ).x
by XCMPLX_1:190
.= AffineMap (1/((1-b)/a+b/a),-((-b)/a)/((1-b)/a+b/a) ).x
by XCMPLX_1:190
.= AffineMap (1/((1-b)/a+b/a),-((-b)/a)/((1-b+b)/a) ).x by XCMPLX_1:62
.= AffineMap (1/((1-b+b)/a),- ((-b)/a) / (1/a) ).x by XCMPLX_1:62
.= AffineMap (1/(1/a),- ((-b)/a)*a ).x by XCMPLX_1:100
.= AffineMap ( a*(1/1),-((-b)/a)*a ).x by XCMPLX_1:81
.= AffineMap ( a,-(a/a)*(-b) ).x by XCMPLX_1:75
.= AffineMap ( a,-1*(-b) ).x by XCMPLX_1:60,A2
.= AffineMap ( a,b ).x;
B38: x < (q-b)/(a+p) by B3,asymTT3,A2,A3,A5;
max(0,min(1, ( ((AffineMap (a,b))|(].-infty,(q-b)/(a+p).[)) +*
((AffineMap (-p,q))|([.(q-b)/(a+p),+infty.[)) ) .x ))
= max(0,min(1, (AffineMap (a,b)|(].-infty,(q-b)/(a+p).[)).x ))
by FUNCT_4:11,D5,XXREAL_1:236,B38
.= max(0,min(1, (AffineMap (a,b)).x )) by FUNCT_1:49,B38,XXREAL_1:233
.= max(0,min(1, a*x+b )) by FCONT_1:def 4
.=max(0, a*x+b ) by XXREAL_0:def 9,B3Xa
.=a*x+b by XXREAL_0:def 10, B2Xa;
hence thesis by FCONT_1:def 4,B34;
end; :::::::::::::::::::::::::::::::::: :::::::B3
suppose B4: (1-b)/a <= x; then
B41a: (q-b)/(a+p) <= x by asymTT3,A2,A3,A5;
(1-q)/(-p)*(-p) >= x*(-p) by XREAL_1:65,A3,B4,A5; then
(-p)/(-p)*(1-q) >= x*(-p) by XCMPLX_1:75; then
1*(1-q) >= x*(-p) by XCMPLX_1:60,A3; then
B43a: (-p)*x+q <= 1-q+q by XREAL_1:6;
B44: max(0,min(1, ( ((AffineMap (a,b))|(].-infty,(q-b)/(a+p).[)) +*
((AffineMap (-p,q))|([.(q-b)/(a+p),+infty.[)) ) .x ))
= max(0,min(1, (AffineMap (-p,q)|([.(q-b)/(a+p),+infty.[)).x ))
by FUNCT_4:13,D5,B41a,XXREAL_1:236
.= max(0,min(1, (AffineMap (-p,q)).x ))
by FUNCT_1:49,B41a,XXREAL_1:236
.= max(0,min(1, (-p)*x+q )) by FCONT_1:def 4
.= max(0,(-p)*x+q ) by XXREAL_0:def 9,B43a;
per cases;
suppose B5: x < q/p; then
B53: x in [.(1-b)/a,q/p.] by B4;
x*p < q/p*p by XREAL_1:68,A3,B5; then
x*p < p/p*q by XCMPLX_1:75; then
x*p < 1*q by XCMPLX_1:60,A3; then
B54a: x*p - x*p < q - p*x by XREAL_1:9;
(TriangularFS ((-b)/a,(1-b)/a,q/p)).x
=(f1 +* f2 +* f3).x by FUZNUM_1:def 7,A0
.= f3.x by FUNCT_4:13,B53,D3
.= (AffineMap ( -1/(q/p-(1-b)/a),(q/p)/(q/p-(1-b)/a) )).x
by FUNCT_1:49,B53
.= (AffineMap ( -1/( q/p+(1-q)/p ),(q/p)/(q/p+-(1-q)/(-p)) )).x
by XCMPLX_1:189,A5
.= (AffineMap ( -1/( q/p+(1-q)/p ),(q/p)/(q/p+(1-q)/p) )).x
by XCMPLX_1:189
.= (AffineMap ( -1/( (q+(1-q))/p ),(q/p)/(q/p+(1-q)/p) )).x
by XCMPLX_1:62
.= (AffineMap ( -1/( 1/p ),(q/p)/((q+(1-q))/p) )).x by XCMPLX_1:62
.= (AffineMap ( -p,(q/p)/(1/p) )).x by XCMPLX_1:56
.= (AffineMap ( -p,(q/p)*p )).x by XCMPLX_1:100
.= (AffineMap ( -p,q )).x by XCMPLX_1:87,A3
.= (-p)*x+q by FCONT_1:def 4
.= max(0,(-p)*x+q ) by XXREAL_0:def 10,B54a;
hence thesis by B44;
end; :::::::::::B5
suppose B6: q/p <= x; then
not x in ].(-b)/a,q/p.[ & x in REAL by XREAL_0:def 1,XXREAL_1:4; then
B14: x in REAL \ ].(-b)/a,q/p.[ by XBOOLE_0:def 5;
B17: dom(f2 +* f3) = (dom f2) \/ (dom f3) by FUNCT_4:def 1
.= ([.(-b)/a,(1-b)/a.]) \/ (dom f3) by FUNCT_2:def 1
.=([.(-b)/a,(1-b)/a.]) \/ ([.(1-b)/a,q/p.]) by FUNCT_2:def 1
.=[.(-b)/a,q/p.] by XXREAL_1:165,A0;
TT2: (q-b)/(a+p) < q/p by asymTT2,A2,A3,A4; then
B62: x in [.(q-b)/(a+p),+infty.[ by XXREAL_1:236,B6,XXREAL_0:2;
B61: x in dom f5 by D5,XXREAL_1:236,B6,XXREAL_0:2,TT2;
per cases;
suppose N3: x = q/p; then
B66: (TriangularFS ((-b)/a,(1-b)/a,q/p)).x = 0 by TrAng1,A0;
max(0,min(1, ( ((AffineMap (a,b))|(].-infty,(q-b)/(a+p).[)) +*
((AffineMap (-p,q))|([.(q-b)/(a+p),+infty.[)) ) .x))
=max(0,min(1, ( (AffineMap (-p,q))|([.(q-b)/(a+p),+infty.[)).x))
by FUNCT_4:13,B61
.=max(0,min(1, (AffineMap (-p,q)).x)) by FUNCT_1:49,B62
.=max(0,min(1, (-p)*x+q )) by FCONT_1:def 4
.=max(0,min(1, -(p*(q/p))+q )) by N3
.=max(0,min(1, -(p*q)/p+q )) by XCMPLX_1:74
.=max(0,min(1, -(q)+q )) by XCMPLX_1:89,A3
.=max(0,0) by XXREAL_0:def 9
.= 0;
hence thesis by B66;
end;
suppose N4: x <> q/p; then
not ((-b)/a <= x & x <= q/p) by B6,XXREAL_0:1; then
B11: not x in dom(f2 +* f3) by XXREAL_1:1,B17;
x > q/p by B6,N4,XXREAL_0:1; then
x*p>q/p*p by XREAL_1:68,A3; then
x*p > p/p*q by XCMPLX_1:75; then
x*p > 1*q by XCMPLX_1:60,A3; then
B63a: x*p - x*p > q - p*x by XREAL_1:9;
B60:(f1 +* f2 +* f3).x = (f1 +* (f2 +* f3)).x by FUNCT_4:14
.= f1.x by FUNCT_4:11,B11
.= AffineMap (0,0).x by FUNCT_1:49,B14
.= 0*x+0 by FCONT_1:def 4
.=0;
max(0,min(1, ( ((AffineMap (a,b))|(].-infty,(q-b)/(a+p).[)) +*
((AffineMap (-p,q))|([.(q-b)/(a+p),+infty.[)) ) .x))
=max(0,min(1, ( (AffineMap (-p,q))|([.(q-b)/(a+p),+infty.[)).x))
by FUNCT_4:13,B61
.=max(0,min(1, (AffineMap (-p,q)).x)) by FUNCT_1:49,B62
.=max(0,min(1, (-p)*x+q )) by FCONT_1:def 4
.=max(0,(-p)*x+q) by B63a,XXREAL_0:def 9
.= 0 by B63a,XXREAL_0:def 10;
hence thesis by B60,FUZNUM_1:def 7,A0;
end;
end; ::::::::::::B6
end; :::::::::B4
end; :::::::::B2
end;
hence thesis;
end;
theorem asymTT7:
for a,b,p,q be Real st
a > 0 & p > 0 & (1-b)/a < (1-q)/(-p) holds
for x be Real holds
(TrapezoidalFS ((-b)/a,(1-b)/a,(1-q)/(-p),q/p)).x
= max(0,min(1, ( (AffineMap (a,b) |].-infty,(q-b)/(a+p).[) +*
(AffineMap (-p,q)|[.(q-b)/(a+p),+infty.[) ) .x ))
proof
let a,b,p,q be Real;
assume AA: a > 0;
assume PP: p > 0;
assume A5: (1-b)/a < (1-q)/(-p);
0+(-q) < 1+(-q) & -p < 0 by PP, XREAL_1:8; then
A6: (1-q)/(-p)< (-q)/(-p) by XREAL_1:75;
0+(-b) < 1+(-b) by XREAL_1:8; then
A0: (-b)/a < (1-b)/a & (1-b)/a < (1-q)/(-p) & (1-q)/(-p) < q/p
by XREAL_1:74,AA,A5,A6,XCMPLX_1:191; then
A00: (1-b)/a < q/p by XXREAL_0:2;
set f0 = ( AffineMap (0,0) | (REAL \ ].(-b)/a,q/p.[));
set f1 = ( AffineMap (1/((1-b)/a - (-b)/a),-(((-b)/a)/((1-b)/a-((-b)/a))) )
| ([.(-b)/a,(1-b)/a.]));
set f2 = ( AffineMap (0,1) | [.(1-b)/a,(1-q)/(-p).] );
set f3 = ( AffineMap ( -(1/((q/p)-(1-q)/(-p))),(q/p)/((q/p)-(1-q)/(-p)) )
| [.(1-q)/(-p),q/p.] );
set f4 = ( AffineMap (a,b)|(].-infty,(q-b)/(a+p).[) );
set f5 = ( AffineMap (-p,q)|([.(q-b)/(a+p),+infty.[) );
D2: dom f2 = [.(1-b)/a,(1-q)/(-p).] by FUNCT_2:def 1;
D3: dom f3 = [.(1-q)/(-p),q/p.] by FUNCT_2:def 1;
D5: dom f5 = [.(q-b)/(a+p),+infty.[ by FUNCT_2:def 1;
for x be Real holds
(TrapezoidalFS ((-b)/a,(1-b)/a,(1-q)/(-p),q/p)).x
= max(0,min(1, (f4 +* f5).x ))
proof
let x be Real;
B170: dom (f2 +* f3)= (dom f2 \/ dom f3) by FUNCT_4:def 1
.= ([.(1-b)/a,(1-q)/(-p).] \/ dom f3) by FUNCT_2:def 1
.= ([.(1-b)/a,(1-q)/(-p).] \/ [.(1-q)/(-p),q/p.]) by FUNCT_2:def 1
.= ([.(1-b)/a,q/p.]) by XXREAL_1:165,A0;
B17: dom(f1 +* (f2 +* f3))
= (dom f1) \/ (dom (f2 +* f3)) by FUNCT_4:def 1
.= ([.(-b)/a,(1-b)/a.]) \/ (dom (f2 +* f3)) by FUNCT_2:def 1
.= [.(-b)/a,q/p.] by XXREAL_1:165,A0,A00,B170;
F1: AffineMap (1/((1-b)/a+-(-b)/a),-((-b)/a)/((1-b)/a+-(-b)/a) ).x
= AffineMap (1/((1-b)/a+-(-b)/a),-((-b)/a)/((1-b)/a+b/a) ).x
by XCMPLX_1:190
.= AffineMap (1/((1-b)/a+b/a),-((-b)/a)/((1-b)/a+b/a) ).x by XCMPLX_1:190
.= AffineMap (1/((1-b)/a+b/a),-((-b)/a)/((1-b+b)/a) ).x by XCMPLX_1:62
.= AffineMap (1/((1-b+b)/a),- ((-b)/a) / (1/a) ).x by XCMPLX_1:62
.= AffineMap (1/(1/a),- ((-b)/a)*a ).x by XCMPLX_1:100
.= AffineMap ( a*(1/1),-((-b)/a)*a ).x by XCMPLX_1:81
.= AffineMap ( a,-(a/a)*(-b) ).x by XCMPLX_1:75
.= AffineMap ( a,-1*(-b) ).x by XCMPLX_1:60,AA
.= AffineMap ( a,b ).x;
F3: (AffineMap ( -1/(q/p-(1-q)/(-p)),(q/p)/(q/p-(1-q)/(-p)) )).x
= (AffineMap ( -1/( q/p+(1-q)/p ),(q/p)/(q/p+-(1-q)/(-p)) )).x
by XCMPLX_1:189
.= (AffineMap ( -1/( q/p+(1-q)/p ),(q/p)/(q/p+(1-q)/p) )).x
by XCMPLX_1:189
.= (AffineMap ( -1/( (q+(1-q))/p ),(q/p)/(q/p+(1-q)/p) )).x
by XCMPLX_1:62
.= (AffineMap ( -1/( 1/p ),(q/p)/((q+(1-q))/p) )).x by XCMPLX_1:62
.= (AffineMap ( -p,(q/p)/(1/p) )).x by XCMPLX_1:56
.= (AffineMap ( -p,(q/p)*p )).x by XCMPLX_1:100
.= (AffineMap ( -p,q )).x by XCMPLX_1:87,PP
.= (-p)*x+q by FCONT_1:def 4;
per cases;
suppose B1: x <= (-b)/a; then
x*a <= (-b)/a*a by XREAL_1:64,AA; then
x*a <= a/a*(-b) by XCMPLX_1:75; then
x*a <= 1*(-b) by XCMPLX_1:60,AA; then
B14: a*x+b <= -b+b by XREAL_1:6;
0+(-b)/a < 1/a +(-b)/a by XREAL_1:6,AA;then
MM: (-b)/a<(1+(-b))/a by XCMPLX_1:62;
(1-b)/a < (q-b)/(a+p) by asymTT4,A5,AA,PP; then
(-b)/a < (q-b)/(a+p) by MM,XXREAL_0:2; then
B15: x < (q-b)/(a+p) by B1,XXREAL_0:2;
B11: max(0,min(1, (f4 +* f5).x )) = max(0,min(1, f4.x ))
by FUNCT_4:11,D5,XXREAL_1:236,B15
.=max(0,min(1, (AffineMap (a,b)).x )) by FUNCT_1:49,B15,XXREAL_1:233
.=max(0,min(1, a*x+b )) by FCONT_1:def 4
.=max(0, a*x+b ) by XXREAL_0:def 9,B14
.=0 by XXREAL_0:def 10,B14;
per cases;
suppose E1: x=(-b)/a;
(TrapezoidalFS ((-b)/a,(1-b)/a,(1-q)/(-p),q/p)).x
= 0 by TrZoi1,A0,E1;
hence thesis by B11;
end;
suppose E2: x<>(-b)/a;
not x in ].(-b)/a,q/p.[ & x in REAL by B1,XREAL_0:def 1,XXREAL_1:4; then
B14: x in REAL \ ].(-b)/a,q/p.[ by XBOOLE_0:def 5;
x < (-b)/a by B1,E2,XXREAL_0:1; then
E21: not x in dom(f1 +* (f2 +* f3)) by XXREAL_1:1,B17;
(f0 +* f1 +* f2 +* f3).x
= (f0 +* f1 +* (f2 +* f3)).x by FUNCT_4:14
.= (f0 +* (f1 +* (f2 +* f3))).x by FUNCT_4:14
.= f0.x by FUNCT_4:11,E21
.= AffineMap (0,0).x by FUNCT_1:49,B14
.= 0*x+0 by FCONT_1:def 4
.=0;
hence thesis by B11,FUZNUM_1:def 8,A0;
end;
end;
suppose B2: (-b)/a < x; then
x*a > (-b)/a*a by XREAL_1:68,AA; then
x*a > a/a*(-b) by XCMPLX_1:75; then
x*a > 1*(-b) by XCMPLX_1:60,AA; then
B21: a*x+b > -b+b by XREAL_1:6;
per cases;
suppose B3: x <= (1-b)/a;
x*a <= (1-b)/a*a by XREAL_1:64,B3,AA; then
x*a <= a/a*(1-b) by XCMPLX_1:75; then
x*a <= 1*(1-b) by XCMPLX_1:60,AA; then
B33: x*a+b <= 1-b+b by XREAL_1:6;
(1-b)/a < (q-b)/(a+p) by asymTT4,AA,PP,A5; then
B31: x < (q-b)/(a+p) by B3,XXREAL_0:2;
B61: max(0,min(1, (f4 +* f5).x ))
= max(0,min(1, f4.x )) by FUNCT_4:11,D5,XXREAL_1:236,B31
.=max(0,min(1, (AffineMap (a,b)).x )) by FUNCT_1:49,B31,XXREAL_1:233
.=max(0,min(1, a*x+b )) by FCONT_1:def 4
.=max(0, a*x+b ) by XXREAL_0:def 9,B33;
B34: x in [.(-b)/a,(1-b)/a.] by B2,B3; then
B35: x in dom f1 by FUNCT_2:def 1;
per cases;
suppose E1B3: x = (1-b)/a; then
E1B31: (TrapezoidalFS ((-b)/a,(1-b)/a,(1-q)/(-p),q/p)).x
= 1 by TrZoi1,A0;
max(0,min(1, (f4 +* f5).x))
=max(0, a/a*(1-b)+b) by XCMPLX_1:75,E1B3,B61
.=max(0, 1*(1-b)+b) by XCMPLX_1:60,AA
.=1 by XXREAL_0:def 10;
hence thesis by E1B31;
end;
suppose x <> (1-b)/a; then
not ((1-b)/a <= x & x <= q/p) by B3,XXREAL_0:1; then
B36: not x in dom (f2 +* f3) by B170,XXREAL_1:1;
(f0 +* f1 +* f2 +* f3).x
= (f0 +* f1 +* (f2 +* f3)).x by FUNCT_4:14
.= (f0 +* f1).x by FUNCT_4:11,B36
.= f1.x by FUNCT_4:13,B35
.=(AffineMap (1/((1-b)/a - (-b)/a),-(((-b)/a)/((1-b)/a-((-b)/a))) ) ).x
by FUNCT_1:49,B34
.= a*x+b by FCONT_1:def 4,F1
.=max(0, a*x+b ) by XXREAL_0:def 10,B21;
hence thesis by B61,FUZNUM_1:def 8,A0;
end;
end;
suppose B4: (1-b)/a < x; then
x*a > (1-b)/a*a by XREAL_1:68,AA; then
x*a > a/a*(1-b) by XCMPLX_1:75; then
x*a > 1*(1-b) by XCMPLX_1:60,AA; then
B41: x*a+b > 1-b+b by XREAL_1:6;
per cases;
suppose B5: x <= (1-q)/(-p);
per cases;
suppose B5E: x = (1-q)/(-p); then
AS: (q-b)/(a+p) < x by asymTT4,A5,AA,PP;
B5E3: max(0,min(1, (f4 +* f5).x ))
= max(0,min(1, f5.x )) by FUNCT_4:13,D5,AS,XXREAL_1:236
.=max(0,min(1, (AffineMap (-p,q)).x )) by FUNCT_1:49,AS,XXREAL_1:236
.=max(0,min(1, (-p)*x+q )) by FCONT_1:def 4
.=max(0,min(1, (-p)/(-p)*(1-q)+q )) by XCMPLX_1:75,B5E
.=max(0,min(1, 1*(1-q)+q )) by XCMPLX_1:60,PP
.= 1 by XXREAL_0:def 10;
(TrapezoidalFS ((-b)/a,(1-b)/a,(1-q)/(-p),q/p)).x
=1 by TrZoi1,A0,B5E;
hence thesis by B5E3;
end;
suppose B5N: x <> (1-q)/(-p); then
B5N5: x < (1-q)/(-p) by B5,XXREAL_0:1;
not ((1-q)/(-p) <= x & x <= q/p) by B5,XXREAL_0:1,B5N; then
B5N1: not x in dom f3 by D3,XXREAL_1:1;
(1-q)/(-p)*(-p) < x*(-p) by XREAL_1:69,PP,B5N5; then
(-p)/(-p)*(1-q) < x*(-p) by XCMPLX_1:75; then
1*(1-q) < x*(-p) by XCMPLX_1:60,PP; then
BB: (-p)*x+q > 1-q+q by XREAL_1:6;
B5N3: x in [.(1-b)/a,(1-q)/(-p).] by B4,B5;
B5N2: x in dom f2 by D2,B4,B5;
B5N4: (f0 +* f1 +* f2 +* f3).x
= (f0 +* f1 +* f2).x by FUNCT_4:11,B5N1
.= f2.x by FUNCT_4:13,B5N2
.= AffineMap (0,1).x by FUNCT_1:49,B5N3
.= 0*x+1 by FCONT_1:def 4
.=1;
per cases;
suppose B9: x < (q-b)/(a+p); then
max(0,min(1, (f4 +* f5).x ))
= max(0,min(1, f4.x )) by FUNCT_4:11,D5,XXREAL_1:236
.=max(0,min(1, (AffineMap (a,b)).x )) by FUNCT_1:49,B9,XXREAL_1:233
.=max(0,min(1, a*x+b )) by FCONT_1:def 4
.=max(0, 1 ) by XXREAL_0:def 9,B41
.=1 by XXREAL_0:def 10;
hence thesis by B5N4,FUZNUM_1:def 8,A0;
end;
suppose B10: (q-b)/(a+p) <= x; then
max(0,min(1, (f4 +* f5).x )) = max(0,min(1, f5.x ))
by FUNCT_4:13,D5,XXREAL_1:236
.=max(0,min(1, (AffineMap (-p,q)).x )) by FUNCT_1:49,B10,XXREAL_1:236
.=max(0,min(1, (-p)*x+q )) by FCONT_1:def 4
.=max(0, 1 ) by XXREAL_0:def 9,BB
.=1 by XXREAL_0:def 10;
hence thesis by B5N4,FUZNUM_1:def 8,A0;
end;
end;
end;
suppose B6: (1-q)/(-p) < x; then
(1-q)/(-p)*(-p) > x*(-p) by XREAL_1:69,PP; then
(-p)/(-p)*(1-q) > x*(-p) by XCMPLX_1:75; then
1*(1-q) > x*(-p) by XCMPLX_1:60,PP; then
B63: (-p)*x+q < 1-q+q by XREAL_1:6;
AZ: (q-b)/(a+p) < (1-q)/(-p) by asymTT4,A5,AA,PP;
B62: x in [.(q-b)/(a+p),+infty.[ by XXREAL_1:236,AZ,B6,XXREAL_0:2;
x in dom f5 by D5,AZ,B6,XXREAL_0:2,XXREAL_1:236;
then
B61: max(0,min(1, (f4 +* f5).x )) = max(0,min(1, f5.x )) by FUNCT_4:13
.=max(0,min(1, (AffineMap (-p,q)).x )) by FUNCT_1:49,B62
.=max(0,min(1, (-p)*x+q )) by FCONT_1:def 4
.=max(0, (-p)*x+q ) by XXREAL_0:def 9,B63;
per cases;
suppose B7: x <= q/p; then
B71: x in [.(1-q)/(-p), q/p.] by B6;
B72: x in dom f3 by D3,B7,B6;
x*p <= q/p*p by XREAL_1:64,PP,B7; then
x*p <= p/p*q by XCMPLX_1:75; then
x*p <= 1*q by XCMPLX_1:60,PP; then
B73: x*p - x*p <= q - p*x by XREAL_1:9;
(f0 +* f1 +* f2 +* f3).x
= f3.x by FUNCT_4:13,B72
.= AffineMap ( -(1/((q/p)-(1-q)/(-p))),(q/p)/((q/p)-(1-q)/(-p)) ).x
by FUNCT_1:49,B71
.=max(0, (-p)*x+q ) by XXREAL_0:def 10,B73,F3;
hence thesis by FUZNUM_1:def 8,A0,B61;
end;
suppose B8: q/p < x; then
not x in ].(-b)/a,q/p.[ & x in REAL by XREAL_0:def 1,XXREAL_1:4; then
B81: x in REAL \ ].(-b)/a,q/p.[ by XBOOLE_0:def 5;
E21: not x in dom(f1 +* (f2 +* f3)) by XXREAL_1:1,B17,B8;
B82: (f0 +* f1 +* f2 +* f3).x
= (f0 +* f1 +* (f2 +* f3)).x by FUNCT_4:14
.= (f0 +* (f1 +* (f2 +* f3))).x by FUNCT_4:14
.= f0.x by FUNCT_4:11,E21
.= AffineMap (0,0).x by FUNCT_1:49,B81
.= 0*x+0 by FCONT_1:def 4
.=0;
x*p>q/p*p by XREAL_1:68,PP,B8; then
x*p > p/p*q by XCMPLX_1:75; then
x*p > 1*q by XCMPLX_1:60,PP; then
B83: x*p - x*p > q - p*x by XREAL_1:9;
max(0,min(1, (f4 +* f5).x)) = 0 by XXREAL_0:def 10,B83,B61;
hence thesis by B82,FUZNUM_1:def 8,A0;
end;
end;::::::: B6
end; :::::::::::::: B4
end;:::::::::::::::::::::B2
end;
hence thesis;
end;
theorem asymTT50:
for a,b,p,q be Real, f be Function of REAL,REAL st a > 0 & p > 0 &
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;
let f be Function of REAL,REAL;
assume AP: a > 0 & p > 0;
assume FF: f= (AffineMap (a,b)|].-infty,(q-b)/(a+p).[) +*
(AffineMap (-p,q)|[.(q-b)/(a+p),+infty.[);
set fa = AffineMap (a,b)|].-infty,(q-b)/(a+p).[;
set fp = AffineMap (-p,q)|[.(q-b)/(a+p),+infty.[;
set f1 = fa +* fp;
Dfp: dom fp = [.(q-b)/(a+p),+infty.[ by FUNCT_2:def 1;
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(a+p+a,a+p+p);
0+a < p+a+a & a+p+a <= max(a+p+a,a+p+p) by XREAL_1:6,AP,XXREAL_0:25; then
a <= max(a+p+a,a+p+p) by XXREAL_0:2; then
AA: |. a .| <= max(a+p+a,a+p+p) by ABSVALUE:def 1,AP;
PP0: -(-p) = |. -p .| by ABSVALUE:def 1,AP;
0+p < p+a+p & a+p+p <= max(a+p+a,a+p+p) by XREAL_1:6,AP,XXREAL_0:25; then
PP: |. -p .| <= max(a+p+a,a+p+p) by XXREAL_0:2,PP0;
for x1, x2 being Real st x1 in dom f & x2 in dom f holds
|. f . x1 - f . x2 .| <= max(a+p+a,a+p+p) * |. x1 - x2 .|
proof
let x1, x2 be Real;
A3: |. x1 - x2 .| >= 0 by COMPLEX1:46;
per cases;
suppose B1: x1 < (q-b)/(a+p); then
B12: f.x1 = fa.x1 by FUNCT_4:11,Dfp,XXREAL_1:236,FF
.= AffineMap (a,b).x1 by FUNCT_1:49,B1,XXREAL_1:233;
per cases;
suppose C1: x2 < (q-b)/(a+p);
C13: f.x2 = fa.x2 by FUNCT_4:11,Dfp,XXREAL_1:236,C1,FF
.= AffineMap (a,b).x2 by FUNCT_1:49,C1,XXREAL_1:233;
|. f.x1 - f.x2 .|
= |. a*x1 +b - AffineMap (a,b).x2 .| by FCONT_1:def 4,C13,B12
.= |. a*x1 +b - (a*x2 +b) .| by FCONT_1:def 4
.= |. a*(x1 - x2) .|
.= |. a .|*|.(x1 - x2) .| by COMPLEX1:65;
hence thesis by AA,A3,XREAL_1:64;
end;
suppose C2: x2 >= (q-b)/(a+p); then
x2 in [.(q-b)/(a+p),+infty.[ by XXREAL_1:236;then
C22: x2 in dom fp by FUNCT_2:def 1;
C23: f.x2 = fp.x2 by FUNCT_4:13,C22,FF
.= AffineMap (-p,q).x2 by FUNCT_1:49,C2,XXREAL_1:236;
C24: |. f.x1 - f.x2 .| = |. AffineMap (a,b).x1 - f.x2 .| by B12
.= |. a*x1 +b - AffineMap (-p,q).x2 .| by FCONT_1:def 4,C23
.= |. a*x1 +b - ((-p)*x2 +q) .| by FCONT_1:def 4
.=|. (a+p)*x2 -(q-b)+ a*(x1-x2) .|;
x2*(a+p) >= (q-b)/(a+p)*(a+p) by XREAL_1:64,AP,C2;then
(q-b)<= (a+p)*x2 by XCMPLX_1:87,AP;then
C25: (a+p)*x2-(q-b)>=0 by XREAL_1:48;
x1*(a+p) < (q-b)/(a+p)*(a+p) by XREAL_1:68,AP,B1;then
(a+p)*x1 < q-b by XCMPLX_1:87,AP; then
-(a+p)*x1 > -(q-b) by XREAL_1:24; then
-(a+p)*x1+(a+p)*x2 > -(q-b)+(a+p)*x2 by XREAL_1:6;then
|.(a+p)*x2-(q-b).| <= |. (a+p)*x2-(a+p)*x1 .| by C25,ABS1; then
C30X: |.(a+p)*x2-(q-b).|+|.a*(x1-x2).|
<= |. (a+p)*(x2-x1) .|+|.a*(x1-x2).| by XREAL_1:6;
C299: |. (a+p)*x2 -(q-b)+ a*(x1-x2) .|
<= |.(a+p)*x2-(q-b).|+|.a*(x1-x2).| by COMPLEX1:56;
|. (a+p)*(x2-x1) .|+|.a*(x1-x2).|
= |.(a+p).|*|.(x2-x1) .|+|.a*(x1-x2).| by COMPLEX1:65
.= |.(a+p).|*|.x2-x1.|+|.a.|*|.(x1-x2).| by COMPLEX1:65
.= |.(a+p).|*|.x1-x2.|+|.a.|*|.(x1-x2).| by COMPLEX1:60
.= (a+p)*|.x1-x2.|+|.a.|*|.(x1-x2).| by ABSVALUE:def 1,AP
.= (a+p)*|.x1-x2.| + a*|.(x1-x2).| by ABSVALUE:def 1,AP
.= (a+p+a)*|.x1-x2.|; then
C30: |. f.x1 - f.x2 .| <= (a+p+a)*|.x1-x2.| by C24,C299,C30X,XXREAL_0:2;
a+p+a <= max(a+p+a,a+p+p) & |.x1-x2.|>= 0 by XXREAL_0:25, COMPLEX1:46;
then
(a+p+a)*|.x1-x2.| <= max(a+p+a,a+p+p)*|.x1-x2.| by XREAL_1:64;
hence thesis by C30,XXREAL_0:2;
end;
end;
suppose B2: x1 >= (q-b)/(a+p); then
x1 in [.(q-b)/(a+p),+infty.[ by XXREAL_1:236;then
B22: x1 in dom fp by FUNCT_2:def 1;
B23: f.x1 = fp.x1 by FUNCT_4:13,B22,FF
.= AffineMap (-p,q).x1 by FUNCT_1:49,B2,XXREAL_1:236;
per cases;
suppose D1: x2 < (q-b)/(a+p);
D4: f.x2 = fa.x2 by FUNCT_4:11,Dfp,XXREAL_1:236,D1,FF
.= AffineMap (a,b).x2 by FUNCT_1:49,D1,XXREAL_1:233;
D5: |. f.x1 - f.x2 .| =
|. (-p)*x1 +q - AffineMap (a,b).x2 .| by FCONT_1:def 4,D4,B23
.= |. (-p)*x1 +q - (a*x2+b) .| by FCONT_1:def 4
.= |. q -b -(a+p)*x2 +(-p)*(x1-x2).|;
x1*(a+p) >= (q-b)/(a+p)*(a+p) by XREAL_1:64,AP,B2;then
D27: (q-b)<= (a+p)*x1 by XCMPLX_1:87,AP;
x2*(a+p) < (q-b)/(a+p)*(a+p) by XREAL_1:68,AP,D1;then
(a+p)*x2 < q-b by XCMPLX_1:87,AP; then
D25: (q-b)-(a+p)*x2 >= 0 by XREAL_1:48;
q-b -(a+p)*x2 <= (a+p)*x1 -(a+p)*x2 by XREAL_1:9,D27;then
|.(a+p)*(x1 -x2).| >= |. q -b -(a+p)*x2 .| by D25,ABS1; then
D30: |.(a+p)*(x1 -x2).|+|.(-p)*(x1-x2).|
>= |. q -b -(a+p)*x2 .|+|.(-p)*(x1-x2).| by XREAL_1:6;
X29: |. q-b -(a+p)*x2 +(-p)*(x1-x2).|
<= |. q-b -(a+p)*x2 .| + |.(-p)*(x1-x2).| by COMPLEX1:56;
|.(a+p)*(x1 -x2).|+|.(-p)*(x1-x2).|
= |.(a+p).|*|.(x1 -x2).|+|.(-p)*(x1-x2).| by COMPLEX1:65
.= |.(a+p).|*|.(x1 -x2).|+|.(-p).|*|.(x1-x2).| by COMPLEX1:65
.= (a+p)*|.(x1 -x2).|+|.(-p).|*|.(x1-x2).| by ABSVALUE:def 1,AP
.= (a+p)*|.(x1 -x2).|+(-(-p))*|.(x1-x2).| by ABSVALUE:def 1,AP
.= (a+p+p)*|.x1-x2.|;
then
D31: |. f.x1 - f.x2 .| <= (a+p+p)*|.x1-x2.| by D5,X29,D30,XXREAL_0:2;
a+p+p <= max(a+p+a,a+p+p) & |.x1-x2.|>= 0 by XXREAL_0:25, COMPLEX1:46;
then
(a+p+p)*|.x1-x2.| <= max(a+p+a,a+p+p)*|.x1-x2.| by XREAL_1:64;
hence thesis by D31,XXREAL_0:2;
end;
suppose E1: x2 >= (q-b)/(a+p);
then
x2 in [.(q-b)/(a+p),+infty.[ by XXREAL_1:236; then
E3: x2 in dom fp by FUNCT_2:def 1;
E4: f.x2 = fp.x2 by FUNCT_4:13,E3,FF
.= AffineMap (-p,q).x2 by FUNCT_1:49,E1,XXREAL_1:236;
|. f.x1 - f.x2 .|
= |. (-p)*x1 +q - AffineMap (-p,q).x2 .| by FCONT_1:def 4,E4,B23
.= |. (-p)*x1 +q - ((-p)*x2 +q) .| by FCONT_1:def 4
.= |. (-p)*(x1 - x2) .|
.= |. (-p) .|*|.(x1 - x2) .| by COMPLEX1:65;
hence thesis by PP,A3,XREAL_1:64;
end;
end;
end;
hence thesis by XXREAL_0:def 10,AP;
end;
hence thesis;
end;
theorem asymTT51:
for a,b,p,q be Real st a > 0 & p > 0 holds
ex r being Real st
( 0 < r &
( for x1, x2 being Real st
x1 in dom ((AffineMap (a,b)|].-infty,(q-b)/(a+p).[)
+* (AffineMap (-p,q)|[.(q-b)/(a+p),+infty.[)) &
x2 in dom ((AffineMap (a,b)|].-infty,(q-b)/(a+p).[)
+* (AffineMap (-p,q)|[.(q-b)/(a+p),+infty.[)) holds
|. ((AffineMap (a,b)|].-infty,(q-b)/(a+p).[)
+* (AffineMap (-p,q)|[.(q-b)/(a+p),+infty.[)) . x1
- ((AffineMap (a,b)|].-infty,(q-b)/(a+p).[)
+* (AffineMap (-p,q)|[.(q-b)/(a+p),+infty.[)) . x2.|
<= r * |.(x1 - x2).| ) )
proof
let a,b,p,q be Real;
assume AP: a > 0 & p > 0;
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 asymTT10;
f is Lipschitzian by asymTT50,AP;
hence thesis;
end;
theorem asymTT5:
for a,b,p,q,r,s be Real, f be Function of REAL,REAL st
a > 0 & p > 0 &
for x be Real holds
f.x = max(r,min(s, ( (AffineMap (a,b)|].-infty,(q-b)/(a+p).[) +*
(AffineMap (-p,q)|[.(q-b)/(a+p),+infty.[) ) .x ))
holds f is Lipschitzian
proof
let a,b,p,q,r,s be Real, f be Function of REAL,REAL;
assume AP: a > 0 & p > 0;
assume A2: for x be Real holds
f.x = max(r,min(s, ( (AffineMap (a,b)|].-infty,(q-b)/(a+p).[) +*
(AffineMap (-p,q)|[.(q-b)/(a+p),+infty.[) ) .x ));
set f1 = AffineMap (a,b)|].-infty,(q-b)/(a+p).[ +*
AffineMap (-p,q)|[.(q-b)/(a+p),+infty.[;
f1 is Function of REAL,REAL by asymTT10;then
A4: dom f = REAL & dom f1 = REAL by FUNCT_2:def 1;
ex r1 being Real st
( 0 < r1 &
( for x1, x2 being Real st x1 in dom f & x2 in dom f holds
|.((f . x1) - (f . x2)).| <= r1 * |.(x1 - x2).| ) )
proof
consider r0 being Real such that
A1: 0 < r0 and
A3: for x1, x2 being Real st x1 in dom f1 & x2 in dom f1 holds
|.f1.x1 - f1.x2.| <= r0 * |.x1 - x2.| by asymTT51,AP;
take r0;
for x1, x2 being Real st x1 in dom f & x2 in dom f holds
|. f . x1 - f . x2 .| <= r0 * |. x1 - x2 .|
proof
let x1, x2 be Real;
assume x1 in dom f & x2 in dom f; then
A5: |.f1.x1 - f1.x2.| <= r0 * |.x1 - x2.| by A3,A4;
|. f . x1 - f . x2 .|
=|. max(r,min(s, f1 .x1 )) - f . x2 .| by A2
.=|. max(r,min(s, f1.x1)) - max(r,min(s, f1.x2)) .| by A2; then
|. f . x1 - f . x2 .| <= |. f1.x1 - f1.x2 .| by LeMM01;
hence thesis by A5,XXREAL_0:2;
end;
hence thesis by A1;
end;
hence thesis;
end;
theorem asymTT9:
for a, b, c being Real st a < b & b < c holds
for x being Real holds
TriangularFS (a,b,c).x =
max(0,min(1, ( (AffineMap ( 1/(b-a),- a/(b-a) )|].-infty,b.[) +*
(AffineMap ( - 1/(c-b),c/(c-b) )|[.b,+infty.[) ).x ))
proof
let a, b, c be Real;
assume A1:a < b & b < c;
set f = TriangularFS (a,b,c);
for x being Real holds
TriangularFS (a,b,c).x =
max(0,min(1, ( (AffineMap ( 1/(b-a),- a/(b-a) )|].-infty,b.[) +*
(AffineMap ( - 1/(c-b),c/(c-b) )|[.b,+infty.[) ).x ))
proof
let x be Real;
set a1 = 1/(b-a);
set b1 = - a/(b-a);
set p1 = 1/(c-b);
set q1 = c/(c-b);
b1: b-a >a-a & b -b < c -b by XREAL_1:9,A1;
a*1 < 1*c by A1,XXREAL_0:2;then
(- (-a))*((1/(b-a))/(1/(b-a))) < c*1 by XCMPLX_1:60,b1;then
(- (-a))*((1/(b-a))/(1/(b-a))) < c*(( 1/(c-b))/( 1/(c-b))) by XCMPLX_1:60,b1;
then
((- (-a))*(1/(b-a)))/(1/(b-a)) < c*(( 1/(c-b))/( 1/(c-b))) by XCMPLX_1:74;
then
((- (-a))*(1/(b-a)))/(1/(b-a)) < (c*( 1/(c-b)))/ (1/(c-b)) by XCMPLX_1:74;
then
( - (-a)*(1/(b-a)) ) / (1/(b-a)) < ((c* 1)/(c-b)) / (1/(c-b)) by XCMPLX_1:74;
then
( - ((-a)*1)/(b-a) ) / (1/(b-a)) < (c/(c-b)) / (1/(c-b)) by XCMPLX_1:74;
then
B3: (- (- a/(b-a)))/(1/(b-a)) < q1/p1 by XCMPLX_1:187;
B2: (1 - b1)/a1 = (1+ a/(b-a))*(b-a) by XCMPLX_1:100
.= b-a + a/(b-a)*(b-a)
.= b-a + a by XCMPLX_1:87,b1
.= b;
Bb: (1- c/(c-b))/(- 1/(c-b)) = -(1- c/(c-b))/(1/(c-b)) by XCMPLX_1:188
.= -(1- c/(c-b))*(c-b) by XCMPLX_1:100
.= -(c-b - c/(c-b)*(c-b))
.= -(c-b - c) by XCMPLX_1:87,b1
.= b;
B5: (-b1)/a1 = (b-a)*((a/(b-a))/1) by XCMPLX_1:81
.=a by XCMPLX_1:87,b1;
B7: q1/p1 = (c-b)*((c/(c-b))/1) by XCMPLX_1:81
.= c by XCMPLX_1:87,b1;
a < c by A1,XXREAL_0:2;then
B9: c-a > a-a by XREAL_1:9;
(q1-b1)/(a1+p1) = (c/(c-b)+ a/(b-a))/(1/(b-a)+1/(c-b))
.= (( (c*(b-a)+a*(c-b)) )/((b-a)*(c-b)) )/(1/(b-a)+1/(c-b))
by XCMPLX_1:116,b1
.= (( (c*b-c*a+a*c-a*b) )/((b-a)*(c-b)) )
/(( (1*(b-a)+1*(c-b)) )/((b-a)*(c-b)) ) by XCMPLX_1:116,b1
.= ((c-a)*b) / (c-a) by XCMPLX_1:55,b1
.= b by XCMPLX_1:89,B9;
hence thesis by B5,B7,Bb,b1,B3,asymTT6,B2;
end;
hence thesis;
end;
theorem asymTT8:
for a, b, c, d being Real st a < b & b < c & c < d holds
for x being Real holds
TrapezoidalFS (a,b,c,d).x =
max(0,min(1, (
(AffineMap ( 1/(b-a),- a/(b-a) )|].-infty,(b*d-a*c)/(d-c+b-a).[) +*
(AffineMap ( - 1/(d-c),d/(d-c) )|[.(b*d-a*c)/(d-c+b-a),+infty.[) ).x ))
proof
let a, b, c, d being Real;
assume A1: a < b & b < c & c < d;
set a1 = 1/(b-a);
set b1 = - a/(b-a);
set p1= 1/(d-c);
set q1 = d/(d-c);
A20: a-a < b-a by XREAL_1:9,A1;
A30: c-c < d-c by XREAL_1:9,A1;
B1: (-b1)/a1 = (b-a)*((a/(b-a))/1) by XCMPLX_1:81
.=a by XCMPLX_1:87,A20;
B2: (1 - b1)/a1 = (1+ a/(b-a))*(b-a) by XCMPLX_1:100
.= b-a + a/(b-a)*(b-a)
.= b-a + a by XCMPLX_1:87,A20
.= b;
B3: (1-q1)/(-p1)=- (1 - d/(d-c))/(1/(d-c)) by XCMPLX_1:188
.= - ((1 - d/(d-c))*(d-c)) by XCMPLX_1:100
.= - (1*(d-c) - d/(d-c)*(d-c))
.= -(d-c - d ) by XCMPLX_1:87,A30
.= c;
B4: d = (d-c)*((d/(d-c))/1) by A30,XCMPLX_1:87
.= q1/p1 by XCMPLX_1:81;
(q1-b1)/(a1+p1) = (d/(d-c) + a/(b-a))/(1/(b-a) + 1/(d-c))
.=( (d*(b-a)+a*(d-c)) /((d-c)*(b-a)))/(1/(b-a) + 1/(d-c))
by XCMPLX_1:116,A20,A30
.=((d*b-d*a+a*d-a*c)/((d-c)*(b-a)))/( (1*(b-a)+1*(d-c)) /((d-c)*(b-a)) )
by XCMPLX_1:116,A20,A30
.= (b*d-a*c)/(d-c+b-a) by XCMPLX_1:55,A20,A30;
hence thesis by B1,B4,asymTT7,A20,A30,B2,B3,A1;
end;
theorem
for a,b,p,q be Real, f be Function of REAL,REAL st
a > 0 & p > 0 &
for x be Real holds
f.x = max(0,min(1, ( ((AffineMap (a,b))|(].-infty,(q-b)/(a+p).[)) +*
((AffineMap (-p,q))|([.(q-b)/(a+p),+infty.[)) ) .x ))
holds f is Lipschitzian by asymTT5;
theorem
for a, b, c being Real st a < b & b < c holds
TriangularFS (a,b,c) is Lipschitzian
proof
let a, b, c be Real;
assume A1:a < b & b < c; then
B5: c-b > b-b by XREAL_1:9;
set a1 = 1/(b-a);
set p1 = 1/(c-b);
set b1 = - a/(b-a);
set q1 = c/(c-b);
c > a by A1,XXREAL_0:2;then
B4: c-a > a-a by XREAL_1:9;
B7: b-a > a-a by XREAL_1:9,A1;
(q1-b1)/(a1+p1) = (c/(c-b)+ a/(b-a))/(1/(b-a)+1/(c-b))
.= (( (c*(b-a)+a*(c-b)) )/((b-a)*(c-b)) )/(1/(b-a)+1/(c-b))
by XCMPLX_1:116,B5,B7
.= (( (c*b-c*a+a*c-a*b) )/((b-a)*(c-b)) )
/(( (1*(b-a)+1*(c-b)) )/((b-a)*(c-b)) ) by XCMPLX_1:116,B5,B7
.= ((c-a)*b) / (c-a) by XCMPLX_1:55,B5,B7
.=b by XCMPLX_1:89,B4;then
for x be Real holds TriangularFS (a,b,c).x
= max(0,min(1, ( ((AffineMap (a1,b1))|(].-infty,(q1-b1)/(a1+p1).[)) +*
((AffineMap (-p1,q1))|([.(q1-b1)/(a1+p1),+infty.[)) ) .x )) by asymTT9,A1;
hence thesis by asymTT5,B7,B5;
end;
theorem
for a, b, c, d being Real st a < b & b < c & c < d holds
TrapezoidalFS (a,b,c,d) is Lipschitzian
proof
let a, b, c ,d be Real;
assume A1:a < b & b < c & c < d; then
A20: a-a < b-a by XREAL_1:9;
A30: c-c < d-c by XREAL_1:9,A1;
set a1 = 1/(b-a);
set b1 = - a/(b-a);
set p1 = 1/(d-c);
set q1 = d/(d-c);
B5: (q1-b1)/(a1+p1) = (d/(d-c) + a/(b-a))/(1/(b-a) + 1/(d-c))
.=( (d*(b-a)+a*(d-c)) /((d-c)*(b-a)))/(1/(b-a) + 1/(d-c))
by XCMPLX_1:116,A20,A30
.=((d*b-d*a+a*d-a*c)/((d-c)*(b-a)))/( (1*(b-a)+1*(d-c)) /((d-c)*(b-a)) )
by XCMPLX_1:116,A20,A30
.= (b*d-a*c)/(d-c+b-a) by XCMPLX_1:55,A20,A30;
for x be Real holds
TrapezoidalFS (a,b,c,d).x = max(0,min(1, (
(AffineMap ( 1/(b-a),- a/(b-a) )|].-infty,(b*d-a*c)/(d-c+b-a).[) +*
(AffineMap ( - 1/(d-c),d/(d-c) )|[.(b*d-a*c)/(d-c+b-a),+infty.[) ).x ))
by asymTT8,A1;
hence thesis by asymTT5,A20,A30,B5;
end;
theorem
for a,b,p,q be Real, f be FuzzySet of REAL st
a > 0 & p > 0 & (-b)/a < q/p & (1-b)/a = (1-q)/(-p) &
for x be Real holds
f.x
= max(0,min(1, ( (AffineMap (a,b) |].-infty,(q-b)/(a+p).[) +*
(AffineMap (-p,q)|[.(q-b)/(a+p),+infty.[) ) .x ))
holds f is triangular & f is strictly-normalized
proof
let a,b,p,q be Real, f be FuzzySet of REAL;
assume that
A1: a > 0 & p > 0 & (-b)/a < q/p & (1-b)/a = (1-q)/(-p) and
A2: for x be Real holds
f.x = max(0,min(1, ( (AffineMap (a,b) |].-infty,(q-b)/(a+p).[) +*
(AffineMap (-p,q)|[.(q-b)/(a+p),+infty.[) ) .x ));
D1: REAL = dom f & REAL = dom (TriangularFS ((-b)/a,(1-b)/a,q/p))
by FUNCT_2:52;
for x being object st x in dom f holds
(TriangularFS ((-b)/a,(1-b)/a,q/p)).x =f.x
proof
let x be object;
assume x in dom f;
then reconsider x as Real by D1;
f.x = max(0,min(1, ( (AffineMap (a,b) |].-infty,(q-b)/(a+p).[) +*
(AffineMap (-p,q)|[.(q-b)/(a+p),+infty.[) ) .x )) by A2
.= (TriangularFS ((-b)/a,(1-b)/a,q/p)).x by A1,asymTT6;
hence thesis;
end; then
A4: f = (TriangularFS ((-b)/a,(1-b)/a,q/p)) by FUNCT_1:2,D1;
0+(-q) < 1+(-q) & -p < 0 by A1, XREAL_1:8; then
A7: (1-q)/(-p)< (-q)/(-p) by XREAL_1:75;
0+(-b) < 1+(-b) by XREAL_1:8; then
(-b)/a < (1-b)/a & (1-b)/a < q/p by XREAL_1:74,A7,A1,XCMPLX_1:191;
hence thesis by FUZNUM_1:29,A4;
end;
theorem
for a,b,p,q be Real, f be FuzzySet of REAL st
a > 0 & p > 0 & (1-b)/a < (1-q)/(-p) &
for x be Real holds
f.x
= max(0,min(1, ( (AffineMap (a,b) |].-infty,(q-b)/(a+p).[) +*
(AffineMap (-p,q)|[.(q-b)/(a+p),+infty.[) ) .x ))
holds f is trapezoidal & f is normalized
proof
let a,b,p,q be Real, f be FuzzySet of REAL;
assume that
A1: a > 0 & p > 0 & (1-b)/a < (1-q)/(-p) and
A2: for x be Real holds
f.x = max(0,min(1, ( (AffineMap (a,b) |].-infty,(q-b)/(a+p).[) +*
(AffineMap (-p,q)|[.(q-b)/(a+p),+infty.[) ) .x ));
D1: REAL = dom f &
REAL = dom (TrapezoidalFS ((-b)/a,(1-b)/a,(1-q)/(-p),q/p))
by FUNCT_2:52;
for x being object st x in dom f holds
TrapezoidalFS ((-b)/a,(1-b)/a,(1-q)/(-p),q/p).x =f.x
proof
let x be object;
assume x in dom f;
then reconsider x as Real by D1;
f.x = max(0,min(1, ( (AffineMap (a,b) |].-infty,(q-b)/(a+p).[) +*
(AffineMap (-p,q)|[.(q-b)/(a+p),+infty.[) ) .x )) by A2
.= TrapezoidalFS ((-b)/a,(1-b)/a,(1-q)/(-p),q/p).x by A1,asymTT7;
hence thesis;
end; then
A4: f = TrapezoidalFS ((-b)/a,(1-b)/a,(1-q)/(-p),q/p) by FUNCT_1:2,D1;
0+(-q) < 1+(-q) & -p < 0 by A1, XREAL_1:8; then
A7: (1-q)/(-p)< (-q)/(-p) by XREAL_1:75;
0+(-b) < 1+(-b) by XREAL_1:8; then
(-b)/a < (1-b)/a & (1-b)/a < (1-q)/(-p) & (1-q)/(-p) < q/p
by XREAL_1:74,A1,A7,XCMPLX_1:191;
hence thesis by FUZNUM_1:31,A4;
end;
theorem
{f where f is FuzzySet of REAL:f is triangular}
c= Membership_Funcs (REAL)
proof
let x be object;
assume x in {f where f is FuzzySet of REAL: f is triangular};
then ex f be FuzzySet of REAL st x=f & f is triangular;
hence thesis by Def1;
end;
theorem
{TriangularFS (a,b,c) where a,b,c is Real : a < b & b < c}
c= Membership_Funcs (REAL) by TR2XX;
theorem
{f where f is FuzzySet of REAL:f is trapezoidal}
c= Membership_Funcs (REAL)
proof
let x be object;
assume x in {f where f is FuzzySet of REAL: f is trapezoidal};
then ex f be FuzzySet of REAL st x=f & f is trapezoidal;
hence thesis by Def1;
end;
theorem
{TrapezoidalFS (a,b,c,d) where a,b,c,d is Real : a < b & b < c & c < d}
c= Membership_Funcs (REAL)
proof
let x be object;
assume x in {TrapezoidalFS (a,b,c,d)
where a,b,c,d is Real : a < b & b < c & c < d}; then
ex a,b,c,d be Real st x=TrapezoidalFS (a,b,c,d) & a < b & b < c & c < d;
hence thesis by Def1;
end;