:: CONVEX2 semantic presentation
begin
reconsider rr = 1 as Real ;
set ff = <*rr*>;
theorem :: CONVEX2:1
for V being non empty RLSStruct
for M, N being convex Subset of V holds M /\ N is convex ;
theorem :: CONVEX2:2
for V being non empty RealUnitarySpace-like UNITSTR
for M being Subset of V
for F being FinSequence of the carrier of V
for B being FinSequence of REAL st M = { u where u is VECTOR of V : for i being Element of NAT st i in (dom F) /\ (dom B) holds
ex v being VECTOR of V st
( v = F . i & u .|. v <= B . i ) } holds
M is convex
proof
let V be non empty RealUnitarySpace-like UNITSTR ; ::_thesis: for M being Subset of V
for F being FinSequence of the carrier of V
for B being FinSequence of REAL st M = { u where u is VECTOR of V : for i being Element of NAT st i in (dom F) /\ (dom B) holds
ex v being VECTOR of V st
( v = F . i & u .|. v <= B . i ) } holds
M is convex
let M be Subset of V; ::_thesis: for F being FinSequence of the carrier of V
for B being FinSequence of REAL st M = { u where u is VECTOR of V : for i being Element of NAT st i in (dom F) /\ (dom B) holds
ex v being VECTOR of V st
( v = F . i & u .|. v <= B . i ) } holds
M is convex
let F be FinSequence of the carrier of V; ::_thesis: for B being FinSequence of REAL st M = { u where u is VECTOR of V : for i being Element of NAT st i in (dom F) /\ (dom B) holds
ex v being VECTOR of V st
( v = F . i & u .|. v <= B . i ) } holds
M is convex
let B be FinSequence of REAL ; ::_thesis: ( M = { u where u is VECTOR of V : for i being Element of NAT st i in (dom F) /\ (dom B) holds
ex v being VECTOR of V st
( v = F . i & u .|. v <= B . i ) } implies M is convex )
assume A1: M = { u where u is VECTOR of V : for i being Element of NAT st i in (dom F) /\ (dom B) holds
ex v being VECTOR of V st
( v = F . i & u .|. v <= B . i ) } ; ::_thesis: M is convex
let u1, v1 be VECTOR of V; :: according to CONVEX1:def_2 ::_thesis: for b1 being Element of REAL holds
( b1 <= 0 or 1 <= b1 or not u1 in M or not v1 in M or (b1 * u1) + ((1 - b1) * v1) in M )
let r be Real; ::_thesis: ( r <= 0 or 1 <= r or not u1 in M or not v1 in M or (r * u1) + ((1 - r) * v1) in M )
assume that
A2: 0 < r and
A3: r < 1 and
A4: u1 in M and
A5: v1 in M ; ::_thesis: (r * u1) + ((1 - r) * v1) in M
consider v9 being VECTOR of V such that
A6: v1 = v9 and
A7: for i being Element of NAT st i in (dom F) /\ (dom B) holds
ex v being VECTOR of V st
( v = F . i & v9 .|. v <= B . i ) by A1, A5;
consider u9 being VECTOR of V such that
A8: u1 = u9 and
A9: for i being Element of NAT st i in (dom F) /\ (dom B) holds
ex v being VECTOR of V st
( v = F . i & u9 .|. v <= B . i ) by A1, A4;
for i being Element of NAT st i in (dom F) /\ (dom B) holds
ex v being VECTOR of V st
( v = F . i & ((r * u1) + ((1 - r) * v1)) .|. v <= B . i )
proof
0 + r < 1 by A3;
then A10: 1 - r > 0 by XREAL_1:20;
let i be Element of NAT ; ::_thesis: ( i in (dom F) /\ (dom B) implies ex v being VECTOR of V st
( v = F . i & ((r * u1) + ((1 - r) * v1)) .|. v <= B . i ) )
assume A11: i in (dom F) /\ (dom B) ; ::_thesis: ex v being VECTOR of V st
( v = F . i & ((r * u1) + ((1 - r) * v1)) .|. v <= B . i )
then i in dom B by XBOOLE_0:def_4;
then reconsider b = B . i as Real by PARTFUN1:4;
consider x being VECTOR of V such that
A12: x = F . i and
A13: u9 .|. x <= b by A9, A11;
take v = x; ::_thesis: ( v = F . i & ((r * u1) + ((1 - r) * v1)) .|. v <= B . i )
A14: ((r * u1) + ((1 - r) * v1)) .|. v = ((r * u1) .|. v) + (((1 - r) * v1) .|. v) by BHSP_1:def_2
.= (r * (u1 .|. v)) + (((1 - r) * v1) .|. v) by BHSP_1:def_2
.= (r * (u1 .|. v)) + ((1 - r) * (v1 .|. v)) by BHSP_1:def_2 ;
r * (u1 .|. v) <= r * b by A2, A8, A13, XREAL_1:64;
then ((r * u1) + ((1 - r) * v1)) .|. v <= (r * b) + ((1 - r) * (v1 .|. v)) by A14, XREAL_1:6;
then A15: (((r * u1) + ((1 - r) * v1)) .|. v) - (r * b) <= (1 - r) * (v1 .|. v) by XREAL_1:20;
ex y being VECTOR of V st
( y = F . i & v9 .|. y <= b ) by A7, A11;
then (1 - r) * (v1 .|. v) <= (1 - r) * b by A6, A12, A10, XREAL_1:64;
then (((r * u1) + ((1 - r) * v1)) .|. v) - (r * b) <= (1 - r) * b by A15, XXREAL_0:2;
then ((r * u1) + ((1 - r) * v1)) .|. v <= (r * b) + ((1 - r) * b) by XREAL_1:20;
hence ( v = F . i & ((r * u1) + ((1 - r) * v1)) .|. v <= B . i ) by A12; ::_thesis: verum
end;
hence (r * u1) + ((1 - r) * v1) in M by A1; ::_thesis: verum
end;
theorem :: CONVEX2:3
for V being non empty RealUnitarySpace-like UNITSTR
for M being Subset of V
for F being FinSequence of the carrier of V
for B being FinSequence of REAL st M = { u where u is VECTOR of V : for i being Element of NAT st i in (dom F) /\ (dom B) holds
ex v being VECTOR of V st
( v = F . i & u .|. v < B . i ) } holds
M is convex
proof
let V be non empty RealUnitarySpace-like UNITSTR ; ::_thesis: for M being Subset of V
for F being FinSequence of the carrier of V
for B being FinSequence of REAL st M = { u where u is VECTOR of V : for i being Element of NAT st i in (dom F) /\ (dom B) holds
ex v being VECTOR of V st
( v = F . i & u .|. v < B . i ) } holds
M is convex
let M be Subset of V; ::_thesis: for F being FinSequence of the carrier of V
for B being FinSequence of REAL st M = { u where u is VECTOR of V : for i being Element of NAT st i in (dom F) /\ (dom B) holds
ex v being VECTOR of V st
( v = F . i & u .|. v < B . i ) } holds
M is convex
let F be FinSequence of the carrier of V; ::_thesis: for B being FinSequence of REAL st M = { u where u is VECTOR of V : for i being Element of NAT st i in (dom F) /\ (dom B) holds
ex v being VECTOR of V st
( v = F . i & u .|. v < B . i ) } holds
M is convex
let B be FinSequence of REAL ; ::_thesis: ( M = { u where u is VECTOR of V : for i being Element of NAT st i in (dom F) /\ (dom B) holds
ex v being VECTOR of V st
( v = F . i & u .|. v < B . i ) } implies M is convex )
assume A1: M = { u where u is VECTOR of V : for i being Element of NAT st i in (dom F) /\ (dom B) holds
ex v being VECTOR of V st
( v = F . i & u .|. v < B . i ) } ; ::_thesis: M is convex
let u1, v1 be VECTOR of V; :: according to CONVEX1:def_2 ::_thesis: for b1 being Element of REAL holds
( b1 <= 0 or 1 <= b1 or not u1 in M or not v1 in M or (b1 * u1) + ((1 - b1) * v1) in M )
let r be Real; ::_thesis: ( r <= 0 or 1 <= r or not u1 in M or not v1 in M or (r * u1) + ((1 - r) * v1) in M )
assume that
A2: 0 < r and
A3: r < 1 and
A4: u1 in M and
A5: v1 in M ; ::_thesis: (r * u1) + ((1 - r) * v1) in M
consider v9 being VECTOR of V such that
A6: v1 = v9 and
A7: for i being Element of NAT st i in (dom F) /\ (dom B) holds
ex v being VECTOR of V st
( v = F . i & v9 .|. v < B . i ) by A1, A5;
consider u9 being VECTOR of V such that
A8: u1 = u9 and
A9: for i being Element of NAT st i in (dom F) /\ (dom B) holds
ex v being VECTOR of V st
( v = F . i & u9 .|. v < B . i ) by A1, A4;
for i being Element of NAT st i in (dom F) /\ (dom B) holds
ex v being VECTOR of V st
( v = F . i & ((r * u1) + ((1 - r) * v1)) .|. v < B . i )
proof
0 + r < 1 by A3;
then A10: 1 - r > 0 by XREAL_1:20;
let i be Element of NAT ; ::_thesis: ( i in (dom F) /\ (dom B) implies ex v being VECTOR of V st
( v = F . i & ((r * u1) + ((1 - r) * v1)) .|. v < B . i ) )
assume A11: i in (dom F) /\ (dom B) ; ::_thesis: ex v being VECTOR of V st
( v = F . i & ((r * u1) + ((1 - r) * v1)) .|. v < B . i )
then i in dom B by XBOOLE_0:def_4;
then reconsider b = B . i as Real by PARTFUN1:4;
consider x being VECTOR of V such that
A12: x = F . i and
A13: u9 .|. x < b by A9, A11;
take v = x; ::_thesis: ( v = F . i & ((r * u1) + ((1 - r) * v1)) .|. v < B . i )
A14: ((r * u1) + ((1 - r) * v1)) .|. v = ((r * u1) .|. v) + (((1 - r) * v1) .|. v) by BHSP_1:def_2
.= (r * (u1 .|. v)) + (((1 - r) * v1) .|. v) by BHSP_1:def_2
.= (r * (u1 .|. v)) + ((1 - r) * (v1 .|. v)) by BHSP_1:def_2 ;
r * (u1 .|. v) < r * b by A2, A8, A13, XREAL_1:68;
then ((r * u1) + ((1 - r) * v1)) .|. v < (r * b) + ((1 - r) * (v1 .|. v)) by A14, XREAL_1:8;
then A15: (((r * u1) + ((1 - r) * v1)) .|. v) - (r * b) < (1 - r) * (v1 .|. v) by XREAL_1:19;
ex y being VECTOR of V st
( y = F . i & v9 .|. y < b ) by A7, A11;
then (1 - r) * (v1 .|. v) <= (1 - r) * b by A6, A12, A10, XREAL_1:64;
then (((r * u1) + ((1 - r) * v1)) .|. v) - (r * b) < (1 - r) * b by A15, XXREAL_0:2;
then ((r * u1) + ((1 - r) * v1)) .|. v < (r * b) + ((1 - r) * b) by XREAL_1:19;
hence ( v = F . i & ((r * u1) + ((1 - r) * v1)) .|. v < B . i ) by A12; ::_thesis: verum
end;
hence (r * u1) + ((1 - r) * v1) in M by A1; ::_thesis: verum
end;
theorem :: CONVEX2:4
for V being non empty RealUnitarySpace-like UNITSTR
for M being Subset of V
for F being FinSequence of the carrier of V
for B being FinSequence of REAL st M = { u where u is VECTOR of V : for i being Element of NAT st i in (dom F) /\ (dom B) holds
ex v being VECTOR of V st
( v = F . i & u .|. v >= B . i ) } holds
M is convex
proof
let V be non empty RealUnitarySpace-like UNITSTR ; ::_thesis: for M being Subset of V
for F being FinSequence of the carrier of V
for B being FinSequence of REAL st M = { u where u is VECTOR of V : for i being Element of NAT st i in (dom F) /\ (dom B) holds
ex v being VECTOR of V st
( v = F . i & u .|. v >= B . i ) } holds
M is convex
let M be Subset of V; ::_thesis: for F being FinSequence of the carrier of V
for B being FinSequence of REAL st M = { u where u is VECTOR of V : for i being Element of NAT st i in (dom F) /\ (dom B) holds
ex v being VECTOR of V st
( v = F . i & u .|. v >= B . i ) } holds
M is convex
let F be FinSequence of the carrier of V; ::_thesis: for B being FinSequence of REAL st M = { u where u is VECTOR of V : for i being Element of NAT st i in (dom F) /\ (dom B) holds
ex v being VECTOR of V st
( v = F . i & u .|. v >= B . i ) } holds
M is convex
let B be FinSequence of REAL ; ::_thesis: ( M = { u where u is VECTOR of V : for i being Element of NAT st i in (dom F) /\ (dom B) holds
ex v being VECTOR of V st
( v = F . i & u .|. v >= B . i ) } implies M is convex )
assume A1: M = { u where u is VECTOR of V : for i being Element of NAT st i in (dom F) /\ (dom B) holds
ex v being VECTOR of V st
( v = F . i & u .|. v >= B . i ) } ; ::_thesis: M is convex
let u1, v1 be VECTOR of V; :: according to CONVEX1:def_2 ::_thesis: for b1 being Element of REAL holds
( b1 <= 0 or 1 <= b1 or not u1 in M or not v1 in M or (b1 * u1) + ((1 - b1) * v1) in M )
let r be Real; ::_thesis: ( r <= 0 or 1 <= r or not u1 in M or not v1 in M or (r * u1) + ((1 - r) * v1) in M )
assume that
A2: 0 < r and
A3: r < 1 and
A4: u1 in M and
A5: v1 in M ; ::_thesis: (r * u1) + ((1 - r) * v1) in M
consider v9 being VECTOR of V such that
A6: v1 = v9 and
A7: for i being Element of NAT st i in (dom F) /\ (dom B) holds
ex v being VECTOR of V st
( v = F . i & v9 .|. v >= B . i ) by A1, A5;
consider u9 being VECTOR of V such that
A8: u1 = u9 and
A9: for i being Element of NAT st i in (dom F) /\ (dom B) holds
ex v being VECTOR of V st
( v = F . i & u9 .|. v >= B . i ) by A1, A4;
for i being Element of NAT st i in (dom F) /\ (dom B) holds
ex v being VECTOR of V st
( v = F . i & ((r * u1) + ((1 - r) * v1)) .|. v >= B . i )
proof
0 + r < 1 by A3;
then A10: 1 - r > 0 by XREAL_1:20;
let i be Element of NAT ; ::_thesis: ( i in (dom F) /\ (dom B) implies ex v being VECTOR of V st
( v = F . i & ((r * u1) + ((1 - r) * v1)) .|. v >= B . i ) )
assume A11: i in (dom F) /\ (dom B) ; ::_thesis: ex v being VECTOR of V st
( v = F . i & ((r * u1) + ((1 - r) * v1)) .|. v >= B . i )
then i in dom B by XBOOLE_0:def_4;
then reconsider b = B . i as Real by PARTFUN1:4;
consider x being VECTOR of V such that
A12: x = F . i and
A13: u9 .|. x >= b by A9, A11;
take v = x; ::_thesis: ( v = F . i & ((r * u1) + ((1 - r) * v1)) .|. v >= B . i )
A14: ((r * u1) + ((1 - r) * v1)) .|. v = ((r * u1) .|. v) + (((1 - r) * v1) .|. v) by BHSP_1:def_2
.= (r * (u1 .|. v)) + (((1 - r) * v1) .|. v) by BHSP_1:def_2
.= (r * (u1 .|. v)) + ((1 - r) * (v1 .|. v)) by BHSP_1:def_2 ;
r * (u1 .|. v) >= r * b by A2, A8, A13, XREAL_1:64;
then ((r * u1) + ((1 - r) * v1)) .|. v >= (r * b) + ((1 - r) * (v1 .|. v)) by A14, XREAL_1:6;
then A15: (((r * u1) + ((1 - r) * v1)) .|. v) - (r * b) >= (1 - r) * (v1 .|. v) by XREAL_1:19;
ex y being VECTOR of V st
( y = F . i & v9 .|. y >= b ) by A7, A11;
then (1 - r) * (v1 .|. v) >= (1 - r) * b by A6, A12, A10, XREAL_1:64;
then (((r * u1) + ((1 - r) * v1)) .|. v) - (r * b) >= (1 - r) * b by A15, XXREAL_0:2;
then ((r * u1) + ((1 - r) * v1)) .|. v >= (r * b) + ((1 - r) * b) by XREAL_1:19;
hence ( v = F . i & ((r * u1) + ((1 - r) * v1)) .|. v >= B . i ) by A12; ::_thesis: verum
end;
hence (r * u1) + ((1 - r) * v1) in M by A1; ::_thesis: verum
end;
theorem :: CONVEX2:5
for V being non empty RealUnitarySpace-like UNITSTR
for M being Subset of V
for F being FinSequence of the carrier of V
for B being FinSequence of REAL st M = { u where u is VECTOR of V : for i being Element of NAT st i in (dom F) /\ (dom B) holds
ex v being VECTOR of V st
( v = F . i & u .|. v > B . i ) } holds
M is convex
proof
let V be non empty RealUnitarySpace-like UNITSTR ; ::_thesis: for M being Subset of V
for F being FinSequence of the carrier of V
for B being FinSequence of REAL st M = { u where u is VECTOR of V : for i being Element of NAT st i in (dom F) /\ (dom B) holds
ex v being VECTOR of V st
( v = F . i & u .|. v > B . i ) } holds
M is convex
let M be Subset of V; ::_thesis: for F being FinSequence of the carrier of V
for B being FinSequence of REAL st M = { u where u is VECTOR of V : for i being Element of NAT st i in (dom F) /\ (dom B) holds
ex v being VECTOR of V st
( v = F . i & u .|. v > B . i ) } holds
M is convex
let F be FinSequence of the carrier of V; ::_thesis: for B being FinSequence of REAL st M = { u where u is VECTOR of V : for i being Element of NAT st i in (dom F) /\ (dom B) holds
ex v being VECTOR of V st
( v = F . i & u .|. v > B . i ) } holds
M is convex
let B be FinSequence of REAL ; ::_thesis: ( M = { u where u is VECTOR of V : for i being Element of NAT st i in (dom F) /\ (dom B) holds
ex v being VECTOR of V st
( v = F . i & u .|. v > B . i ) } implies M is convex )
assume A1: M = { u where u is VECTOR of V : for i being Element of NAT st i in (dom F) /\ (dom B) holds
ex v being VECTOR of V st
( v = F . i & u .|. v > B . i ) } ; ::_thesis: M is convex
let u1, v1 be VECTOR of V; :: according to CONVEX1:def_2 ::_thesis: for b1 being Element of REAL holds
( b1 <= 0 or 1 <= b1 or not u1 in M or not v1 in M or (b1 * u1) + ((1 - b1) * v1) in M )
let r be Real; ::_thesis: ( r <= 0 or 1 <= r or not u1 in M or not v1 in M or (r * u1) + ((1 - r) * v1) in M )
assume that
A2: 0 < r and
A3: r < 1 and
A4: u1 in M and
A5: v1 in M ; ::_thesis: (r * u1) + ((1 - r) * v1) in M
consider v9 being VECTOR of V such that
A6: v1 = v9 and
A7: for i being Element of NAT st i in (dom F) /\ (dom B) holds
ex v being VECTOR of V st
( v = F . i & v9 .|. v > B . i ) by A1, A5;
consider u9 being VECTOR of V such that
A8: u1 = u9 and
A9: for i being Element of NAT st i in (dom F) /\ (dom B) holds
ex v being VECTOR of V st
( v = F . i & u9 .|. v > B . i ) by A1, A4;
for i being Element of NAT st i in (dom F) /\ (dom B) holds
ex v being VECTOR of V st
( v = F . i & ((r * u1) + ((1 - r) * v1)) .|. v > B . i )
proof
0 + r < 1 by A3;
then A10: 1 - r > 0 by XREAL_1:20;
let i be Element of NAT ; ::_thesis: ( i in (dom F) /\ (dom B) implies ex v being VECTOR of V st
( v = F . i & ((r * u1) + ((1 - r) * v1)) .|. v > B . i ) )
assume A11: i in (dom F) /\ (dom B) ; ::_thesis: ex v being VECTOR of V st
( v = F . i & ((r * u1) + ((1 - r) * v1)) .|. v > B . i )
then i in dom B by XBOOLE_0:def_4;
then reconsider b = B . i as Real by PARTFUN1:4;
consider x being VECTOR of V such that
A12: x = F . i and
A13: u9 .|. x > b by A9, A11;
take v = x; ::_thesis: ( v = F . i & ((r * u1) + ((1 - r) * v1)) .|. v > B . i )
A14: ((r * u1) + ((1 - r) * v1)) .|. v = ((r * u1) .|. v) + (((1 - r) * v1) .|. v) by BHSP_1:def_2
.= (r * (u1 .|. v)) + (((1 - r) * v1) .|. v) by BHSP_1:def_2
.= (r * (u1 .|. v)) + ((1 - r) * (v1 .|. v)) by BHSP_1:def_2 ;
r * (u1 .|. v) > r * b by A2, A8, A13, XREAL_1:68;
then ((r * u1) + ((1 - r) * v1)) .|. v > (r * b) + ((1 - r) * (v1 .|. v)) by A14, XREAL_1:8;
then A15: (((r * u1) + ((1 - r) * v1)) .|. v) - (r * b) > (1 - r) * (v1 .|. v) by XREAL_1:20;
ex y being VECTOR of V st
( y = F . i & v9 .|. y > b ) by A7, A11;
then (1 - r) * (v1 .|. v) >= (1 - r) * b by A6, A12, A10, XREAL_1:64;
then (((r * u1) + ((1 - r) * v1)) .|. v) - (r * b) > (1 - r) * b by A15, XXREAL_0:2;
then ((r * u1) + ((1 - r) * v1)) .|. v > (r * b) + ((1 - r) * b) by XREAL_1:20;
hence ( v = F . i & ((r * u1) + ((1 - r) * v1)) .|. v > B . i ) by A12; ::_thesis: verum
end;
hence (r * u1) + ((1 - r) * v1) in M by A1; ::_thesis: verum
end;
Lm1: for V being RealLinearSpace
for M being convex Subset of V
for N being Subset of V
for L being Linear_Combination of N st L is convex & N c= M holds
Sum L in M
proof
let V be RealLinearSpace; ::_thesis: for M being convex Subset of V
for N being Subset of V
for L being Linear_Combination of N st L is convex & N c= M holds
Sum L in M
let M be convex Subset of V; ::_thesis: for N being Subset of V
for L being Linear_Combination of N st L is convex & N c= M holds
Sum L in M
let N be Subset of V; ::_thesis: for L being Linear_Combination of N st L is convex & N c= M holds
Sum L in M
let L be Linear_Combination of N; ::_thesis: ( L is convex & N c= M implies Sum L in M )
assume that
A1: L is convex and
A2: N c= M ; ::_thesis: Sum L in M
consider F being FinSequence of the carrier of V such that
A3: F is one-to-one and
A4: rng F = Carrier L and
A5: ex f being FinSequence of REAL st
( len f = len F & Sum f = 1 & ( for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 ) ) ) by A1, CONVEX1:def_3;
consider f being FinSequence of REAL such that
A6: len f = len F and
A7: Sum f = 1 and
A8: for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 ) by A5;
not Carrier L, {} are_equipotent by A1, CARD_1:26, CONVEX1:21;
then A9: card (Carrier L) <> card {} by CARD_1:5;
then reconsider i = len F as non empty Element of NAT by A3, A4, FINSEQ_4:62;
A10: len (L (#) F) = len F by RLVECT_2:def_7;
defpred S1[ Nat] means (1 / (Sum (mid (f,1,$1)))) * (Sum (mid ((L (#) F),1,$1))) in M;
A11: len (L (#) F) = len F by RLVECT_2:def_7;
A12: for k being non empty Nat st S1[k] holds
S1[k + 1]
proof
let k be non empty Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
A13: k >= 1 by NAT_1:14;
assume A14: (1 / (Sum (mid (f,1,k)))) * (Sum (mid ((L (#) F),1,k))) in M ; ::_thesis: S1[k + 1]
now__::_thesis:_S1[k_+_1]
percases ( k >= len f or k < len f ) ;
supposeA15: k >= len f ; ::_thesis: S1[k + 1]
A16: mid ((L (#) F),1,(k + 1)) = (L (#) F) | (k + 1) by FINSEQ_6:116, NAT_1:12
.= L (#) F by A6, A11, A15, FINSEQ_1:58, NAT_1:12 ;
A17: mid (f,1,k) = f | k by FINSEQ_6:116, NAT_1:14
.= f by A15, FINSEQ_1:58 ;
A18: mid (f,1,(k + 1)) = f | (k + 1) by FINSEQ_6:116, NAT_1:12
.= f by A15, FINSEQ_1:58, NAT_1:12 ;
mid ((L (#) F),1,k) = (L (#) F) | k by FINSEQ_6:116, NAT_1:14
.= L (#) F by A6, A11, A15, FINSEQ_1:58 ;
hence S1[k + 1] by A14, A17, A18, A16; ::_thesis: verum
end;
supposeA19: k < len f ; ::_thesis: S1[k + 1]
mid (f,1,k) = f | k by FINSEQ_6:116, NAT_1:14;
then A20: len (mid (f,1,k)) = k by A19, FINSEQ_1:59;
A21: ex i being Element of NAT st
( i in dom (mid (f,1,k)) & 0 < (mid (f,1,k)) . i )
proof
take 1 ; ::_thesis: ( 1 in dom (mid (f,1,k)) & 0 < (mid (f,1,k)) . 1 )
1 <= len f by A19, NAT_1:14;
then A22: 1 in Seg (len f) ;
then 1 in dom f by FINSEQ_1:def_3;
then A23: ( f . 1 = L . (F . 1) & f . 1 >= 0 ) by A8;
1 in dom F by A6, A22, FINSEQ_1:def_3;
then F . 1 in Carrier L by A4, FUNCT_1:def_3;
then F . 1 in { v where v is Element of V : L . v <> 0 } by RLVECT_2:def_4;
then A24: ex v being Element of V st
( v = F . 1 & L . v <> 0 ) ;
1 in Seg (len (mid (f,1,k))) by A13, A20;
hence ( 1 in dom (mid (f,1,k)) & 0 < (mid (f,1,k)) . 1 ) by A13, A19, A23, A24, FINSEQ_1:def_3, FINSEQ_6:123; ::_thesis: verum
end;
A25: for i being Nat st i in dom <*((mid (f,1,(k + 1))) . (k + 1))*> holds
(mid (f,1,(k + 1))) . ((len (mid (f,1,k))) + i) = <*((mid (f,1,(k + 1))) . (k + 1))*> . i
proof
let i be Nat; ::_thesis: ( i in dom <*((mid (f,1,(k + 1))) . (k + 1))*> implies (mid (f,1,(k + 1))) . ((len (mid (f,1,k))) + i) = <*((mid (f,1,(k + 1))) . (k + 1))*> . i )
assume i in dom <*((mid (f,1,(k + 1))) . (k + 1))*> ; ::_thesis: (mid (f,1,(k + 1))) . ((len (mid (f,1,k))) + i) = <*((mid (f,1,(k + 1))) . (k + 1))*> . i
then i in Seg 1 by FINSEQ_1:38;
then i = 1 by FINSEQ_1:2, TARSKI:def_1;
hence (mid (f,1,(k + 1))) . ((len (mid (f,1,k))) + i) = <*((mid (f,1,(k + 1))) . (k + 1))*> . i by A20, FINSEQ_1:40; ::_thesis: verum
end;
A26: mid (f,1,(k + 1)) = f | (k + 1) by FINSEQ_6:116, NAT_1:14;
set r1 = Sum (mid (f,1,k));
for i being Nat st i in dom (mid (f,1,k)) holds
0 <= (mid (f,1,k)) . i
proof
let i be Nat; ::_thesis: ( i in dom (mid (f,1,k)) implies 0 <= (mid (f,1,k)) . i )
assume i in dom (mid (f,1,k)) ; ::_thesis: 0 <= (mid (f,1,k)) . i
then A27: i in Seg k by A20, FINSEQ_1:def_3;
then A28: 1 <= i by FINSEQ_1:1;
A29: i <= k by A27, FINSEQ_1:1;
then i <= len f by A19, XXREAL_0:2;
then A30: i in dom f by A28, FINSEQ_3:25;
(mid (f,1,k)) . i = f . i by A19, A28, A29, FINSEQ_6:123;
hence 0 <= (mid (f,1,k)) . i by A8, A30; ::_thesis: verum
end;
then A31: Sum (mid (f,1,k)) > 0 by A21, RVSUM_1:85;
A32: k + 1 <= len f by A19, NAT_1:13;
then A33: len (f | (k + 1)) = k + 1 by FINSEQ_1:59;
A34: for i being Nat st i in dom (mid (f,1,k)) holds
(mid (f,1,(k + 1))) . i = (mid (f,1,k)) . i
proof
let i be Nat; ::_thesis: ( i in dom (mid (f,1,k)) implies (mid (f,1,(k + 1))) . i = (mid (f,1,k)) . i )
A35: mid (f,1,k) = f | k by FINSEQ_6:116, NAT_1:14;
assume A36: i in dom (mid (f,1,k)) ; ::_thesis: (mid (f,1,(k + 1))) . i = (mid (f,1,k)) . i
then A37: i in Seg (len (f | k)) by A35, FINSEQ_1:def_3;
len (f | k) = k by A19, FINSEQ_1:59;
then i <= k by A37, FINSEQ_1:1;
then A38: i <= k + 1 by NAT_1:12;
(f | k) . i = (f | k) /. i by A36, A35, PARTFUN1:def_6;
then A39: (mid (f,1,k)) . i = f /. i by A36, A35, FINSEQ_4:70;
( i in NAT & 1 <= i ) by A37, FINSEQ_1:1;
then i in Seg (k + 1) by A38;
then A40: i in dom (f | (k + 1)) by A33, FINSEQ_1:def_3;
then (f | (k + 1)) . i = (f | (k + 1)) /. i by PARTFUN1:def_6;
hence (mid (f,1,(k + 1))) . i = (mid (f,1,k)) . i by A26, A39, A40, FINSEQ_4:70; ::_thesis: verum
end;
A41: k + 1 >= 1 by NAT_1:14;
then A42: k + 1 in Seg (len f) by A32;
then A43: k + 1 in dom f by FINSEQ_1:def_3;
A44: k + 1 in dom F by A6, A42, FINSEQ_1:def_3;
k + 1 in Seg (k + 1) by A41;
then A45: k + 1 in dom (f | (k + 1)) by A33, FINSEQ_1:def_3;
then (f | (k + 1)) /. (k + 1) = f /. (k + 1) by FINSEQ_4:70;
then (mid (f,1,(k + 1))) . (k + 1) = f /. (k + 1) by A26, A45, PARTFUN1:def_6;
then (mid (f,1,(k + 1))) . (k + 1) = f . (k + 1) by A43, PARTFUN1:def_6
.= L . (F . (k + 1)) by A8, A43 ;
then A46: (mid (f,1,(k + 1))) . (k + 1) = L . (F /. (k + 1)) by A44, PARTFUN1:def_6;
mid (f,1,(k + 1)) = f | (k + 1) by FINSEQ_6:116, NAT_1:14;
then ( len <*((mid (f,1,(k + 1))) . (k + 1))*> = 1 & len (mid (f,1,(k + 1))) = k + 1 ) by A32, FINSEQ_1:40, FINSEQ_1:59;
then dom (mid (f,1,(k + 1))) = Seg ((len (mid (f,1,k))) + (len <*((mid (f,1,(k + 1))) . (k + 1))*>)) by A20, FINSEQ_1:def_3;
then mid (f,1,(k + 1)) = (mid (f,1,k)) ^ <*((mid (f,1,(k + 1))) . (k + 1))*> by A34, A25, FINSEQ_1:def_7;
then A47: Sum (mid (f,1,(k + 1))) = (Sum (mid (f,1,k))) + (L . (F /. (k + 1))) by A46, RVSUM_1:74;
A48: mid ((L (#) F),1,(k + 1)) = (L (#) F) | (k + 1) by FINSEQ_6:116, NAT_1:14;
set w2 = F /. (k + 1);
set w1 = Sum (mid ((L (#) F),1,k));
set r2 = L . (F /. (k + 1));
A49: (1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * (Sum (mid (f,1,k))) = (Sum (mid (f,1,k))) / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1)))) by XCMPLX_1:99;
A50: ( F /. (k + 1) in M & L . (F /. (k + 1)) > 0 )
proof
k + 1 in Seg (len f) by A41, A32;
then k + 1 in dom f by FINSEQ_1:def_3;
then A51: ( f . (k + 1) = L . (F . (k + 1)) & f . (k + 1) >= 0 ) by A8;
k + 1 in Seg (len F) by A6, A41, A32;
then A52: k + 1 in dom F by FINSEQ_1:def_3;
then F /. (k + 1) = F . (k + 1) by PARTFUN1:def_6;
then A53: F /. (k + 1) in Carrier L by A4, A52, FUNCT_1:def_3;
Carrier L c= N by RLVECT_2:def_6;
hence F /. (k + 1) in M by A2, A53, TARSKI:def_3; ::_thesis: L . (F /. (k + 1)) > 0
F /. (k + 1) in { v where v is Element of V : L . v <> 0 } by A53, RLVECT_2:def_4;
then ex v being Element of V st
( v = F /. (k + 1) & L . v <> 0 ) ;
hence L . (F /. (k + 1)) > 0 by A52, A51, PARTFUN1:def_6; ::_thesis: verum
end;
then (Sum (mid (f,1,k))) + (L . (F /. (k + 1))) > Sum (mid (f,1,k)) by XREAL_1:29;
then A54: (1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * (Sum (mid (f,1,k))) < 1 by A31, A49, XREAL_1:189;
A55: (Sum (mid (f,1,k))) + (L . (F /. (k + 1))) > 0 + 0 by A31, A50, XREAL_1:8;
then 1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1)))) > 0 by XREAL_1:139;
then A56: 0 < (1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * (Sum (mid (f,1,k))) by A31, XREAL_1:129;
k + 1 <= len (L (#) F) by A6, A32, RLVECT_2:def_7;
then A57: k + 1 in dom (L (#) F) by A41, FINSEQ_3:25;
A58: k < len (L (#) F) by A6, A19, RLVECT_2:def_7;
then A59: k + 1 <= len (L (#) F) by NAT_1:13;
then A60: len ((L (#) F) | (k + 1)) = k + 1 by FINSEQ_1:59;
A61: for i being Nat st i in dom (mid ((L (#) F),1,k)) holds
(mid ((L (#) F),1,(k + 1))) . i = (mid ((L (#) F),1,k)) . i
proof
let i be Nat; ::_thesis: ( i in dom (mid ((L (#) F),1,k)) implies (mid ((L (#) F),1,(k + 1))) . i = (mid ((L (#) F),1,k)) . i )
A62: mid ((L (#) F),1,k) = (L (#) F) | k by FINSEQ_6:116, NAT_1:14;
assume A63: i in dom (mid ((L (#) F),1,k)) ; ::_thesis: (mid ((L (#) F),1,(k + 1))) . i = (mid ((L (#) F),1,k)) . i
then A64: i in Seg (len ((L (#) F) | k)) by A62, FINSEQ_1:def_3;
len ((L (#) F) | k) = k by A58, FINSEQ_1:59;
then i <= k by A64, FINSEQ_1:1;
then A65: i <= k + 1 by NAT_1:12;
((L (#) F) | k) . i = ((L (#) F) | k) /. i by A63, A62, PARTFUN1:def_6;
then A66: (mid ((L (#) F),1,k)) . i = (L (#) F) /. i by A63, A62, FINSEQ_4:70;
( i in NAT & 1 <= i ) by A64, FINSEQ_1:1;
then i in Seg (k + 1) by A65;
then A67: i in dom ((L (#) F) | (k + 1)) by A60, FINSEQ_1:def_3;
then ((L (#) F) | (k + 1)) . i = ((L (#) F) | (k + 1)) /. i by PARTFUN1:def_6;
hence (mid ((L (#) F),1,(k + 1))) . i = (mid ((L (#) F),1,k)) . i by A48, A66, A67, FINSEQ_4:70; ::_thesis: verum
end;
k + 1 in Seg (k + 1) by A41;
then A68: k + 1 in dom ((L (#) F) | (k + 1)) by A60, FINSEQ_1:def_3;
then ((L (#) F) | (k + 1)) /. (k + 1) = (L (#) F) /. (k + 1) by FINSEQ_4:70;
then (mid ((L (#) F),1,(k + 1))) . (k + 1) = (L (#) F) /. (k + 1) by A48, A68, PARTFUN1:def_6;
then A69: (mid ((L (#) F),1,(k + 1))) . (k + 1) = (L (#) F) . (k + 1) by A57, PARTFUN1:def_6
.= (L . (F /. (k + 1))) * (F /. (k + 1)) by A57, RLVECT_2:def_7 ;
mid ((L (#) F),1,k) = (L (#) F) | k by FINSEQ_6:116, NAT_1:14;
then A70: len (mid ((L (#) F),1,k)) = k by A58, FINSEQ_1:59;
A71: for i being Nat st i in dom <*((mid ((L (#) F),1,(k + 1))) . (k + 1))*> holds
(mid ((L (#) F),1,(k + 1))) . ((len (mid ((L (#) F),1,k))) + i) = <*((mid ((L (#) F),1,(k + 1))) . (k + 1))*> . i
proof
let i be Nat; ::_thesis: ( i in dom <*((mid ((L (#) F),1,(k + 1))) . (k + 1))*> implies (mid ((L (#) F),1,(k + 1))) . ((len (mid ((L (#) F),1,k))) + i) = <*((mid ((L (#) F),1,(k + 1))) . (k + 1))*> . i )
assume i in dom <*((mid ((L (#) F),1,(k + 1))) . (k + 1))*> ; ::_thesis: (mid ((L (#) F),1,(k + 1))) . ((len (mid ((L (#) F),1,k))) + i) = <*((mid ((L (#) F),1,(k + 1))) . (k + 1))*> . i
then i in Seg 1 by FINSEQ_1:38;
then i = 1 by FINSEQ_1:2, TARSKI:def_1;
hence (mid ((L (#) F),1,(k + 1))) . ((len (mid ((L (#) F),1,k))) + i) = <*((mid ((L (#) F),1,(k + 1))) . (k + 1))*> . i by A70, FINSEQ_1:40; ::_thesis: verum
end;
( len <*((mid ((L (#) F),1,(k + 1))) . (k + 1))*> = 1 & len (mid ((L (#) F),1,(k + 1))) = k + 1 ) by A59, A48, FINSEQ_1:40, FINSEQ_1:59;
then dom (mid ((L (#) F),1,(k + 1))) = Seg ((len (mid ((L (#) F),1,k))) + (len <*((mid ((L (#) F),1,(k + 1))) . (k + 1))*>)) by A70, FINSEQ_1:def_3;
then mid ((L (#) F),1,(k + 1)) = (mid ((L (#) F),1,k)) ^ <*((mid ((L (#) F),1,(k + 1))) . (k + 1))*> by A61, A71, FINSEQ_1:def_7;
then A72: (1 / (Sum (mid (f,1,(k + 1))))) * (Sum (mid ((L (#) F),1,(k + 1)))) = (1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * ((Sum (mid ((L (#) F),1,k))) + ((L . (F /. (k + 1))) * (F /. (k + 1)))) by A47, A69, FVSUM_1:71
.= (1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * ((1 * (Sum (mid ((L (#) F),1,k)))) + ((L . (F /. (k + 1))) * (F /. (k + 1)))) by RLVECT_1:def_8
.= (1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * ((((Sum (mid (f,1,k))) * (1 / (Sum (mid (f,1,k))))) * (Sum (mid ((L (#) F),1,k)))) + ((L . (F /. (k + 1))) * (F /. (k + 1)))) by A31, XCMPLX_1:106
.= (1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * (((Sum (mid (f,1,k))) * ((1 / (Sum (mid (f,1,k)))) * (Sum (mid ((L (#) F),1,k))))) + ((L . (F /. (k + 1))) * (F /. (k + 1)))) by RLVECT_1:def_7
.= ((1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * ((Sum (mid (f,1,k))) * ((1 / (Sum (mid (f,1,k)))) * (Sum (mid ((L (#) F),1,k)))))) + ((1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * ((L . (F /. (k + 1))) * (F /. (k + 1)))) by RLVECT_1:def_5
.= (((1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * (Sum (mid (f,1,k)))) * ((1 / (Sum (mid (f,1,k)))) * (Sum (mid ((L (#) F),1,k))))) + ((1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * ((L . (F /. (k + 1))) * (F /. (k + 1)))) by RLVECT_1:def_7
.= (((1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * (Sum (mid (f,1,k)))) * ((1 / (Sum (mid (f,1,k)))) * (Sum (mid ((L (#) F),1,k))))) + (((1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * (L . (F /. (k + 1)))) * (F /. (k + 1))) by RLVECT_1:def_7 ;
1 - ((1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * (Sum (mid (f,1,k)))) = (((Sum (mid (f,1,k))) + (L . (F /. (k + 1)))) * (1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1)))))) - ((1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * (Sum (mid (f,1,k)))) by A55, XCMPLX_1:106
.= (((Sum (mid (f,1,k))) + (L . (F /. (k + 1)))) - (Sum (mid (f,1,k)))) * (1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) ;
hence S1[k + 1] by A14, A50, A56, A54, A72, CONVEX1:def_2; ::_thesis: verum
end;
end;
end;
hence S1[k + 1] ; ::_thesis: verum
end;
len F > 0 by A3, A4, A9, CARD_1:27, FINSEQ_4:62;
then A73: len F >= 0 + 1 by NAT_1:13;
A74: S1[1]
proof
mid (f,1,1) = f | 1 by FINSEQ_6:116;
then A75: len (mid (f,1,1)) = 1 by A6, A73, FINSEQ_1:59;
then 1 in dom (mid (f,1,1)) by FINSEQ_3:25;
then reconsider m = (mid (f,1,1)) . 1 as Element of REAL by PARTFUN1:4;
mid (f,1,1) = <*((mid (f,1,1)) . 1)*> by A75, FINSEQ_1:40;
then A76: Sum (mid (f,1,1)) = m by FINSOP_1:11;
Carrier L c= N by RLVECT_2:def_6;
then A77: Carrier L c= M by A2, XBOOLE_1:1;
mid ((L (#) F),1,1) = (L (#) F) | 1 by FINSEQ_6:116;
then len (mid ((L (#) F),1,1)) = 1 by A73, A11, FINSEQ_1:59;
then A78: mid ((L (#) F),1,1) = <*((mid ((L (#) F),1,1)) . 1)*> by FINSEQ_1:40;
A79: 1 in Seg (len (L (#) F)) by A73, A11;
then A80: 1 in dom F by A11, FINSEQ_1:def_3;
then A81: F /. 1 = F . 1 by PARTFUN1:def_6;
A82: 1 in dom (L (#) F) by A79, FINSEQ_1:def_3;
A83: F . 1 in rng F by A80, FUNCT_1:def_3;
then F . 1 in { v where v is Element of V : L . v <> 0 } by A4, RLVECT_2:def_4;
then A84: ex v2 being Element of V st
( F . 1 = v2 & L . v2 <> 0 ) ;
1 in dom f by A6, A11, A79, FINSEQ_1:def_3;
then f . 1 = L . (F . 1) by A8
.= L . (F /. 1) by A80, PARTFUN1:def_6 ;
then A85: Sum (mid (f,1,1)) = L . (F /. 1) by A6, A73, A76, FINSEQ_6:123;
(mid ((L (#) F),1,1)) . 1 = (L (#) F) . 1 by A73, A11, FINSEQ_6:123
.= (L . (F /. 1)) * (F /. 1) by A82, RLVECT_2:def_7 ;
then (1 / (Sum (mid (f,1,1)))) * (Sum (mid ((L (#) F),1,1))) = (1 / (Sum (mid (f,1,1)))) * ((L . (F /. 1)) * (F /. 1)) by A78, RLVECT_1:44
.= ((1 / (Sum (mid (f,1,1)))) * (L . (F /. 1))) * (F /. 1) by RLVECT_1:def_7
.= 1 * (F /. 1) by A81, A85, A84, XCMPLX_1:106
.= F /. 1 by RLVECT_1:def_8 ;
hence S1[1] by A4, A81, A83, A77; ::_thesis: verum
end;
for k being non empty Nat holds S1[k] from NAT_1:sch_10(A74, A12);
then A86: (1 / (Sum (mid (f,1,i)))) * (Sum (mid ((L (#) F),1,i))) in M ;
Sum (mid (f,1,(len f))) = 1 by A6, A7, A73, FINSEQ_6:120;
then (1 / (Sum (mid (f,1,(len f))))) * (Sum (mid ((L (#) F),1,(len (L (#) F))))) = Sum (mid ((L (#) F),1,(len (L (#) F)))) by RLVECT_1:def_8
.= Sum (L (#) F) by A73, A10, FINSEQ_6:120 ;
hence Sum L in M by A3, A4, A6, A86, A10, RLVECT_2:def_8; ::_thesis: verum
end;
Lm2: for V being RealLinearSpace
for M being Subset of V st ( for N being Subset of V
for L being Linear_Combination of N st L is convex & N c= M holds
Sum L in M ) holds
M is convex
proof
let V be RealLinearSpace; ::_thesis: for M being Subset of V st ( for N being Subset of V
for L being Linear_Combination of N st L is convex & N c= M holds
Sum L in M ) holds
M is convex
let M be Subset of V; ::_thesis: ( ( for N being Subset of V
for L being Linear_Combination of N st L is convex & N c= M holds
Sum L in M ) implies M is convex )
assume A1: for N being Subset of V
for L being Linear_Combination of N st L is convex & N c= M holds
Sum L in M ; ::_thesis: M is convex
let u, v be VECTOR of V; :: according to CONVEX1:def_2 ::_thesis: for b1 being Element of REAL holds
( b1 <= 0 or 1 <= b1 or not u in M or not v in M or (b1 * u) + ((1 - b1) * v) in M )
let r be Real; ::_thesis: ( r <= 0 or 1 <= r or not u in M or not v in M or (r * u) + ((1 - r) * v) in M )
assume that
A2: 0 < r and
A3: r < 1 and
A4: ( u in M & v in M ) ; ::_thesis: (r * u) + ((1 - r) * v) in M
set N = {u,v};
A5: {u,v} c= M by A4, ZFMISC_1:32;
reconsider N = {u,v} as Subset of V ;
now__::_thesis:_(r_*_u)_+_((1_-_r)_*_v)_in_M
percases ( u <> v or u = v ) ;
supposeA6: u <> v ; ::_thesis: (r * u) + ((1 - r) * v) in M
consider L being Linear_Combination of {u,v} such that
A7: ( L . u = r & L . v = 1 - r ) by A6, RLVECT_4:38;
reconsider L = L as Linear_Combination of N ;
A8: L is convex
proof
A9: r - r < 1 - r by A3, XREAL_1:9;
then v in { w where w is Element of V : L . w <> 0 } by A7;
then A10: v in Carrier L by RLVECT_2:def_4;
A11: for n being Element of NAT st n in dom <*r,(1 - r)*> holds
( <*r,(1 - r)*> . n = L . (<*u,v*> . n) & <*r,(1 - r)*> . n >= 0 )
proof
let n be Element of NAT ; ::_thesis: ( n in dom <*r,(1 - r)*> implies ( <*r,(1 - r)*> . n = L . (<*u,v*> . n) & <*r,(1 - r)*> . n >= 0 ) )
assume n in dom <*r,(1 - r)*> ; ::_thesis: ( <*r,(1 - r)*> . n = L . (<*u,v*> . n) & <*r,(1 - r)*> . n >= 0 )
then n in Seg (len <*r,(1 - r)*>) by FINSEQ_1:def_3;
then A12: n in {1,2} by FINSEQ_1:2, FINSEQ_1:44;
now__::_thesis:_(_<*r,(1_-_r)*>_._n_=_L_._(<*u,v*>_._n)_&_<*r,(1_-_r)*>_._n_>=_0_)
percases ( n = 1 or n = 2 ) by A12, TARSKI:def_2;
supposeA13: n = 1 ; ::_thesis: ( <*r,(1 - r)*> . n = L . (<*u,v*> . n) & <*r,(1 - r)*> . n >= 0 )
then L . (<*u,v*> . n) = r by A7, FINSEQ_1:44;
hence ( <*r,(1 - r)*> . n = L . (<*u,v*> . n) & <*r,(1 - r)*> . n >= 0 ) by A2, A13, FINSEQ_1:44; ::_thesis: verum
end;
supposeA14: n = 2 ; ::_thesis: ( <*r,(1 - r)*> . n = L . (<*u,v*> . n) & <*r,(1 - r)*> . n >= 0 )
then L . (<*u,v*> . n) = 1 - r by A7, FINSEQ_1:44;
hence ( <*r,(1 - r)*> . n = L . (<*u,v*> . n) & <*r,(1 - r)*> . n >= 0 ) by A9, A14, FINSEQ_1:44; ::_thesis: verum
end;
end;
end;
hence ( <*r,(1 - r)*> . n = L . (<*u,v*> . n) & <*r,(1 - r)*> . n >= 0 ) ; ::_thesis: verum
end;
u in { w where w is Element of V : L . w <> 0 } by A2, A7;
then u in Carrier L by RLVECT_2:def_4;
then A15: ( Carrier L c= {u,v} & {u,v} c= Carrier L ) by A10, RLVECT_2:def_6, ZFMISC_1:32;
take F = <*u,v*>; :: according to CONVEX1:def_3 ::_thesis: ( F is one-to-one & rng F = Carrier L & ex b1 being FinSequence of REAL st
( len b1 = len F & Sum b1 = 1 & ( for b2 being set holds
( not b2 in dom b1 or ( b1 . b2 = L . (F . b2) & 0 <= b1 . b2 ) ) ) ) )
A16: Sum <*r,(1 - r)*> = r + (1 - r) by RVSUM_1:77
.= 1 ;
thus F is one-to-one by A6, FINSEQ_3:94; ::_thesis: ( rng F = Carrier L & ex b1 being FinSequence of REAL st
( len b1 = len F & Sum b1 = 1 & ( for b2 being set holds
( not b2 in dom b1 or ( b1 . b2 = L . (F . b2) & 0 <= b1 . b2 ) ) ) ) )
thus rng F = (rng <*u*>) \/ (rng <*v*>) by FINSEQ_1:31
.= {u} \/ (rng <*v*>) by FINSEQ_1:38
.= {u} \/ {v} by FINSEQ_1:38
.= {u,v} by ENUMSET1:1
.= Carrier L by A15, XBOOLE_0:def_10 ; ::_thesis: ex b1 being FinSequence of REAL st
( len b1 = len F & Sum b1 = 1 & ( for b2 being set holds
( not b2 in dom b1 or ( b1 . b2 = L . (F . b2) & 0 <= b1 . b2 ) ) ) )
take f = <*r,(1 - r)*>; ::_thesis: ( len f = len F & Sum f = 1 & ( for b1 being set holds
( not b1 in dom f or ( f . b1 = L . (F . b1) & 0 <= f . b1 ) ) ) )
len <*r,(1 - r)*> = 2 by FINSEQ_1:44
.= len <*u,v*> by FINSEQ_1:44 ;
hence ( len f = len F & Sum f = 1 & ( for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 ) ) ) by A16, A11; ::_thesis: verum
end;
Sum L = (r * u) + ((1 - r) * v) by A6, A7, RLVECT_2:33;
hence (r * u) + ((1 - r) * v) in M by A1, A5, A8; ::_thesis: verum
end;
supposeA17: u = v ; ::_thesis: (r * u) + ((1 - r) * v) in M
consider L being Linear_Combination of {u} such that
A18: L . u = 1 by RLVECT_4:37;
reconsider L = L as Linear_Combination of N by A17, ENUMSET1:29;
ex F being FinSequence of the carrier of V st
( F is one-to-one & rng F = Carrier L & ex f being FinSequence of REAL st
( len f = len F & Sum f = 1 & ( for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 ) ) ) )
proof
take <*u*> ; ::_thesis: ( <*u*> is one-to-one & rng <*u*> = Carrier L & ex f being FinSequence of REAL st
( len f = len <*u*> & Sum f = 1 & ( for n being Nat st n in dom f holds
( f . n = L . (<*u*> . n) & f . n >= 0 ) ) ) )
A19: ex f being FinSequence of REAL st
( len f = len <*u*> & Sum f = 1 & ( for n being Nat st n in dom f holds
( f . n = L . (<*u*> . n) & f . n >= 0 ) ) )
proof
take <*rr*> ; ::_thesis: ( len <*rr*> = len <*u*> & Sum <*rr*> = 1 & ( for n being Nat st n in dom <*rr*> holds
( <*rr*> . n = L . (<*u*> . n) & <*rr*> . n >= 0 ) ) )
A20: for n being Element of NAT st n in dom <*rr*> holds
( <*rr*> . n = L . (<*u*> . n) & <*rr*> . n >= 0 )
proof
let n be Element of NAT ; ::_thesis: ( n in dom <*rr*> implies ( <*rr*> . n = L . (<*u*> . n) & <*rr*> . n >= 0 ) )
assume n in dom <*rr*> ; ::_thesis: ( <*rr*> . n = L . (<*u*> . n) & <*rr*> . n >= 0 )
then n in {1} by FINSEQ_1:2, FINSEQ_1:38;
then A21: n = 1 by TARSKI:def_1;
then <*rr*> . n = 1 by FINSEQ_1:40
.= L . (<*u*> . n) by A18, A21, FINSEQ_1:40 ;
hence ( <*rr*> . n = L . (<*u*> . n) & <*rr*> . n >= 0 ) by A21, FINSEQ_1:40; ::_thesis: verum
end;
len <*1*> = 1 by FINSEQ_1:39
.= len <*u*> by FINSEQ_1:39 ;
hence ( len <*rr*> = len <*u*> & Sum <*rr*> = 1 & ( for n being Nat st n in dom <*rr*> holds
( <*rr*> . n = L . (<*u*> . n) & <*rr*> . n >= 0 ) ) ) by A20, FINSOP_1:11; ::_thesis: verum
end;
u in { w where w is Element of V : L . w <> 0 } by A18;
then A22: u in Carrier L by RLVECT_2:def_4;
v in { w where w is Element of V : L . w <> 0 } by A17, A18;
then v in Carrier L by RLVECT_2:def_4;
then ( Carrier L c= {u,v} & {u,v} c= Carrier L ) by A22, RLVECT_2:def_6, ZFMISC_1:32;
then Carrier L = {u,v} by XBOOLE_0:def_10;
then Carrier L = {u} by A17, ENUMSET1:29;
hence ( <*u*> is one-to-one & rng <*u*> = Carrier L & ex f being FinSequence of REAL st
( len f = len <*u*> & Sum f = 1 & ( for n being Nat st n in dom f holds
( f . n = L . (<*u*> . n) & f . n >= 0 ) ) ) ) by A19, FINSEQ_1:38, FINSEQ_3:93; ::_thesis: verum
end;
then L is convex by CONVEX1:def_3;
then A23: Sum L in M by A1, A5;
(r * u) + ((1 - r) * v) = (r + (1 - r)) * u by A17, RLVECT_1:def_6
.= (0 + 1) * u ;
hence (r * u) + ((1 - r) * v) in M by A18, A23, RLVECT_2:32; ::_thesis: verum
end;
end;
end;
hence (r * u) + ((1 - r) * v) in M ; ::_thesis: verum
end;
theorem :: CONVEX2:6
for V being RealLinearSpace
for M being Subset of V holds
( ( for N being Subset of V
for L being Linear_Combination of N st L is convex & N c= M holds
Sum L in M ) iff M is convex ) by Lm1, Lm2;
definition
let V be RealLinearSpace;
let M be Subset of V;
defpred S1[ set ] means $1 is Linear_Combination of M;
func LinComb M -> set means :: CONVEX2:def 1
for L being set holds
( L in it iff L is Linear_Combination of M );
existence
ex b1 being set st
for L being set holds
( L in b1 iff L is Linear_Combination of M )
proof
consider A being set such that
A1: for x being set holds
( x in A iff ( x in Funcs ( the carrier of V,REAL) & S1[x] ) ) from XBOOLE_0:sch_1();
take A ; ::_thesis: for L being set holds
( L in A iff L is Linear_Combination of M )
let L be set ; ::_thesis: ( L in A iff L is Linear_Combination of M )
thus ( L in A implies L is Linear_Combination of M ) by A1; ::_thesis: ( L is Linear_Combination of M implies L in A )
assume L is Linear_Combination of M ; ::_thesis: L in A
hence L in A by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being set st ( for L being set holds
( L in b1 iff L is Linear_Combination of M ) ) & ( for L being set holds
( L in b2 iff L is Linear_Combination of M ) ) holds
b1 = b2
proof
thus for X1, X2 being set st ( for x being set holds
( x in X1 iff S1[x] ) ) & ( for x being set holds
( x in X2 iff S1[x] ) ) holds
X1 = X2 from XBOOLE_0:sch_3(); ::_thesis: verum
end;
end;
:: deftheorem defines LinComb CONVEX2:def_1_:_
for V being RealLinearSpace
for M being Subset of V
for b3 being set holds
( b3 = LinComb M iff for L being set holds
( L in b3 iff L is Linear_Combination of M ) );
registration
let V be RealLinearSpace;
cluster Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V123() V124() V125() convex for Linear_Combination of V;
existence
ex b1 being Linear_Combination of V st b1 is convex
proof
set u = the Element of V;
consider L being Linear_Combination of { the Element of V} such that
A1: L . the Element of V = 1 by RLVECT_4:37;
reconsider L = L as Linear_Combination of V ;
take L ; ::_thesis: L is convex
L is convex
proof
take <* the Element of V*> ; :: according to CONVEX1:def_3 ::_thesis: ( <* the Element of V*> is one-to-one & rng <* the Element of V*> = Carrier L & ex b1 being FinSequence of REAL st
( len b1 = len <* the Element of V*> & Sum b1 = 1 & ( for b2 being set holds
( not b2 in dom b1 or ( b1 . b2 = L . (<* the Element of V*> . b2) & 0 <= b1 . b2 ) ) ) ) )
thus <* the Element of V*> is one-to-one by FINSEQ_3:93; ::_thesis: ( rng <* the Element of V*> = Carrier L & ex b1 being FinSequence of REAL st
( len b1 = len <* the Element of V*> & Sum b1 = 1 & ( for b2 being set holds
( not b2 in dom b1 or ( b1 . b2 = L . (<* the Element of V*> . b2) & 0 <= b1 . b2 ) ) ) ) )
the Element of V in { w where w is Element of V : L . w <> 0 } by A1;
then the Element of V in Carrier L by RLVECT_2:def_4;
then ( Carrier L c= { the Element of V} & { the Element of V} c= Carrier L ) by RLVECT_2:def_6, ZFMISC_1:31;
hence Carrier L = { the Element of V} by XBOOLE_0:def_10
.= rng <* the Element of V*> by FINSEQ_1:38 ;
::_thesis: ex b1 being FinSequence of REAL st
( len b1 = len <* the Element of V*> & Sum b1 = 1 & ( for b2 being set holds
( not b2 in dom b1 or ( b1 . b2 = L . (<* the Element of V*> . b2) & 0 <= b1 . b2 ) ) ) )
take f = <*rr*>; ::_thesis: ( len f = len <* the Element of V*> & Sum f = 1 & ( for b1 being set holds
( not b1 in dom f or ( f . b1 = L . (<* the Element of V*> . b1) & 0 <= f . b1 ) ) ) )
A2: for n being Element of NAT st n in dom f holds
( f . n = L . (<* the Element of V*> . n) & f . n >= 0 )
proof
let n be Element of NAT ; ::_thesis: ( n in dom f implies ( f . n = L . (<* the Element of V*> . n) & f . n >= 0 ) )
assume n in dom f ; ::_thesis: ( f . n = L . (<* the Element of V*> . n) & f . n >= 0 )
then n in {1} by FINSEQ_1:2, FINSEQ_1:38;
then A3: n = 1 by TARSKI:def_1;
then f . n = L . the Element of V by A1, FINSEQ_1:40
.= L . (<* the Element of V*> . n) by A3, FINSEQ_1:40 ;
hence ( f . n = L . (<* the Element of V*> . n) & f . n >= 0 ) by A3, FINSEQ_1:40; ::_thesis: verum
end;
len <*1*> = 1 by FINSEQ_1:39
.= len <* the Element of V*> by FINSEQ_1:39 ;
hence ( len f = len <* the Element of V*> & Sum f = 1 & ( for b1 being set holds
( not b1 in dom f or ( f . b1 = L . (<* the Element of V*> . b1) & 0 <= f . b1 ) ) ) ) by A2, FINSOP_1:11; ::_thesis: verum
end;
hence L is convex ; ::_thesis: verum
end;
end;
definition
let V be RealLinearSpace;
mode Convex_Combination of V is convex Linear_Combination of V;
end;
registration
let V be RealLinearSpace;
let M be non empty Subset of V;
cluster Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V123() V124() V125() convex for Linear_Combination of M;
existence
ex b1 being Linear_Combination of M st b1 is convex
proof
consider u being set such that
A1: u in M by XBOOLE_0:def_1;
reconsider u = u as Element of V by A1;
consider L being Linear_Combination of {u} such that
A2: L . u = 1 by RLVECT_4:37;
{u} c= M by A1, ZFMISC_1:31;
then reconsider L = L as Linear_Combination of M by RLVECT_2:21;
take L ; ::_thesis: L is convex
L is convex
proof
take <*u*> ; :: according to CONVEX1:def_3 ::_thesis: ( <*u*> is one-to-one & rng <*u*> = Carrier L & ex b1 being FinSequence of REAL st
( len b1 = len <*u*> & Sum b1 = 1 & ( for b2 being set holds
( not b2 in dom b1 or ( b1 . b2 = L . (<*u*> . b2) & 0 <= b1 . b2 ) ) ) ) )
thus <*u*> is one-to-one by FINSEQ_3:93; ::_thesis: ( rng <*u*> = Carrier L & ex b1 being FinSequence of REAL st
( len b1 = len <*u*> & Sum b1 = 1 & ( for b2 being set holds
( not b2 in dom b1 or ( b1 . b2 = L . (<*u*> . b2) & 0 <= b1 . b2 ) ) ) ) )
u in { w where w is Element of V : L . w <> 0 } by A2;
then u in Carrier L by RLVECT_2:def_4;
then ( Carrier L c= {u} & {u} c= Carrier L ) by RLVECT_2:def_6, ZFMISC_1:31;
hence Carrier L = {u} by XBOOLE_0:def_10
.= rng <*u*> by FINSEQ_1:38 ;
::_thesis: ex b1 being FinSequence of REAL st
( len b1 = len <*u*> & Sum b1 = 1 & ( for b2 being set holds
( not b2 in dom b1 or ( b1 . b2 = L . (<*u*> . b2) & 0 <= b1 . b2 ) ) ) )
take f = <*rr*>; ::_thesis: ( len f = len <*u*> & Sum f = 1 & ( for b1 being set holds
( not b1 in dom f or ( f . b1 = L . (<*u*> . b1) & 0 <= f . b1 ) ) ) )
A3: for n being Element of NAT st n in dom f holds
( f . n = L . (<*u*> . n) & f . n >= 0 )
proof
let n be Element of NAT ; ::_thesis: ( n in dom f implies ( f . n = L . (<*u*> . n) & f . n >= 0 ) )
assume n in dom f ; ::_thesis: ( f . n = L . (<*u*> . n) & f . n >= 0 )
then n in {1} by FINSEQ_1:2, FINSEQ_1:38;
then A4: n = 1 by TARSKI:def_1;
then f . n = L . u by A2, FINSEQ_1:40
.= L . (<*u*> . n) by A4, FINSEQ_1:40 ;
hence ( f . n = L . (<*u*> . n) & f . n >= 0 ) by A4, FINSEQ_1:40; ::_thesis: verum
end;
len <*1*> = 1 by FINSEQ_1:39
.= len <*u*> by FINSEQ_1:39 ;
hence ( len f = len <*u*> & Sum f = 1 & ( for b1 being set holds
( not b1 in dom f or ( f . b1 = L . (<*u*> . b1) & 0 <= f . b1 ) ) ) ) by A3, FINSOP_1:11; ::_thesis: verum
end;
hence L is convex ; ::_thesis: verum
end;
end;
definition
let V be RealLinearSpace;
let M be non empty Subset of V;
mode Convex_Combination of M is convex Linear_Combination of M;
end;
Lm3: for V being RealLinearSpace
for W1, W2 being Subspace of V holds Up (W1 + W2) = (Up W1) + (Up W2)
proof
let V be RealLinearSpace; ::_thesis: for W1, W2 being Subspace of V holds Up (W1 + W2) = (Up W1) + (Up W2)
let W1, W2 be Subspace of V; ::_thesis: Up (W1 + W2) = (Up W1) + (Up W2)
A1: Up (W1 + W2) = the carrier of (W1 + W2) by RUSUB_4:def_5
.= { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } by RLSUB_2:def_1 ;
for x being set st x in (Up W1) + (Up W2) holds
x in Up (W1 + W2)
proof
let x be set ; ::_thesis: ( x in (Up W1) + (Up W2) implies x in Up (W1 + W2) )
assume x in (Up W1) + (Up W2) ; ::_thesis: x in Up (W1 + W2)
then x in { (u + v) where u, v is Element of V : ( u in Up W1 & v in Up W2 ) } by RUSUB_4:def_9;
then consider u, v being Element of V such that
A2: x = u + v and
A3: u in Up W1 and
A4: v in Up W2 ;
v in the carrier of W2 by A4, RUSUB_4:def_5;
then A5: v in W2 by STRUCT_0:def_5;
u in the carrier of W1 by A3, RUSUB_4:def_5;
then u in W1 by STRUCT_0:def_5;
hence x in Up (W1 + W2) by A1, A2, A5; ::_thesis: verum
end;
then A6: (Up W1) + (Up W2) c= Up (W1 + W2) by TARSKI:def_3;
for x being set st x in Up (W1 + W2) holds
x in (Up W1) + (Up W2)
proof
let x be set ; ::_thesis: ( x in Up (W1 + W2) implies x in (Up W1) + (Up W2) )
assume x in Up (W1 + W2) ; ::_thesis: x in (Up W1) + (Up W2)
then consider v, u being VECTOR of V such that
A7: x = v + u and
A8: v in W1 and
A9: u in W2 by A1;
u in the carrier of W2 by A9, STRUCT_0:def_5;
then A10: u in Up W2 by RUSUB_4:def_5;
v in the carrier of W1 by A8, STRUCT_0:def_5;
then v in Up W1 by RUSUB_4:def_5;
then x in { (u9 + v9) where u9, v9 is Element of V : ( u9 in Up W1 & v9 in Up W2 ) } by A7, A10;
hence x in (Up W1) + (Up W2) by RUSUB_4:def_9; ::_thesis: verum
end;
then Up (W1 + W2) c= (Up W1) + (Up W2) by TARSKI:def_3;
hence Up (W1 + W2) = (Up W1) + (Up W2) by A6, XBOOLE_0:def_10; ::_thesis: verum
end;
Lm4: for V being RealLinearSpace
for W1, W2 being Subspace of V holds Up (W1 /\ W2) = (Up W1) /\ (Up W2)
proof
let V be RealLinearSpace; ::_thesis: for W1, W2 being Subspace of V holds Up (W1 /\ W2) = (Up W1) /\ (Up W2)
let W1, W2 be Subspace of V; ::_thesis: Up (W1 /\ W2) = (Up W1) /\ (Up W2)
A1: Up (W1 /\ W2) = the carrier of (W1 /\ W2) by RUSUB_4:def_5
.= the carrier of W1 /\ the carrier of W2 by RLSUB_2:def_2 ;
for x being set st x in (Up W1) /\ (Up W2) holds
x in Up (W1 /\ W2)
proof
let x be set ; ::_thesis: ( x in (Up W1) /\ (Up W2) implies x in Up (W1 /\ W2) )
assume A2: x in (Up W1) /\ (Up W2) ; ::_thesis: x in Up (W1 /\ W2)
then x in Up W2 by XBOOLE_0:def_4;
then A3: x in the carrier of W2 by RUSUB_4:def_5;
x in Up W1 by A2, XBOOLE_0:def_4;
then x in the carrier of W1 by RUSUB_4:def_5;
hence x in Up (W1 /\ W2) by A1, A3, XBOOLE_0:def_4; ::_thesis: verum
end;
then A4: (Up W1) /\ (Up W2) c= Up (W1 /\ W2) by TARSKI:def_3;
for x being set st x in Up (W1 /\ W2) holds
x in (Up W1) /\ (Up W2)
proof
let x be set ; ::_thesis: ( x in Up (W1 /\ W2) implies x in (Up W1) /\ (Up W2) )
assume A5: x in Up (W1 /\ W2) ; ::_thesis: x in (Up W1) /\ (Up W2)
then x in the carrier of W2 by A1, XBOOLE_0:def_4;
then A6: x in Up W2 by RUSUB_4:def_5;
x in the carrier of W1 by A1, A5, XBOOLE_0:def_4;
then x in Up W1 by RUSUB_4:def_5;
hence x in (Up W1) /\ (Up W2) by A6, XBOOLE_0:def_4; ::_thesis: verum
end;
then Up (W1 /\ W2) c= (Up W1) /\ (Up W2) by TARSKI:def_3;
hence Up (W1 /\ W2) = (Up W1) /\ (Up W2) by A4, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: CONVEX2:7
for V being RealLinearSpace
for M being Subset of V holds Convex-Family M <> {} ;
Lm5: for V being RealLinearSpace
for L1, L2 being Convex_Combination of V
for a, b being Real st a * b > 0 holds
Carrier ((a * L1) + (b * L2)) = (Carrier (a * L1)) \/ (Carrier (b * L2))
proof
let V be RealLinearSpace; ::_thesis: for L1, L2 being Convex_Combination of V
for a, b being Real st a * b > 0 holds
Carrier ((a * L1) + (b * L2)) = (Carrier (a * L1)) \/ (Carrier (b * L2))
let L1, L2 be Convex_Combination of V; ::_thesis: for a, b being Real st a * b > 0 holds
Carrier ((a * L1) + (b * L2)) = (Carrier (a * L1)) \/ (Carrier (b * L2))
let a, b be Real; ::_thesis: ( a * b > 0 implies Carrier ((a * L1) + (b * L2)) = (Carrier (a * L1)) \/ (Carrier (b * L2)) )
assume a * b > 0 ; ::_thesis: Carrier ((a * L1) + (b * L2)) = (Carrier (a * L1)) \/ (Carrier (b * L2))
then A1: ( not ( a >= 0 & b <= 0 ) & not ( a <= 0 & b >= 0 ) ) by XREAL_1:131;
then A2: Carrier L2 = Carrier (b * L2) by RLVECT_2:42;
A3: Carrier L1 = Carrier (a * L1) by A1, RLVECT_2:42;
for x being set st x in (Carrier (a * L1)) \/ (Carrier (b * L2)) holds
x in Carrier ((a * L1) + (b * L2))
proof
let x be set ; ::_thesis: ( x in (Carrier (a * L1)) \/ (Carrier (b * L2)) implies x in Carrier ((a * L1) + (b * L2)) )
assume A4: x in (Carrier (a * L1)) \/ (Carrier (b * L2)) ; ::_thesis: x in Carrier ((a * L1) + (b * L2))
now__::_thesis:_x_in_Carrier_((a_*_L1)_+_(b_*_L2))
percases ( x in Carrier (a * L1) or x in Carrier (b * L2) ) by A4, XBOOLE_0:def_3;
supposeA5: x in Carrier (a * L1) ; ::_thesis: x in Carrier ((a * L1) + (b * L2))
then x in { v where v is Element of V : (a * L1) . v <> 0 } by RLVECT_2:def_4;
then consider v being Element of V such that
A6: v = x and
A7: (a * L1) . v <> 0 ;
A8: L1 . v > 0 by A3, A5, A6, CONVEX1:22;
v in Carrier ((a * L1) + (b * L2))
proof
now__::_thesis:_v_in_Carrier_((a_*_L1)_+_(b_*_L2))
percases ( v in Carrier L2 or not v in Carrier L2 ) ;
supposeA9: v in Carrier L2 ; ::_thesis: v in Carrier ((a * L1) + (b * L2))
then A10: L2 . v > 0 by CONVEX1:22;
now__::_thesis:_v_in_Carrier_((a_*_L1)_+_(b_*_L2))
percases ( ( a > 0 & b > 0 ) or ( a < 0 & b < 0 ) ) by A1;
supposeA11: ( a > 0 & b > 0 ) ; ::_thesis: v in Carrier ((a * L1) + (b * L2))
then b * (L2 . v) > 0 by A10, XREAL_1:129;
then (b * L2) . v > 0 by RLVECT_2:def_11;
then A12: ((a * L1) . v) + ((b * L2) . v) > (a * L1) . v by XREAL_1:29;
a * (L1 . v) > 0 by A8, A11, XREAL_1:129;
then (a * L1) . v > 0 by RLVECT_2:def_11;
then ((a * L1) + (b * L2)) . v > 0 by A12, RLVECT_2:def_10;
hence v in Carrier ((a * L1) + (b * L2)) by RLVECT_2:19; ::_thesis: verum
end;
supposeA13: ( a < 0 & b < 0 ) ; ::_thesis: v in Carrier ((a * L1) + (b * L2))
then a * (L1 . v) < 0 by A3, A5, A6, CONVEX1:22, XREAL_1:132;
then (a * L1) . v < 0 by RLVECT_2:def_11;
then A14: ((a * L1) . v) + ((b * L2) . v) < (b * L2) . v by XREAL_1:30;
b * (L2 . v) < 0 by A9, A13, CONVEX1:22, XREAL_1:132;
then (b * L2) . v < 0 by RLVECT_2:def_11;
then ((a * L1) + (b * L2)) . v < 0 by A14, RLVECT_2:def_10;
hence v in Carrier ((a * L1) + (b * L2)) by RLVECT_2:19; ::_thesis: verum
end;
end;
end;
hence v in Carrier ((a * L1) + (b * L2)) ; ::_thesis: verum
end;
suppose not v in Carrier L2 ; ::_thesis: v in Carrier ((a * L1) + (b * L2))
then L2 . v = 0 by RLVECT_2:19;
then b * (L2 . v) = 0 ;
then (b * L2) . v = 0 by RLVECT_2:def_11;
then ((a * L1) . v) + ((b * L2) . v) = (a * L1) . v ;
then ((a * L1) + (b * L2)) . v <> 0 by A7, RLVECT_2:def_10;
hence v in Carrier ((a * L1) + (b * L2)) by RLVECT_2:19; ::_thesis: verum
end;
end;
end;
hence v in Carrier ((a * L1) + (b * L2)) ; ::_thesis: verum
end;
hence x in Carrier ((a * L1) + (b * L2)) by A6; ::_thesis: verum
end;
supposeA15: x in Carrier (b * L2) ; ::_thesis: x in Carrier ((a * L1) + (b * L2))
then x in { v where v is Element of V : (b * L2) . v <> 0 } by RLVECT_2:def_4;
then consider v being Element of V such that
A16: v = x and
A17: (b * L2) . v <> 0 ;
A18: L2 . v > 0 by A2, A15, A16, CONVEX1:22;
v in Carrier ((a * L1) + (b * L2))
proof
now__::_thesis:_v_in_Carrier_((a_*_L1)_+_(b_*_L2))
percases ( v in Carrier L1 or not v in Carrier L1 ) ;
supposeA19: v in Carrier L1 ; ::_thesis: v in Carrier ((a * L1) + (b * L2))
then A20: L1 . v > 0 by CONVEX1:22;
now__::_thesis:_v_in_Carrier_((a_*_L1)_+_(b_*_L2))
percases ( ( a > 0 & b > 0 ) or ( a < 0 & b < 0 ) ) by A1;
supposeA21: ( a > 0 & b > 0 ) ; ::_thesis: v in Carrier ((a * L1) + (b * L2))
then b * (L2 . v) > 0 by A18, XREAL_1:129;
then (b * L2) . v > 0 by RLVECT_2:def_11;
then A22: ((a * L1) . v) + ((b * L2) . v) > (a * L1) . v by XREAL_1:29;
a * (L1 . v) > 0 by A20, A21, XREAL_1:129;
then (a * L1) . v > 0 by RLVECT_2:def_11;
then ((a * L1) + (b * L2)) . v > 0 by A22, RLVECT_2:def_10;
hence v in Carrier ((a * L1) + (b * L2)) by RLVECT_2:19; ::_thesis: verum
end;
supposeA23: ( a < 0 & b < 0 ) ; ::_thesis: v in Carrier ((a * L1) + (b * L2))
then a * (L1 . v) < 0 by A19, CONVEX1:22, XREAL_1:132;
then (a * L1) . v < 0 by RLVECT_2:def_11;
then A24: ((a * L1) . v) + ((b * L2) . v) < (b * L2) . v by XREAL_1:30;
b * (L2 . v) < 0 by A2, A15, A16, A23, CONVEX1:22, XREAL_1:132;
then (b * L2) . v < 0 by RLVECT_2:def_11;
then ((a * L1) + (b * L2)) . v < 0 by A24, RLVECT_2:def_10;
hence v in Carrier ((a * L1) + (b * L2)) by RLVECT_2:19; ::_thesis: verum
end;
end;
end;
hence v in Carrier ((a * L1) + (b * L2)) ; ::_thesis: verum
end;
suppose not v in Carrier L1 ; ::_thesis: v in Carrier ((a * L1) + (b * L2))
then L1 . v = 0 by RLVECT_2:19;
then a * (L1 . v) = 0 ;
then (a * L1) . v = 0 by RLVECT_2:def_11;
then ((a * L1) . v) + ((b * L2) . v) = (b * L2) . v ;
then ((a * L1) + (b * L2)) . v <> 0 by A17, RLVECT_2:def_10;
hence v in Carrier ((a * L1) + (b * L2)) by RLVECT_2:19; ::_thesis: verum
end;
end;
end;
hence v in Carrier ((a * L1) + (b * L2)) ; ::_thesis: verum
end;
hence x in Carrier ((a * L1) + (b * L2)) by A16; ::_thesis: verum
end;
end;
end;
hence x in Carrier ((a * L1) + (b * L2)) ; ::_thesis: verum
end;
then A25: (Carrier (a * L1)) \/ (Carrier (b * L2)) c= Carrier ((a * L1) + (b * L2)) by TARSKI:def_3;
Carrier ((a * L1) + (b * L2)) c= (Carrier (a * L1)) \/ (Carrier (b * L2)) by RLVECT_2:37;
hence Carrier ((a * L1) + (b * L2)) = (Carrier (a * L1)) \/ (Carrier (b * L2)) by A25, XBOOLE_0:def_10; ::_thesis: verum
end;
Lm6: for F, G being Function st F,G are_fiberwise_equipotent holds
for x1, x2 being set st x1 in dom F & x2 in dom F & x1 <> x2 holds
ex z1, z2 being set st
( z1 in dom G & z2 in dom G & z1 <> z2 & F . x1 = G . z1 & F . x2 = G . z2 )
proof
let F, G be Function; ::_thesis: ( F,G are_fiberwise_equipotent implies for x1, x2 being set st x1 in dom F & x2 in dom F & x1 <> x2 holds
ex z1, z2 being set st
( z1 in dom G & z2 in dom G & z1 <> z2 & F . x1 = G . z1 & F . x2 = G . z2 ) )
assume F,G are_fiberwise_equipotent ; ::_thesis: for x1, x2 being set st x1 in dom F & x2 in dom F & x1 <> x2 holds
ex z1, z2 being set st
( z1 in dom G & z2 in dom G & z1 <> z2 & F . x1 = G . z1 & F . x2 = G . z2 )
then consider H being Function such that
A1: dom H = dom F and
A2: rng H = dom G and
A3: H is one-to-one and
A4: F = G * H by CLASSES1:77;
let x1, x2 be set ; ::_thesis: ( x1 in dom F & x2 in dom F & x1 <> x2 implies ex z1, z2 being set st
( z1 in dom G & z2 in dom G & z1 <> z2 & F . x1 = G . z1 & F . x2 = G . z2 ) )
assume that
A5: x1 in dom F and
A6: x2 in dom F and
A7: x1 <> x2 ; ::_thesis: ex z1, z2 being set st
( z1 in dom G & z2 in dom G & z1 <> z2 & F . x1 = G . z1 & F . x2 = G . z2 )
A8: ( H . x1 in dom G & H . x2 in dom G ) by A5, A6, A1, A2, FUNCT_1:3;
A9: F . x2 = G . (H . x2) by A6, A4, FUNCT_1:12;
( H . x1 <> H . x2 & F . x1 = G . (H . x1) ) by A5, A6, A7, A1, A3, A4, FUNCT_1:12, FUNCT_1:def_4;
hence ex z1, z2 being set st
( z1 in dom G & z2 in dom G & z1 <> z2 & F . x1 = G . z1 & F . x2 = G . z2 ) by A8, A9; ::_thesis: verum
end;
Lm7: for V being RealLinearSpace
for L being Linear_Combination of V
for A being Subset of V st A c= Carrier L holds
ex L1 being Linear_Combination of V st Carrier L1 = A
proof
let V be RealLinearSpace; ::_thesis: for L being Linear_Combination of V
for A being Subset of V st A c= Carrier L holds
ex L1 being Linear_Combination of V st Carrier L1 = A
let L be Linear_Combination of V; ::_thesis: for A being Subset of V st A c= Carrier L holds
ex L1 being Linear_Combination of V st Carrier L1 = A
let A be Subset of V; ::_thesis: ( A c= Carrier L implies ex L1 being Linear_Combination of V st Carrier L1 = A )
consider F being Function such that
A1: L = F and
A2: dom F = the carrier of V and
A3: rng F c= REAL by FUNCT_2:def_2;
defpred S1[ set , set ] means ( ( $1 in A implies $2 = F . $1 ) & ( not $1 in A implies $2 = 0 ) );
A4: for x being set st x in the carrier of V holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in the carrier of V implies ex y being set st S1[x,y] )
assume x in the carrier of V ; ::_thesis: ex y being set st S1[x,y]
now__::_thesis:_ex_y_being_set_st_S1[x,y]
percases ( x in A or not x in A ) ;
suppose x in A ; ::_thesis: ex y being set st S1[x,y]
hence ex y being set st S1[x,y] ; ::_thesis: verum
end;
suppose not x in A ; ::_thesis: ex y being set st S1[x,y]
hence ex y being set st S1[x,y] ; ::_thesis: verum
end;
end;
end;
hence ex y being set st S1[x,y] ; ::_thesis: verum
end;
consider L1 being Function such that
A5: ( dom L1 = the carrier of V & ( for x being set st x in the carrier of V holds
S1[x,L1 . x] ) ) from CLASSES1:sch_1(A4);
for y being set st y in rng L1 holds
y in REAL
proof
let y be set ; ::_thesis: ( y in rng L1 implies y in REAL )
assume y in rng L1 ; ::_thesis: y in REAL
then consider x being set such that
A6: x in dom L1 and
A7: y = L1 . x by FUNCT_1:def_3;
reconsider x = x as Element of V by A5, A6;
now__::_thesis:_y_in_REAL
percases ( x in A or not x in A ) ;
supposeA8: x in A ; ::_thesis: y in REAL
A9: F . x in rng F by A2, FUNCT_1:3;
y = F . x by A5, A7, A8;
hence y in REAL by A3, A9; ::_thesis: verum
end;
suppose not x in A ; ::_thesis: y in REAL
then L1 . x = 0 by A5;
hence y in REAL by A7; ::_thesis: verum
end;
end;
end;
hence y in REAL ; ::_thesis: verum
end;
then rng L1 c= REAL by TARSKI:def_3;
then A10: L1 is Element of Funcs ( the carrier of V,REAL) by A5, FUNCT_2:def_2;
assume A11: A c= Carrier L ; ::_thesis: ex L1 being Linear_Combination of V st Carrier L1 = A
then reconsider A = A as finite Subset of V by FINSET_1:1;
for v being Element of V st not v in A holds
L1 . v = 0 by A5;
then reconsider L1 = L1 as Linear_Combination of V by A10, RLVECT_2:def_3;
for v being set st v in Carrier L1 holds
v in A
proof
let v be set ; ::_thesis: ( v in Carrier L1 implies v in A )
assume A12: v in Carrier L1 ; ::_thesis: v in A
then reconsider v = v as Element of V ;
L1 . v <> 0 by A12, RLVECT_2:19;
hence v in A by A5; ::_thesis: verum
end;
then A13: Carrier L1 c= A by TARSKI:def_3;
take L1 ; ::_thesis: Carrier L1 = A
for v being set st v in A holds
v in Carrier L1
proof
let v be set ; ::_thesis: ( v in A implies v in Carrier L1 )
assume A14: v in A ; ::_thesis: v in Carrier L1
then reconsider v = v as Element of V ;
( L1 . v = F . v & L . v <> 0 ) by A11, A5, A14, RLVECT_2:19;
hence v in Carrier L1 by A1, RLVECT_2:19; ::_thesis: verum
end;
then A c= Carrier L1 by TARSKI:def_3;
hence Carrier L1 = A by A13, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th8: :: CONVEX2:8
for V being RealLinearSpace
for L1, L2 being Convex_Combination of V
for r being Real st 0 < r & r < 1 holds
(r * L1) + ((1 - r) * L2) is Convex_Combination of V
proof
let V be RealLinearSpace; ::_thesis: for L1, L2 being Convex_Combination of V
for r being Real st 0 < r & r < 1 holds
(r * L1) + ((1 - r) * L2) is Convex_Combination of V
let L1, L2 be Convex_Combination of V; ::_thesis: for r being Real st 0 < r & r < 1 holds
(r * L1) + ((1 - r) * L2) is Convex_Combination of V
let r be Real; ::_thesis: ( 0 < r & r < 1 implies (r * L1) + ((1 - r) * L2) is Convex_Combination of V )
assume that
A1: 0 < r and
A2: r < 1 ; ::_thesis: (r * L1) + ((1 - r) * L2) is Convex_Combination of V
A3: Carrier (r * L1) = Carrier L1 by A1, RLVECT_2:42;
set Mid = (Carrier (r * L1)) /\ (Carrier ((1 - r) * L2));
set L = (r * L1) + ((1 - r) * L2);
consider F2 being FinSequence of the carrier of V such that
A4: F2 is one-to-one and
A5: rng F2 = Carrier L2 and
A6: ex f being FinSequence of REAL st
( len f = len F2 & Sum f = 1 & ( for n being Nat st n in dom f holds
( f . n = L2 . (F2 . n) & f . n >= 0 ) ) ) by CONVEX1:def_3;
set Btm = (Carrier ((r * L1) + ((1 - r) * L2))) \ (Carrier (r * L1));
set Top = (Carrier ((r * L1) + ((1 - r) * L2))) \ (Carrier ((1 - r) * L2));
consider F1 being FinSequence of the carrier of V such that
A7: F1 is one-to-one and
A8: rng F1 = Carrier L1 and
A9: ex f being FinSequence of REAL st
( len f = len F1 & Sum f = 1 & ( for n being Nat st n in dom f holds
( f . n = L1 . (F1 . n) & f . n >= 0 ) ) ) by CONVEX1:def_3;
consider Lt being Linear_Combination of V such that
A10: Carrier Lt = (Carrier ((r * L1) + ((1 - r) * L2))) \ (Carrier ((1 - r) * L2)) by Lm7, XBOOLE_1:36;
A11: r - r < 1 - r by A2, XREAL_1:9;
then A12: Carrier ((1 - r) * L2) = Carrier L2 by RLVECT_2:42;
A13: r * (1 - r) > 0 by A1, A11, XREAL_1:129;
then A14: Carrier ((r * L1) + ((1 - r) * L2)) = (Carrier (r * L1)) \/ (Carrier ((1 - r) * L2)) by Lm5;
then consider Lm being Linear_Combination of V such that
A15: Carrier Lm = (Carrier (r * L1)) /\ (Carrier ((1 - r) * L2)) by Lm7, XBOOLE_1:29;
consider Lb being Linear_Combination of V such that
A16: Carrier Lb = (Carrier ((r * L1) + ((1 - r) * L2))) \ (Carrier (r * L1)) by Lm7, XBOOLE_1:36;
consider Ft being FinSequence of the carrier of V such that
A17: Ft is one-to-one and
A18: rng Ft = Carrier Lt and
Sum Lt = Sum (Lt (#) Ft) by RLVECT_2:def_8;
consider Fb being FinSequence of the carrier of V such that
A19: Fb is one-to-one and
A20: rng Fb = Carrier Lb and
Sum Lb = Sum (Lb (#) Fb) by RLVECT_2:def_8;
consider Fm being FinSequence of the carrier of V such that
A21: Fm is one-to-one and
A22: rng Fm = Carrier Lm and
Sum Lm = Sum (Lm (#) Fm) by RLVECT_2:def_8;
A23: rng (Ft ^ Fm) = (rng Ft) \/ (rng Fm) by FINSEQ_1:31
.= (((Carrier L1) \/ (Carrier L2)) \ (Carrier L2)) \/ ((Carrier L1) /\ (Carrier L2)) by A13, A3, A12, A10, A15, A18, A22, Lm5
.= (((Carrier L1) \ (Carrier L2)) \/ ((Carrier L2) \ (Carrier L2))) \/ ((Carrier L1) /\ (Carrier L2)) by XBOOLE_1:42
.= (((Carrier L1) \ (Carrier L2)) \/ {}) \/ ((Carrier L1) /\ (Carrier L2)) by XBOOLE_1:37
.= (Carrier L1) \ ((Carrier L2) \ (Carrier L2)) by XBOOLE_1:52
.= (Carrier L1) \ {} by XBOOLE_1:37
.= rng F1 by A8 ;
A24: rng Ft misses rng Fm by A10, A15, A18, A22, XBOOLE_1:17, XBOOLE_1:85;
then A25: Ft ^ Fm is one-to-one by A17, A21, FINSEQ_3:91;
set F = (Ft ^ Fm) ^ Fb;
consider f2 being FinSequence of REAL such that
A26: len f2 = len F2 and
A27: Sum f2 = 1 and
A28: for n being Nat st n in dom f2 holds
( f2 . n = L2 . (F2 . n) & f2 . n >= 0 ) by A6;
deffunc H1( set ) -> set = L1 . (Ft . $1);
consider ft being FinSequence such that
A29: ( len ft = len Ft & ( for j being Nat st j in dom ft holds
ft . j = H1(j) ) ) from FINSEQ_1:sch_2();
rng ft c= REAL
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng ft or y in REAL )
consider L1f being Function such that
A30: L1 = L1f and
A31: dom L1f = the carrier of V and
A32: rng L1f c= REAL by FUNCT_2:def_2;
assume y in rng ft ; ::_thesis: y in REAL
then consider x being set such that
A33: x in dom ft and
A34: ft . x = y by FUNCT_1:def_3;
reconsider x = x as Element of NAT by A33;
A35: ft . x = L1 . (Ft . x) by A29, A33;
x in Seg (len Ft) by A29, A33, FINSEQ_1:def_3;
then x in dom Ft by FINSEQ_1:def_3;
then A36: Ft . x in rng Ft by FUNCT_1:3;
rng Ft c= the carrier of V by FINSEQ_1:def_4;
then reconsider Ftx = Ft . x as Element of V by A36;
Ftx in dom L1f by A31;
then ft . x in rng L1f by A35, A30, FUNCT_1:3;
hence y in REAL by A34, A32; ::_thesis: verum
end;
then reconsider ft = ft as FinSequence of REAL by FINSEQ_1:def_4;
deffunc H2( set ) -> set = L1 . (Fm . $1);
consider fm1 being FinSequence such that
A37: ( len fm1 = len Fm & ( for j being Nat st j in dom fm1 holds
fm1 . j = H2(j) ) ) from FINSEQ_1:sch_2();
rng fm1 c= REAL
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng fm1 or y in REAL )
consider L1f being Function such that
A38: L1 = L1f and
A39: dom L1f = the carrier of V and
A40: rng L1f c= REAL by FUNCT_2:def_2;
assume y in rng fm1 ; ::_thesis: y in REAL
then consider x being set such that
A41: x in dom fm1 and
A42: fm1 . x = y by FUNCT_1:def_3;
reconsider x = x as Element of NAT by A41;
A43: fm1 . x = L1 . (Fm . x) by A37, A41;
x in Seg (len Fm) by A37, A41, FINSEQ_1:def_3;
then x in dom Fm by FINSEQ_1:def_3;
then A44: Fm . x in rng Fm by FUNCT_1:3;
rng Fm c= the carrier of V by FINSEQ_1:def_4;
then reconsider Fmx = Fm . x as Element of V by A44;
Fmx in dom L1f by A39;
then fm1 . x in rng L1f by A43, A38, FUNCT_1:3;
hence y in REAL by A42, A40; ::_thesis: verum
end;
then reconsider fm1 = fm1 as FinSequence of REAL by FINSEQ_1:def_4;
deffunc H3( set ) -> set = L2 . (Fm . $1);
consider fm2 being FinSequence such that
A45: ( len fm2 = len Fm & ( for j being Nat st j in dom fm2 holds
fm2 . j = H3(j) ) ) from FINSEQ_1:sch_2();
A46: for x being set st x in dom (ft ^ fm1) holds
(ft ^ fm1) . x = L1 . ((Ft ^ Fm) . x)
proof
let x be set ; ::_thesis: ( x in dom (ft ^ fm1) implies (ft ^ fm1) . x = L1 . ((Ft ^ Fm) . x) )
assume A47: x in dom (ft ^ fm1) ; ::_thesis: (ft ^ fm1) . x = L1 . ((Ft ^ Fm) . x)
then reconsider n = x as Element of NAT ;
now__::_thesis:_(ft_^_fm1)_._x_=_L1_._((Ft_^_Fm)_._x)
percases ( n in dom ft or ex m being Nat st
( m in dom fm1 & n = (len ft) + m ) ) by A47, FINSEQ_1:25;
supposeA48: n in dom ft ; ::_thesis: (ft ^ fm1) . x = L1 . ((Ft ^ Fm) . x)
then n in Seg (len Ft) by A29, FINSEQ_1:def_3;
then A49: n in dom Ft by FINSEQ_1:def_3;
ft . n = L1 . (Ft . n) by A29, A48;
then (ft ^ fm1) . n = L1 . (Ft . n) by A48, FINSEQ_1:def_7;
hence (ft ^ fm1) . x = L1 . ((Ft ^ Fm) . x) by A49, FINSEQ_1:def_7; ::_thesis: verum
end;
suppose ex m being Nat st
( m in dom fm1 & n = (len ft) + m ) ; ::_thesis: (ft ^ fm1) . x = L1 . ((Ft ^ Fm) . x)
then consider m being Element of NAT such that
A50: m in dom fm1 and
A51: n = (len ft) + m ;
m in Seg (len Fm) by A37, A50, FINSEQ_1:def_3;
then A52: m in dom Fm by FINSEQ_1:def_3;
(ft ^ fm1) . n = fm1 . m by A50, A51, FINSEQ_1:def_7
.= L1 . (Fm . m) by A37, A50 ;
hence (ft ^ fm1) . x = L1 . ((Ft ^ Fm) . x) by A29, A51, A52, FINSEQ_1:def_7; ::_thesis: verum
end;
end;
end;
hence (ft ^ fm1) . x = L1 . ((Ft ^ Fm) . x) ; ::_thesis: verum
end;
for x being set holds
( x in dom (ft ^ fm1) iff ( x in dom (Ft ^ Fm) & (Ft ^ Fm) . x in dom L1 ) )
proof
let x be set ; ::_thesis: ( x in dom (ft ^ fm1) iff ( x in dom (Ft ^ Fm) & (Ft ^ Fm) . x in dom L1 ) )
A53: len (ft ^ fm1) = (len ft) + (len fm1) by FINSEQ_1:22
.= len (Ft ^ Fm) by A29, A37, FINSEQ_1:22 ;
A54: dom (ft ^ fm1) = Seg (len (ft ^ fm1)) by FINSEQ_1:def_3
.= dom (Ft ^ Fm) by A53, FINSEQ_1:def_3 ;
( x in dom (ft ^ fm1) implies (Ft ^ Fm) . x in dom L1 )
proof
assume x in dom (ft ^ fm1) ; ::_thesis: (Ft ^ Fm) . x in dom L1
then (Ft ^ Fm) . x in rng (Ft ^ Fm) by A54, FUNCT_1:3;
then A55: (Ft ^ Fm) . x in (Carrier Lt) \/ (Carrier Lm) by A18, A22, FINSEQ_1:31;
dom L1 = the carrier of V by FUNCT_2:92;
hence (Ft ^ Fm) . x in dom L1 by A55; ::_thesis: verum
end;
hence ( x in dom (ft ^ fm1) iff ( x in dom (Ft ^ Fm) & (Ft ^ Fm) . x in dom L1 ) ) by A54; ::_thesis: verum
end;
then A56: ft ^ fm1 = L1 * (Ft ^ Fm) by A46, FUNCT_1:10;
A57: dom L2 = the carrier of V by FUNCT_2:92;
A58: for x being set holds
( x in dom f2 iff ( x in dom F2 & F2 . x in dom L2 ) )
proof
let x be set ; ::_thesis: ( x in dom f2 iff ( x in dom F2 & F2 . x in dom L2 ) )
A59: now__::_thesis:_(_x_in_dom_f2_implies_(_x_in_dom_F2_&_F2_._x_in_dom_L2_)_)
assume x in dom f2 ; ::_thesis: ( x in dom F2 & F2 . x in dom L2 )
then x in Seg (len F2) by A26, FINSEQ_1:def_3;
hence x in dom F2 by FINSEQ_1:def_3; ::_thesis: F2 . x in dom L2
then F2 . x in rng F2 by FUNCT_1:3;
hence F2 . x in dom L2 by A5, A57; ::_thesis: verum
end;
now__::_thesis:_(_x_in_dom_F2_&_F2_._x_in_dom_L2_implies_x_in_dom_f2_)
assume that
A60: x in dom F2 and
F2 . x in dom L2 ; ::_thesis: x in dom f2
x in Seg (len F2) by A60, FINSEQ_1:def_3;
hence x in dom f2 by A26, FINSEQ_1:def_3; ::_thesis: verum
end;
hence ( x in dom f2 iff ( x in dom F2 & F2 . x in dom L2 ) ) by A59; ::_thesis: verum
end;
deffunc H4( set ) -> set = L2 . (Fb . $1);
consider fb being FinSequence such that
A61: ( len fb = len Fb & ( for j being Nat st j in dom fb holds
fb . j = H4(j) ) ) from FINSEQ_1:sch_2();
rng fm2 c= REAL
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng fm2 or y in REAL )
consider L2f being Function such that
A62: L2 = L2f and
A63: dom L2f = the carrier of V and
A64: rng L2f c= REAL by FUNCT_2:def_2;
assume y in rng fm2 ; ::_thesis: y in REAL
then consider x being set such that
A65: x in dom fm2 and
A66: fm2 . x = y by FUNCT_1:def_3;
reconsider x = x as Element of NAT by A65;
A67: fm2 . x = L2 . (Fm . x) by A45, A65;
x in Seg (len Fm) by A45, A65, FINSEQ_1:def_3;
then x in dom Fm by FINSEQ_1:def_3;
then A68: Fm . x in rng Fm by FUNCT_1:3;
rng Fm c= the carrier of V by FINSEQ_1:def_4;
then reconsider Fmx = Fm . x as Element of V by A68;
Fmx in dom L2f by A63;
then fm2 . x in rng L2f by A67, A62, FUNCT_1:3;
hence y in REAL by A66, A64; ::_thesis: verum
end;
then reconsider fm2 = fm2 as FinSequence of REAL by FINSEQ_1:def_4;
A69: len (r * fm1) = len fm1 by RVSUM_1:117
.= len ((1 - r) * fm2) by A37, A45, RVSUM_1:117 ;
rng fb c= REAL
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng fb or y in REAL )
consider L2f being Function such that
A70: L2 = L2f and
A71: dom L2f = the carrier of V and
A72: rng L2f c= REAL by FUNCT_2:def_2;
assume y in rng fb ; ::_thesis: y in REAL
then consider x being set such that
A73: x in dom fb and
A74: fb . x = y by FUNCT_1:def_3;
reconsider x = x as Element of NAT by A73;
A75: fb . x = L2 . (Fb . x) by A61, A73;
x in Seg (len Fb) by A61, A73, FINSEQ_1:def_3;
then x in dom Fb by FINSEQ_1:def_3;
then A76: Fb . x in rng Fb by FUNCT_1:3;
rng Fb c= the carrier of V by FINSEQ_1:def_4;
then reconsider Fbx = Fb . x as Element of V by A76;
Fbx in dom L2f by A71;
then fb . x in rng L2f by A75, A70, FUNCT_1:3;
hence y in REAL by A74, A72; ::_thesis: verum
end;
then reconsider fb = fb as FinSequence of REAL by FINSEQ_1:def_4;
set f = ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb);
consider f1 being FinSequence of REAL such that
A77: len f1 = len F1 and
A78: Sum f1 = 1 and
A79: for n being Nat st n in dom f1 holds
( f1 . n = L1 . (F1 . n) & f1 . n >= 0 ) by A9;
len (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) = (len ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2)))) + (len ((1 - r) * fb)) by FINSEQ_1:22
.= ((len (r * ft)) + (len ((r * fm1) + ((1 - r) * fm2)))) + (len ((1 - r) * fb)) by FINSEQ_1:22
.= ((len ft) + (len ((r * fm1) + ((1 - r) * fm2)))) + (len ((1 - r) * fb)) by RVSUM_1:117
.= ((len ft) + (len ((r * fm1) + ((1 - r) * fm2)))) + (len fb) by RVSUM_1:117
.= ((len ft) + (len (r * fm1))) + (len fb) by A69, INTEGRA5:2
.= ((len Ft) + (len Fm)) + (len Fb) by A29, A37, A61, RVSUM_1:117
.= (len (Ft ^ Fm)) + (len Fb) by FINSEQ_1:22 ;
then A80: len (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) = len ((Ft ^ Fm) ^ Fb) by FINSEQ_1:22;
A81: dom L1 = the carrier of V by FUNCT_2:92;
A82: for x being set holds
( x in dom f1 iff ( x in dom F1 & F1 . x in dom L1 ) )
proof
let x be set ; ::_thesis: ( x in dom f1 iff ( x in dom F1 & F1 . x in dom L1 ) )
A83: now__::_thesis:_(_x_in_dom_f1_implies_(_x_in_dom_F1_&_F1_._x_in_dom_L1_)_)
assume x in dom f1 ; ::_thesis: ( x in dom F1 & F1 . x in dom L1 )
then x in Seg (len F1) by A77, FINSEQ_1:def_3;
hence x in dom F1 by FINSEQ_1:def_3; ::_thesis: F1 . x in dom L1
then F1 . x in rng F1 by FUNCT_1:3;
hence F1 . x in dom L1 by A8, A81; ::_thesis: verum
end;
now__::_thesis:_(_x_in_dom_F1_&_F1_._x_in_dom_L1_implies_x_in_dom_f1_)
assume that
A84: x in dom F1 and
F1 . x in dom L1 ; ::_thesis: x in dom f1
x in Seg (len F1) by A84, FINSEQ_1:def_3;
hence x in dom f1 by A77, FINSEQ_1:def_3; ::_thesis: verum
end;
hence ( x in dom f1 iff ( x in dom F1 & F1 . x in dom L1 ) ) by A83; ::_thesis: verum
end;
A85: rng (Ft ^ Fm) = (Carrier Lt) \/ (Carrier Lm) by A18, A22, FINSEQ_1:31;
for x being set st x in dom f1 holds
f1 . x = L1 . (F1 . x) by A79;
then A86: f1 = L1 * F1 by A82, FUNCT_1:10;
Ft ^ Fm is one-to-one by A17, A21, A24, FINSEQ_3:91;
then A87: F1,Ft ^ Fm are_fiberwise_equipotent by A7, A23, RFINSEQ:26;
then dom F1 = dom (Ft ^ Fm) by RFINSEQ:3;
then A88: Sum f1 = Sum (ft ^ fm1) by A8, A87, A81, A86, A85, A56, CLASSES1:83, RFINSEQ:9;
A89: rng (Fm ^ Fb) = (Carrier Lm) \/ (Carrier Lb) by A22, A20, FINSEQ_1:31;
for x being set st x in dom f2 holds
f2 . x = L2 . (F2 . x) by A28;
then A90: f2 = L2 * F2 by A58, FUNCT_1:10;
A91: rng (Fm ^ Fb) = ((Carrier ((r * L1) + ((1 - r) * L2))) \ (Carrier (r * L1))) \/ ((Carrier (r * L1)) /\ (Carrier ((1 - r) * L2))) by A15, A16, A22, A20, FINSEQ_1:31
.= (((Carrier L1) \/ (Carrier L2)) \ (Carrier L1)) \/ ((Carrier L1) /\ (Carrier L2)) by A13, A3, A12, Lm5
.= (((Carrier L1) \ (Carrier L1)) \/ ((Carrier L2) \ (Carrier L1))) \/ ((Carrier L1) /\ (Carrier L2)) by XBOOLE_1:42
.= (((Carrier L2) \ (Carrier L1)) \/ {}) \/ ((Carrier L1) /\ (Carrier L2)) by XBOOLE_1:37
.= (Carrier L2) \ ((Carrier L1) \ (Carrier L1)) by XBOOLE_1:52
.= (Carrier L2) \ {} by XBOOLE_1:37
.= rng F2 by A5 ;
for n being Element of NAT st n in dom (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) holds
( (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (((Ft ^ Fm) ^ Fb) . n) & (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0 )
proof
let n be Element of NAT ; ::_thesis: ( n in dom (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) implies ( (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (((Ft ^ Fm) ^ Fb) . n) & (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0 ) )
assume A92: n in dom (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) ; ::_thesis: ( (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (((Ft ^ Fm) ^ Fb) . n) & (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0 )
now__::_thesis:_(_(((r_*_ft)_^_((r_*_fm1)_+_((1_-_r)_*_fm2)))_^_((1_-_r)_*_fb))_._n_=_((r_*_L1)_+_((1_-_r)_*_L2))_._(((Ft_^_Fm)_^_Fb)_._n)_&_(((r_*_ft)_^_((r_*_fm1)_+_((1_-_r)_*_fm2)))_^_((1_-_r)_*_fb))_._n_>=_0_)
percases ( n in dom ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) or ex m being Nat st
( m in dom ((1 - r) * fb) & n = (len ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2)))) + m ) ) by A92, FINSEQ_1:25;
supposeA93: n in dom ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ; ::_thesis: ( (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (((Ft ^ Fm) ^ Fb) . n) & (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0 )
then A94: (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) . n by FINSEQ_1:def_7;
now__::_thesis:_(_(((r_*_ft)_^_((r_*_fm1)_+_((1_-_r)_*_fm2)))_^_((1_-_r)_*_fb))_._n_=_((r_*_L1)_+_((1_-_r)_*_L2))_._(((Ft_^_Fm)_^_Fb)_._n)_&_(((r_*_ft)_^_((r_*_fm1)_+_((1_-_r)_*_fm2)))_^_((1_-_r)_*_fb))_._n_>=_0_)
percases ( n in dom (r * ft) or ex k being Nat st
( k in dom ((r * fm1) + ((1 - r) * fm2)) & n = (len (r * ft)) + k ) ) by A93, FINSEQ_1:25;
supposeA95: n in dom (r * ft) ; ::_thesis: ( (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (((Ft ^ Fm) ^ Fb) . n) & (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0 )
len ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) = (len (r * ft)) + (len ((r * fm1) + ((1 - r) * fm2))) by FINSEQ_1:22
.= (len ft) + (len ((r * fm1) + ((1 - r) * fm2))) by RVSUM_1:117
.= (len ft) + (len (r * fm1)) by A69, INTEGRA5:2
.= (len Ft) + (len Fm) by A29, A37, RVSUM_1:117
.= len (Ft ^ Fm) by FINSEQ_1:22 ;
then n in Seg (len (Ft ^ Fm)) by A93, FINSEQ_1:def_3;
then n in dom (Ft ^ Fm) by FINSEQ_1:def_3;
then A96: (Ft ^ Fm) . n = ((Ft ^ Fm) ^ Fb) . n by FINSEQ_1:def_7;
A97: n in dom ft by A95, VALUED_1:def_5;
then n in Seg (len Ft) by A29, FINSEQ_1:def_3;
then A98: n in dom Ft by FINSEQ_1:def_3;
then A99: Ft . n in Carrier Lt by A18, FUNCT_1:3;
then reconsider Ftn = Ft . n as Element of V ;
A100: (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = (r * ft) . n by A94, A95, FINSEQ_1:def_7
.= r * (ft . n) by RVSUM_1:44
.= r * (L1 . (Ft . n)) by A29, A97 ;
not Ft . n in Carrier L2 by A12, A10, A99, XBOOLE_0:def_5;
then L2 . Ftn = 0 by RLVECT_2:19;
then (1 - r) * (L2 . Ftn) = 0 ;
then ((1 - r) * L2) . Ftn = 0 by RLVECT_2:def_11;
then (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) . Ftn) + (((1 - r) * L2) . Ftn) by A100, RLVECT_2:def_11
.= ((r * L1) + ((1 - r) * L2)) . (Ft . n) by RLVECT_2:def_10 ;
hence (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (((Ft ^ Fm) ^ Fb) . n) by A98, A96, FINSEQ_1:def_7; ::_thesis: (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0
A101: rng Ft c= rng (Ft ^ Fm) by FINSEQ_1:29;
Ft . n in rng Ft by A98, FUNCT_1:3;
then consider m9 being set such that
A102: m9 in dom F1 and
A103: F1 . m9 = Ft . n by A23, A101, FUNCT_1:def_3;
reconsider m9 = m9 as Element of NAT by A102;
m9 in Seg (len f1) by A77, A102, FINSEQ_1:def_3;
then m9 in dom f1 by FINSEQ_1:def_3;
then ( f1 . m9 = L1 . (F1 . m9) & f1 . m9 >= 0 ) by A79;
hence (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0 by A1, A100, A103, XREAL_1:127; ::_thesis: verum
end;
suppose ex k being Nat st
( k in dom ((r * fm1) + ((1 - r) * fm2)) & n = (len (r * ft)) + k ) ; ::_thesis: ( (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (((Ft ^ Fm) ^ Fb) . n) & (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0 )
then consider m being Element of NAT such that
A104: m in dom ((r * fm1) + ((1 - r) * fm2)) and
A105: n = (len (r * ft)) + m ;
len (r * fm1) = len fm1 by RVSUM_1:117
.= len ((1 - r) * fm2) by A37, A45, RVSUM_1:117 ;
then A106: len ((r * fm1) + ((1 - r) * fm2)) = len (r * fm1) by INTEGRA5:2
.= len fm1 by RVSUM_1:117 ;
then A107: m in dom Fm by A37, A104, FINSEQ_3:29;
then A108: Fm . m in rng Fm by FUNCT_1:3;
then reconsider Fmm = Fm . m as Element of V by A22;
A109: m in dom fm1 by A104, A106, FINSEQ_3:29;
A110: m in dom fm2 by A37, A45, A104, A106, FINSEQ_3:29;
A111: (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * fm1) + ((1 - r) * fm2)) . m by A94, A104, A105, FINSEQ_1:def_7
.= ((r * fm1) . m) + (((1 - r) * fm2) . m) by A104, VALUED_1:def_1
.= (r * (fm1 . m)) + (((1 - r) * fm2) . m) by RVSUM_1:44
.= (r * (fm1 . m)) + ((1 - r) * (fm2 . m)) by RVSUM_1:44
.= (r * (L1 . (Fm . m))) + ((1 - r) * (fm2 . m)) by A37, A109
.= (r * (L1 . (Fm . m))) + ((1 - r) * (L2 . (Fm . m))) by A45, A110 ;
len ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) = (len (r * ft)) + (len ((r * fm1) + ((1 - r) * fm2))) by FINSEQ_1:22
.= (len ft) + (len ((r * fm1) + ((1 - r) * fm2))) by RVSUM_1:117
.= (len ft) + (len (r * fm1)) by A69, INTEGRA5:2
.= (len Ft) + (len Fm) by A29, A37, RVSUM_1:117
.= len (Ft ^ Fm) by FINSEQ_1:22 ;
then n in Seg (len (Ft ^ Fm)) by A93, FINSEQ_1:def_3;
then n in dom (Ft ^ Fm) by FINSEQ_1:def_3;
then A112: (Ft ^ Fm) . n = ((Ft ^ Fm) ^ Fb) . n by FINSEQ_1:def_7;
A113: len (r * ft) = len Ft by A29, RVSUM_1:117;
( r * (L1 . Fmm) = (r * L1) . (Fm . m) & (1 - r) * (L2 . Fmm) = ((1 - r) * L2) . (Fm . m) ) by RLVECT_2:def_11;
then (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (Fm . m) by A111, RLVECT_2:def_10;
hence (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (((Ft ^ Fm) ^ Fb) . n) by A105, A107, A112, A113, FINSEQ_1:def_7; ::_thesis: (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0
rng Fm c= rng (Ft ^ Fm) by FINSEQ_1:30;
then consider m9 being set such that
A114: m9 in dom F1 and
A115: F1 . m9 = Fm . m by A23, A108, FUNCT_1:def_3;
reconsider m9 = m9 as Element of NAT by A114;
m9 in Seg (len F1) by A114, FINSEQ_1:def_3;
then m9 in dom f1 by A77, FINSEQ_1:def_3;
then ( f1 . m9 = L1 . (F1 . m9) & f1 . m9 >= 0 ) by A79;
then A116: r * (L1 . (Fm . m)) >= 0 by A1, A115, XREAL_1:127;
rng Fm c= rng (Fm ^ Fb) by FINSEQ_1:29;
then consider m9 being set such that
A117: m9 in dom F2 and
A118: F2 . m9 = Fm . m by A91, A108, FUNCT_1:def_3;
reconsider m9 = m9 as Element of NAT by A117;
m9 in Seg (len F2) by A117, FINSEQ_1:def_3;
then m9 in dom f2 by A26, FINSEQ_1:def_3;
then ( f2 . m9 = L2 . (F2 . m9) & f2 . m9 >= 0 ) by A28;
then (1 - r) * (L2 . (Fm . m)) >= 0 by A11, A118, XREAL_1:127;
then (r * (L1 . (Fm . m))) + ((1 - r) * (L2 . (Fm . m))) >= 0 + 0 by A116, XREAL_1:7;
hence (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0 by A111; ::_thesis: verum
end;
end;
end;
hence ( (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (((Ft ^ Fm) ^ Fb) . n) & (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0 ) ; ::_thesis: verum
end;
suppose ex m being Nat st
( m in dom ((1 - r) * fb) & n = (len ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2)))) + m ) ; ::_thesis: ( (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (((Ft ^ Fm) ^ Fb) . n) & (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0 )
then consider m being Element of NAT such that
A119: m in dom ((1 - r) * fb) and
A120: n = (len ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2)))) + m ;
A121: m in dom fb by A119, VALUED_1:def_5;
then m in Seg (len Fb) by A61, FINSEQ_1:def_3;
then A122: m in dom Fb by FINSEQ_1:def_3;
then A123: Fb . m in rng Fb by FUNCT_1:3;
then reconsider Fbm = Fb . m as Element of V by A20;
A124: (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((1 - r) * fb) . m by A119, A120, FINSEQ_1:def_7
.= (1 - r) * (fb . m) by RVSUM_1:44
.= (1 - r) * (L2 . (Fb . m)) by A61, A121 ;
A125: len ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) = (len (r * ft)) + (len ((r * fm1) + ((1 - r) * fm2))) by FINSEQ_1:22
.= (len ft) + (len ((r * fm1) + ((1 - r) * fm2))) by RVSUM_1:117
.= (len ft) + (len (r * fm1)) by A69, INTEGRA5:2
.= (len Ft) + (len Fm) by A29, A37, RVSUM_1:117
.= len (Ft ^ Fm) by FINSEQ_1:22 ;
not Fb . m in Carrier L1 by A3, A16, A20, A123, XBOOLE_0:def_5;
then L1 . Fbm = 0 by RLVECT_2:19;
then r * (L1 . Fbm) = 0 ;
then (r * L1) . Fbm = 0 by RLVECT_2:def_11;
then (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) . Fbm) + (((1 - r) * L2) . Fbm) by A124, RLVECT_2:def_11
.= ((r * L1) + ((1 - r) * L2)) . (Fb . m) by RLVECT_2:def_10 ;
hence (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (((Ft ^ Fm) ^ Fb) . n) by A120, A122, A125, FINSEQ_1:def_7; ::_thesis: (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0
rng Fb c= rng (Fm ^ Fb) by FINSEQ_1:30;
then consider m9 being set such that
A126: m9 in dom F2 and
A127: F2 . m9 = Fb . m by A91, A123, FUNCT_1:def_3;
reconsider m9 = m9 as Element of NAT by A126;
m9 in Seg (len F2) by A126, FINSEQ_1:def_3;
then m9 in dom f2 by A26, FINSEQ_1:def_3;
then ( f2 . m9 = L2 . (F2 . m9) & f2 . m9 >= 0 ) by A28;
hence (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0 by A11, A124, A127, XREAL_1:127; ::_thesis: verum
end;
end;
end;
hence ( (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (((Ft ^ Fm) ^ Fb) . n) & (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0 ) ; ::_thesis: verum
end;
then A128: for n being Nat st n in dom (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) holds
( (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (((Ft ^ Fm) ^ Fb) . n) & (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0 ) ;
A129: rng Fb = (Carrier ((r * L1) + ((1 - r) * L2))) \ (Carrier L1) by A1, A16, A20, RLVECT_2:42;
then rng (Ft ^ Fm) misses rng Fb by A8, A23, XBOOLE_1:79;
then A130: (Ft ^ Fm) ^ Fb is one-to-one by A19, A25, FINSEQ_3:91;
A131: for x being set st x in dom (fm2 ^ fb) holds
(fm2 ^ fb) . x = L2 . ((Fm ^ Fb) . x)
proof
let x be set ; ::_thesis: ( x in dom (fm2 ^ fb) implies (fm2 ^ fb) . x = L2 . ((Fm ^ Fb) . x) )
assume A132: x in dom (fm2 ^ fb) ; ::_thesis: (fm2 ^ fb) . x = L2 . ((Fm ^ Fb) . x)
then reconsider n = x as Element of NAT ;
now__::_thesis:_(fm2_^_fb)_._x_=_L2_._((Fm_^_Fb)_._x)
percases ( n in dom fm2 or ex m being Nat st
( m in dom fb & n = (len fm2) + m ) ) by A132, FINSEQ_1:25;
supposeA133: n in dom fm2 ; ::_thesis: (fm2 ^ fb) . x = L2 . ((Fm ^ Fb) . x)
then n in Seg (len Fm) by A45, FINSEQ_1:def_3;
then A134: n in dom Fm by FINSEQ_1:def_3;
fm2 . n = L2 . (Fm . n) by A45, A133;
then (fm2 ^ fb) . n = L2 . (Fm . n) by A133, FINSEQ_1:def_7;
hence (fm2 ^ fb) . x = L2 . ((Fm ^ Fb) . x) by A134, FINSEQ_1:def_7; ::_thesis: verum
end;
suppose ex m being Nat st
( m in dom fb & n = (len fm2) + m ) ; ::_thesis: (fm2 ^ fb) . x = L2 . ((Fm ^ Fb) . x)
then consider m being Element of NAT such that
A135: m in dom fb and
A136: n = (len fm2) + m ;
m in Seg (len Fb) by A61, A135, FINSEQ_1:def_3;
then A137: m in dom Fb by FINSEQ_1:def_3;
(fm2 ^ fb) . n = fb . m by A135, A136, FINSEQ_1:def_7
.= L2 . (Fb . m) by A61, A135 ;
hence (fm2 ^ fb) . x = L2 . ((Fm ^ Fb) . x) by A45, A136, A137, FINSEQ_1:def_7; ::_thesis: verum
end;
end;
end;
hence (fm2 ^ fb) . x = L2 . ((Fm ^ Fb) . x) ; ::_thesis: verum
end;
for x being set holds
( x in dom (fm2 ^ fb) iff ( x in dom (Fm ^ Fb) & (Fm ^ Fb) . x in dom L2 ) )
proof
let x be set ; ::_thesis: ( x in dom (fm2 ^ fb) iff ( x in dom (Fm ^ Fb) & (Fm ^ Fb) . x in dom L2 ) )
A138: len (fm2 ^ fb) = (len fm2) + (len fb) by FINSEQ_1:22
.= len (Fm ^ Fb) by A45, A61, FINSEQ_1:22 ;
A139: dom (fm2 ^ fb) = Seg (len (fm2 ^ fb)) by FINSEQ_1:def_3
.= dom (Fm ^ Fb) by A138, FINSEQ_1:def_3 ;
( x in dom (fm2 ^ fb) implies (Fm ^ Fb) . x in dom L2 )
proof
assume x in dom (fm2 ^ fb) ; ::_thesis: (Fm ^ Fb) . x in dom L2
then (Fm ^ Fb) . x in rng (Fm ^ Fb) by A139, FUNCT_1:3;
then A140: (Fm ^ Fb) . x in (Carrier Lm) \/ (Carrier Lb) by A22, A20, FINSEQ_1:31;
dom L2 = the carrier of V by FUNCT_2:92;
hence (Fm ^ Fb) . x in dom L2 by A140; ::_thesis: verum
end;
hence ( x in dom (fm2 ^ fb) iff ( x in dom (Fm ^ Fb) & (Fm ^ Fb) . x in dom L2 ) ) by A139; ::_thesis: verum
end;
then A141: fm2 ^ fb = L2 * (Fm ^ Fb) by A131, FUNCT_1:10;
rng Fm misses rng Fb by A15, A16, A22, A20, XBOOLE_1:17, XBOOLE_1:85;
then Fm ^ Fb is one-to-one by A21, A19, FINSEQ_3:91;
then A142: F2,Fm ^ Fb are_fiberwise_equipotent by A4, A91, RFINSEQ:26;
then dom F2 = dom (Fm ^ Fb) by RFINSEQ:3;
then A143: Sum f2 = Sum (fm2 ^ fb) by A5, A142, A57, A90, A89, A141, CLASSES1:83, RFINSEQ:9;
A144: Sum (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) = (Sum ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2)))) + (Sum ((1 - r) * fb)) by RVSUM_1:75
.= ((Sum (r * ft)) + (Sum ((r * fm1) + ((1 - r) * fm2)))) + (Sum ((1 - r) * fb)) by RVSUM_1:75
.= ((r * (Sum ft)) + (Sum ((r * fm1) + ((1 - r) * fm2)))) + (Sum ((1 - r) * fb)) by RVSUM_1:87
.= ((r * (Sum ft)) + (Sum ((r * fm1) + ((1 - r) * fm2)))) + ((1 - r) * (Sum fb)) by RVSUM_1:87
.= ((r * (Sum ft)) + ((Sum (r * fm1)) + (Sum ((1 - r) * fm2)))) + ((1 - r) * (Sum fb)) by A69, INTEGRA5:2
.= ((r * (Sum ft)) + ((r * (Sum fm1)) + (Sum ((1 - r) * fm2)))) + ((1 - r) * (Sum fb)) by RVSUM_1:87
.= ((r * (Sum ft)) + ((r * (Sum fm1)) + ((1 - r) * (Sum fm2)))) + ((1 - r) * (Sum fb)) by RVSUM_1:87
.= (r * ((Sum ft) + (Sum fm1))) + ((1 - r) * ((Sum fm2) + (Sum fb)))
.= (r * (Sum (ft ^ fm1))) + ((1 - r) * ((Sum fm2) + (Sum fb))) by RVSUM_1:75
.= (r * 1) + ((1 - r) * 1) by A78, A27, A88, A143, RVSUM_1:75
.= 0 + 1 ;
rng ((Ft ^ Fm) ^ Fb) = (Carrier L1) \/ ((Carrier ((r * L1) + ((1 - r) * L2))) \ (Carrier L1)) by A8, A23, A129, FINSEQ_1:31
.= (Carrier L1) \/ (Carrier ((r * L1) + ((1 - r) * L2))) by XBOOLE_1:39
.= Carrier ((r * L1) + ((1 - r) * L2)) by A3, A14, XBOOLE_1:7, XBOOLE_1:12 ;
hence (r * L1) + ((1 - r) * L2) is Convex_Combination of V by A130, A144, A80, A128, CONVEX1:def_3; ::_thesis: verum
end;
theorem :: CONVEX2:9
for V being RealLinearSpace
for M being non empty Subset of V
for L1, L2 being Convex_Combination of M
for r being Real st 0 < r & r < 1 holds
(r * L1) + ((1 - r) * L2) is Convex_Combination of M
proof
let V be RealLinearSpace; ::_thesis: for M being non empty Subset of V
for L1, L2 being Convex_Combination of M
for r being Real st 0 < r & r < 1 holds
(r * L1) + ((1 - r) * L2) is Convex_Combination of M
let M be non empty Subset of V; ::_thesis: for L1, L2 being Convex_Combination of M
for r being Real st 0 < r & r < 1 holds
(r * L1) + ((1 - r) * L2) is Convex_Combination of M
let L1, L2 be Convex_Combination of M; ::_thesis: for r being Real st 0 < r & r < 1 holds
(r * L1) + ((1 - r) * L2) is Convex_Combination of M
let r be Real; ::_thesis: ( 0 < r & r < 1 implies (r * L1) + ((1 - r) * L2) is Convex_Combination of M )
A1: ( r * L1 is Linear_Combination of M & (1 - r) * L2 is Linear_Combination of M ) by RLVECT_2:44;
assume ( 0 < r & r < 1 ) ; ::_thesis: (r * L1) + ((1 - r) * L2) is Convex_Combination of M
hence (r * L1) + ((1 - r) * L2) is Convex_Combination of M by A1, Th8, RLVECT_2:38; ::_thesis: verum
end;
begin
theorem :: CONVEX2:10
for V being RealLinearSpace
for W1, W2 being Subspace of V holds Up (W1 + W2) = (Up W1) + (Up W2) by Lm3;
theorem :: CONVEX2:11
for V being RealLinearSpace
for W1, W2 being Subspace of V holds Up (W1 /\ W2) = (Up W1) /\ (Up W2) by Lm4;
theorem :: CONVEX2:12
for V being RealLinearSpace
for L1, L2 being Convex_Combination of V
for a, b being Real st a * b > 0 holds
Carrier ((a * L1) + (b * L2)) = (Carrier (a * L1)) \/ (Carrier (b * L2)) by Lm5;
theorem :: CONVEX2:13
for F, G being Function st F,G are_fiberwise_equipotent holds
for x1, x2 being set st x1 in dom F & x2 in dom F & x1 <> x2 holds
ex z1, z2 being set st
( z1 in dom G & z2 in dom G & z1 <> z2 & F . x1 = G . z1 & F . x2 = G . z2 ) by Lm6;
theorem :: CONVEX2:14
for V being RealLinearSpace
for L being Linear_Combination of V
for A being Subset of V st A c= Carrier L holds
ex L1 being Linear_Combination of V st Carrier L1 = A by Lm7;