:: Sorting Operators for Finite Sequences
:: by Yatsuka Nakamura
::
:: Received October 17, 2003
:: Copyright (c) 2003-2021 Association of Mizar Users

definition
let f be FinSequence of REAL ;
func max_p f -> Nat means :Def1: :: RFINSEQ2:def 1
( ( len f = 0 implies it = 0 ) & ( len f > 0 implies ( it in dom f & ( for i being Nat
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . it holds
r1 <= r2 ) & ( for j being Nat st j in dom f & f . j = f . it holds
it <= j ) ) ) );
existence
ex b1 being Nat st
( ( len f = 0 implies b1 = 0 ) & ( len f > 0 implies ( b1 in dom f & ( for i being Nat
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b1 holds
r1 <= r2 ) & ( for j being Nat st j in dom f & f . j = f . b1 holds
b1 <= j ) ) ) )
proof end;
uniqueness
for b1, b2 being Nat st ( len f = 0 implies b1 = 0 ) & ( len f > 0 implies ( b1 in dom f & ( for i being Nat
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b1 holds
r1 <= r2 ) & ( for j being Nat st j in dom f & f . j = f . b1 holds
b1 <= j ) ) ) & ( len f = 0 implies b2 = 0 ) & ( len f > 0 implies ( b2 in dom f & ( for i being Nat
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b2 holds
r1 <= r2 ) & ( for j being Nat st j in dom f & f . j = f . b2 holds
b2 <= j ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines max_p RFINSEQ2:def 1 :
for f being FinSequence of REAL
for b2 being Nat holds
( b2 = max_p f iff ( ( len f = 0 implies b2 = 0 ) & ( len f > 0 implies ( b2 in dom f & ( for i being Nat
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b2 holds
r1 <= r2 ) & ( for j being Nat st j in dom f & f . j = f . b2 holds
b2 <= j ) ) ) ) );

definition
let f be FinSequence of REAL ;
func min_p f -> Nat means :Def2: :: RFINSEQ2:def 2
( ( len f = 0 implies it = 0 ) & ( len f > 0 implies ( it in dom f & ( for i being Nat
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . it holds
r1 >= r2 ) & ( for j being Nat st j in dom f & f . j = f . it holds
it <= j ) ) ) );
existence
ex b1 being Nat st
( ( len f = 0 implies b1 = 0 ) & ( len f > 0 implies ( b1 in dom f & ( for i being Nat
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b1 holds
r1 >= r2 ) & ( for j being Nat st j in dom f & f . j = f . b1 holds
b1 <= j ) ) ) )
proof end;
uniqueness
for b1, b2 being Nat st ( len f = 0 implies b1 = 0 ) & ( len f > 0 implies ( b1 in dom f & ( for i being Nat
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b1 holds
r1 >= r2 ) & ( for j being Nat st j in dom f & f . j = f . b1 holds
b1 <= j ) ) ) & ( len f = 0 implies b2 = 0 ) & ( len f > 0 implies ( b2 in dom f & ( for i being Nat
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b2 holds
r1 >= r2 ) & ( for j being Nat st j in dom f & f . j = f . b2 holds
b2 <= j ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines min_p RFINSEQ2:def 2 :
for f being FinSequence of REAL
for b2 being Nat holds
( b2 = min_p f iff ( ( len f = 0 implies b2 = 0 ) & ( len f > 0 implies ( b2 in dom f & ( for i being Nat
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b2 holds
r1 >= r2 ) & ( for j being Nat st j in dom f & f . j = f . b2 holds
b2 <= j ) ) ) ) );

definition
let f be FinSequence of REAL ;
func max f -> Real equals :: RFINSEQ2:def 3
f . ();
correctness
coherence
f . () is Real
;
;
func min f -> Real equals :: RFINSEQ2:def 4
f . ();
correctness
coherence
f . () is Real
;
;
end;

:: deftheorem defines max RFINSEQ2:def 3 :
for f being FinSequence of REAL holds max f = f . ();

:: deftheorem defines min RFINSEQ2:def 4 :
for f being FinSequence of REAL holds min f = f . ();

theorem Th1: :: RFINSEQ2:1
for f being FinSequence of REAL
for i being Nat st 1 <= i & i <= len f holds
( f . i <= f . () & f . i <= max f )
proof end;

theorem Th2: :: RFINSEQ2:2
for f being FinSequence of REAL
for i being Nat st 1 <= i & i <= len f holds
( f . i >= f . () & f . i >= min f )
proof end;

theorem :: RFINSEQ2:3
for f being FinSequence of REAL
for r being Real st f = <*r*> holds
( max_p f = 1 & max f = r )
proof end;

theorem :: RFINSEQ2:4
for f being FinSequence of REAL
for r being Real st f = <*r*> holds
( min_p f = 1 & min f = r )
proof end;

theorem :: RFINSEQ2:5
for f being FinSequence of REAL
for r1, r2 being Real st f = <*r1,r2*> holds
( max f = max (r1,r2) & max_p f = IFEQ (r1,(max (r1,r2)),1,2) )
proof end;

theorem :: RFINSEQ2:6
for f being FinSequence of REAL
for r1, r2 being Real st f = <*r1,r2*> holds
( min f = min (r1,r2) & min_p f = IFEQ (r1,(min (r1,r2)),1,2) )
proof end;

theorem :: RFINSEQ2:7
for f1, f2 being FinSequence of REAL st len f1 = len f2 & len f1 > 0 holds
max (f1 + f2) <= (max f1) + (max f2)
proof end;

theorem :: RFINSEQ2:8
for f1, f2 being FinSequence of REAL st len f1 = len f2 & len f1 > 0 holds
min (f1 + f2) >= (min f1) + (min f2)
proof end;

theorem :: RFINSEQ2:9
for f being FinSequence of REAL
for a being Real st len f > 0 & a > 0 holds
( max (a * f) = a * (max f) & max_p (a * f) = max_p f )
proof end;

theorem :: RFINSEQ2:10
for f being FinSequence of REAL
for a being Real st len f > 0 & a > 0 holds
( min (a * f) = a * (min f) & min_p (a * f) = min_p f )
proof end;

theorem :: RFINSEQ2:11
for f being FinSequence of REAL st len f > 0 holds
( max (- f) = - (min f) & max_p (- f) = min_p f )
proof end;

theorem :: RFINSEQ2:12
for f being FinSequence of REAL st len f > 0 holds
( min (- f) = - (max f) & min_p (- f) = max_p f )
proof end;

theorem :: RFINSEQ2:13
for f being FinSequence of REAL
for n being Nat st n < len f holds
( max (f /^ n) <= max f & min (f /^ n) >= min f )
proof end;

Lm1: for f, g being FinSequence of REAL st f,g are_fiberwise_equipotent holds
max f <= max g

proof end;

theorem Th14: :: RFINSEQ2:14
for f, g being FinSequence of REAL st f,g are_fiberwise_equipotent holds
max f = max g
proof end;

Lm2: for f, g being FinSequence of REAL st f,g are_fiberwise_equipotent holds
min f >= min g

proof end;

theorem Th15: :: RFINSEQ2:15
for f, g being FinSequence of REAL st f,g are_fiberwise_equipotent holds
min f = min g
proof end;

definition
let f be FinSequence of REAL ;
::Descend Sorting or Rearrangement of FinSequences
func sort_d f -> non-increasing FinSequence of REAL means :Def5: :: RFINSEQ2:def 5
f,it are_fiberwise_equipotent ;
existence
ex b1 being non-increasing FinSequence of REAL st f,b1 are_fiberwise_equipotent
by RFINSEQ:22;
uniqueness
for b1, b2 being non-increasing FinSequence of REAL st f,b1 are_fiberwise_equipotent & f,b2 are_fiberwise_equipotent holds
b1 = b2
by ;
projectivity
for b1 being non-increasing FinSequence of REAL
for b2 being FinSequence of REAL st b2,b1 are_fiberwise_equipotent holds
b1,b1 are_fiberwise_equipotent
;
end;

:: deftheorem Def5 defines sort_d RFINSEQ2:def 5 :
for f being FinSequence of REAL
for b2 being non-increasing FinSequence of REAL holds
( b2 = sort_d f iff f,b2 are_fiberwise_equipotent );

theorem Th16: :: RFINSEQ2:16
for R being FinSequence of REAL st ( len R = 0 or len R = 1 ) holds
R is non-decreasing
proof end;

theorem Th17: :: RFINSEQ2:17
for R being FinSequence of REAL holds
( R is non-decreasing iff for n, m being Nat st n in dom R & m in dom R & n < m holds
R . n <= R . m )
proof end;

Lm3: for f, g being non-decreasing FinSequence of REAL
for n being Nat st len f = n + 1 & len f = len g & f,g are_fiberwise_equipotent holds
( f . (len f) = g . (len g) & f | n,g | n are_fiberwise_equipotent )

proof end;

theorem Th18: :: RFINSEQ2:18
for R being non-decreasing FinSequence of REAL
for n being Nat holds R | n is non-decreasing FinSequence of REAL
proof end;

Lm4: for n being Nat
for g1, g2 being non-decreasing FinSequence of REAL st n = len g1 & g1,g2 are_fiberwise_equipotent holds
g1 = g2

proof end;

theorem Th19: :: RFINSEQ2:19
for R1, R2 being non-decreasing FinSequence of REAL st R1,R2 are_fiberwise_equipotent holds
R1 = R2
proof end;

definition
let f be FinSequence of REAL ;
::Ascend Sorting or Rearrangement of FinSequences
func sort_a f -> non-decreasing FinSequence of REAL means :Def6: :: RFINSEQ2:def 6
f,it are_fiberwise_equipotent ;
existence
ex b1 being non-decreasing FinSequence of REAL st f,b1 are_fiberwise_equipotent
by INTEGRA2:3;
uniqueness
for b1, b2 being non-decreasing FinSequence of REAL st f,b1 are_fiberwise_equipotent & f,b2 are_fiberwise_equipotent holds
b1 = b2
by ;
projectivity
for b1 being non-decreasing FinSequence of REAL
for b2 being FinSequence of REAL st b2,b1 are_fiberwise_equipotent holds
b1,b1 are_fiberwise_equipotent
;
end;

:: deftheorem Def6 defines sort_a RFINSEQ2:def 6 :
for f being FinSequence of REAL
for b2 being non-decreasing FinSequence of REAL holds
( b2 = sort_a f iff f,b2 are_fiberwise_equipotent );

theorem :: RFINSEQ2:20
for f being non-increasing FinSequence of REAL holds sort_d f = f by Def5;

theorem :: RFINSEQ2:21
for f being non-decreasing FinSequence of REAL holds sort_a f = f by Def6;

theorem :: RFINSEQ2:22
canceled;

theorem :: RFINSEQ2:23
canceled;

::\$CT 2
theorem Th22: :: RFINSEQ2:24
for f being FinSequence of REAL st f is non-increasing holds
- f is non-decreasing
proof end;

theorem Th23: :: RFINSEQ2:25
for f being FinSequence of REAL st f is non-decreasing holds
- f is non-increasing
proof end;

theorem Th24: :: RFINSEQ2:26
for f, g being FinSequence of REAL
for P being Permutation of (dom g) st f = g * P & len g >= 1 holds
- f = (- g) * P
proof end;

theorem Th25: :: RFINSEQ2:27
for f, g being FinSequence of REAL st f,g are_fiberwise_equipotent holds
- f, - g are_fiberwise_equipotent
proof end;

theorem :: RFINSEQ2:28
for f being FinSequence of REAL holds sort_d (- f) = - ()
proof end;

theorem :: RFINSEQ2:29
for f being FinSequence of REAL holds sort_a (- f) = - ()
proof end;

theorem Th28: :: RFINSEQ2:30
for f being FinSequence of REAL holds
( dom () = dom f & len () = len f )
proof end;

theorem Th29: :: RFINSEQ2:31
for f being FinSequence of REAL holds
( dom () = dom f & len () = len f )
proof end;

theorem :: RFINSEQ2:32
for f being FinSequence of REAL st len f >= 1 holds
( max_p () = 1 & min_p () = 1 & () . 1 = max f & () . 1 = min f )
proof end;