:: 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;