:: 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 b₁ being Nat st
( ( len f = 0 implies b₁ = 0 ) & ( len f > 0 implies ( b₁ in dom f & ( for i being Nat
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b₁ holds
r1 <= r2 ) & ( for j being Nat st j in dom f & f . j = f . b₁ holds
b₁ <= j ) ) ) )

proof end;

uniqueness
for b₁, b₂ being Nat st ( len f = 0 implies b₁ = 0 ) & ( len f > 0 implies ( b₁ in dom f & ( for i being Nat
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b₁ holds
r1 <= r2 ) & ( for j being Nat st j in dom f & f . j = f . b₁ holds
b₁ <= j ) ) ) & ( len f = 0 implies b₂ = 0 ) & ( len f > 0 implies ( b₂ in dom f & ( for i being Nat
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b₂ holds
r1 <= r2 ) & ( for j being Nat st j in dom f & f . j = f . b₂ holds
b₂ <= j ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines max_p RFINSEQ2:def 1 :
for f being FinSequence of REAL
for b₂ being Nat holds
( b₂ = max_p f iff ( ( len f = 0 implies b₂ = 0 ) & ( len f > 0 implies ( b₂ in dom f & ( for i being Nat
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b₂ holds
r1 <= r2 ) & ( for j being Nat st j in dom f & f . j = f . b₂ holds
b₂ <= 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 b₁ being Nat st
( ( len f = 0 implies b₁ = 0 ) & ( len f > 0 implies ( b₁ in dom f & ( for i being Nat
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b₁ holds
r1 >= r2 ) & ( for j being Nat st j in dom f & f . j = f . b₁ holds
b₁ <= j ) ) ) )

proof end;

uniqueness
for b₁, b₂ being Nat st ( len f = 0 implies b₁ = 0 ) & ( len f > 0 implies ( b₁ in dom f & ( for i being Nat
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b₁ holds
r1 >= r2 ) & ( for j being Nat st j in dom f & f . j = f . b₁ holds
b₁ <= j ) ) ) & ( len f = 0 implies b₂ = 0 ) & ( len f > 0 implies ( b₂ in dom f & ( for i being Nat
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b₂ holds
r1 >= r2 ) & ( for j being Nat st j in dom f & f . j = f . b₂ holds
b₂ <= j ) ) ) holds
b₁ = b₂

proof end;

end;

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

definition

let f be FinSequence of REAL ;

func max f -> Real equals :: RFINSEQ2:def 3
f . (max_p f);

correctness
coherence
f . (max_p f) is Real;
;

func min f -> Real equals :: RFINSEQ2:def 4
f . (min_p f);

correctness
coherence
f . (min_p f) is Real;
;

end;

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

:: deftheorem defines min RFINSEQ2:def 4 :
for f being FinSequence of REAL holds min f = f . (min_p 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 . (max_p 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 . (min_p 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 b₁ being non-increasing FinSequence of REAL st f,b₁ are_fiberwise_equipotent by RFINSEQ:22;
uniqueness
for b₁, b₂ being non-increasing FinSequence of REAL st f,b₁ are_fiberwise_equipotent & f,b₂ are_fiberwise_equipotent holds
b₁ = b₂ by CLASSES1:76, RFINSEQ:23;
projectivity
for b₁ being non-increasing FinSequence of REAL
for b₂ being FinSequence of REAL st b₂,b₁ are_fiberwise_equipotent holds
b₁,b₁ are_fiberwise_equipotent ;

end;

:: deftheorem Def5 defines sort_d RFINSEQ2:def 5 :
for f being FinSequence of REAL
for b₂ being non-increasing FinSequence of REAL holds
( b₂ = sort_d f iff f,b₂ 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 b₁ being non-decreasing FinSequence of REAL st f,b₁ are_fiberwise_equipotent by INTEGRA2:3;
uniqueness
for b₁, b₂ being non-decreasing FinSequence of REAL st f,b₁ are_fiberwise_equipotent & f,b₂ are_fiberwise_equipotent holds
b₁ = b₂ by Th19, CLASSES1:76;
projectivity
for b₁ being non-decreasing FinSequence of REAL
for b₂ being FinSequence of REAL st b₂,b₁ are_fiberwise_equipotent holds
b₁,b₁ are_fiberwise_equipotent ;

end;

:: deftheorem Def6 defines sort_a RFINSEQ2:def 6 :
for f being FinSequence of REAL
for b₂ being non-decreasing FinSequence of REAL holds
( b₂ = sort_a f iff f,b₂ 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) = - (sort_a f)

proof end;

theorem :: RFINSEQ2:29

for f being FinSequence of REAL holds sort_a (- f) = - (sort_d f)

proof end;

theorem Th28: :: RFINSEQ2:30

for f being FinSequence of REAL holds
( dom (sort_d f) = dom f & len (sort_d f) = len f )

proof end;

theorem Th29: :: RFINSEQ2:31

for f being FinSequence of REAL holds
( dom (sort_a f) = dom f & len (sort_a f) = len f )

proof end;

theorem :: RFINSEQ2:32

for f being FinSequence of REAL st len f >= 1 holds
( max_p (sort_d f) = 1 & min_p (sort_a f) = 1 & (sort_d f) . 1 = max f & (sort_a f) . 1 = min f )

proof end;