structure Valley : Type

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

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

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.