Finite-array permutations and ranks

Use ordinary List.Perm on List.ofFn to transport predicates and their multiplicities. If an entry has a unique key, its sorted position is the number of strictly smaller keys; other keys may repeat. The key order need only be a partial order.

Main results

• List.Perm.exists_ofFn_iff, List.Perm.existsUnique_ofFn_iff: predicate transport.
• List.Perm.card_filter_ofFn_eq: preservation of predicate counts.
• List.countP_range_eq_card_filter: counting the numbers below n that pass a test is counting the elements of Fin n that pass it.
• List.Perm.apply_ofFn_eq_of_rank: identify an entire entry at its sorted position.

References

The rank argument supports the two-sort routing construction in S. Schlesinger, Boolean circuit mass production formalization.

theorem List.Perm.exists_ofFn_iff {α : Type u_1} {m n : ℕ} {f : Fin m → α} {g : Fin n → α} (perm : (ofFn f).Perm (ofFn g)) (p : α → Prop) : (∃ (i : Fin m), p (f i)) ↔ ∃ (i : Fin n), p (g i)

Permuting a finite array preserves whether any entry satisfies a predicate.

theorem List.countP_ofFn {α : Type u_1} {n : ℕ} (f : Fin n → α) (p : α → Bool) : countP p (ofFn f) = ∑ i : Fin n, if p (f i) = true then 1 else 0

Count satisfying array entries by summing their Boolean indicators.

theorem List.countP_range_eq_card_filter (n : ℕ) (p : ℕ → Bool) : countP p (range n) = {j : Fin n | p ↑j = true}.card

The numbers below n that pass a test are as many as the elements of Fin n that pass it.

theorem List.Perm.card_filter_ofFn_eq {α : Type u_1} {n : ℕ} {f g : Fin n → α} (perm : (ofFn f).Perm (ofFn g)) (p : α → Prop) [DecidablePred p] : {i : Fin n | p (f i)}.card = {i : Fin n | p (g i)}.card

Permuting a finite array preserves the number of entries satisfying a predicate.

theorem List.Perm.existsUnique_ofFn_iff {α : Type u_1} {n : ℕ} {f g : Fin n → α} (perm : (ofFn f).Perm (ofFn g)) (p : α → Prop) : (∃! i : Fin n, p (f i)) ↔ ∃! i : Fin n, p (g i)

Permuting a finite array preserves unique occurrence of a predicate.

theorem Fin.card_lt_of_monotone_of_unique {α : Type u_1} [PartialOrder α] [DecidableLT α] {n : ℕ} {f : Fin n → α} (sorted : Monotone f) (j : Fin n) (unique : ∀ (i : Fin n), f i = f j → i = j) : {i : Fin n | f i < f j}.card = ↑j

A unique value in a monotone finite array has exactly its index many smaller entries.

theorem List.Perm.key_ofFn_eq_of_rank {α : Type u_1} {β : Type u_2} [PartialOrder β] [DecidableLT β] {n : ℕ} {f g : Fin n → α} (perm : (ofFn f).Perm (ofFn g)) (key : α → β) (sorted : Monotone (key ∘ g)) (target : β) (unique : ∃! i : Fin n, key (f i) = target) (j : Fin n) (rank : {i : Fin n | key (f i) < target}.card = ↑j) : key (g j) = target

A unique key occurs at its rank after a finite array is sorted by that key.

theorem List.Perm.apply_ofFn_eq_of_rank {α : Type u_1} {β : Type u_2} [PartialOrder β] [DecidableLT β] {n : ℕ} {f g : Fin n → α} (perm : (ofFn f).Perm (ofFn g)) (key : α → β) (sorted : Monotone (key ∘ g)) (source j : Fin n) (unique : ∀ (i : Fin n), key (f i) = key (f source) → i = source) (rank : {i : Fin n | key (f i) < key (f source)}.card = ↑j) : g j = f source

Sorting places an entry with a unique key at the number of strictly smaller keys.