:: The Geometric Interior in Real Linear Spaces
:: by Karol P\c{a}k
::
:: Received February 9, 2010
:: Copyright (c) 2010-2011 Association of Mizar Users

begin

Lm1: for r being Real
for V being RealLinearSpace
for u, w, v being VECTOR of V st r <> 1 & (r * u) + ((1 - r) * w) = v holds
w = ((1 / (1 - r)) * v) + ((1 - (1 / (1 - r))) * u)

proof end;

theorem Th1: :: RLAFFIN2:1

for V being RealLinearSpace
for v being VECTOR of V
for A being Subset of V
for L being Linear_Combination of A st L is convex & v <> Sum L & L . v <> 0 holds
ex p being VECTOR of V 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 )

proof end;

theorem :: RLAFFIN2:2

for r, s being Real
for V being RealLinearSpace
for v, u being VECTOR of V
for I being affinely-independent Subset of V
for p1, p2, w1, w2 being 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 )

proof end;

theorem Th3: :: RLAFFIN2:3

for V being RealLinearSpace
for Af being finite Subset of V
for If being finite affinely-independent Subset of V
for L being Linear_Combination of Af st Af c= conv If & sum L = 1 holds
( Sum L in Affin If & ( for x being Element of V ex F being FinSequence of REAL ex G being 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 being Nat st n in dom F holds
F . n = (L . (G . n)) * (((G . n) |-- If) . x) ) ) ) )

proof end;

theorem :: RLAFFIN2:4

for V being RealLinearSpace
for v being VECTOR of V
for A, B, Aff being 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)

proof end;

begin

definition

let V be non empty RLSStruct ;
let A be Subset of V;
func Int A -> Subset of V means :Def1: :: RLAFFIN2:def 1
for x being set holds
( x in it iff ( x in conv A & ( for B being Subset of V holds
( not B c< A or not x in conv B ) ) ) );
existence
ex b₁ being Subset of V st
for x being set holds
( x in b₁ iff ( x in conv A & ( for B being Subset of V holds
( not B c< A or not x in conv B ) ) ) )

proof end;

uniqueness
for b₁, b₂ being Subset of V st ( for x being set holds
( x in b₁ iff ( x in conv A & ( for B being Subset of V holds
( not B c< A or not x in conv B ) ) ) ) ) & ( for x being set holds
( x in b₂ iff ( x in conv A & ( for B being Subset of V holds
( not B c< A or not x in conv B ) ) ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines Int RLAFFIN2:def 1 :
for V being non empty RLSStruct
for A, b₃ being Subset of V holds
( b₃ = Int A iff for x being set holds
( x in b₃ iff ( x in conv A & ( for B being Subset of V holds
( not B c< A or not x in conv B ) ) ) ) );

Lm2: for V being non empty RLSStruct
for A being Subset of V holds Int A c= conv A

proof end;

registration

let V be non empty RLSStruct ;
let A be empty Subset of V;
cluster Int A -> empty ;
coherence
Int A is empty

proof end;

end;

theorem :: RLAFFIN2:5

for V being non empty RLSStruct
for A being Subset of V holds Int A c= conv A by Lm2;

theorem :: RLAFFIN2:6

for V being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for A being Subset of V holds
( Int A = A iff A is trivial )

proof end;

theorem :: RLAFFIN2:7

for V being RealLinearSpace
for A, B being Subset of V st A c< B holds
conv A misses Int B

proof end;

theorem Th8: :: RLAFFIN2:8

for V being RealLinearSpace
for A being Subset of V holds conv A = union { (Int B) where B is Subset of V : B c= A }

proof end;

theorem :: RLAFFIN2:9

for V being RealLinearSpace
for A being Subset of V holds conv A = (Int A) \/ (union { (conv (A \ {v})) where v is VECTOR of V : v in A } )

proof end;

theorem Th10: :: RLAFFIN2:10

for x being set
for V being RealLinearSpace
for A being Subset of V st x in Int A holds
ex L being Linear_Combination of A st
( L is convex & x = Sum L )

proof end;

theorem Th11: :: RLAFFIN2:11

for V being RealLinearSpace
for A being Subset of V
for L being Linear_Combination of A st L is convex & Sum L in Int A holds
Carrier L = A

proof end;

theorem Th12: :: RLAFFIN2:12

for V being RealLinearSpace
for I being affinely-independent Subset of V
for L being Linear_Combination of I st L is convex & Carrier L = I holds
Sum L in Int I

proof end;

theorem :: RLAFFIN2:13

for V being RealLinearSpace
for A being Subset of V st not Int A is empty holds
A is finite

proof end;

theorem :: RLAFFIN2:14

for r being Real
for V being RealLinearSpace
for v, u, p being VECTOR of V
for I being affinely-independent Subset of V st v in I & u in Int I & p in conv (I \ {v}) & (r * v) + ((1 - r) * p) = u holds
p in Int (I \ {v})

proof end;

begin

definition

let V be RealLinearSpace;
func center_of_mass V -> Function of (BOOL the carrier of V), the carrier of V means :Def2: :: RLAFFIN2:def 2
( ( for A being non empty finite Subset of V holds it . A = (1 / (card A)) * (Sum A) ) & ( for A being Subset of V st not A is finite holds
it . A = 0. V ) );
existence
ex b₁ being Function of (BOOL the carrier of V), the carrier of V st
( ( for A being non empty finite Subset of V holds b₁ . A = (1 / (card A)) * (Sum A) ) & ( for A being Subset of V st not A is finite holds
b₁ . A = 0. V ) )

proof end;

uniqueness
for b₁, b₂ being Function of (BOOL the carrier of V), the carrier of V st ( for A being non empty finite Subset of V holds b₁ . A = (1 / (card A)) * (Sum A) ) & ( for A being Subset of V st not A is finite holds
b₁ . A = 0. V ) & ( for A being non empty finite Subset of V holds b₂ . A = (1 / (card A)) * (Sum A) ) & ( for A being Subset of V st not A is finite holds
b₂ . A = 0. V ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines center_of_mass RLAFFIN2:def 2 :
for V being RealLinearSpace
for b₂ being Function of (BOOL the carrier of V), the carrier of V holds
( b₂ = center_of_mass V iff ( ( for A being non empty finite Subset of V holds b₂ . A = (1 / (card A)) * (Sum A) ) & ( for A being Subset of V st not A is finite holds
b₂ . A = 0. V ) ) );

theorem Th15: :: RLAFFIN2:15

for r being Real
for V being RealLinearSpace
for Af being finite Subset of V ex L being Linear_Combination of Af st
( Sum L = r * (Sum Af) & sum L = r * (card Af) & L = (ZeroLC V) +* (Af --> r) )

proof end;

theorem Th16: :: RLAFFIN2:16

for V being RealLinearSpace
for Af being finite Subset of V st not Af is empty holds
(center_of_mass V) . Af in conv Af

proof end;

theorem Th17: :: RLAFFIN2:17

for V being RealLinearSpace
for F being Subset-Family of V st union F is finite holds
(center_of_mass V) .: F c= conv (union F)

proof end;

theorem Th18: :: RLAFFIN2:18

for V being RealLinearSpace
for v being VECTOR of V
for If being finite affinely-independent Subset of V st v in If holds
(((center_of_mass V) . If) |-- If) . v = 1 / (card If)

proof end;

theorem Th19: :: RLAFFIN2:19

for V being RealLinearSpace
for If being finite affinely-independent Subset of V holds
( (center_of_mass V) . If in If iff card If = 1 )

proof end;

theorem Th20: :: RLAFFIN2:20

for V being RealLinearSpace
for If being finite affinely-independent Subset of V st not If is empty holds
(center_of_mass V) . If in Int If

proof end;

theorem :: RLAFFIN2:21

for V being RealLinearSpace
for A being Subset of V
for If being finite affinely-independent Subset of V st A c= If & (center_of_mass V) . If in Affin A holds
If = A

proof end;

theorem Th22: :: RLAFFIN2:22

for V being RealLinearSpace
for v being VECTOR of V
for Af being finite Subset of V st v in Af & not Af \ {v} is empty holds
(center_of_mass V) . Af = ((1 - (1 / (card Af))) * ((center_of_mass V) /. (Af \ {v}))) + ((1 / (card Af)) * v)

proof end;

theorem :: RLAFFIN2:23

for V being RealLinearSpace
for A being Subset of V
for If being finite affinely-independent Subset of V st conv A c= conv If & not If is empty & conv A misses Int If holds
ex B being Subset of V st
( B c< If & conv A c= conv B )

proof end;

theorem Th24: :: RLAFFIN2:24

for V being RealLinearSpace
for L1, L2 being Linear_Combination of V st Sum L1 <> Sum L2 & sum L1 = sum L2 holds
ex v being VECTOR of V st L1 . v > L2 . v

proof end;

Lm3: for r, s being Real
for V being RealLinearSpace
for v being VECTOR of V
for L1, L2 being Linear_Combination of V st L1 . v <> L2 . v holds
( ((r * L1) + ((1 - r) * L2)) . v = s iff r = ((L2 . v) - s) / ((L2 . v) - (L1 . v)) )

proof end;

theorem Th25: :: RLAFFIN2:25

for r, s being Real
for V being RealLinearSpace
for v being VECTOR of V
for L1, L2 being Linear_Combination of V
for p being Real st ((r * L1) + ((1 - r) * L2)) . v <= p & p <= ((s * L1) + ((1 - s) * L2)) . v holds
ex rs being Real st
( ((rs * L1) + ((1 - rs) * L2)) . v = p & ( r <= s implies ( r <= rs & rs <= s ) ) & ( s <= r implies ( s <= rs & rs <= r ) ) )

proof end;

theorem :: RLAFFIN2:26

for V being RealLinearSpace
for v, u being VECTOR of V
for A being Subset of V st v in conv A & u in conv A & v <> u holds
ex p, w being VECTOR of V ex r being Real st
( p in A & w in conv (A \ {p}) & 0 <= r & r < 1 & (r * u) + ((1 - r) * w) = v )

proof end;

theorem Th27: :: RLAFFIN2:27

for V being RealLinearSpace
for v being VECTOR of V
for A being Subset of V holds
( A \/ {v} is affinely-independent iff ( A is affinely-independent & ( v in A or not v in Affin A ) ) ) by RLAFFIN1:82;

theorem Th28: :: RLAFFIN2:28

for V being RealLinearSpace
for v being VECTOR of V
for Af being finite Subset of V
for I being affinely-independent Subset of V st Af c= I & v in Af holds
(I \ {v}) \/ {((center_of_mass V) . Af)} is affinely-independent Subset of V

proof end;

theorem Th29: :: RLAFFIN2:29

for V being RealLinearSpace
for F being c=-linear Subset-Family of V st union F is finite & union F is affinely-independent holds
(center_of_mass V) .: F is affinely-independent Subset of V

proof end;

theorem :: RLAFFIN2:30

for V being RealLinearSpace
for F being c=-linear Subset-Family of V st union F is affinely-independent & union F is finite holds
Int ((center_of_mass V) .: F) c= Int (union F)

proof end;