Documentation

instance instCoeFunSlipFaceForallIntForall :

CoeFun SlipFace fun (x : SlipFace) => ℤ → ℤ → ℤ

Equations

instCoeFunSlipFaceForallIntForall = { coe := SlipFace.func }

theorem SF_ext (s t : SlipFace) :

s = t ↔ ∀ (a b : ℤ), s.func a b = t.func a b

def SlipFace.dual (sf : SlipFace) :

The dual slipface $s^\vee$, characterized by $$ s(a,b) - s^\vee(b,a) = \chi + a - b. $$

In Lean the dual is sf.dual, and its value at (b,a) is written sf.dual b a. Definition 3.4 (defn:sdual).

Equations

sf.dual = { func := fun (b a : ℤ) => sf.func a b - a + b - sf.χ, χ := -sf.χ, a_step := ⋯, b_step := ⋯, nonneg := ⋯, ge_diff := ⋯, small_a := ⋯, large_a := ⋯, small_b := ⋯, large_b := ⋯ }

Instances For

theorem SlipFace.dual_dual (s : SlipFace) :

s.dual.dual = s

theorem SlipFace.duality (sf : SlipFace) (a b : ℤ) :

sf.func a b - sf.dual.func b a = a - b + sf.χ

theorem SlipFace.s_eq (sf : SlipFace) (a b : ℤ) :

sf.func a b = a - b + sf.χ + sf.dual.func b a

theorem SlipFace.s'_eq (sf : SlipFace) (b a : ℤ) :

sf.dual.func b a = sf.func a b - a + b - sf.χ

structure SlipFace.D_props (f : ℤ → ℤ → ℤ) :

Prop

The one-sided monotonicity and vanishing conditions providing a simplified criterion for slipfaces.

These are the paper's conditions (D1) and (D2), extracted into a reusable Lean structure. Properties D1 and D2.

a_step (a b : ℤ) : f (a + 1) b ≥ f a b
b_step (a b : ℤ) : f a (b + 1) ≤ f a b
large_b (a : ℤ) : ∃ (B : ℤ), ∀ b ≥ B, f a b = 0
small_a (b : ℤ) : ∃ (A : ℤ), ∀ a ≤ A, f a b = 0

Instances For

theorem SlipFace.mono_a_of_D_props (f : ℤ → ℤ → ℤ) (h : D_props f) (a a' b : ℤ) :

a ≤ a' → f a' b ≥ f a b

theorem SlipFace.mono_b_of_D_props (f : ℤ → ℤ → ℤ) (h : D_props f) (a b b' : ℤ) :

b ≤ b' → f a b' ≤ f a b

theorem SlipFace.sf_of_D_props {s t : ℤ → ℤ → ℤ} {χ : ℤ} (h : ∀ (a b : ℤ), s a b - t b a = a - b + χ) :

D_props s ∧ D_props t → ∃ (sf : SlipFace), (sf.func = s ∧ sf.χ = χ) ∧ sf.dual.func = t

Construct a slipface from a pair of functions satisfying D_props and the duality relation s a b - t b a = a - b + χ. Lemma 3.6 (lem:dualCrit).

theorem SlipFace.D_props_of_sf (sf : SlipFace) :

D_props sf.func ∧ D_props sf.dual.func

theorem SlipFace.nondec (sf : SlipFace) {a a' b b' : ℤ} (a_le_a' : a ≤ a') (b'_le_b : b' ≤ b) :

sf.func a b ≤ sf.func a' b'

theorem SlipFace.zero_below (sf : SlipFace) {a a' b b' : ℤ} (a_le_a' : a ≤ a') (b'_le_b : b' ≤ b) :

sf.func a' b' = 0 → sf.func a b = 0

Slip Valleys and the Product Formula #

A Valley is an integer function rising on both sides, which therefore has a well-defined minimum achieved at finitely many places.

This section packages the minimization problem defining slipface product into a Valley, then uses it to construct the product s ⋆ t and prove its basic properties.

noncomputable def SlipFace.SlipValley (s t : SlipFace) (a b : ℤ) :

Valley

The valley $\ell \mapsto s(a,\ell) + t(\ell,b)$ whose minimum computes the slipface product at (a,b).

Equations

s.SlipValley t a b = { f := fun (l : ℤ) => s.func a l + t.func l b, rises := ⋯ }

Instances For

noncomputable def SlipFace.star_func (s t : SlipFace) :

ℤ → ℤ → ℤ

The min-plus product formula $$ (s \star t)(a,b) = \min_{\ell \in \mathbb{Z}} [s(a,\ell) + t(\ell,b)]. $$

In Lean, star_func s t a b is this integer value, while s ⋆ t is the resulting SlipFace. Definition 3.7 (defn:sfAlgebra), part 1/3.

Equations

s.star_func t a b = (s.SlipValley t a b).min

Instances For

theorem SlipFace.star_dual_ineq (s t : SlipFace) (a b : ℤ) :

t.dual.star_func s.dual b a ≤ s.star_func t a b - a + b - s.χ - t.χ

theorem SlipFace.star_dual_eq (s t : SlipFace) (a b : ℤ) :

s.star_func t a b - t.dual.star_func s.dual b a = a - b + s.χ + t.χ

theorem SlipFace.D_props_of_star_func (s t : SlipFace) :

D_props (s.star_func t)

theorem SlipFace.star_exists (s t : SlipFace) :

∃ (p : SlipFace), (p.func = s.star_func t ∧ p.χ = s.χ + t.χ) ∧ p.dual.func = t.dual.star_func s.dual

The product function star_func s t comes from a slipface of shift s.χ + t.χ. Proposition 3.9 (prop:sfAlgebraDefined), part 1/5.

noncomputable def SlipFace.star (s t : SlipFace) :

The product of two slipfaces, obtained from the minimum formula star_func.

Equations

s ⋆ t = Classical.choose ⋯

Instances For

noncomputable instance SlipFace.instMul :

Mul SlipFace

Equations

SlipFace.instMul = { mul := SlipFace.star }

def SlipFace.«term_⋆_» :

Lean.TrailingParserDescr

Equations

SlipFace.«term_⋆_» = Lean.ParserDescr.trailingNode `SlipFace.«term_⋆_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⋆ ") (Lean.ParserDescr.cat `term 71))

Instances For

theorem SlipFace.star_func_eq (s t : SlipFace) :

(s ⋆ t).func = s.star_func t

@[simp]

theorem SlipFace.chi_star (s t : SlipFace) :

(s ⋆ t).χ = s.χ + t.χ

@[simp]

theorem SlipFace.star_dual (s t : SlipFace) :

(s ⋆ t).dual = t.dual ⋆ s.dual

Duality reverses the product ⋆. Proposition 3.9 (prop:sfAlgebraDefined), part 4/5.

Order Structure and Comparison with `⋆` #

This section puts the pointwise order on SlipFace and records the basic comparison lemmas relating that order to the product ⋆. The order is the paper's Bruhat order on slipfaces. Definition 3.2.

instance SlipFace.instPartialOrder :

PartialOrder SlipFace

Equations

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

theorem SlipFace.star_val_le (s t : SlipFace) (a b l : ℤ) :

(s ⋆ t).func a b ≤ s.func a l + t.func l b

noncomputable def SlipFace.star_wit (s t : SlipFace) (a b : ℤ) :

Equations

s.star_wit t a b = (s.SlipValley t a b).M

Instances For

theorem SlipFace.star_wit_spec (s t : SlipFace) (a b : ℤ) :

(s ⋆ t).func a b = s.func a (s.star_wit t a b) + t.func (s.star_wit t a b) b

theorem SlipFace.le_star_val_iff (r s t : SlipFace) (a b : ℤ) :

r.func a b ≤ (s ⋆ t).func a b ↔ ∀ (l : ℤ), r.func a b ≤ s.func a l + t.func l b

A lower bound for (s ⋆ t) a b is equivalent to a uniform lower bound against every witness l.

theorem SlipFace.ge_star_val_iff (r s t : SlipFace) (a b : ℤ) :

r.func a b ≥ (s ⋆ t).func a b ↔ ∃ (l : ℤ), r.func a b ≥ s.func a l + t.func l b

An upper bound for (s ⋆ t) a b is equivalent to exhibiting a single witness l that realizes it.

Monoid Structure #

The product ⋆ is associative and has the positive-part function as identity, giving SlipFace a monoid structure.

theorem SlipFace.star_assoc (r s t : SlipFace) :

r ⋆ s ⋆ t = r ⋆ (s ⋆ t)

Slipface product is associative. Lemma 3.11 (lem:sfAlgebra), part 1/3.

def SlipFace.id :

The identity slipface, given by the positive part of a - b.

Equations

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

Instances For

theorem SlipFace.id_mul (s : SlipFace) :

id ⋆ s = s

theorem SlipFace.mul_id (s : SlipFace) :

s ⋆ id = s

noncomputable instance SlipFace.instMonoid :

Monoid SlipFace

Equations

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

The contraction operations `◃` and `▹` #

This section develops the basic properties of the operations $s \triangleleft t$ and $s \triangleright t$ at the level of slipface functions.

theorem SlipFace.left_contraction_exists (s t : SlipFace) (a b : ℤ) :

∃ (m : ℤ), ∀ (l : ℤ), s.func a l - t.dual.func b l ≤ s.func a m - t.dual.func b m

noncomputable def SlipFace.lc_wit (s t : SlipFace) (a b : ℤ) :

The argmax witnessing the left contraction value $s \triangleleft t (a,b)$.

Equations

s.lc_wit t a b = Classical.choose ⋯

Instances For

noncomputable def SlipFace.lc_func (s t : SlipFace) :

ℤ → ℤ → ℤ

The left contraction function $$ (s \triangleleft t)(a,b) = \max_{\ell \in \mathbb{Z}} \bigl[s(a,\ell) - t^\vee(b,\ell)\bigr]. $$ Definition 3.7 (defn:sfAlgebra), part 2/3.

Equations

s.lc_func t a b = s.func a (s.lc_wit t a b) - t.dual.func b (s.lc_wit t a b)

Instances For

theorem SlipFace.lc_val_ge (s t : SlipFace) (a b l : ℤ) :

s.func a l - t.dual.func b l ≤ s.lc_func t a b

Every value $s(a,\ell) - t^\vee(b,\ell)$ is at most $s \triangleleft t (a,b)$.

theorem SlipFace.lc_func_nonneg (s t : SlipFace) (a b : ℤ) :

0 ≤ s.lc_func t a b

The left contraction is nonnegative, since for l ≫ 0 both terms in the maximizing expression vanish.

theorem SlipFace.D_props_of_lc_func (s t : SlipFace) :

D_props (s.lc_func t)

The left contraction function $s \triangleleft t$ satisfies D_props. Proposition 3.9 (prop:sfAlgebraDefined), proof component for part 2/5.

theorem SlipFace.right_contraction_exists (s t : SlipFace) (a b : ℤ) :

∃ (m : ℤ), ∀ (l : ℤ), t.func l b - s.dual.func l a ≤ t.func m b - s.dual.func m a

noncomputable def SlipFace.rc_wit (s t : SlipFace) (a b : ℤ) :

The argmax witnessing the right contraction value $s \triangleright t (a,b)$.

Equations

s.rc_wit t a b = Classical.choose ⋯

Instances For

noncomputable def SlipFace.rc_func (s t : SlipFace) :

ℤ → ℤ → ℤ

The right contraction function $$ (s \triangleright t)(a,b) = \max_{\ell \in \mathbb{Z}} \bigl[t(\ell,b) - s^\vee(\ell,a)\bigr]. $$ Definition 3.7 (defn:sfAlgebra), part 3/3.

Equations

s.rc_func t a b = t.func (s.rc_wit t a b) b - s.dual.func (s.rc_wit t a b) a

Instances For

theorem SlipFace.rc_val_ge (s t : SlipFace) (a b l : ℤ) :

t.func l b - s.dual.func l a ≤ s.rc_func t a b

Every value $t(\ell,b) - s^\vee(\ell,a)$ is at most $s \triangleright t (a,b)$.

theorem SlipFace.rc_func_nonneg (s t : SlipFace) (a b : ℤ) :

0 ≤ s.rc_func t a b

The right contraction is nonnegative, since for l ≪ 0 both terms in the maximizing expression vanish.

theorem SlipFace.D_props_of_rc_func (s t : SlipFace) :

D_props (s.rc_func t)

The right contraction function $s \triangleright t$ satisfies D_props. Proposition 3.9 (prop:sfAlgebraDefined), proof component for part 3/5.

theorem SlipFace.lc_rc_dual_eq (s t : SlipFace) (a b : ℤ) :

s.lc_func t a b - t.dual.rc_func s.dual b a = a - b + s.χ + t.χ

The left contraction is dual to the right contraction. Proposition 3.9 (prop:sfAlgebraDefined), proof component for part 5/5.

theorem SlipFace.lc_exists (s t : SlipFace) :

∃ (p : SlipFace), (p.func = s.lc_func t ∧ p.χ = s.χ + t.χ) ∧ p.dual.func = t.dual.rc_func s.dual

The function lc_func s t satisfies the slipface axioms and therefore comes from a slipface. Proposition 3.9 (prop:sfAlgebraDefined), part 2/5.

noncomputable def SlipFace.left_contract (s t : SlipFace) :

The left contraction of two slipfaces, obtained from the maximum formula lc_func. Proposition 3.9 (prop:sfAlgebraDefined), part 2/5.

Equations

s ◃ t = Classical.choose ⋯

Instances For

def SlipFace.«term_◃_» :

Lean.TrailingParserDescr

Equations

SlipFace.«term_◃_» = Lean.ParserDescr.trailingNode `SlipFace.«term_◃_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ◃ ") (Lean.ParserDescr.cat `term 71))

Instances For

theorem SlipFace.lc_func_eq (s t : SlipFace) :

(s ◃ t).func = s.lc_func t

theorem SlipFace.lc_wit_spec (s t : SlipFace) (a b : ℤ) :

(s ◃ t).func a b = s.func a (s.lc_wit t a b) - t.dual.func b (s.lc_wit t a b)

@[simp]

theorem SlipFace.chi_lc (s t : SlipFace) :

(s ◃ t).χ = s.χ + t.χ

noncomputable def SlipFace.right_contract (s t : SlipFace) :

The right contraction of two slipfaces, defined by duality from left contraction. Proposition 3.9 (prop:sfAlgebraDefined), part 3/5.

Equations

s ▹ t = (t.dual ◃ s.dual).dual

Instances For

def SlipFace.«term_▹_» :

Lean.TrailingParserDescr

Equations

SlipFace.«term_▹_» = Lean.ParserDescr.trailingNode `SlipFace.«term_▹_» 70 71 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ▹ ") (Lean.ParserDescr.cat `term 70))

Instances For

theorem SlipFace.rc_func_eq (s t : SlipFace) :

(s ▹ t).func = s.rc_func t

theorem SlipFace.rc_wit_spec (s t : SlipFace) (a b : ℤ) :

(s ▹ t).func a b = t.func (s.rc_wit t a b) b - s.dual.func (s.rc_wit t a b) a

@[simp]

theorem SlipFace.chi_rc (s t : SlipFace) :

(s ▹ t).χ = s.χ + t.χ

@[simp]

theorem SlipFace.left_contract_dual (s t : SlipFace) :

(s ◃ t).dual = t.dual ▹ s.dual

The stated left/right contraction duality. Proposition 3.9 (prop:sfAlgebraDefined), part 5/5.

@[simp]

theorem SlipFace.right_contract_dual (s t : SlipFace) :

(s ▹ t).dual = t.dual ◃ s.dual

The corresponding right/left contraction duality, obtained by applying the left/right duality to dual slipfaces. Consequence of Proposition 3.9 (prop:sfAlgebraDefined), part 5/5.

def SlipFace.bend_set (t : SlipFace) (b : ℤ) :

Set ℤ

Equations

t.bend_set b = {l : ℤ | t.func (l - 1) b = t.func l b ∧ t.func l b ≠ t.func (l + 1) b}

Instances For

theorem SlipFace.bend_set_finite (t : SlipFace) (b : ℤ) :

Finite ↑(t.bend_set b)

@[irreducible]

theorem SlipFace.bend_set_witness_helper (s t : SlipFace) (a b l : ℤ) (hl : t.func l b ≠ t.func (l + 1) b) :

∃ (m : ℤ), t.func (m - 1) b = t.func m b ∧ t.func m b ≠ t.func (m + 1) b ∧ s.func a m + t.func m b ≤ s.func a l + t.func l b

theorem SlipFace.bend_set_witness (s t : SlipFace) (a b : ℤ) :

∃ l ∈ t.bend_set b, (s ⋆ t).func a b = s.func a l + t.func l b

@[irreducible]

theorem SlipFace.bend_set_witness_lc_right_helper (s t : SlipFace) (a b l : ℤ) (hmax : ∀ (n : ℤ), s.func a n - t.dual.func b n ≤ s.func a l - t.dual.func b l) :

∃ (m : ℤ), t.func m b ≠ t.func (m + 1) b ∧ s.func a l - t.dual.func b l ≤ s.func a m - t.dual.func b m

@[irreducible]

theorem SlipFace.bend_set_witness_lc_helper (s t : SlipFace) (a b l : ℤ) (hl : t.func l b ≠ t.func (l + 1) b) :

∃ (m : ℤ), t.func (m - 1) b = t.func m b ∧ t.func m b ≠ t.func (m + 1) b ∧ s.func a l - t.dual.func b l ≤ s.func a m - t.dual.func b m

theorem SlipFace.bend_set_witness_lc (s t : SlipFace) (a b : ℤ) :

∃ l ∈ t.bend_set b, (s ◃ t).func a b = s.func a l - t.dual.func b l

theorem SlipFace.star_mono {s₁ s₂ t₁ t₂ : SlipFace} (hs : s₁ ≤ s₂) (ht : t₁ ≤ t₂) :

s₁ ⋆ t₁ ≤ s₂ ⋆ t₂

The $\star$ operation is Bruhat-increasing in both arguments. Lemma 3.8 (lem:compatLeq), part 1/3.

theorem SlipFace.left_contract_mono {s₁ s₂ t₁ t₂ : SlipFace} (hs : s₁ ≤ s₂) (ht : t₁ ≤ t₂) :

s₁ ◃ t₂.dual ≤ s₂ ◃ t₁.dual

The contraction (s, t) ↦ s ◃ t.dual is increasing in s and decreasing in t. Lemma 3.8 (lem:compatLeq), part 2/3.

theorem SlipFace.right_contract_mono {s₁ s₂ t₁ t₂ : SlipFace} (hs : s₁ ≤ s₂) (ht : t₁ ≤ t₂) :

t₂.dual ▹ s₁ ≤ t₁.dual ▹ s₂

The contraction (s, t) ↦ t.dual ▹ s is increasing in s and decreasing in t. Lemma 3.8 (lem:compatLeq), part 3/3.

theorem SlipFace.ge_star_iff_ge_left_contract (s t u : SlipFace) :

s ≥ u ◃ t.dual ↔ s ⋆ t ≥ u

The left contraction $u \triangleleft t^∨$ as a Bruhat minimum: the minimum slipface such that $s \star t ≥ u$. Lemma 3.10 (lem:sfOpChar), part 1/2.

theorem SlipFace.ge_star_iff_ge_right_contract (s t u : SlipFace) :

t ≥ s.dual ▹ u ↔ s ⋆ t ≥ u

The right contraction $s^∨ \triangleright u$ as a Bruhat minimum: the minimum slipface such that $s \star t ≥ u$. Lemma 3.10 (lem:sfOpChar), part 2/2.

theorem SlipFace.left_contract_assoc (s t u : SlipFace) :

s ◃ t ◃ u = s ◃ (t ⋆ u)

Left contraction associates with the product on the right. Lemma 3.11 (lem:sfAlgebra), part 2/3.

theorem SlipFace.right_contract_assoc (s t u : SlipFace) :

s ▹ t ▹ u = (s ⋆ t) ▹ u

Right contraction associates with the product on the left. Lemma 3.11 (lem:sfAlgebra), part 3/3.

The Mixed Difference `Δ` #

This section studies the discrete mixed difference Δ, its behavior under duality, and the finite summation identities used later in submodularity arguments.

def SlipFace.Δ (sf : SlipFace) (a b : ℤ) :

The mixed difference $$ \Delta s(a,b) = s(a+1,b) - s(a,b) - s(a+1,b+1) + s(a,b+1). $$

In Lean this is written sf.Δ a b.

Equations

sf.Δ a b = sf.func (a + 1) b - sf.func a b - sf.func (a + 1) (b + 1) + sf.func a (b + 1)

Instances For

theorem SlipFace.Δ_dual (sf : SlipFace) (a b : ℤ) :

sf.dual.Δ b a = sf.Δ a b

Duality preserves the mixed difference Δ after swapping the coordinates. Equation (18).

theorem SlipFace.Δ_values (sf : SlipFace) (a b : ℤ) :

sf.Δ a b = 0 ∨ sf.Δ a b = 1 ∨ sf.Δ a b = -1

theorem SlipFace.Δ_zero_of_s_zero (sf : SlipFace) (a b : ℤ) (h0 : sf.func (a + 1) b = 0) :

sf.Δ a b = 0

theorem SlipFace.sum_a (sf : SlipFace) {a₁ a₂ : ℤ} (ha : a₁ ≤ a₂) (b : ℤ) :

∑ a ∈ Finset.Ico a₁ a₂, sf.Δ a b = sf.func a₂ b - sf.func a₂ (b + 1) - (sf.func a₁ b - sf.func a₁ (b + 1))

theorem SlipFace.sum_b (sf : SlipFace) (a : ℤ) {b₁ b₂ : ℤ} (hb : b₁ ≤ b₂) :

∑ b ∈ Finset.Ico b₁ b₂, sf.Δ a b = sf.func (a + 1) b₁ - sf.func a b₁ - (sf.func (a + 1) b₂ - sf.func a b₂)

theorem SlipFace.sum_ab (sf : SlipFace) {a₁ a₂ b₁ b₂ : ℤ} (ha : a₁ ≤ a₂) (hb : b₁ ≤ b₂) :

∑ b ∈ Finset.Ico b₁ b₂, ∑ a ∈ Finset.Ico a₁ a₂, sf.Δ a b = sf.func a₂ b₁ - sf.func a₁ b₁ - (sf.func a₂ b₂ - sf.func a₁ b₂)

Summing Δ over a rectangle recovers the corresponding boundary term in sf. Modification of Equation (17) to a finite sum.

def SlipFace.submodular (sf : SlipFace) :

Prop

A slipface is submodular if $\Delta s(a,b) \ge 0$ for all a, b. Definition 4.2 (defn:submodular).

Equations

sf.submodular = ∀ (a b : ℤ), sf.Δ a b ≥ 0

Instances For

def SlipFace.Γ (sf : SlipFace) :

Set (ℤ × ℤ)

The set of boxes where the mixed difference Δ is equal to 1.

Equations

sf.Γ = {(a, b) : ℤ × ℤ | sf.Δ a b = 1}

Instances For