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 LeanPool.DemazureProduct.Valley : Type

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

• f : ℤ → ℤ

  The integer-valued function.

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

  Every sublevel set is finite.

@[implicit_reducible]

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

Equations

• LeanPool.DemazureProduct.instCoeFunValleyForallInt = { coe := LeanPool.DemazureProduct.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 LeanPool.DemazureProduct.Valley.floor (v : Valley) (m : ℤ) : Finset ℤ

The finite sublevel set {n | v n ≤ m}.

Equations

• v.floor m = ⋯.toFinset

@[simp]

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

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

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

The minimum value of a valley.

Equations

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

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

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

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

noncomputable def LeanPool.DemazureProduct.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 LeanPool.DemazureProduct.Valley.f_M (v : Valley) : v.f v.M = v.min

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

def LeanPool.DemazureProduct.Valley.shiftDown (v : Valley) (k : ℤ) : Valley

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

Equations

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

theorem LeanPool.DemazureProduct.Valley.shift_down_M (v : Valley) (k : ℤ) : (v.shiftDown k).M = v.M

Shifting a valley downward does not change its rightmost minimizer.

theorem LeanPool.DemazureProduct.Valley.shift_down_min (v : Valley) (k : ℤ) : (v.shiftDown k).min = v.min - k

Shifting a valley downward subtracts k from its minimum value.