Skip to content

refactor: thin exists_perm_extending_strictMono via mathlib API (−46 lines) #18

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
cameronfreer merged 2 commits into from
May 18, 2026
Merged

refactor: thin exists_perm_extending_strictMono via mathlib API (−46 lines) #18

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
07695a9
refactor: thin exists_perm_extending_strictMono via mathlib API
cameronfreer May 18, 2026
c6d3cb9
docs: update Contractability docstrings to match refactored proof
cameronfreer May 18, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
76 changes: 15 additions & 61 deletions Exchangeability/Contractability.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -54,8 +54,8 @@ extension argument.

The key technical challenge is constructing permutations that extend strictly monotone
selections. Given `k : Fin m → ℕ` with `k(0) < k(1) < ... < k(m-1)`, we construct
a permutation `σ : Perm (Fin n)` such that `σ(i) = k(i)` for `i < m`. This uses
`Equiv.extendSubtype` to extend a bijection between subtypes to a full permutation.
a permutation `σ : Perm (Fin n)` such that `σ(i) = k(i)` for `i < m`. This is a thin
wrapper around mathlib's `Equiv.Perm.exists_extending_pair`.

## References

Expand Down Expand Up @@ -301,11 +301,9 @@ as the image of the first `m` positions. Since `k` is strictly increasing, it's
injective, so its image has cardinality `m`. We can extend this to a full
permutation by arbitrarily pairing up the remaining elements.

**Construction outline:**
1. **Domain partition:** `{0,...,m-1}` ∪ `{m,...,n-1}` = `Fin n`
2. **Codomain partition:** `{k(0),...,k(m-1)}` ∪ `complement` = `Fin n`
3. Map first `m` positions to `k`-values: `σ(i) = k(i)` for `i < m`
4. Extend arbitrarily to remaining positions using `Equiv.extendSubtype`
**Construction:** Thin wrapper around mathlib's `Equiv.Perm.exists_extending_pair`,
applied to `f = Fin.castLE hmn` (initial-segment inclusion) and
`g i = ⟨k i, hk_bound i⟩` (strictly monotone embedding via `k`).

This is the key combinatorial lemma enabling `contractable_of_exchangeable`:
any strictly increasing subsequence can be realized via a permutation.
Expand All @@ -314,60 +312,16 @@ lemma exists_perm_extending_strictMono {m n : ℕ} (k : Fin m → ℕ)
(hk_mono : StrictMono k) (hk_bound : ∀ i, k i < n) (hmn : m ≤ n) :
∃ (σ : Equiv.Perm (Fin n)), ∀ (i : Fin m),
(σ ⟨i.val, Nat.lt_of_lt_of_le i.isLt hmn⟩).val = k i := by
classical
-- Embed `Fin m` into `Fin n` via the initial segment.
let ι : Fin m → Fin n := fun i => ⟨i.val, Nat.lt_of_lt_of_le i.isLt hmn⟩
let p : Fin n → Prop := fun x => x.val < m
let q : Fin n → Prop := fun x => ∃ i : Fin m, x = ⟨k i, hk_bound i⟩
have hι_mem : ∀ i : Fin m, p (ι i) := fun i => i.isLt
let kFin : Fin m → Fin n := fun i => ⟨k i, hk_bound i⟩
have hk_mem : ∀ i : Fin m, q (kFin i) := fun i => ⟨i, rfl⟩
haveI : DecidablePred p := fun x => inferInstance
haveI : DecidablePred q := fun x => inferInstance
-- Equivalence between the first `m` coordinates and `Fin m`.
let e_dom : {x : Fin n // p x} ≃ Fin m :=
{ toFun := fun x => ⟨x.1.val, x.2⟩
, invFun := fun i => ⟨ι i, by
dsimp [p, ι]
exact i.isLt⟩
, left_inv := by
rintro ⟨x, hx⟩
ext; simp [ι]
, right_inv := by
intro i
cases i with
| mk i hi =>
simp [ι] }
-- Equivalence between the image of `k` and `Fin m`.
-- For injectivity of k, we use that it's strictly monotone
have hk_inj : Function.Injective kFin :=
fun i j hij => hk_mono.injective (Fin.ext_iff.mp hij)
let e_cod : Fin m ≃ {x : Fin n // q x} :=
{ toFun := fun i => ⟨kFin i, hk_mem i⟩
, invFun := fun y => Classical.choose y.2
, left_inv := by
intro i
have h_spec := Classical.choose_spec (hk_mem i)
have : k (Classical.choose (hk_mem i)) = k i := by
simpa [kFin] using (Fin.ext_iff.mp h_spec).symm
exact hk_mono.injective this
, right_inv := by
rintro ⟨y, hy⟩
apply Subtype.ext
simp only [kFin]
exact (Classical.choose_spec hy).symm }
-- Equivalence between the subtypes describing the first `m` coordinates and the image of `k`.
let e : {x : Fin n // p x} ≃ {x : Fin n // q x} := e_dom.trans e_cod
-- Extend this equivalence to a permutation of `Fin n`.
let σ : Equiv.Perm (Fin n) := Equiv.extendSubtype e
have hσ_apply : ∀ i : Fin m, σ (ι i) = kFin i := by
intro i
have h_apply := Equiv.extendSubtype_apply_of_mem (e:=e) (x:=ι i) (hι_mem i)
dsimp [σ, e, Equiv.trans, e_dom, e_cod, ι, Fin.castLEEmb, kFin] at h_apply
simpa using h_apply
refine ⟨σ, fun i => ?_⟩
have hσ_val : (σ (ι i)).val = k i := by simpa [kFin] using congrArg Fin.val (hσ_apply i)
simpa [ι] using hσ_val
-- Wrap mathlib's `Equiv.Perm.exists_extending_pair`: given injective `f g : Fin m → Fin n`,
-- there is a permutation of `Fin n` sending `f` to `g`. Take `f` = initial-segment inclusion
-- and `g` = the strictly monotone embedding via `k`.
let f : Fin m → Fin n := Fin.castLE hmn
let g : Fin m → Fin n := fun i => ⟨k i, hk_bound i⟩
have hf : Function.Injective f := Fin.castLE_injective hmn
have hg : Function.Injective g := fun i j hij =>
hk_mono.injective (Fin.mk.inj hij)
obtain ⟨σ, hσ⟩ := Equiv.Perm.exists_extending_pair f g hf hg
exact ⟨σ, fun i => congrArg Fin.val (hσ i)⟩

/- Helper: relabeling coordinates by a finite permutation is measurable as a map
from (Fin n → α) to itself (with product σ-algebra). -/
Expand Down