def inv_set (τ : ℤ → ℤ) : Set (ℤ × ℤ)

The inversion set $\operatorname{Inv} \tau = \{(u,v) \in \mathbb{Z}^2 : u < v \text{ and } \tau(u) > \tau(v)\}$.

In Lean, membership is written ⟨u, v⟩ ∈ inv_set τ, and the inequality is encoded as τ v < τ u.

Equations

• inv_set τ = {(i, j) : ℤ × ℤ | i < j ∧ τ j < τ i}

def southeast_set (τ : ℤ → ℤ) (m n : ℤ) : Set ℤ

Equations

• southeast_set τ m n = {k : ℤ | n ≤ k ∧ τ k < m}

def northwest_set (τ : ℤ → ℤ) (m n : ℤ) : Set ℤ

Equations

• northwest_set τ m n = {k : ℤ | k < n ∧ m ≤ τ k}

@[reducible, inline]

abbrev flip_func (f : ℤ → ℤ) : ℤ → ℤ

Equations

• flip_func f k = -1 - f (-1 - k)

theorem flip_quadrant (f : ℤ → ℤ) (a b : ℤ) : (fun (x : ℤ) => -1 - x) '' southeast_set f a b = northwest_set (flip_func f) (-a) (-b)

theorem se_finite_of_finite {τ : ℤ → ℤ} (h_inj : Function.Injective τ) (m n m' n' : ℤ) : (southeast_set τ m n).Finite → (southeast_set τ m' n').Finite

theorem nw_finite_of_finite {τ : ℤ → ℤ} (h_inj : Function.Injective τ) (m n m' n' : ℤ) : (northwest_set τ m n).Finite → (northwest_set τ m' n').Finite

def is_asp (τ : ℤ → ℤ) : Prop

The almost-sign-preserving condition: the set $\{ n \in \mathbb{Z} : n \tau(n) < 0 \}$ is finite.

Equivalently, only finitely many integers change sign under τ.

Equations

• is_asp τ = {n : ℤ | n * τ n < 0}.Finite

theorem se_finite_of_asp {τ : ℤ → ℤ} (h_inj : Function.Injective τ) (m n : ℤ) : is_asp τ → (southeast_set τ m n).Finite

theorem nw_finite_of_asp {τ : ℤ → ℤ} (h_inj : Function.Injective τ) (m n : ℤ) : is_asp τ → (northwest_set τ m n).Finite

theorem asp_of_finite_quadrants {τ : ℤ → ℤ} (h_inj : Function.Injective τ) {m n m' n' : ℤ} (fin_se : (southeast_set τ m n).Finite) (fin_nw : (northwest_set τ m' n').Finite) : is_asp τ

structure AspPerm : Type

An almost-sign-preserving permutation of ℤ, abbreviated ASP permutation.

This is the paper's group $\mathrm{ASP}$, packaged in Lean as a function together with proofs of bijectivity and the ASP condition.

• func : ℤ → ℤ
• bijective : Function.Bijective self.func
• asp : is_asp self.func

instance instCoeFunAspPermForallInt : CoeFun AspPerm fun (x : AspPerm) => ℤ → ℤ

Equations

• instCoeFunAspPermForallInt = { coe := AspPerm.func }

theorem AspPerm.injective (τ : AspPerm) : Function.Injective τ.func

theorem AspPerm.surjective (τ : AspPerm) : Function.Surjective τ.func

theorem AspPerm.inv_iff_lt (τ : AspPerm) {i j : ℤ} (i_le_j : i ≤ j) : (i, j) ∈ inv_set τ.func ↔ τ.func j < τ.func i

theorem AspPerm.inv_iff_le (τ : AspPerm) {i j : ℤ} (i_lt_j : i < j) : (i, j) ∈ inv_set τ.func ↔ τ.func j ≤ τ.func i

@[simp]

theorem AspPerm.ext {σ τ : AspPerm} : σ = τ ↔ σ.func = τ.func

def AspPerm.mul (σ τ : AspPerm) : AspPerm

Equations

• σ.mul τ = { func := σ.func ∘ τ.func, bijective := ⋯, asp := ⋯ }

noncomputable def AspPerm.inv (τ : AspPerm) : AspPerm

Equations

• τ.inv = { func := Function.invFun τ.func, bijective := ⋯, asp := ⋯ }

def AspPerm.id : AspPerm

Equations

• AspPerm.id = { func := id, bijective := AspPerm.id._proof_1, asp := AspPerm.id._proof_2 }

noncomputable instance AspPerm.instGroup : Group AspPerm

Equations

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

@[simp]

theorem AspPerm.inv_mul_cancel_eval (τ : AspPerm) (n : ℤ) : τ⁻¹.func (τ.func n) = n

@[simp]

theorem AspPerm.mul_inv_cancel_eval (τ : AspPerm) (n : ℤ) : τ.func (τ⁻¹.func n) = n

theorem AspPerm.se_finite (τ : AspPerm) (a b : ℤ) : (southeast_set τ.func a b).Finite

theorem AspPerm.nw_finite (τ : AspPerm) (a b : ℤ) : (northwest_set τ.func a b).Finite

noncomputable def AspPerm.se_finset (τ : AspPerm) (a b : ℤ) : Finset ℤ

Equations

• τ.se_finset a b = ⋯.toFinset

@[simp]

theorem AspPerm.mem_se (τ : AspPerm) (a b n : ℤ) : n ∈ τ.se_finset a b ↔ n ≥ b ∧ τ.func n < a

noncomputable def AspPerm.nw_finset (τ : AspPerm) (a b : ℤ) : Finset ℤ

Equations

• τ.nw_finset a b = ⋯.toFinset

@[simp]

theorem AspPerm.mem_nw (τ : AspPerm) (a b n : ℤ) : n ∈ τ.nw_finset a b ↔ n < b ∧ τ.func n ≥ a

theorem AspPerm.inv_set_inverse (τ : AspPerm) (u v : ℤ) : (u, v) ∈ inv_set τ.func ↔ (τ.func v, τ.func u) ∈ inv_set τ⁻¹.func

def AspPerm.rev_map (τ : AspPerm) : ℤ × ℤ → ℤ × ℤ

Equations

• τ.rev_map (i, j) = (τ.func j, τ.func i)

noncomputable def AspPerm.s (τ : AspPerm) (a b : ℤ) : ℤ

The slipface value $s_\tau(a,b) = \#\{n \geq b : \tau(n) < a\}$.

This is one of the main notation shifts from the paper to Lean: the paper writes $s_\tau(a,b)$, while the code writes τ.s a b.

Equations

• τ.s a b = ↑(southeast_set τ.func a b).ncard

noncomputable def AspPerm.s' (τ : AspPerm) (b a : ℤ) : ℤ

The companion counting function $s_{\tau^{-1}}(b,a)$.

In Lean this is written τ.s' b a; later dual_inverse identifies it with (τ⁻¹).s.

Equations

• τ.s' b a = ↑(northwest_set τ.func a b).ncard

noncomputable def AspPerm.χ (τ : AspPerm) : ℤ

The shift $\chi_\tau = s_\tau(0,0) - s_{\tau^{-1}}(0,0)$.

The paper writes this as $\chi_\tau$; Lean writes it as τ.χ.

Equations

• τ.χ = τ.s 0 0 - τ.s' 0 0

@[simp]

theorem AspPerm.id_chi : id.χ = 0

theorem AspPerm.s_eq_se_card (τ : AspPerm) (a b : ℤ) : τ.s a b = ↑(τ.se_finset a b).card

theorem AspPerm.s'_eq_nw_card (τ : AspPerm) (b a : ℤ) : τ.s' b a = ↑(τ.nw_finset a b).card

theorem AspPerm.s_nonneg (τ : AspPerm) (a b : ℤ) : τ.s a b ≥ 0

theorem AspPerm.s'_nonneg (τ : AspPerm) (a b : ℤ) : τ.s' a b ≥ 0

theorem AspPerm.s'_pos_of_lt (τ : AspPerm) {u b : ℤ} (u_lt_b : u < b) : τ.s' b (τ.func u) ≥ 1

theorem AspPerm.dual_inverse (τ : AspPerm) : τ.s' = τ⁻¹.s

theorem AspPerm.chi_dual (τ : AspPerm) : τ⁻¹.χ = -τ.χ

theorem AspPerm.chi_dual' (τ : AspPerm) : τ.χ = -τ⁻¹.χ

theorem AspPerm.flip_bij (τ : AspPerm) : Function.Bijective (flip_func τ.func)

def AspPerm.flip (τ : AspPerm) : AspPerm

Equations

• τ.flip = { func := fun (n : ℤ) => -1 - τ.func (-1 - n), bijective := ⋯, asp := ⋯ }

theorem AspPerm.flip_inv (τ : AspPerm) : τ.flip⁻¹ = τ⁻¹.flip

theorem AspPerm.flip_flip (τ : AspPerm) : τ.flip.flip = τ

theorem AspPerm.flip_s (τ : AspPerm) (a b : ℤ) : τ.flip.s a b = τ.s' (-b) (-a)

theorem AspPerm.s_flip (τ : AspPerm) (a b : ℤ) : τ.s a b = τ⁻¹.flip.s (-b) (-a)

theorem AspPerm.b_move_up (τ : AspPerm) (a b b' : ℤ) (b_le_b' : b ≤ b') : τ.s a b' = τ.s a b - ↑{x ∈ Finset.Ico b b' | τ.func x < a}.card

theorem AspPerm.s_noninc (τ : AspPerm) (a : ℤ) {b b' : ℤ} (b_le_b' : b ≤ b') : τ.s a b ≥ τ.s a b' ∧ (τ.s a b = τ.s a b' ↔ ∀ (x : ℤ), b ≤ x → x < b' → τ.func x ≥ a)

theorem AspPerm.b_step (τ : AspPerm) (a b : ℤ) : τ.s a (b + 1) = τ.s a b - if τ.func b < a then 1 else 0

theorem AspPerm.b_step_one_iff (τ : AspPerm) (a b : ℤ) : τ.s a (b + 1) = τ.s a b - 1 ↔ τ.func b < a

theorem AspPerm.b_step_eq_iff (τ : AspPerm) (a b : ℤ) : τ.s a (b + 1) = τ.s a b ↔ τ.func b ≥ a

theorem AspPerm.a_move_up (τ : AspPerm) (a a' b : ℤ) (a_le_a' : a ≤ a') : τ.s a' b = τ.s a b + ↑{x ∈ Finset.Ico a a' | τ⁻¹.func x ≥ b}.card

theorem AspPerm.s_nondec (τ : AspPerm) {a a' : ℤ} (a_le_a' : a ≤ a') (b : ℤ) : τ.s a b ≤ τ.s a' b ∧ (τ.s a b = τ.s a' b ↔ ∀ (x : ℤ), a ≤ τ.func x → τ.func x < a' → x < b)

theorem AspPerm.a_step (τ : AspPerm) (a b : ℤ) : τ.s (a + 1) b = τ.s a b + if τ⁻¹.func a ≥ b then 1 else 0

theorem AspPerm.a_step_one_iff (τ : AspPerm) (a b : ℤ) : τ.s (a + 1) b = τ.s a b + 1 ↔ τ⁻¹.func a ≥ b

theorem AspPerm.a_step_one_iff' (τ : AspPerm) (u b : ℤ) : τ.s (τ.func u + 1) b = τ.s (τ.func u) b + 1 ↔ u ≥ b

theorem AspPerm.a_step_eq_iff (τ : AspPerm) (a b : ℤ) : τ.s (a + 1) b = τ.s a b ↔ τ⁻¹.func a < b

theorem AspPerm.a_step_eq_iff' (τ : AspPerm) (u b : ℤ) : τ.s (τ.func u + 1) b = τ.s (τ.func u) b ↔ u < b

theorem AspPerm.duality (τ : AspPerm) (a b : ℤ) : τ.s a b - τ⁻¹.s b a = τ.χ + a - b

def AspPerm.inset (τ : AspPerm) (v : ℤ) : Set ℤ

Equations

• τ.inset v = {u : ℤ | (u, v) ∈ inv_set τ.func}

theorem AspPerm.inset_eq_nw (τ : AspPerm) (v : ℤ) : τ.inset v = northwest_set τ.func (τ.func v) v

theorem AspPerm.invset_iff_inset (τ : AspPerm) (u v : ℤ) : (u, v) ∈ inv_set τ.func ↔ u ∈ τ.inset v

theorem AspPerm.inset_finite (τ : AspPerm) (v : ℤ) : (τ.inset v).Finite

def AspPerm.outset (τ : AspPerm) (u : ℤ) : Set ℤ

Equations

• τ.outset u = {v : ℤ | (u, v) ∈ inv_set τ.func}

theorem AspPerm.outset_eq_se (τ : AspPerm) (u : ℤ) : τ.outset u = southeast_set τ.func (τ.func u) u

theorem AspPerm.invset_iff_outset (τ : AspPerm) (u v : ℤ) : (u, v) ∈ inv_set τ.func ↔ v ∈ τ.outset u

theorem AspPerm.outset_finite (τ : AspPerm) (u : ℤ) : (τ.outset u).Finite

theorem AspPerm.reconstruction (τ : AspPerm) (n : ℤ) : τ.func n = n - τ.χ + ↑(τ.outset n).ncard - ↑(τ.inset n).ncard

Reconstruct τ n from its shift and inversion set: $\tau(n) = n - \chi_\tau$ $+ \#\{v \in \mathbb{Z} : (n,v) \in \operatorname{Inv} \tau\}$ $- \#\{u \in \mathbb{Z} : (u,n) \in \operatorname{Inv} \tau\}$.

In Lean the two finite sets are implemented as τ.outset n and τ.inset n.

theorem AspPerm.eq_of_inv_set_eq_of_chi_eq (σ τ : AspPerm) (h_inv : inv_set σ.func = inv_set τ.func) (h_χ : σ.χ = τ.χ) : σ = τ

Two ASP permutations are equal if they have the same inversion set and the same shift.

theorem AspPerm.eq_id_of_inv_set_eq_empty_of_chi_eq_zero (τ : AspPerm) (h_inv : inv_set τ.func = ∅) (h_χ : τ.χ = 0) : τ = id

An ASP permutation with empty inversion set and zero shift is the identity.

@[simp]

theorem AspPerm.inv_set_id : inv_set id.func = ∅

theorem AspPerm.s_eq (τ : AspPerm) (a b : ℤ) : τ.s a b = τ⁻¹.s b a + τ.χ + a - b

theorem AspPerm.s'_eq (τ : AspPerm) (a b : ℤ) : τ⁻¹.s a b = τ.s b a - τ.χ + a - b

theorem AspPerm.s_ge (τ : AspPerm) (a b : ℤ) : τ.s a b ≥ a - b + τ.χ

theorem AspPerm.s'_ge (τ : AspPerm) (a b : ℤ) : τ.s' a b ≥ a - b - τ.χ

theorem AspPerm.tend_zero_a (τ : AspPerm) (b : ℤ) : ∃ (a : ℤ), τ.s a b = 0

theorem AspPerm.tend_zero_b (τ : AspPerm) (a : ℤ) : ∃ (b : ℤ), τ.s a b = 0

noncomputable def AspPerm.sf (τ : AspPerm) : SlipFace

The slipface attached to τ.

The paper writes its values as $s_\tau(a,b)$; in Lean the corresponding value is τ.s a b, and τ.sf packages the same data as a SlipFace.

Equations

• τ.sf = { func := τ.s, χ := τ.χ, a_step := ⋯, b_step := ⋯, nonneg := ⋯, ge_diff := ⋯, small_a := ⋯, large_a := ⋯, small_b := ⋯, large_b := ⋯ }

@[simp]

theorem AspPerm.sf_func_eq_s (τ : AspPerm) : τ.sf.func = τ.s

@[simp]

theorem AspPerm.sf_chi_eq (τ : AspPerm) : τ.sf.χ = τ.χ

theorem AspPerm.sf_dual (τ : AspPerm) : τ.sf.dual = τ⁻¹.sf

theorem AspPerm.Δ_eq (τ : AspPerm) (a b : ℤ) : τ.sf.Δ a b = if τ.func b = a then 1 else 0

theorem AspPerm.Γ_eq (τ : AspPerm) : τ.sf.Γ = {(a, b) : ℤ × ℤ | τ.func b = a}

theorem AspPerm.submodular (τ : AspPerm) : τ.sf.submodular

Ramps, Lamps, and Wing Parameters

This section defines the ramp and lamp regions associated to an ASP permutation and develops the auxiliary wing parameters u and v used to move between inequalities for s and geometric statements about inversion sets.

def AspPerm.ramp (τ : AspPerm) (b : ℤ) : Set (ℤ × ℤ)

The b-ramp of an ASP permutation: the region cut out by the inequality τ.s m n ≥ n - b + 1.

Equations

• τ.ramp b = {(m, n) : ℤ × ℤ | ∃ (l : ℤ), τ.s l b ≥ m ∧ τ.s' b l ≥ n}

def AspPerm.lamp (τ : AspPerm) (a : ℤ) : Set (ℤ × ℤ)

The a-lamp of an ASP permutation, defined as the dual of a ramp.

Equations

• τ.lamp a = {(m, n) : ℤ × ℤ | ∃ (l : ℤ), τ.s a l ≥ m ∧ τ.s' l a ≥ n}

def AspPerm.ramp_closed (τ : AspPerm) (b : ℤ) {m₁ n₁ m₂ n₂ : ℤ} (hm : m₁ ≤ m₂) (hn : n₁ ≤ n₂) : (m₂, n₂) ∈ τ.ramp b → (m₁, n₁) ∈ τ.ramp b

Equations

• ⋯ = ⋯

theorem AspPerm.ramp_lamp_dual (τ : AspPerm) (b m n : ℤ) : (m, n) ∈ τ.ramp b ↔ (n, m) ∈ τ⁻¹.lamp b

theorem AspPerm.mem_ramp_iff_s_ge (τ : AspPerm) (b m n : ℤ) : (m, n) ∈ τ.ramp b ↔ τ.s (b + m - n - τ.χ) b ≥ m

theorem AspPerm.mem_lamp_iff_s_ge (τ : AspPerm) (a m n : ℤ) : (m, n) ∈ τ.lamp a ↔ τ⁻¹.s (a - m + n + τ.χ) a ≥ n

def AspPerm.Wings.R (τ : AspPerm) (b m : ℤ) : Set ℤ

Equations

• AspPerm.Wings.R τ b m = {n : ℤ | τ.s n b < m}

theorem AspPerm.Wings.R_nonempty (τ : AspPerm) (b m : ℤ) (m_pos : m > 0) : (R τ b m).Nonempty

theorem AspPerm.Wings.R_bddAbove (τ : AspPerm) (b m : ℤ) : ∃ (N : ℤ), ∀ n ∈ R τ b m, n ≤ N

def AspPerm.Wings.L (τ : AspPerm) (b n : ℤ) : Set ℤ

Equations

• AspPerm.Wings.L τ b n = {a : ℤ | τ.s' b a ≥ n}

theorem AspPerm.Wings.L_nonnempty (τ : AspPerm) (b n : ℤ) : (L τ b n).Nonempty

theorem AspPerm.Wings.L_bddAbove (τ : AspPerm) (b n : ℤ) (n_pos : n > 0) : ∃ (A : ℤ), ∀ a ∈ L τ b n, A ≥ a

noncomputable def AspPerm.v (τ : AspPerm) (b : ℤ) {m : ℤ} (m_pos : m > 0) : ℤ

Equations

• τ.v b m_pos = τ⁻¹.func (Classical.choose ⋯)

theorem AspPerm.v_spec (τ : AspPerm) (b : ℤ) {m : ℤ} (m_pos : m > 0) : τ.s (τ.func (τ.v b m_pos)) b < m ∧ ∀ (a : ℤ), τ.s a b < m → a ≤ τ.func (τ.v b m_pos)

theorem AspPerm.v_crit (τ : AspPerm) (b : ℤ) {m : ℤ} (m_pos : m > 0) (v : ℤ) : v = τ.v b m_pos ↔ τ.s (τ.func v) b = m - 1 ∧ b ≤ v

theorem AspPerm.s_τv_b (τ : AspPerm) (b : ℤ) {m : ℤ} (m_pos : m > 0) : τ.s (τ.func (τ.v b m_pos)) b = m - 1

theorem AspPerm.v_ge (τ : AspPerm) (b : ℤ) {m : ℤ} (m_pos : m > 0) : b ≤ τ.v b m_pos

theorem AspPerm.τv_lt (τ : AspPerm) (b : ℤ) {m : ℤ} (m_pos : m > 0) {a : ℤ} (s_ge_m : m ≤ τ.s a b) : τ.func (τ.v b m_pos) < a

noncomputable def AspPerm.u (τ : AspPerm) (b : ℤ) {n : ℤ} (n_pos : n > 0) : ℤ

Equations

• τ.u b n_pos = τ⁻¹.func (Classical.choose ⋯)

theorem AspPerm.u_spec (τ : AspPerm) (b : ℤ) {n : ℤ} (n_pos : n > 0) : τ.s' b (τ.func (τ.u b n_pos)) ≥ n ∧ ∀ (a : ℤ), τ.s' b a ≥ n → a ≤ τ.func (τ.u b n_pos)

theorem AspPerm.u_crit (τ : AspPerm) (b : ℤ) {n : ℤ} (n_pos : n > 0) (u : ℤ) : u = τ.u b n_pos ↔ τ.s' b (τ.func u) = n ∧ u < b

theorem AspPerm.s'_b_τu (τ : AspPerm) (b : ℤ) {n : ℤ} (n_pos : n > 0) : τ.s' b (τ.func (τ.u b n_pos)) = n

theorem AspPerm.u_lt (τ : AspPerm) (b : ℤ) {n : ℤ} (n_pos : n > 0) : τ.u b n_pos < b

theorem AspPerm.τu_ge (τ : AspPerm) (b : ℤ) {n : ℤ} (n_pos : n > 0) {a : ℤ} (s_ge_n : n ≤ τ.s' b a) : τ.func (τ.u b n_pos) ≥ a

theorem AspPerm.inv_ramp_correspondence (τ : AspPerm) (b : ℤ) {m n : ℤ} (m_pos : m > 0) (n_pos : n > 0) : (m, n) ∈ τ.ramp b ↔ (τ.u b n_pos, τ.v b m_pos) ∈ inv_set τ.func

A box lies in the ramp exactly when it corresponds to an inversion between the wing parameters u and v.

Weak Order and Demazure Comparison Data

This section introduces the left and right weak orders, the shifted-right map sr, and the comparison predicates used to express Demazure-product inequalities in terms of inversion sets and the functions s and s'.

def AspPerm.le_weak_L (σ τ : AspPerm) : Prop

The left weak order: σ ≤L τ if and only if $\operatorname{Inv} \sigma \subseteq \operatorname{Inv} \tau$.

Equations

• (σ ≤L τ) = (inv_set σ.func ⊆ inv_set τ.func)

def AspPerm.«term_≤L_» : Lean.TrailingParserDescr

Equations

• AspPerm.«term_≤L_» = Lean.ParserDescr.trailingNode `AspPerm.«term_≤L_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≤L ") (Lean.ParserDescr.cat `term 51))

def AspPerm.le_weak_R (σ τ : AspPerm) : Prop

The right weak order: σ ≤R τ if and only if $\operatorname{Inv}(\sigma^{-1}) \subseteq \operatorname{Inv}(\tau^{-1})$.

Equations

• (σ ≤R τ) = (inv_set σ⁻¹.func ⊆ inv_set τ⁻¹.func)

def AspPerm.«term_≤R_» : Lean.TrailingParserDescr

Equations

• AspPerm.«term_≤R_» = Lean.ParserDescr.trailingNode `AspPerm.«term_≤R_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≤R ") (Lean.ParserDescr.cat `term 51))

theorem AspPerm.le_weak_L_of_R {σ τ : AspPerm} (h_R : σ ≤R τ) : σ⁻¹ ≤L τ⁻¹

theorem AspPerm.le_weak_R_of_L {σ τ : AspPerm} (h_L : σ ≤L τ) : σ⁻¹ ≤R τ⁻¹

noncomputable def AspPerm.sr (τ α : AspPerm) : ℤ × ℤ → ℤ × ℤ

Equations

• τ.sr α x = (τ⁻¹.func (α.func x.1), τ⁻¹.func (α.func x.2))

theorem AspPerm.sr_crit (τ α : AspPerm) (u v : ℤ) : (u, v) ∈ τ.sr α '' inv_set α.func ↔ (τ.func v, τ.func u) ∈ inv_set α⁻¹.func

theorem AspPerm.sr_subset (τ α : AspPerm) (h_R : α ≤R τ) : τ.sr α '' inv_set α.func ⊆ inv_set τ.func

def AspPerm.dprod_val_ge (α β : AspPerm) (a b n : ℤ) : Prop

Equations

• α.dprod_val_ge β a b n = ∀ (l : ℤ), α.s a l + β.s l b ≥ n

def AspPerm.le_dprod (τ α β : AspPerm) : Prop

Equations

• τ.le_dprod α β = ∀ (a b : ℤ), α.dprod_val_ge β a b (τ.s a b)

def AspPerm.dprod_val_le (α β : AspPerm) (a b n : ℤ) : Prop

Equations

• α.dprod_val_le β a b n = ∃ (l : ℤ), α.s a l + β.s l b ≤ n

def AspPerm.ge_dprod (τ α β : AspPerm) : Prop

Equations

• τ.ge_dprod α β = ∀ (a b : ℤ), α.dprod_val_le β a b (τ.s a b)

def AspPerm.eq_dprod (τ α β : AspPerm) : Prop

Equations

• τ.eq_dprod α β = (τ.le_dprod α β ∧ τ.ge_dprod α β)

theorem AspPerm.chi_ge_of_dprod_ge {α β τ : AspPerm} (h_ge : τ.le_dprod α β) : α.χ + β.χ ≥ τ.χ

theorem AspPerm.chi_le_of_dprod_le {α β τ : AspPerm} (h_le : τ.ge_dprod α β) : α.χ + β.χ ≤ τ.χ

theorem AspPerm.chi_eq_of_drop_eq {τ α β : AspPerm} (h_eq : τ.eq_dprod α β) : α.χ + β.χ = τ.χ

theorem AspPerm.dprod_inv_eq_inv_dprod (τ α β : AspPerm) (h_eq : τ.eq_dprod α β) : τ⁻¹.eq_dprod β⁻¹ α⁻¹

theorem AspPerm.ramp_dprod_legos (α β : AspPerm) (a b M N : ℤ) (habMN : a - b + α.χ + β.χ = M - N) : α.dprod_val_ge β a b M ↔ ∀ m ∈ Set.Icc 1 M, ∀ n ∈ Set.Icc 1 N, (m, n) ∈ β.ramp b ∨ (M + 1 - m, N + 1 - n) ∈ α.lamp a