let X be RealLinearSpace; :: thesis: for f being Function of the carrier of X,ExtREAL st ( for x being VECTOR of X holds f . x <> -infty ) holds
( f is convex iff for n being non empty Element of NAT
for p being FinSequence of REAL
for F being FinSequence of ExtREAL
for y, z being FinSequence of the carrier of X st len p = n & len F = n & len y = n & len z = n & Sum p = 1 & ( for i being Element of NAT st i in Seg n holds
( p . i >= 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds
f . (Sum z) <= Sum F )
let f be Function of the carrier of X,ExtREAL ; :: thesis: ( ( for x being VECTOR of X holds f . x <> -infty ) implies ( f is convex iff for n being non empty Element of NAT
for p being FinSequence of REAL
for F being FinSequence of ExtREAL
for y, z being FinSequence of the carrier of X st len p = n & len F = n & len y = n & len z = n & Sum p = 1 & ( for i being Element of NAT st i in Seg n holds
( p . i >= 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds
f . (Sum z) <= Sum F ) )
assume A1:
for x being VECTOR of X holds f . x <> -infty
; :: thesis: ( f is convex iff for n being non empty Element of NAT
for p being FinSequence of REAL
for F being FinSequence of ExtREAL
for y, z being FinSequence of the carrier of X st len p = n & len F = n & len y = n & len z = n & Sum p = 1 & ( for i being Element of NAT st i in Seg n holds
( p . i >= 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds
f . (Sum z) <= Sum F )
thus
( f is convex implies for n being non empty Element of NAT
for p being FinSequence of REAL
for F being FinSequence of ExtREAL
for y, z being FinSequence of the carrier of X st len p = n & len F = n & len y = n & len z = n & Sum p = 1 & ( for i being Element of NAT st i in Seg n holds
( p . i >= 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds
f . (Sum z) <= Sum F )
:: thesis: ( ( for n being non empty Element of NAT
for p being FinSequence of REAL
for F being FinSequence of ExtREAL
for y, z being FinSequence of the carrier of X st len p = n & len F = n & len y = n & len z = n & Sum p = 1 & ( for i being Element of NAT st i in Seg n holds
( p . i >= 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds
f . (Sum z) <= Sum F ) implies f is convex )proof
assume A2:
f is
convex
;
:: thesis: for n being non empty Element of NAT
for p being FinSequence of REAL
for F being FinSequence of ExtREAL
for y, z being FinSequence of the carrier of X st len p = n & len F = n & len y = n & len z = n & Sum p = 1 & ( for i being Element of NAT st i in Seg n holds
( p . i >= 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds
f . (Sum z) <= Sum F
let n be non
empty Element of
NAT ;
:: thesis: for p being FinSequence of REAL
for F being FinSequence of ExtREAL
for y, z being FinSequence of the carrier of X st len p = n & len F = n & len y = n & len z = n & Sum p = 1 & ( for i being Element of NAT st i in Seg n holds
( p . i >= 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds
f . (Sum z) <= Sum Flet p be
FinSequence of
REAL ;
:: thesis: for F being FinSequence of ExtREAL
for y, z being FinSequence of the carrier of X st len p = n & len F = n & len y = n & len z = n & Sum p = 1 & ( for i being Element of NAT st i in Seg n holds
( p . i >= 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds
f . (Sum z) <= Sum Flet F be
FinSequence of
ExtREAL ;
:: thesis: for y, z being FinSequence of the carrier of X st len p = n & len F = n & len y = n & len z = n & Sum p = 1 & ( for i being Element of NAT st i in Seg n holds
( p . i >= 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds
f . (Sum z) <= Sum Flet y,
z be
FinSequence of the
carrier of
X;
:: thesis: ( len p = n & len F = n & len y = n & len z = n & Sum p = 1 & ( for i being Element of NAT st i in Seg n holds
( p . i >= 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) implies f . (Sum z) <= Sum F )
assume that A3:
(
len p = n &
len F = n &
len y = n &
len z = n )
and A4:
Sum p = 1
and A5:
for
i being
Element of
NAT st
i in Seg n holds
(
p . i >= 0 &
z . i = (p . i) * (y /. i) &
F . i = (R_EAL (p . i)) * (f . (y /. i)) )
;
:: thesis: f . (Sum z) <= Sum F
consider s being
Permutation of
(dom p),
k being
Element of
NAT such that A6:
for
i being
Element of
NAT st
i in dom p holds
(
i in Seg k iff
p . (s . i) <> 0 )
by Lm18;
A8:
dom p = Seg n
by A3, FINSEQ_1:def 3;
then A9:
dom s = Seg n
by FUNCT_2:def 1;
reconsider s1 =
s as
FinSequence of
Seg n by A8, FINSEQ_2:28;
A10:
len s1 = n
by A9, FINSEQ_1:def 3;
A11:
p is
Function of
(Seg n),
REAL
by A8, FINSEQ_2:30;
then reconsider p' =
p * s1 as
FinSequence of
REAL by FINSEQ_2:36;
A12:
len p' = n
by A10, A11, FINSEQ_2:37;
A13:
dom z = Seg n
by A3, FINSEQ_1:def 3;
then A14:
z is
Function of
(Seg n),the
carrier of
X
by FINSEQ_2:30;
then reconsider z' =
z * s1 as
FinSequence of the
carrier of
X by FINSEQ_2:36;
A15:
len z' = n
by A10, A14, FINSEQ_2:37;
A16:
Sum z' = Sum z
by A8, A13, RLVECT_2:9;
A17:
dom y = Seg n
by A3, FINSEQ_1:def 3;
then A18:
y is
Function of
(Seg n),the
carrier of
X
by FINSEQ_2:30;
then reconsider y' =
y * s1 as
FinSequence of the
carrier of
X by FINSEQ_2:36;
A19:
len y' = n
by A10, A18, FINSEQ_2:37;
A20:
dom F = Seg n
by A3, FINSEQ_1:def 3;
then A21:
F is
Function of
(Seg n),
ExtREAL
by FINSEQ_2:30;
then reconsider F' =
F * s1 as
FinSequence of
ExtREAL by FINSEQ_2:36;
A22:
len F' = n
by A10, A21, FINSEQ_2:37;
for
i being
Element of
NAT st
i in Seg n holds
(
p . i >= 0 &
F . i = (R_EAL (p . i)) * (f . (y /. i)) )
by A5;
then A23:
not
-infty in rng F
by A1, A3, Lm17;
then A24:
Sum F' = Sum F
by A8, A20, Th8;
p' = (p' | k) ^ (p' /^ k)
by RFINSEQ:21;
then A25:
Sum p' = (Sum (p' | k)) + (Sum (p' /^ k))
by RVSUM_1:105;
A26:
for
i being
Element of
NAT st 1
<= i &
i <= n - k holds
(
i + k in Seg n &
p . (s . (i + k)) = 0 )
A32:
Sum (p' /^ k) = 0
proof
per cases
( k >= n or k < n )
;
suppose A33:
k < n
;
:: thesis: Sum (p' /^ k) = 0
for
w being
set st
w in rng (p' /^ k) holds
w in {0 }
proof
let w be
set ;
:: thesis: ( w in rng (p' /^ k) implies w in {0 } )
assume
w in rng (p' /^ k)
;
:: thesis: w in {0 }
then consider i being
set such that A34:
i in dom (p' /^ k)
and A35:
(p' /^ k) . i = w
by FUNCT_1:def 5;
reconsider i =
i as
Element of
NAT by A34;
reconsider k1 =
n - k as
Element of
NAT by A33, INT_1:18;
len (p' /^ k) = k1
by A12, A33, RFINSEQ:def 2;
then
i in Seg k1
by A34, FINSEQ_1:def 3;
then
( 1
<= i &
i <= n - k )
by FINSEQ_1:3;
then A36:
(
i + k in Seg n &
p . (s . (i + k)) = 0 )
by A26;
then
i + k in dom p'
by A12, FINSEQ_1:def 3;
then
p' . (i + k) = 0
by A36, FUNCT_1:22;
then
w = 0
by A12, A33, A34, A35, RFINSEQ:def 2;
hence
w in {0 }
by TARSKI:def 1;
:: thesis: verum
end; then
rng (p' /^ k) c= {0 }
by TARSKI:def 3;
hence
Sum (p' /^ k) = 0
by Lm13;
:: thesis: verum
end;
p',
p are_fiberwise_equipotent
by RFINSEQ:17;
then A37:
Sum (p' | k) = 1
by A4, A25, A32, RFINSEQ:22;
z' = (z' | k) ^ (z' /^ k)
by RFINSEQ:21;
then A38:
Sum z' = (Sum (z' | k)) + (Sum (z' /^ k))
by RLVECT_1:58;
Sum (z' /^ k) = 0. X
proof
per cases
( k >= n or k < n )
;
suppose A39:
k < n
;
:: thesis: Sum (z' /^ k) = 0. X
for
w being
set st
w in rng (z' /^ k) holds
w in {(0. X)}
proof
let w be
set ;
:: thesis: ( w in rng (z' /^ k) implies w in {(0. X)} )
assume
w in rng (z' /^ k)
;
:: thesis: w in {(0. X)}
then consider i being
set such that A40:
i in dom (z' /^ k)
and A41:
(z' /^ k) . i = w
by FUNCT_1:def 5;
reconsider i =
i as
Element of
NAT by A40;
reconsider k1 =
n - k as
Element of
NAT by A39, INT_1:18;
len (z' /^ k) = k1
by A15, A39, RFINSEQ:def 2;
then
i in Seg k1
by A40, FINSEQ_1:def 3;
then
( 1
<= i &
i <= n - k )
by FINSEQ_1:3;
then A42:
(
i + k in Seg n &
p . (s . (i + k)) = 0 )
by A26;
then
s . (i + k) in Seg n
by A8, FUNCT_2:7;
then
z . (s . (i + k)) = (p . (s . (i + k))) * (y /. (s . (i + k)))
by A5;
then A43:
z . (s . (i + k)) = 0. X
by A42, RLVECT_1:23;
i + k in dom z'
by A15, A42, FINSEQ_1:def 3;
then
z' . (i + k) = 0. X
by A43, FUNCT_1:22;
then
w = 0. X
by A15, A39, A40, A41, RFINSEQ:def 2;
hence
w in {(0. X)}
by TARSKI:def 1;
:: thesis: verum
end; then
rng (z' /^ k) c= {(0. X)}
by TARSKI:def 3;
hence
Sum (z' /^ k) = 0. X
by Lm14;
:: thesis: verum
end;
then A44:
Sum (z' | k) = Sum z
by A16, A38, RLVECT_1:def 7;
A45:
F' = (F' | k) ^ (F' /^ k)
by RFINSEQ:21;
not
-infty in rng F'
by A23, FUNCT_1:25;
then
not
-infty in (rng (F' | k)) \/ (rng (F' /^ k))
by A45, FINSEQ_1:44;
then
( not
-infty in rng (F' | k) & not
-infty in rng (F' /^ k) )
by XBOOLE_0:def 3;
then A46:
Sum F' = (Sum (F' | k)) + (Sum (F' /^ k))
by A45, Th7;
Sum (F' /^ k) = 0.
proof
per cases
( k >= n or k < n )
;
suppose A47:
k < n
;
:: thesis: Sum (F' /^ k) = 0.
for
w being
set st
w in rng (F' /^ k) holds
w in {0. }
proof
let w be
set ;
:: thesis: ( w in rng (F' /^ k) implies w in {0. } )
assume
w in rng (F' /^ k)
;
:: thesis: w in {0. }
then consider i being
set such that A48:
i in dom (F' /^ k)
and A49:
(F' /^ k) . i = w
by FUNCT_1:def 5;
reconsider i =
i as
Element of
NAT by A48;
reconsider k1 =
n - k as
Element of
NAT by A47, INT_1:18;
len (F' /^ k) = k1
by A22, A47, RFINSEQ:def 2;
then
i in Seg k1
by A48, FINSEQ_1:def 3;
then
( 1
<= i &
i <= n - k )
by FINSEQ_1:3;
then A50:
(
i + k in Seg n &
p . (s . (i + k)) = 0 )
by A26;
then
s . (i + k) in Seg n
by A8, FUNCT_2:7;
then
F . (s . (i + k)) = (R_EAL 0 ) * (f . (y /. (s . (i + k))))
by A5, A50;
then
F . (s . (i + k)) = 0. * (f . (y /. (s . (i + k))))
;
then A51:
F . (s . (i + k)) = 0.
;
i + k in dom F'
by A22, A50, FINSEQ_1:def 3;
then
F' . (i + k) = 0.
by A51, FUNCT_1:22;
then
w = 0.
by A22, A47, A48, A49, RFINSEQ:def 2;
hence
w in {0. }
by TARSKI:def 1;
:: thesis: verum
end; then
rng (F' /^ k) c= {0. }
by TARSKI:def 3;
hence
Sum (F' /^ k) = 0.
by Lm12;
:: thesis: verum
end;
then A52:
Sum (F' | k) = Sum F
by A24, A46, XXREAL_3:4;
set k' =
min k,
n;
reconsider k' =
min k,
n as
Element of
NAT ;
A53:
(
p' | k = p' | (Seg k) &
y' | k = y' | (Seg k) &
z' | k = z' | (Seg k) &
F' | k = F' | (Seg k) )
by FINSEQ_1:def 15;
then A54:
(
len (p' | k) = k' &
len (y' | k) = k' &
len (z' | k) = k' &
len (F' | k) = k' )
by A12, A15, A19, A22, FINSEQ_2:24;
p' | k <> {}
by A37, RVSUM_1:102;
then reconsider k' =
k' as non
empty Element of
NAT by A54;
for
i being
Element of
NAT st
i in Seg k' holds
(
(p' | k) . i > 0 &
(z' | k) . i = ((p' | k) . i) * ((y' | k) /. i) &
(F' | k) . i = (R_EAL ((p' | k) . i)) * (f . ((y' | k) /. i)) )
proof
let i be
Element of
NAT ;
:: thesis: ( i in Seg k' implies ( (p' | k) . i > 0 & (z' | k) . i = ((p' | k) . i) * ((y' | k) /. i) & (F' | k) . i = (R_EAL ((p' | k) . i)) * (f . ((y' | k) /. i)) ) )
assume A55:
i in Seg k'
;
:: thesis: ( (p' | k) . i > 0 & (z' | k) . i = ((p' | k) . i) * ((y' | k) /. i) & (F' | k) . i = (R_EAL ((p' | k) . i)) * (f . ((y' | k) /. i)) )
then A56:
(
i in dom (p' | k) &
i in dom (y' | k) &
i in dom (z' | k) &
i in dom (F' | k) )
by A54, FINSEQ_1:def 3;
(
dom (p' | k) = (dom p') /\ (Seg k) &
dom (y' | k) = (dom y') /\ (Seg k) &
dom (z' | k) = (dom z') /\ (Seg k) &
dom (F' | k) = (dom F') /\ (Seg k) )
by A53, RELAT_1:90;
then A57:
(
i in dom p' &
i in dom y' &
i in dom z' &
i in dom F' )
by A56, XBOOLE_0:def 4;
then A58:
(
p' /. i = p' . i &
y' /. i = y' . i &
z' /. i = z' . i &
F' /. i = F' . i )
by PARTFUN1:def 8;
A59:
(
(p' | k) /. i = p' /. i &
(y' | k) /. i = y' /. i &
(z' | k) /. i = z' /. i &
(F' | k) /. i = F' /. i )
by A56, FINSEQ_4:85;
A60:
(
p' . i = p . (s . i) &
y' . i = y . (s . i) &
z' . i = z . (s . i) &
F' . i = F . (s . i) )
by A57, FUNCT_1:22;
A61:
i in Seg n
by A12, A57, FINSEQ_1:def 3;
then A62:
s . i in Seg n
by A8, FUNCT_2:7;
A63:
(
(p' | k) . i = p . (s . i) &
(y' | k) /. i = y /. (s . i) &
(z' | k) . i = z . (s . i) &
(F' | k) . i = F . (s . i) )
by A8, A17, A56, A58, A59, A60, A61, FUNCT_2:7, PARTFUN1:def 8;
k' <= k
by XXREAL_0:17;
then
Seg k' c= Seg k
by FINSEQ_1:7;
then
p . (s . i) <> 0
by A6, A8, A55, A61;
hence
(
(p' | k) . i > 0 &
(z' | k) . i = ((p' | k) . i) * ((y' | k) /. i) &
(F' | k) . i = (R_EAL ((p' | k) . i)) * (f . ((y' | k) /. i)) )
by A5, A62, A63;
:: thesis: verum
end;
hence
f . (Sum z) <= Sum F
by A1, A2, A37, A44, A52, A54, Th13;
:: thesis: verum
end;
thus
( ( for n being non empty Element of NAT
for p being FinSequence of REAL
for F being FinSequence of ExtREAL
for y, z being FinSequence of the carrier of X st len p = n & len F = n & len y = n & len z = n & Sum p = 1 & ( for i being Element of NAT st i in Seg n holds
( p . i >= 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds
f . (Sum z) <= Sum F ) implies f is convex )
:: thesis: verum