structure SlipFace : Type

A slipface function of shift χ, i.e. a function $s : \mathbb{Z}^2 \to \mathbb{N}$ satisfying the paper's conditions (S1) to (S3):

• first differences in the a- and b-directions are in {0,1}
• $s(a,b) \ge \max\{0, \chi + a - b\}$
• each row and column eventually agrees with $\max\{0, \chi + a - b\}$

Lean stores the function as func and the shift as χ; the paper would write this as $s \in \mathrm{SF}_\chi$. Definition 3.1.

• func : ℤ → ℤ → ℤ
• χ : ℤ
• a_step (a b : ℤ) : self.func a b ≤ self.func (a + 1) b ∧ self.func (a + 1) b ≤ self.func a b + 1
• b_step (a b : ℤ) : self.func a (b + 1) ≤ self.func a b ∧ self.func a b ≤ self.func a (b + 1) + 1
• nonneg (a b : ℤ) : self.func a b ≥ 0
• ge_diff (a b : ℤ) : self.func a b ≥ a - b + self.χ
• small_a (b : ℤ) : ∃ (A : ℤ), ∀ a ≤ A, self.func a b = 0
• large_a (b : ℤ) : ∃ (A : ℤ), ∀ a ≥ A, self.func a b = a - b + self.χ
• small_b (a : ℤ) : ∃ (B : ℤ), ∀ b ≤ B, self.func a b = a - b + self.χ
• large_b (a : ℤ) : ∃ (B : ℤ), ∀ b ≥ B, self.func a b = 0

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) : 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.

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 := ⋯ }

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

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.

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 := ⋯ }

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.

Equations

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

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 function star_func s t satisfies the slipface axioms and therefore comes from a slipface.

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

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

Equations

• s ⋆ t = Classical.choose ⋯

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))

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

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 ⋆.

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

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.

def SlipFace.id : SlipFace

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

Equations

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

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 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)

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.

Equations

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

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}

theorem SlipFace.Γ_dual (sf : SlipFace) (a b : ℤ) : (a, b) ∈ sf.Γ ↔ (b, a) ∈ sf.dual.Γ