:: The Geometric Interior in Real Linear Spaces
:: by Karol P\c{a}k
::
:: Received February 9, 2010
:: Copyright (c) 2010-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 ARYTM_1, ARYTM_3, XBOOLE_0, CARD_1, CONVEX1, CONVEX2, CONVEX3,
FINSEQ_1, FINSEQ_2, FINSEQ_4, FINSET_1, FUNCOP_1, FUNCT_1, FUNCT_2,
FUNCT_4, MEMBERED, ORDERS_1, RELAT_1, RLVECT_1, RLVECT_2, RUSUB_4,
SEMI_AF1, SETFAM_1, TARSKI, TOPS_1, RLAFFIN1, RLAFFIN2, ZFMISC_1, REAL_1,
CARD_3, XXREAL_0, NAT_1, SUBSET_1, NUMBERS, ORDINAL1, STRUCT_0, SUPINF_2,
ORDINAL4, VALUED_1, XREAL_0, PARTFUN1;
notations TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, ORDINAL1, NUMBERS, XCMPLX_0,
XXREAL_0, ORDERS_1, CARD_1, XREAL_0, REAL_1, FINSET_1, SETFAM_1,
DOMAIN_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, RELSET_1, FINSEQ_1,
STRUCT_0, FINSEQ_2, FINSEQOP, RVSUM_1, RLVECT_1, RLVECT_2, RUSUB_4,
CONVEX1, CONVEX2, CONVEX3, RLAFFIN1, FUNCT_4, FUNCOP_1, MEMBERED,
XXREAL_2;
constructors BINOP_2, CONVEX1, CONVEX3, DOMAIN_1, FINSEQOP, REAL_1, RVSUM_1,
RUSUB_5, SETFAM_1, RLAFFIN1, SIMPLEX0, XXREAL_2, FUNCT_4, RELSET_1;
registrations CARD_1, FINSET_1, FINSEQ_2, FUNCT_2, MEMBERED, NAT_1, NUMBERS,
RELAT_1, RLVECT_1, STRUCT_0, SUBSET_1, VALUED_0, XCMPLX_0, XREAL_0,
XXREAL_0, RLAFFIN1, FUNCOP_1, SETFAM_1, XXREAL_2, ABIAN, RELSET_1,
RLVECT_2, ORDINAL1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
begin :: Preliminaries
reserve x,y for set,
r,s for Real,
n for Nat,
V for RealLinearSpace,
v,u,w,p for VECTOR of V,
A,B for Subset of V,
Af for finite Subset of V,
I for affinely-independent Subset of V,
If for finite affinely-independent Subset of V,
F for Subset-Family of V,
L1,L2 for Linear_Combination of V;
theorem :: RLAFFIN2:1
for L be Linear_Combination of A st L is convex & v <> Sum L & L.v <> 0
ex p st p in conv(A\{v}) & Sum L = L.v*v + (1-L.v)*p &
1/L.v*(Sum L) + (1-1/L.v)*p = v;
theorem :: RLAFFIN2:2
for p1,p2,w1,w2 be Element of V st v in conv I & u in conv I &
not u in conv(I\{p1}) & not u in conv(I\{p2}) &
w1 in conv(I\{p1}) & w2 in conv(I\{p2}) &
r*u+(1-r)*w1 = v & s*u + (1-s)*w2 = v & r < 1 & s < 1
holds w1 = w2 & r = s;
theorem :: RLAFFIN2:3
for L be Linear_Combination of Af st Af c=conv If & sum L=1 holds
Sum L in Affin If
& for x be Element of V
ex F be FinSequence of REAL,G be FinSequence of V st
(Sum L|--If).x = Sum F & len G = len F & G is one-to-one &
rng G = Carrier L &
for n st n in dom F holds F.n = L.(G.n)*(G.n|--If).x;
theorem :: RLAFFIN2:4
for Aff be Subset of V st Aff is Affine & conv A /\ conv B c= Aff &
conv(A\{v}) c= Aff & not v in Aff
holds conv (A\{v}) /\ conv B = conv A /\ conv B;
begin :: The Geometric Interior
definition
let V be non empty RLSStruct;
let A be Subset of V;
func Int A -> Subset of V means
:: RLAFFIN2:def 1
x in it iff x in conv A & not ex B be Subset of V st B c< A & x in conv B;
end;
registration
let V be non empty RLSStruct;
let A be empty Subset of V;
cluster Int A -> empty;
end;
theorem :: RLAFFIN2:5
for V be non empty RLSStruct for A be Subset of V holds Int A c= conv A;
theorem :: RLAFFIN2:6
for V be vector-distributive scalar-distributive scalar-associative
scalar-unitalnon empty RLSStruct
for A be Subset of V holds Int A = A iff A is trivial;
theorem :: RLAFFIN2:7
A c< B implies conv A misses Int B;
theorem :: RLAFFIN2:8
conv A = union {Int B : B c= A};
theorem :: RLAFFIN2:9
conv A = Int A \/ union{conv (A\{v}) : v in A};
theorem :: RLAFFIN2:10
x in Int A implies ex L be Linear_Combination of A st L is convex & x = Sum L
;
theorem :: RLAFFIN2:11
for L be Linear_Combination of A st L is convex & Sum L in Int A
holds Carrier L = A;
theorem :: RLAFFIN2:12
for L be Linear_Combination of I st L is convex & Carrier L = I holds
Sum L in Int I;
theorem :: RLAFFIN2:13
Int A is non empty implies A is finite;
theorem :: RLAFFIN2:14
v in I & u in Int I & p in conv(I\{v}) & r*v + (1-r)*p = u implies
p in Int (I\{v});
begin :: The Center of Mass
definition let V;
func center_of_mass V -> Function of BOOL the carrier of V,the carrier of V
means
:: RLAFFIN2:def 2
(for A be non empty finite Subset of V holds it.A = 1/card A * Sum(A)) &
for A st A is infinite holds it.A = 0.V;
end;
theorem :: RLAFFIN2:15
ex L be Linear_Combination of Af st Sum L = r*Sum Af & sum L = r * card Af &
L = (ZeroLC V) +* (Af-->r);
theorem :: RLAFFIN2:16
Af is non empty implies (center_of_mass V).Af in conv Af;
theorem :: RLAFFIN2:17
union F is finite implies (center_of_mass V).:F c= conv union F;
theorem :: RLAFFIN2:18
v in If implies ((center_of_mass V).If |-- If).v = 1/card If;
theorem :: RLAFFIN2:19
(center_of_mass V).If in If iff card If=1;
theorem :: RLAFFIN2:20
If is non empty implies (center_of_mass V).If in Int If;
theorem :: RLAFFIN2:21
A c= If & (center_of_mass V).If in Affin A implies If = A;
theorem :: RLAFFIN2:22
v in Af & Af\{v} is non empty implies (center_of_mass V).Af =
(1-1/card Af) * (center_of_mass V)/.(Af\{v}) + 1/card Af*v;
theorem :: RLAFFIN2:23
conv A c=conv If & If is non empty & conv A misses Int If implies
ex B be Subset of V st B c< If & conv A c= conv B;
theorem :: RLAFFIN2:24
Sum L1 <> Sum L2 & sum L1 = sum L2 implies ex v st L1.v > L2.v;
theorem :: RLAFFIN2:25
for p be Real st (r*L1+(1-r)*L2).v <= p & p <= (s*L1+(1-s)*L2).v
ex rs be Real st (rs*L1+(1-rs)*L2).v = p &
(r <= s implies r <= rs & rs <= s) &
(s <= r implies s <= rs & rs <= r);
theorem :: RLAFFIN2:26
v in conv A & u in conv A & v <> u implies
ex p,w,r st p in A & w in conv(A\{p}) & 0<=r & r<1 & r*u+(1-r)*w = v;
theorem :: RLAFFIN2:27
A\/{v} is affinely-independent iff
A is affinely-independent & (v in A or not v in Affin A);
theorem :: RLAFFIN2:28
Af c= I & v in Af implies
I\{v}\/{(center_of_mass V).Af} is affinely-independent Subset of V;
theorem :: RLAFFIN2:29
for F be c=-linear Subset-Family of V st
union F is finite affinely-independent
holds (center_of_mass V).:F is affinely-independent Subset of V;
theorem :: RLAFFIN2:30
for F be c=-linear Subset-Family of V st
union F is affinely-independent finite
holds Int ((center_of_mass V).:F) c= Int union F;