Valleys

A valley is a function f : ℤ → ℤ tending to positive infinity on both sides. This terminology is not used in An extended Demazure product; it is introduced here in order to package some elementary arguments that are needed about such functions. In particular, we need to keep track of the set where the minimum value is achieved, and some facts about how this set changes when the valley is modified in simple ways.

structure Valley : Type

A function on ℤ whose sublevel sets are finite. This is the abstraction used to talk about minima and rightmost minimizers.

• f : ℤ → ℤ
• rises (m : ℤ) : {n : ℤ | self.f n ≤ m}.Finite

@[implicit_reducible]

instance instCoeFunValleyForallInt : CoeFun Valley fun (x : Valley) => ℤ → ℤ

Equations

• instCoeFunValleyForallInt = { coe := Valley.f }

Minima and rightmost minimizers

This namespace develops the basic API for working with a Valley: its minimum value, the rightmost index where that minimum is attained, and behavior under vertical shifts.

noncomputable def Valley.floor (v : Valley) (m : ℤ) : Finset ℤ

Equations

• v.floor m = ⋯.toFinset

@[simp]

theorem Valley.mem_floor (v : Valley) (m n : ℤ) : n ∈ v.floor m ↔ v.f n ≤ m

theorem Valley.floor_image_nonempty (v : Valley) (n : ℤ) : (Finset.image v.f (v.floor (v.f n))).Nonempty

noncomputable def Valley.min (v : Valley) : ℤ

The minimum value of a valley.

Equations

• v.min = (Finset.image v.f (v.floor (v.f 0))).min' ⋯

theorem Valley.min_mem (v : Valley) : ∃ a ∈ {n : ℤ | v.f n ≤ v.f 0}, v.f a = v.min

theorem Valley.min_spec (v : Valley) (n : ℤ) : v.f n ≥ v.min

theorem Valley.argmin_set_nonempty (v : Valley) : (v.floor v.min).Nonempty

noncomputable def Valley.M (v : Valley) : ℤ

The largest index at which the minimum of the valley is attained.

Equations

• v.M = (v.floor v.min).max' ⋯

theorem Valley.f_M (v : Valley) : v.f v.M = v.min

theorem Valley.M_spec (v : Valley) (n : ℤ) : v.f n ≥ v.f v.M ∧ (n > v.M → v.f n > v.f v.M)

def Valley.shift_down (v : Valley) (k : ℤ) : Valley

Shift every value of a valley downward by the constant k.

Equations

• v.shift_down k = { f := fun (n : ℤ) => v.f n - k, rises := ⋯ }

theorem Valley.shift_down_M (v : Valley) (k : ℤ) : (v.shift_down k).M = v.M

Shifting a valley downward does not change its rightmost minimizer.

theorem Valley.shift_down_min (v : Valley) (k : ℤ) : (v.shift_down k).min = v.min - k

Shifting a valley downward subtracts k from its minimum value.