structure AspSet_prop (I : Set (ℤ × ℤ)) : Prop

The axioms characterizing inversion sets of ASP permutations: directedness, closure, coclosure, and finite in/out degree.

• directed (u v : ℤ) : (u, v) ∈ I → u < v
• closed (u v w : ℤ) : (u, v) ∈ I → (v, w) ∈ I → (u, w) ∈ I
• coclosed (u v w : ℤ) : u < v → v < w → (u, v) ∉ I → (v, w) ∉ I → (u, w) ∉ I
• finite_outdegree (u : ℤ) : {v : ℤ | (u, v) ∈ I}.Finite
• finite_indegree (v : ℤ) : {u : ℤ | (u, v) ∈ I}.Finite

structure AspSet : Type

An abstract ASP inversion set: a set of boxes equipped with the axioms of AspSet_prop.

• I : Set (ℤ × ℤ)
• prop : AspSet_prop self.I

instance instSetLikeAspSetProdInt : SetLike AspSet (ℤ × ℤ)

Equations

• instSetLikeAspSetProdInt = { coe := AspSet.I, coe_injective' := instSetLikeAspSetProdInt._proof_1 }

@[simp]

theorem mem_AspSet (asps : AspSet) (u v : ℤ) : (u, v) ∈ asps ↔ (u, v) ∈ asps.I

theorem AspSet.ext {A B : AspSet} (hI : A.I = B.I) : A = B

Two AspSets are equal if their underlying sets of boxes are equal.

@[reducible, inline]

abbrev AspSet.directed (asps : AspSet) (u v : ℤ) : (u, v) ∈ asps.I → u < v

Equations

• ⋯ = ⋯

@[reducible, inline]

abbrev AspSet.closed (asps : AspSet) (u v w : ℤ) : (u, v) ∈ asps.I → (v, w) ∈ asps.I → (u, w) ∈ asps.I

Equations

• ⋯ = ⋯

@[reducible, inline]

abbrev AspSet.coclosed (asps : AspSet) (u v w : ℤ) : u < v → v < w → (u, v) ∉ asps.I → (v, w) ∉ asps.I → (u, w) ∉ asps.I

Equations

• ⋯ = ⋯

@[reducible, inline]

abbrev AspSet.finite_outdegree (asps : AspSet) (u : ℤ) : {v : ℤ | (u, v) ∈ asps.I}.Finite

Equations

• ⋯ = ⋯

@[reducible, inline]

abbrev AspSet.finite_indegree (asps : AspSet) (v : ℤ) : {u : ℤ | (u, v) ∈ asps.I}.Finite

Equations

• ⋯ = ⋯

theorem AspSet.AspSet_InvSet_of_AspPerm (τ : AspPerm) : AspSet_prop (inv_set τ.func)

def AspSet.of_AspPerm (τ : AspPerm) : AspSet

Equations

• AspSet.of_AspPerm τ = { I := inv_set τ.func, prop := ⋯ }

@[reducible, inline]

noncomputable abbrev AspSet.inset (asps : AspSet) (n : ℤ) : Finset ℤ

Equations

• asps.inset n = ⋯.toFinset

@[reducible, inline]

noncomputable abbrev AspSet.outset (asps : AspSet) (n : ℤ) : Finset ℤ

Equations

• asps.outset n = ⋯.toFinset

@[simp]

theorem AspSet.mem_inset (asps : AspSet) (n x : ℤ) : x ∈ asps.inset n ↔ (x, n) ∈ asps

@[simp]

theorem AspSet.mem_outset (asps : AspSet) (n x : ℤ) : x ∈ asps.outset n ↔ (n, x) ∈ asps

noncomputable def AspSet.recon (asps : AspSet) (χ : ℤ) : ℤ → ℤ

Reconstruct a function ℤ → ℤ from an abstract ASP inversion set and a shift parameter χ.

Equations

• asps.recon χ n = n + ↑(asps.outset n).card - ↑(asps.inset n).card - χ

@[reducible, inline]

noncomputable abbrev AspSet.σ (asps : AspSet) (χ : ℤ) : ℤ → ℤ

Equations

• asps.σ χ = asps.recon χ

@[reducible, inline]

noncomputable abbrev AspSet.lf_pos (asps : AspSet) (m n : ℤ) : Finset ℤ

Equations

• asps.lf_pos m n = asps.inset m \ asps.inset n

@[simp]

theorem AspSet.mem_lf_pos (asps : AspSet) (m n x : ℤ) : x ∈ asps.lf_pos m n ↔ x < m ∧ (x, m) ∈ asps ∧ (x, n) ∉ asps

@[reducible, inline]

noncomputable abbrev AspSet.md_pos (asps : AspSet) (m n : ℤ) : Finset ℤ

Equations

• asps.md_pos m n = Finset.Ico m n \ (asps.outset m ∪ asps.inset n)

@[simp]

theorem AspSet.mem_md_pos (asps : AspSet) (m n x : ℤ) : x ∈ asps.md_pos m n ↔ m ≤ x ∧ x < n ∧ (m, x) ∉ asps ∧ (x, n) ∉ asps

@[reducible, inline]

noncomputable abbrev AspSet.rt_pos (asps : AspSet) (m n : ℤ) : Finset ℤ

Equations

• asps.rt_pos m n = asps.outset n \ asps.outset m

@[simp]

theorem AspSet.mem_rt_pos (asps : AspSet) (m n x : ℤ) : x ∈ asps.rt_pos m n ↔ x ≥ n ∧ (m, x) ∉ asps ∧ (n, x) ∈ asps

@[reducible, inline]

noncomputable abbrev AspSet.lf_neg (asps : AspSet) (m n : ℤ) : Finset ℤ

Equations

• asps.lf_neg m n = {x ∈ asps.inset n \ asps.inset m | x < m}

@[simp]

theorem AspSet.mem_lf_neg (asps : AspSet) (m n x : ℤ) : x ∈ asps.lf_neg m n ↔ x < m ∧ (x, m) ∉ asps ∧ (x, n) ∈ asps

@[reducible, inline]

noncomputable abbrev AspSet.md_neg (asps : AspSet) (m n : ℤ) : Finset ℤ

Equations

• asps.md_neg m n = Finset.Ico m n ∩ (asps.outset m ∩ asps.inset n)

@[simp]

theorem AspSet.mem_md_neg (asps : AspSet) (m n x : ℤ) : x ∈ asps.md_neg m n ↔ m ≤ x ∧ x < n ∧ (m, x) ∈ asps ∧ (x, n) ∈ asps

@[reducible, inline]

noncomputable abbrev AspSet.rt_neg (asps : AspSet) (m n : ℤ) : Finset ℤ

Equations

• asps.rt_neg m n = {x ∈ asps.outset m \ asps.outset n | x ≥ n}

@[simp]

theorem AspSet.mem_rt_neg (asps : AspSet) (m n x : ℤ) : x ∈ asps.rt_neg m n ↔ x ≥ n ∧ (m, x) ∈ asps ∧ (n, x) ∉ asps

theorem AspSet.σ_diff (asps : AspSet) (m n χ : ℤ) (m_le_n : m ≤ n) : asps.σ χ n - asps.σ χ m = ↑(asps.lf_pos m n).card + ↑(asps.md_pos m n).card + ↑(asps.rt_pos m n).card - (↑(asps.lf_neg m n).card + ↑(asps.md_neg m n).card + ↑(asps.rt_neg m n).card)

theorem AspSet.σ_diff_pos (asps : AspSet) (m n χ : ℤ) (m_lt_n : m < n) (mn_I : (m, n) ∉ asps) : asps.σ χ n - asps.σ χ m = ↑(asps.lf_pos m n).card + ↑(asps.md_pos m n).card + ↑(asps.rt_pos m n).card

theorem AspSet.σ_inc (asps : AspSet) (m n χ : ℤ) (m_lt_n : m < n) (mn_nI : (m, n) ∉ asps) : asps.σ χ m < asps.σ χ n

theorem AspSet.σ_dec (asps : AspSet) (m n χ : ℤ) (m_lt_n : m < n) (mn_I : (m, n) ∈ asps) : asps.σ χ m > asps.σ χ n

theorem AspSet.mem_iff_lt (asps : AspSet) (m n χ : ℤ) (m_le_n : m ≤ n) : (m, n) ∈ asps ↔ asps.σ χ n < asps.σ χ m

theorem AspSet.func_injective (χ : ℤ) (asps : AspSet) : Function.Injective (asps.recon χ)

theorem AspSet.contiguity_helper (asps : AspSet) (m n χ : ℤ) (m_lt_n : m < n) (σ_m_lt_n : asps.σ χ m < asps.σ χ n) : asps.σ χ ⁻¹' Set.Ico (asps.σ χ m) (asps.σ χ n) = ↑(asps.lf_pos m n ∪ asps.md_pos m n ∪ asps.rt_pos m n)

theorem AspSet.func_contiguous (asps : AspSet) (m n χ : ℤ) (m_lt_n : m < n) (σ_m_lt_n : asps.σ χ m < asps.σ χ n) (k : ℤ) : asps.recon χ m ≤ k → k < asps.recon χ n → ∃ (l : ℤ), k = asps.recon χ l

Reconstructing ASP Permutations from ASP Sets

Starting from an abstract ASP set asps and a shift χ, this section proves that the reconstructed function is bijective, ASP, and has the expected inversion data, yielding an AspPerm.

theorem AspSet.invSet_func (asps : AspSet) (χ : ℤ) : inv_set (asps.recon χ) = ↑asps

The reconstructed function has the prescribed inversion set.

theorem AspSet.inset_eq_nw (asps : AspSet) (χ n : ℤ) : ↑(asps.inset n) = northwest_set (asps.σ χ) (asps.σ χ n + 1) n

theorem AspSet.outset_eq_se (asps : AspSet) (χ n : ℤ) : ↑(asps.outset n) = southeast_set (asps.σ χ) (asps.σ χ n) (n + 1)

theorem AspSet.surj_helper_up (asps : AspSet) (χ m : ℤ) (n : ℕ) : ∃ x ≥ m, asps.recon χ x ≥ asps.recon χ m + ↑n

theorem AspSet.surj_helper_down (asps : AspSet) (χ m : ℤ) (n : ℕ) : ∃ x ≤ m, asps.recon χ x ≤ asps.recon χ m - ↑n

theorem AspSet.func_surjective (asps : AspSet) (χ : ℤ) : Function.Surjective (asps.recon χ)

The function reconstructed from an ASP set and a shift is surjective.

theorem AspSet.func_bijective (asps : AspSet) (χ : ℤ) : Function.Bijective (asps.recon χ)

theorem AspSet.func_asp (asps : AspSet) (χ : ℤ) : is_asp (asps.recon χ)

noncomputable def AspSet.toAspPerm (asps : AspSet) (χ : ℤ) : AspPerm

Package the function reconstructed from an ASP set and a shift as an AspPerm.

Equations

• asps.toAspPerm χ = { func := asps.recon χ, bijective := ⋯, asp := ⋯ }

theorem AspSet.invSet_of_toAspPerm (asps : AspSet) (χ : ℤ) : inv_set (asps.toAspPerm χ).func = ↑asps

theorem AspSet.inset_of_toAspPerm (asps : AspSet) (χ n : ℤ) : (asps.toAspPerm χ).inset n = ↑(asps.inset n)

theorem AspSet.outset_of_toAspPerm (asps : AspSet) (χ n : ℤ) : (asps.toAspPerm χ).outset n = ↑(asps.outset n)

theorem AspSet.chi_of_toAspPerm (asps : AspSet) (χ : ℤ) : (asps.toAspPerm χ).χ = χ

noncomputable def AspSet.AspPerm_equiv_AspSet : AspPerm ≃ AspSet × ℤ

ASP permutations are equivalent to abstract ASP inversion sets together with a shift parameter.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AspSet.AspPerm_equiv_AspSet_toFun_fst (τ : AspPerm) : ↑(AspPerm_equiv_AspSet τ).1 = inv_set τ.func

@[simp]

theorem AspSet.AspPerm_equiv_AspSet_toFun_snd (τ : AspPerm) : (AspPerm_equiv_AspSet τ).2 = τ.χ

@[simp]

theorem AspSet.inv_set_AspPerm_equiv_AspSet_invFun (asps : AspSet) (χ : ℤ) : inv_set (AspPerm_equiv_AspSet.invFun (asps, χ)).func = ↑asps

@[simp]

theorem AspSet.chi_AspPerm_equiv_AspSet_invFun (asps : AspSet) (χ : ℤ) : (AspPerm_equiv_AspSet.invFun (asps, χ)).χ = χ

theorem AspSet.invSets_of_AspPerms (I : Set (ℤ × ℤ)) (χ : ℤ) : (∃ (τ : AspPerm), inv_set τ.func = I ∧ τ.χ = χ) ↔ AspSet_prop I