:: Some Properties of Membership Functions Composed of Triangle Functions and
:: Piecewise Linear Functions
:: by Takashi Mitsuishi
::
:: Received June 30, 2021
:: Copyright (c) 2021 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;
begin
theorem :: FUZZY_5:1
for a,b,c,d being Real holds
|. max(c,min(d,a)) - max(c,min(d,b)) .| <= |. a-b .|;
theorem :: FUZZY_5:2
for x being Real holds
|. sin x .| <= |.x.|;
theorem :: FUZZY_5:3
for x,y being Real holds |. sin x - sin y .| <= |.x-y.|;
theorem :: FUZZY_5:4
for x be Real st exp x = 1 holds x = 0;
theorem :: FUZZY_5:5
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;
theorem :: FUZZY_5:6
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);
theorem :: FUZZY_5:7
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);
begin :: The set of membership functions
definition
let X be non empty set;
func Membership_Funcs (X) -> set means
:: FUZZY_5:def 1
for f being object holds
f in it iff f is Membership_Func of X;
end;
theorem :: FUZZY_5:8
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;
theorem :: FUZZY_5:9
Membership_Funcs (REAL)
= {f where f is Function of REAL,REAL : f is FuzzySet of REAL};
:::: characteristic function (indicator function)
theorem :: FUZZY_5:10
for A,X be non empty set holds
{chi (A,X)} c= Membership_Funcs (X);
theorem :: FUZZY_5:11
{chi([.a,b.],REAL) where a,b is Real : a <= b}
c= Membership_Funcs (REAL);
theorem :: FUZZY_5:12
{chi(A,REAL) where A is Subset of REAL : A c= REAL}
c= Membership_Funcs (REAL);
theorem :: FUZZY_5:13
{f where f is FuzzySet of REAL : ex A be Subset of REAL st f=chi(A,REAL) }
c= Membership_Funcs (REAL);
:::: membership functions using min (max) operation
theorem :: FUZZY_5:14
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;
theorem :: FUZZY_5:15 ::: 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;
theorem :: FUZZY_5:16 ::: 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;
theorem :: FUZZY_5:17
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;
theorem :: FUZZY_5:18
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;
theorem :: FUZZY_5:19
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;
theorem :: FUZZY_5:20
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;
theorem :: FUZZY_5:21
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;
theorem :: FUZZY_5:22
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;
theorem :: FUZZY_5:23
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);
theorem :: FUZZY_5:24
{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);
theorem :: FUZZY_5:25
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;
theorem :: FUZZY_5:26
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;
:::: fuzzy Set from trigonometric function
theorem :: FUZZY_5:27
{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);
theorem :: FUZZY_5:28
{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);
theorem :: FUZZY_5:29
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;
theorem :: FUZZY_5:30
{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);
theorem :: FUZZY_5:31
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;
theorem :: FUZZY_5:32
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;
theorem :: FUZZY_5:33
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;
theorem :: FUZZY_5:34
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;
theorem :: FUZZY_5:35
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;
:::: periodicity of membership functions
theorem :: FUZZY_5:36
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;
theorem :: FUZZY_5:37
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;
theorem :: FUZZY_5:38
{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);
theorem :: FUZZY_5:39
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;
theorem :: FUZZY_5:40
{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);
theorem :: FUZZY_5:41
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;
theorem :: FUZZY_5:42
{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))};
theorem :: FUZZY_5:43
{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);
theorem :: FUZZY_5:44
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;
theorem :: FUZZY_5:45
{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))};
theorem :: FUZZY_5:46
{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);
theorem :: FUZZY_5:47
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;
theorem :: FUZZY_5:48
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;
theorem :: FUZZY_5:49
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;
:::: membership functions from Gaussian function
theorem :: FUZZY_5:50
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;
theorem :: FUZZY_5:51
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;
theorem :: FUZZY_5:52
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);
theorem :: FUZZY_5:53
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;
theorem :: FUZZY_5:54:: 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;
theorem :: FUZZY_5:55
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;
theorem :: FUZZY_5:56
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;
theorem :: FUZZY_5:57
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;
theorem :: FUZZY_5:58
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;
theorem :: FUZZY_5:59
{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);
:::: S or Z type Membership function
theorem :: FUZZY_5:60
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;
theorem :: FUZZY_5:61
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;
theorem :: FUZZY_5:62:: 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;
theorem :: FUZZY_5:63
{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);
:::: symmetrical Triangular or Trapezoidal Fuzzy Sets
theorem :: FUZZY_5:64
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;
theorem :: FUZZY_5:65
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.|);
theorem :: FUZZY_5:66
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;
theorem :: FUZZY_5:67:: 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;
theorem :: FUZZY_5:68
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;
theorem :: FUZZY_5:69
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;
theorem :: FUZZY_5:70
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;
theorem :: FUZZY_5:71
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;
theorem :: FUZZY_5:72
{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);
theorem :: FUZZY_5:73
{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);
:::: asymmetry Trapezoidal or Triangular membership function
theorem :: FUZZY_5:74
for a,b,p,q,s be Real holds
( AffineMap (a,b)|].-infty,s.[ ) +* ( AffineMap (p,q)|[.s,+infty.[ )
is Function of REAL,REAL;
theorem :: FUZZY_5:75:: 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;
theorem :: FUZZY_5:76
for a,b,c 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 ));
theorem :: FUZZY_5:79
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 ));
theorem :: FUZZY_5:80
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;
theorem :: FUZZY_5:81
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).| ) );
theorem :: FUZZY_5:82
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;
theorem :: FUZZY_5:83
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 ));
theorem :: FUZZY_5:84
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 ));
theorem :: FUZZY_5:85
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;
theorem :: FUZZY_5:86
for a, b, c being Real st a < b & b < c holds
TriangularFS (a,b,c) is Lipschitzian;
theorem :: FUZZY_5:87
for a, b, c, d being Real st a < b & b < c & c < d holds
TrapezoidalFS (a,b,c,d) is Lipschitzian;
theorem :: FUZZY_5:88
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;
theorem :: FUZZY_5:89
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;
theorem :: FUZZY_5:90
{f where f is FuzzySet of REAL:f is triangular}
c= Membership_Funcs (REAL);
theorem :: FUZZY_5:91
{TriangularFS (a,b,c) where a,b,c is Real : a < b & b < c}
c= Membership_Funcs (REAL);
theorem :: FUZZY_5:92
{f where f is FuzzySet of REAL:f is trapezoidal}
c= Membership_Funcs (REAL);
theorem :: FUZZY_5:93
{TrapezoidalFS (a,b,c,d) where a,b,c,d is Real : a < b & b < c & c < d}
c= Membership_Funcs (REAL);
**