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.not_mem_of_ge (asps : AspSet) {m n : ℤ} (n_le_m : n ≤ m) : (m, n) ∉ asps

@[simp]

theorem AspSet.not_mem_self (asps : AspSet) (n : ℤ) : (n, n) ∉ asps

def AspSet.post_lt (asps : AspSet) (m n : ℤ) : Prop

The order on indices after the inversions in asps are applied.

Equations

• asps.post_lt m n = (m < n ∧ (m, n) ∉ asps ∨ n < m ∧ (n, m) ∈ asps)

@[simp]

theorem AspSet.not_post_lt_self (asps : AspSet) (n : ℤ) : ¬asps.post_lt n n

theorem AspSet.post_lt_iff_not_mem (asps : AspSet) {m n : ℤ} (m_lt_n : m < n) : asps.post_lt m n ↔ (m, n) ∉ asps

theorem AspSet.post_lt_swap_iff_mem (asps : AspSet) {m n : ℤ} (m_le_n : m ≤ n) : asps.post_lt n m ↔ (m, n) ∈ asps

theorem AspSet.post_lt_trans (asps : AspSet) {l m n : ℤ} (hlm : asps.post_lt l m) (hmn : asps.post_lt m n) : asps.post_lt l n

theorem AspSet.post_lt_trichotomous (asps : AspSet) : Std.Trichotomous asps.post_lt

instance AspSet.instIsStrictTotalOrderIntPost_lt (asps : AspSet) : IsStrictTotalOrder ℤ asps.post_lt

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

theorem AspSet.post_Ico_set_finite (asps : AspSet) (m n : ℤ) : {l : ℤ | asps.post_lt l n ∧ ¬asps.post_lt l m}.Finite

The half-open interval for the order post_lt. These are the elements l with m ≤ l < n in the post-inversion order.

noncomputable def AspSet.post_Ico (asps : AspSet) (m n : ℤ) : Finset ℤ

Equations

• asps.post_Ico m n = ⋯.toFinset

@[simp]

theorem AspSet.mem_post_Ico (asps : AspSet) (m n l : ℤ) : l ∈ asps.post_Ico m n ↔ asps.post_lt l n ∧ ¬asps.post_lt l m

theorem AspSet.post_Ico_swap_eq_empty_of_post_lt (asps : AspSet) {m n : ℤ} (hmn : asps.post_lt m n) : asps.post_Ico n m = ∅

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 χ

theorem AspSet.σ_diff_post (asps : AspSet) (m n χ : ℤ) (m_le_n : m ≤ n) : asps.σ χ n - asps.σ χ m = ↑(asps.post_Ico m n).card - ↑(asps.post_Ico n m).card

theorem AspSet.σ_diff_of_post_lt (asps : AspSet) (m n χ : ℤ) (hmn : asps.post_lt m n) : asps.σ χ n - asps.σ χ m = ↑(asps.post_Ico m n).card

theorem AspSet.σ_lt_of_post_lt (asps : AspSet) (m n χ : ℤ) (hmn : asps.post_lt m n) : asps.σ χ m < asps.σ χ n

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.post_lt_iff_σ_lt (asps : AspSet) (m n χ : ℤ) : asps.post_lt m n ↔ asps.σ χ m < asps.σ χ n

theorem AspSet.not_post_lt_iff_σ_le (asps : AspSet) (m n χ : ℤ) : ¬asps.post_lt m n ↔ asps.σ χ n ≤ asps.σ χ m

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 χ : ℤ) : asps.σ χ ⁻¹' Set.Ico (asps.σ χ m) (asps.σ χ n) = ↑(asps.post_Ico m n)

theorem AspSet.func_contiguous (asps : AspSet) (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