:: Developing Complementary Rough Inclusion Functions
:: by Adam Grabowski
::
:: Received February 26, 2020
:: Copyright (c) 2020-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 STRUCT_0, RELAT_1, TARSKI, ZFMISC_1, XBOOLE_0, SUBSET_1, FUNCT_1,
ROUGHS_1, ROUGHIF1, ROUGHIF2, FINSET_1, CARD_1, REAL_1, NUMBERS, ARYTM_3,
XXREAL_0, XXREAL_1, ARYTM_1, FUNCT_7, MCART_1, METRIC_1, RELAT_2,
PARTFUN3;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, BINOP_1, NUMBERS,
XCMPLX_0, XXREAL_0, FINSET_1, CARD_1, XREAL_0, FUNCT_2, DOMAIN_1,
METRIC_1, RCOMP_1, STRUCT_0, ROUGHS_1, PARTFUN3, ROUGHIF1;
constructors REALSET2, RELSET_1, PARTFUN3, METRIC_1, ROUGHIF1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FINSET_1, NAT_1, STRUCT_0, FUNCT_2,
CARD_1, ORDINAL1, METRIC_1, NUMBERS, XXREAL_0, XREAL_0, MEMBERED,
FUZNORM1, XCMPLX_0, ROUGHIF1;
requirements BOOLE, SUBSET, NUMERALS, REAL, ARITHM;
begin :: Preliminaries
theorem :: ROUGHIF2:1
for a,b,c being Real st a <= b & b > 0 & c >= 0
holds a / b <= (a + c) / (b + c);
theorem :: ROUGHIF2:2
for x1,x2 being finite set holds
card (x1 \+\ x2) = card (x1 \ x2) + card (x2 \ x1);
theorem :: ROUGHIF2:3
for x1,x2 being finite set holds
(2 * card (x1 \+\ x2)) / (card x1 + card x2 + card (x1 \+\ x2))
= card (x1 \+\ x2) / card (x1 \/ x2);
theorem :: ROUGHIF2:4
for A,B,C being set holds
A \+\ C = (A \+\ B) \+\ (B \+\ C);
theorem :: ROUGHIF2:5
for A, B be finite set st A \/ B <> {} holds
1 - card (A /\ B) / card (A \/ B) = card (A \+\ B) / card (A \/ B);
theorem :: ROUGHIF2:6
for R being finite set
for X,Y being Subset of R holds
card (X \/ Y) = card (X /\ Y) iff X = Y;
registration
cluster finite non empty for MetrSpace;
end;
begin :: Complementary RIFs
reserve R for finite Approximation_Space;
reserve X,Y,Z for Subset of R;
definition let R be finite Approximation_Space;
let f be preRIF of R;
func CMap f -> preRIF of R means
:: ROUGHIF2:def 1
for x,y being Subset of R holds
it.(x,y) = 1 - f.(x,y);
end;
theorem :: ROUGHIF2:7
for f being preRIF of R holds
CMap CMap f = f;
theorem :: ROUGHIF2:8
X <> {} implies (CMap kappa R).(X,Y) = card (X \ Y) / card X;
theorem :: ROUGHIF2:9
X = {} implies (CMap kappa R).(X,Y) = 0;
theorem :: ROUGHIF2:10
X <> {} implies (CMap kappa R).(X,Y) = kappa (X, Y`);
theorem :: ROUGHIF2:11
X \/ Y <> {} implies
(CMap kappa_1 R).(X,Y) = card (X \ Y) / card (X \/ Y);
theorem :: ROUGHIF2:12
X \/ Y = {} implies (CMap kappa_1 R).(X,Y) = 0;
theorem :: ROUGHIF2:13
(CMap kappa_2 R).(X,Y) = card (X \ Y) / card [#]R;
theorem :: ROUGHIF2:14 :: Proposition 5
X <> {} implies
kappa (X,Y) = ((CMap kappa_1 R).(X,Y`)) / (kappa_1 (Y`,X))
= ((CMap kappa_2 R).(X,Y`)) / (kappa_2 ([#]R,X));
begin :: co-RIFs
definition
let R;
let f be preRIF of R;
attr f is co-RIF-like means
:: ROUGHIF2:def 2
CMap f is RIF of R;
end;
registration let R;
let f be RIF of R;
cluster CMap f -> co-RIF-like;
end;
registration let R;
cluster co-RIF-like for preRIF of R;
end;
definition let R;
mode co-RIF of R is co-RIF-like preRIF of R;
end;
begin :: Proposition 6 REMARK: arbitrary kappa should be taken
reserve kap for RIF of R;
theorem :: ROUGHIF2:15 :: Proposition 6 a)
(CMap kap).(X,Y) = 0 iff X c= Y;
theorem :: ROUGHIF2:16 :: Proposition 6 a), specified for kappa, unnecessary
(CMap kappa R).(X,Y) = 0 iff X c= Y;
theorem :: ROUGHIF2:17 :: Proposition 6 b)
Y c= Z implies (CMap kap).(X,Z) <= (CMap kap).(X,Y);
theorem :: ROUGHIF2:18
:: Proposition 6 b) probably will be removed as a consequence
Y c= Z implies (CMap kappa R).(X,Z) <= (CMap kappa R).(X,Y);
theorem :: ROUGHIF2:19 :: Proposition 6 c)
(CMap kappa_2 R).(X,Y) <= (CMap kappa_1 R).(X,Y) <= (CMap kappa R).(X,Y);
theorem :: ROUGHIF2:20
for a,b,c being Real st a <= b & b > 0 & c >= 0 & b > c
holds a / b >= (a - c) / (b - c);
theorem :: ROUGHIF2:21
X <> {} & Y = {} implies (CMap kappa_1 R).(X,Y) = 1;
theorem :: ROUGHIF2:22
X = {} & Y <> {} implies (CMap kappa_1 R).(X,Y) = 0;
theorem :: ROUGHIF2:23 :: Proposition 6 d1)
(CMap kappa_1 R).(X,Y) + (CMap kappa_1 R).(Y,Z) >= (CMap kappa_1 R).(X,Z);
::: satisfies the triangle inequality as an attribute?
theorem :: ROUGHIF2:24 :: Proposition 6 e)
0 <= (CMap kappa R).(X,Y) <= 1;
theorem :: ROUGHIF2:25 :: Proposition 6 e1)
0 <= (CMap kappa_1 R).(X,Y) + (CMap kappa_1 R).(Y,X) <= 1;
theorem :: ROUGHIF2:26 :: Proposition 6 e2)
0 <= (CMap kappa_2 R).(X,Y) + (CMap kappa_2 R).(Y,X) <= 1;
theorem :: ROUGHIF2:27 :: Proposition 6 f)
(X = {} & Y <> {}) or (X <> {} & Y = {}) implies
(CMap kappa R).(X,Y) + (CMap kappa R).(Y,X) =
(CMap kappa_1 R).(X,Y) + (CMap kappa_1 R).(Y,X) = 1;
definition let R;
func delta_L R -> preRIF of R means
:: ROUGHIF2:def 3
for x,y being Subset of R holds
it.(x,y) = ((CMap kappa R).(x,y) + (CMap kappa R).(y,x)) / 2;
func delta_1 R -> preRIF of R means
:: ROUGHIF2:def 4
for x,y being Subset of R holds
it.(x,y) = (CMap kappa_1 R).(x,y) + (CMap kappa_1 R).(y,x);
func delta_2 R -> preRIF of R means
:: ROUGHIF2:def 5
for x,y being Subset of R holds
it.(x,y) = (CMap kappa_2 R).(x,y) + (CMap kappa_2 R).(y,x);
end;
theorem :: ROUGHIF2:28 :: Proposition 7 aL)
(delta_L R).(X,Y) = 0 iff X = Y;
theorem :: ROUGHIF2:29 :: Proposition 7 bL)
(delta_L R).(X,Y) = (delta_L R).(Y,X);
theorem :: ROUGHIF2:30 :: Formula (19)
(X <> {} & Y = {}) or (X = {} & Y <> {}) implies
(delta_L R).(X,Y) = 1 / 2;
theorem :: ROUGHIF2:31 :: Formula (19)
X <> {} & Y <> {} implies
(delta_L R).(X,Y) = ((card (X \ Y) / card X) + (card (Y \ X) / card Y)) / 2
;
theorem :: ROUGHIF2:32 :: (19)
(delta_1 R).(X,Y) = card (X \+\ Y) / card (X \/ Y);
theorem :: ROUGHIF2:33 :: (19)
(delta_2 R).(X,Y) = card (X \+\ Y) / card [#]R;
theorem :: ROUGHIF2:34 :: Proposition 7 c1)
(delta_1 R).(X,Y) + (delta_1 R).(Y,Z) >= (delta_1 R).(X,Z);
theorem :: ROUGHIF2:35 :: Proposition 7 a1)
(delta_1 R).(X,Y) = 0 iff X = Y;
theorem :: ROUGHIF2:36 :: Proposition 7 bL)
(delta_1 R).(X,Y) = (delta_1 R).(Y,X);
theorem :: ROUGHIF2:37 :: Proposition 7 a2)
(delta_2 R).(X,Y) = 0 iff X = Y;
theorem :: ROUGHIF2:38 :: Proposition 7 b2)
(delta_2 R).(X,Y) = (delta_2 R).(Y,X);
theorem :: ROUGHIF2:39 :: Proposition 6 d2)
(CMap kappa_2 R).(X,Y) + (CMap kappa_2 R).(Y,Z) >= (CMap kappa_2 R).(X,Z);
theorem :: ROUGHIF2:40 :: Proposition 7 c2)
(delta_2 R).(X,Y) + (delta_2 R).(Y,Z) >= (delta_2 R).(X,Z);
begin :: Jaccard Index Measuring Similarity of Sets
definition let R be finite set;
let A, B be Subset of R;
func JaccardIndex (A,B) -> Element of [.0,1.] equals
:: ROUGHIF2:def 6
card (A /\ B) / card (A \/ B) if A \/ B <> {}
otherwise 1;
end;
theorem :: ROUGHIF2:41
for R being finite set
for A,B being Subset of R holds
JaccardIndex (A,B) = 1 iff A = B;
theorem :: ROUGHIF2:42
for R being finite set
for A,B being Subset of R holds
JaccardIndex (A,B) = JaccardIndex (B,A);
begin :: Marczewski-Steinhaus metric
definition let R be finite set;
func JaccardDist R -> Function of [:bool R, bool R:], REAL means
:: ROUGHIF2:def 7
for A, B being Subset of R holds
it.(A,B) = 1 - JaccardIndex (A,B);
end;
definition let R be finite 1-sorted;
func MarczewskiDistance R -> Function of
[:bool the carrier of R, bool the carrier of R:], REAL equals
:: ROUGHIF2:def 8
JaccardDist [#]R;
end;
begin :: Some Properties of Distances
definition let X be non empty set, ::: should be generalized in DBLSEQ_2
f be Function of [:X,X:], REAL;
redefine attr f is nonnegative-yielding means
:: ROUGHIF2:def 9
for x,y being Element of X holds
f.(x,y) >= 0;
end;
registration let X be non empty set;
cluster discerning symmetric Reflexive triangle for
Function of [:X,X:],REAL;
end;
registration
let X be non empty set;
cluster Reflexive symmetric triangle -> nonnegative-yielding for
Function of [:X,X:], REAL;
end;
theorem :: ROUGHIF2:43 ::: Discerning
for X being non empty set
for f being nonnegative-yielding discerning triangle Reflexive
Function of [:X,X:], REAL,
x,y being Element of X st x <> y holds
f.(x,y) > 0;
begin :: Steinhaus Generate Metric
definition let X be non empty set,
p be Element of X;
let f be Function of [:X,X:], REAL;
func SteinhausGen (f,p) -> Function of [:X,X:], REAL means
:: ROUGHIF2:def 10
for x,y being Element of X holds
it.(x,y) = (2 * f.(x,y)) / (f.(x,p) + f.(y,p) + f.(x,y));
end;
registration
let X be non empty set,
f be nonnegative-yielding Function of [:X,X:], REAL,
p be Element of X;
cluster SteinhausGen (f,p) -> nonnegative-yielding;
end;
registration
let X be non empty set,
f be nonnegative-yielding Reflexive Function of [:X,X:], REAL,
p be Element of X;
cluster SteinhausGen (f,p) -> Reflexive;
end;
registration
let X be non empty set,
f be nonnegative-yielding discerning Function of [:X,X:], REAL,
p be Element of X;
cluster SteinhausGen (f,p) -> discerning;
end;
registration
let X be non empty set,
f be nonnegative-yielding symmetric Function of [:X,X:], REAL,
p be Element of X;
cluster SteinhausGen (f,p) -> symmetric;
end;
registration
let X be non empty set,
f be discerning symmetric triangle Reflexive Function of [:X,X:], REAL,
p be Element of X;
cluster SteinhausGen (f,p) -> triangle;
end;
begin :: Metric Given by Symmetric Difference
:: Minsum Location Problem by Sp\"ath
definition let X be finite set;
func SymmetricDiffDist X -> Function of [:bool X, bool X:], REAL means
:: ROUGHIF2:def 11
for x,y being Subset of X holds
it.(x,y) = card (x \+\ y);
end;
registration let X be finite set;
cluster SymmetricDiffDist X -> Reflexive discerning symmetric triangle;
end;
definition let X be finite set;
func SymDifMetrSpace X -> MetrStruct equals
:: ROUGHIF2:def 12
MetrStruct (# bool X, SymmetricDiffDist X #);
end;
registration let X be finite set;
cluster SymDifMetrSpace X -> non empty;
end;
registration let X be finite set;
cluster SymDifMetrSpace X -> Reflexive discerning symmetric triangle;
end;
begin :: Marczewski-Steinhaus Metric is Generated by Steinhaus Generate Metric
theorem :: ROUGHIF2:44
for R being finite set
for A, B being Subset of R holds
(JaccardDist R).(A,B) = card (A \+\ B) / card (A \/ B);
theorem :: ROUGHIF2:45
for X being finite set holds
JaccardDist X = SteinhausGen (SymmetricDiffDist X, {}X);
begin :: Steinhaus Metric Spaces
registration let M be finite non empty MetrSpace;
cluster the distance of M -> symmetric Reflexive discerning triangle;
end;
definition let M be finite non empty MetrStruct,
p be Element of M;
func SteinhausMetrSpace (M,p) -> MetrStruct equals
:: ROUGHIF2:def 13
MetrStruct (# the carrier of M, SteinhausGen (the distance of M, p) #);
end;
definition let M be MetrStruct;
attr M is with_nonnegative_distance means
:: ROUGHIF2:def 14
the distance of M is nonnegative-yielding;
end;
registration let A be finite non empty set;
cluster discrete_dist A -> finite non empty nonnegative-yielding;
end;
registration
cluster finite non empty with_nonnegative_distance for MetrSpace;
end;
registration let M be finite non empty with_nonnegative_distance MetrStruct,
p be Element of M;
cluster SteinhausMetrSpace (M,p) -> with_nonnegative_distance;
end;
registration let M be finite non empty with_nonnegative_distance
discerning MetrStruct,
p be Element of M;
cluster SteinhausMetrSpace (M,p) -> discerning;
end;
registration let M be finite non empty with_nonnegative_distance
Reflexive MetrStruct,
p be Element of M;
cluster SteinhausMetrSpace (M,p) -> Reflexive;
end;
registration let M be finite non empty with_nonnegative_distance
symmetric MetrStruct,
p be Element of M;
cluster SteinhausMetrSpace (M,p) -> symmetric;
end;
registration let M be finite non empty discerning symmetric Reflexive
triangle MetrStruct,
p be Element of M;
cluster SteinhausMetrSpace (M,p) -> triangle;
end;
registration let R be finite 1-sorted;
cluster MarczewskiDistance R -> Reflexive discerning symmetric;
end;
theorem :: ROUGHIF2:46
for R being finite Approximation_Space
for A, B being Subset of R holds
(MarczewskiDistance R).(A,B) = (delta_1 R).(A,B);
registration let R be finite 1-sorted;
cluster MarczewskiDistance R -> triangle;
end;