Strictly Monotone Function Utilities

Utility lemmas for strictly monotone functions on Fin m → ℕ, commonly used in subsequence selection and permutation construction arguments.

Main Results

• strictMono_Fin_ge_id: For strictly monotone k : Fin m → ℕ, values dominate indices
• strictMono_add_left, strictMono_add_right: Addition preserves strict monotonicity
• fin_val_strictMono: The identity Fin n → ℕ is strictly monotone
• injective_implies_strictMono_perm: Any injective k : Fin m → ℕ can be composed with a permutation to become strictly monotone

These lemmas are used extensively in exchangeability and contractability proofs when working with strictly increasing subsequences.

Implementation Notes

The file has no project dependencies - imports only mathlib. All lemmas are general-purpose utilities for Fin and strict monotonicity.

theorem Exchangeability.Util.StrictMono.strictMono_add_left {m : ℕ} (k : Fin m → ℕ) (hk : StrictMono k) (c : ℕ) : StrictMono fun (i : Fin m) => c + k i

Composing strictly monotone functions with left addition preserves strict monotonicity.

For any strictly monotone k : Fin m → ℕ and constant c, the function i ↦ c + k(i) is also strictly monotone.

theorem Exchangeability.Util.StrictMono.strictMono_add_right {m : ℕ} (k : Fin m → ℕ) (hk : StrictMono k) (c : ℕ) : StrictMono fun (i : Fin m) => k i + c

Composing strictly monotone functions with right addition preserves strict monotonicity.

For any strictly monotone k : Fin m → ℕ and constant c, the function i ↦ k(i) + c is also strictly monotone.

theorem Exchangeability.Util.StrictMono.strictMono_Fin_ge_id {m : ℕ} {k : Fin m → ℕ} (hk : StrictMono k) (i : Fin m) : ↑i ≤ k i

For a strictly monotone function k : Fin m → ℕ, the values dominate the indices.

Statement: For all i : Fin m, we have i ≤ k(i).

Intuition: If you select m values from ℕ in strictly increasing order, the i-th selected value must be at least i (since you've already selected i values before it, all distinct).

Example: If k = [3, 5, 7] (selecting 3 values), then:

• k(0) = 3 ≥ 0 ✓
• k(1) = 5 ≥ 1 ✓
• k(2) = 7 ≥ 2 ✓

This is crucial for proving that strictly increasing subsequences can be realized by permutations.

theorem Exchangeability.Util.StrictMono.fin_val_strictMono {n : ℕ} : StrictMono fun (i : Fin n) => ↑i

The identity function Fin n → ℕ is strictly monotone.

The canonical embedding of Fin n into ℕ preserves the order structure.

theorem Exchangeability.Util.StrictMono.injective_implies_strictMono_perm {m : ℕ} (k : Fin m → ℕ) (hk : Function.Injective k) : ∃ (σ : Equiv.Perm (Fin m)), StrictMono fun (i : Fin m) => k (σ i)

Any injective function k : Fin m → ℕ can be composed with a permutation to become strictly monotone.

Construction: Let s := image k univ (the image of k as a finset of ℕ). Since k is injective, s.card = m. The orderIsoOfFin gives the sorted enumeration of s. We define σ to map i to the position of k(i) in the sorted order.

Key property: (fun i => k (σ i)) is strictly increasing (sorted order).

This is a key lemma for reducing proofs about injective index selections to proofs about strictly monotone (consecutive-like) selections via contractability.