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.countP_eq_card_filter_getElem: elements of a list xs passing p are counted by the indices in Fin xs.length where p holds.
• List.sum_map_range, List.sum_map_drop_range, List.sum_map_drop_range_fin: sums over List.range n and its tails as Fin or interval sums.
• Fin.card_lt_of_monotone_of_unique: a unique value in a monotone array has its index many smaller entries.
• List.Perm.key_ofFn_eq_of_rank: a unique key occurs at its rank after sorting.
• 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.
• [OAI26d]

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.countP_eq_card_filter_getElem {α : Type u_1} (xs : List α) (p : α → Bool) : countP p xs = {i : Fin xs.length | p xs[i] = true}.card

Elements of xs satisfying p are counted by the indices in Fin xs.length where p holds.

theorem List.sum_map_range {M : Type u_1} [AddCommMonoid M] (n : ℕ) (f : ℕ → M) : (map f (range n)).sum = ∑ i : Fin n, f ↑i

A sum over List.range n is a sum over Fin n.

theorem List.sum_map_drop_range {M : Type u_1} [AddCommMonoid M] (n lo : ℕ) (f : ℕ → M) : (map f (drop lo (range n))).sum = ∑ k ∈ Finset.Ico lo n, f k

A tail of List.range n, summed as a list, is the sum over Finset.Ico lo n.

theorem List.sum_map_drop_range_fin {M : Type u_1} [AddCommMonoid M] {n : ℕ} (i : Fin n) (f : ℕ → M) : (map f (drop (↑i + 1) (range n))).sum = ∑ k > i, f ↑k

A tail of List.range n after i : Fin n, summed as a list, is the sum over Finset.Ioi i.

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.