let a be non empty positive at_most_one FinSequence of REAL ; :: thesis: for f being non empty FinSequence of NAT
for k being Nat st f = OnlinePacking (a,(NextFit a)) & k = card (rng f) holds
k div 2 < Sum a
let f be non empty FinSequence of NAT ; :: thesis: for k being Nat st f = OnlinePacking (a,(NextFit a)) & k = card (rng f) holds
k div 2 < Sum a
let k be Nat; :: thesis: ( f = OnlinePacking (a,(NextFit a)) & k = card (rng f) implies k div 2 < Sum a )
assume that
HL00: f = OnlinePacking (a,(NextFit a)) and
BK00: k = card (rng f) ; :: thesis: k div 2 < Sum a
consider k0 being Nat such that
B00: rng f = Seg k0 by HL00, NF910;
BN00: rng f = Seg k by FINSEQ_1:57, BK00, B00;
L00: dom f = dom a by HL00, NF540;
per cases ( k = 1 or 2 <= k ) by BK00, NAT_1:23;
suppose L55: k = 1 ; :: thesis: k div 2 < Sum a
L57: for n being Nat st n in dom a holds
0 <= a . n by RVSUM_3:def 1;
L575: len a >= 1 by FINSEQ_1:20;
a is positive ;
then 0 < a . 1 by L575, FINSEQ_3:25;
then 0 < Sum a by L57, L575, FINSEQ_3:25, RVSUM_1:85;
hence k div 2 < Sum a by L55, NAT_D:27; :: thesis: verum
end;
suppose L60: 2 <= k ; :: thesis: k div 2 < Sum a
set kd2 = k div 2;
reconsider kd2 = k div 2 as Element of NAT by INT_1:55, INT_1:3;
2 div 2 <= k div 2 by L60, NAT_2:24;
then L80: 1 <= kd2 by NAT_2:3;
deffunc H1( Nat) -> set = (SumBin (a,f,{((2 * $1) - 1)})) + (SumBin (a,f,{(2 * $1)}));
ex p being FinSequence st
( len p = kd2 & ( for i being Nat st i in dom p holds
p . i = H1(i) ) ) from FINSEQ_1:sch 2();
then consider SBP being FinSequence such that
L100: len SBP = kd2 and
L101: for i being Nat st i in dom SBP holds
SBP . i = (SumBin (a,f,{((2 * i) - 1)})) + (SumBin (a,f,{(2 * i)})) ;
deffunc H2( Nat) -> Real = SumBin (a,f,{$1});
ex p being FinSequence st
( len p = 2 * kd2 & ( for j being Nat st j in dom p holds
p . j = H2(j) ) ) from FINSEQ_1:sch 2();
then consider SB being FinSequence such that
L150: len SB = 2 * kd2 and
L151: for j being Nat st j in dom SB holds
SB . j = SumBin (a,f,{j}) ;
for i being Nat st i in dom SBP holds
SBP . i in REAL
proof
let i be Nat; :: thesis: ( i in dom SBP implies SBP . i in REAL )
assume i in dom SBP ; :: thesis: SBP . i in REAL
then SBP . i = (SumBin (a,f,{((2 * i) - 1)})) + (SumBin (a,f,{(2 * i)})) by L101;
hence SBP . i in REAL by XREAL_0:def 1; :: thesis: verum
end;
then LSBP55: SBP is FinSequence of REAL by NF315;
SBP is kd2 -element by L100;
then reconsider SBP = SBP as kd2 -element real-valued FinSequence by LSBP55;
for j being Nat st j in dom SB holds
SB . j in REAL
proof
let j be Nat; :: thesis: ( j in dom SB implies SB . j in REAL )
assume j in dom SB ; :: thesis: SB . j in REAL
then SB . j = SumBin (a,f,{j}) by L151;
hence SB . j in REAL by XREAL_0:def 1; :: thesis: verum
end;
then LSB55: SB is FinSequence of REAL by NF315;
SB is 2 * kd2 -element by L150;
then reconsider SB = SB as 2 * kd2 -element real-valued FinSequence by LSB55;
set R2 = kd2 |-> 1;
reconsider R2 = kd2 |-> 1 as kd2 -element real-valued FinSequence ;
L170: Sum R2 = kd2 * 1 by RVSUM_1:80;
L175: for i being Nat st i in Seg kd2 holds
R2 . i < SBP . i
proof
let i be Nat; :: thesis: ( i in Seg kd2 implies R2 . i < SBP . i )
assume LR271: i in Seg kd2 ; :: thesis: R2 . i < SBP . i
Seg kd2 = dom SBP by L100, FINSEQ_1:def 3;
then LR278: SBP . i = (SumBin (a,f,{((2 * i) - 1)})) + (SumBin (a,f,{(2 * i)})) by LR271, L101;
LR279: R2 . i = 1 by LR271, FINSEQ_2:57;
( 1 <= i & i <= k div 2 ) by LR271, FINSEQ_1:1;
hence R2 . i < SBP . i by HL00, BN00, NF950, LR278, LR279; :: thesis: verum
end;
L180: for i being Nat st i in Seg kd2 holds
R2 . i <= SBP . i by L175;
ex i being Nat st
( i in Seg kd2 & R2 . i < SBP . i )
proof
reconsider i0 = 1 as Nat ;
take i0 ; :: thesis: ( i0 in Seg kd2 & R2 . i0 < SBP . i0 )
i0 in Seg kd2 by L80;
hence ( i0 in Seg kd2 & R2 . i0 < SBP . i0 ) by L175; :: thesis: verum
end;
then L200: kd2 < Sum SBP by L180, RVSUM_1:83, L170;
defpred S1[ Nat] means for SBPi, SBi being real-valued FinSequence st SBPi = SBP | (Seg $1) & SBi = SB | (Seg (2 * $1)) holds
Sum SBPi = Sum SBi;
for SBP1, SB1 being real-valued FinSequence st SBP1 = SBP | (Seg 1) & SB1 = SB | (Seg (2 * 1)) holds
Sum SBP1 = Sum SB1
proof
let sbp1, sb1 be real-valued FinSequence; :: thesis: ( sbp1 = SBP | (Seg 1) & sb1 = SB | (Seg (2 * 1)) implies Sum sbp1 = Sum sb1 )
assume that
B00: sbp1 = SBP | (Seg 1) and
B01: sb1 = SB | (Seg (2 * 1)) ; :: thesis: Sum sbp1 = Sum sb1
Seg kd2 = dom SBP by FINSEQ_1:def 3, L100;
then B140: 1 in dom SBP by L80;
1 in Seg 1 ;
then B160: sbp1 . 1 = SBP . 1 by B00, FUNCT_1:49
.= (SumBin (a,f,{((2 * 1) - 1)})) + (SumBin (a,f,{(2 * 1)})) by B140, L101
.= (SumBin (a,f,{1})) + (SumBin (a,f,{2})) ;
dom sbp1 = Seg 1 by L100, L80, B00, FINSEQ_1:17;
then B180: sbp1 = <*((SumBin (a,f,{1})) + (SumBin (a,f,{2})))*> by B160, FINSEQ_1:def 8;
B220: Seg (2 * kd2) = dom SB by FINSEQ_1:def 3, L150;
B229: 1 * 2 <= kd2 * 2 by XREAL_1:64, L80;
then 2 - 1 <= (2 * kd2) - 0 by XREAL_1:13;
then B240: 1 in dom SB by B220;
B241: 2 in dom SB by B229, B220;
B250: 1 in Seg 2 ;
B251: 2 in Seg 2 ;
B260: sb1 . 1 = SB . 1 by B01, B250, FUNCT_1:49
.= SumBin (a,f,{1}) by B240, L151 ;
B261: sb1 . 2 = SB . 2 by B01, B251, FUNCT_1:49
.= SumBin (a,f,{2}) by B241, L151 ;
B263: 1 * 2 <= kd2 * 2 by XREAL_1:64, L80;
len sb1 = min (2,(len SB)) by B01, FINSEQ_2:21
.= 2 by B263, L150, XXREAL_0:def 9 ;
then B280: sb1 = <*(SumBin (a,f,{1})),(SumBin (a,f,{2}))*> by B260, B261, FINSEQ_1:44;
Sum sbp1 = (SumBin (a,f,{1})) + (SumBin (a,f,{2})) by B180, RVSUM_1:73
.= Sum sb1 by B280, RVSUM_1:77 ;
hence Sum sbp1 = Sum sb1 ; :: thesis: verum
end;
then L230: S1[1] ;
L260: for i being Element of NAT st 1 <= i & i < kd2 & S1[i] holds
S1[i + 1]
proof
let i0 be Element of NAT ; :: thesis: ( 1 <= i0 & i0 < kd2 & S1[i0] implies S1[i0 + 1] )
assume that
1 <= i0 and
A262: i0 < kd2 and
A263: S1[i0] ; :: thesis: S1[i0 + 1]
reconsider sbpi0 = SBP | (Seg i0) as real-valued FinSequence by FINSEQ_1:15;
reconsider sbi0 = SB | (Seg (2 * i0)) as real-valued FinSequence by FINSEQ_1:15;
reconsider sbpi0p = SBP | (Seg (i0 + 1)) as real-valued FinSequence by FINSEQ_1:15;
reconsider sbi0p = SB | (Seg (2 * (i0 + 1))) as real-valued FinSequence by FINSEQ_1:15;
reconsider sbi0h = SB | (Seg ((2 * i0) + 1)) as real-valued FinSequence by FINSEQ_1:15;
A270: 1 <= i0 + 1 by NAT_1:12;
A271: i0 + 1 <= kd2 by A262, INT_1:7;
i0 + 1 in Seg kd2 by A270, A271;
then A272: i0 + 1 in dom SBP by L100, FINSEQ_1:def 3;
then A274: SBP . (i0 + 1) = (SumBin (a,f,{((2 * (i0 + 1)) - 1)})) + (SumBin (a,f,{(2 * (i0 + 1))})) by L101;
A280: Sum sbpi0p = Sum (sbpi0 ^ <*(SBP . (i0 + 1))*>) by A272, FINSEQ_5:10
.= (Sum sbpi0) + (SBP . (i0 + 1)) by RVSUM_1:74
.= ((Sum sbpi0) + (SumBin (a,f,{((2 * i0) + 1)}))) + (SumBin (a,f,{((2 * i0) + 2)})) by A274 ;
A300: 1 <= (2 * i0) + 2 by NAT_1:12;
A304: 2 * (i0 + 1) <= 2 * kd2 by A271, XREAL_1:64;
2 * (i0 + 1) in Seg (2 * kd2) by A300, A304;
then A320: (2 * i0) + 2 in dom SB by L150, FINSEQ_1:def 3;
A330: 1 <= (2 * i0) + 1 by NAT_1:12;
((2 * i0) + 2) - 1 <= (2 * kd2) - 0 by A304, XREAL_1:13;
then (2 * i0) + 1 in Seg (2 * kd2) by A330;
then A340: (2 * i0) + 1 in dom SB by L150, FINSEQ_1:def 3;
A370: SB | (Seg (2 * (i0 + 1))) = SB | (Seg (((2 * i0) + 1) + 1))
.= sbi0h ^ <*(SB . ((2 * i0) + 2))*> by A320, FINSEQ_5:10 ;
A380: sbi0h = sbi0 ^ <*(SB . ((2 * i0) + 1))*> by A340, FINSEQ_5:10;
A390: Sum sbi0h = (Sum sbi0) + (SB . ((2 * i0) + 1)) by A380, RVSUM_1:74
.= (Sum sbi0) + (SumBin (a,f,{((2 * i0) + 1)})) by A340, L151 ;
Sum sbi0p = (Sum sbi0h) + (SB . ((2 * i0) + 2)) by A370, RVSUM_1:74
.= ((Sum sbi0) + (SumBin (a,f,{((2 * i0) + 1)}))) + (SumBin (a,f,{((2 * i0) + 2)})) by A320, L151, A390 ;
hence for SBPi, SBi being real-valued FinSequence st SBPi = SBP | (Seg (i0 + 1)) & SBi = SB | (Seg (2 * (i0 + 1))) holds
Sum SBPi = Sum SBi by A280, A263; :: thesis: verum
end;
L289: for i being Element of NAT st 1 <= i & i <= kd2 holds
S1[i] from INT_1:sch 7(L230, L260);
L298: SBP = SBP | (dom SBP)
.= SBP | (Seg kd2) by L100, FINSEQ_1:def 3 ;
SB = SB | (dom SB)
.= SB | (Seg (2 * kd2)) by L150, FINSEQ_1:def 3 ;
then L300: Sum SBP = Sum SB by L80, L298, L289;
deffunc H3( Nat) -> Real = SumBin (a,f,{$1});
ex p being FinSequence st
( len p = k & ( for j being Nat st j in dom p holds
p . j = H3(j) ) ) from FINSEQ_1:sch 2();
then consider R1 being FinSequence such that
LL40: len R1 = k and
LL41: for j being Nat st j in dom R1 holds
R1 . j = SumBin (a,f,{j}) ;
for j being Nat st j in dom R1 holds
R1 . j in REAL
proof
let j be Nat; :: thesis: ( j in dom R1 implies R1 . j in REAL )
assume j in dom R1 ; :: thesis: R1 . j in REAL
then R1 . j = SumBin (a,f,{j}) by LL41;
hence R1 . j in REAL by XREAL_0:def 1; :: thesis: verum
end;
then LL55: R1 is FinSequence of REAL by NF315;
R1 is k -element by LL40;
then reconsider R1 = R1 as k -element real-valued FinSequence by LL55;
L500: Sum SB <= Sum R1
proof
per cases ( k is even or k is odd ) ;
suppose L530: k is even ; :: thesis: Sum SB <= Sum R1
L539: k div 2 = k / 2 by L530, NAT_6:4;
SB = R1
proof
L5505: dom R1 = Seg (2 * kd2) by LL40, L539, FINSEQ_1:def 3;
L5510: dom SB = Seg (2 * kd2) by L150, FINSEQ_1:def 3;
for k0 being Nat st k0 in dom SB holds
SB . k0 = R1 . k0
proof
let k0 be Nat; :: thesis: ( k0 in dom SB implies SB . k0 = R1 . k0 )
assume L55310: k0 in dom SB ; :: thesis: SB . k0 = R1 . k0
SB . k0 = SumBin (a,f,{k0}) by L55310, L151;
hence SB . k0 = R1 . k0 by L55310, L5505, L5510, LL41; :: thesis: verum
end;
hence SB = R1 by L5505, L5510, FINSEQ_1:13; :: thesis: verum
end;
hence Sum SB <= Sum R1 ; :: thesis: verum
end;
suppose L560: k is odd ; :: thesis: Sum SB <= Sum R1
L569: k div 2 = (k - 1) / 2 by L560, NAT_6:5;
reconsider r12kd2 = R1 | (Seg (2 * kd2)) as real-valued FinSequence by FINSEQ_1:15;
L580: SB = r12kd2
proof
((2 * kd2) + 1) - 1 <= k - 0 by L569, XREAL_1:13;
then L5805: dom r12kd2 = Seg (2 * kd2) by LL40, FINSEQ_1:17;
L5810: dom SB = Seg (2 * kd2) by L150, FINSEQ_1:def 3;
for k0 being Nat st k0 in dom SB holds
SB . k0 = r12kd2 . k0
proof
let k0 be Nat; :: thesis: ( k0 in dom SB implies SB . k0 = r12kd2 . k0 )
assume L58310: k0 in dom SB ; :: thesis: SB . k0 = r12kd2 . k0
L58329: dom r12kd2 c= dom R1 by RELAT_1:60;
k0 in Seg (2 * kd2) by L58310, L150, FINSEQ_1:def 3;
then r12kd2 . k0 = R1 . k0 by FUNCT_1:49
.= SumBin (a,f,{k0}) by L58329, L58310, L5805, L5810, LL41 ;
hence SB . k0 = r12kd2 . k0 by L58310, L151; :: thesis: verum
end;
hence SB = r12kd2 by L5805, L5810, FINSEQ_1:13; :: thesis: verum
end;
L584: Seg ((2 * kd2) + 1) = dom R1 by LL40, FINSEQ_1:def 3, L569;
(2 * 0) + 1 <= (2 * kd2) + 1 by XREAL_1:7;
then L587: (2 * kd2) + 1 in dom R1 by L584;
R1 = R1 | (dom R1)
.= R1 | (Seg ((2 * kd2) + 1)) by LL40, FINSEQ_1:def 3, L569
.= r12kd2 ^ <*(R1 . ((2 * kd2) + 1))*> by L587, FINSEQ_5:10
.= SB ^ <*(SumBin (a,f,{((2 * kd2) + 1)}))*> by L587, LL41, L580 ;
then Sum R1 = (Sum SB) + (SumBin (a,f,{((2 * kd2) + 1)})) by RVSUM_1:74;
then SumBin (a,f,{((2 * kd2) + 1)}) = (Sum R1) - (Sum SB) ;
then Sum SB <= (Sum R1) - 0 by NF280, XREAL_1:11;
hence Sum SB <= Sum R1 ; :: thesis: verum
end;
end;
end;
Sum R1 = SumBin (a,f,(rng f)) by L00, FINSEQ_1:57, BK00, B00, LL40, LL41, NF310
.= Sum a by L00, NF260 ;
hence k div 2 < Sum a by L200, L300, L500, XXREAL_0:2; :: thesis: verum
end;
end;