Convex height sequences

A height sequence takes real values on an integer interval and the value infinity outside it. Convexity means that its real increments on consecutive finite heights are nondecreasing. The finite domain may be empty, a singleton, a bounded interval, or a half-line; infinity never supplies a genuine edge slope.

This file proves supporting-line and chord inequalities, including existence of affine minorants through finite heights and separation at infinite heights. It recovers heights from an anchor and consecutive increments, and characterises convexity by second differences. A sequence is admissible when it has a real affine lower bound, which is equivalent to having a convex minorant; a pointwise minimum is admissible exactly when both sequences are. Convexity and admissibility are invariant under adding a real affine function, that is, under height translation and shear, under scaling the heights by a nonnegative real factor, and under translating the indices. Reflecting the indices in N preserves convexity; it discards the heights beyond N. These results provide the discrete geometry used to construct lower convex envelopes without any coefficient data.

The supporting-line and chord arguments are adapted from William Coram's PhD/TauCeti/Code/NewtonPolygons/ConvexSeq.lean at revision eefb3d91f34b27d0bc7822140fa85fecae029884, using real increments on finite edges rather than extended-valued slope sentinels.

def TauCeti.finiteEdges (h : ℕ → WithTop ℝ) : Set ℕ

Indices of consecutive pairs of finite heights. No index outside this set represents a genuine unit edge.

@[simp]

theorem TauCeti.mem_finiteEdges {h : ℕ → WithTop ℝ} {n : ℕ} : n ∈ finiteEdges h ↔ h n ≠ ⊤ ∧ h (n + 1) ≠ ⊤

A unit edge is finite exactly when both endpoint heights are finite.

noncomputable def TauCeti.unitSlope (h : ℕ → WithTop ℝ) (n : ℕ) : ℝ

The real increment between consecutive heights. This quantity is used as an edge slope only when both h n and h (n + 1) are finite. The default value used at infinity has no geometric meaning.

theorem TauCeti.unitSlope_def (h : ℕ → WithTop ℝ) (n : ℕ) : unitSlope h n = (h (n + 1)).untop₀ - (h n).untop₀

The increment is the difference of the real endpoint heights, with zero used for an infinite endpoint. Use it geometrically only on finiteEdges h.

theorem TauCeti.eq_coe_add_sum_unitSlope {h : ℕ → WithTop ℝ} {i j : ℕ} (hj : h j ≠ ⊤) (hij : i ≤ j) : h j = ↑((h i).untop₀ + ∑ n ∈ Finset.Ico i j, unitSlope h n)

A finite height is recovered from any earlier anchor by summing consecutive increments. This identity itself does not require convexity.

structure TauCeti.IsConvexSeq (h : ℕ → WithTop ℝ) : Prop

A height sequence is convex if its finite domain is order connected and its real increments are nondecreasing on the finite edges. The all-infinite sequence and a sequence with just one finite height are allowed.

• ordConnected : {n : ℕ | h n ≠ ⊤}.OrdConnected

  Every index between two finite heights has finite height.

• monotoneOn : MonotoneOn (unitSlope h) (finiteEdges h)

  Only consecutive pairs of finite heights contribute slopes.

theorem TauCeti.isConvexSeq_iff {h : ℕ → WithTop ℝ} : IsConvexSeq h ↔ {n : ℕ | h n ≠ ⊤}.OrdConnected ∧ MonotoneOn (unitSlope h) (finiteEdges h)

Convexity is equivalent to order-connectedness of the finite domain and monotonicity of real increments on finite edges.

theorem TauCeti.ordConnected_finiteEdges {h : ℕ → WithTop ℝ} (hh : {n : ℕ | h n ≠ ⊤}.OrdConnected) : (finiteEdges h).OrdConnected

If the finite domain is order connected, so is the set of finite unit edges.

theorem TauCeti.isConvexSeq_iff_two_mul_le {h : ℕ → WithTop ℝ} : IsConvexSeq h ↔ {n : ℕ | h n ≠ ⊤}.OrdConnected ∧ ∀ (n : ℕ), h n ≠ ⊤ → h (n + 2) ≠ ⊤ → 2 * (h (n + 1)).untop₀ ≤ (h n).untop₀ + (h (n + 2)).untop₀

Convexity is the second-difference inequality at every three consecutive indices whose outer heights are finite, together with order-connectedness of the finite domain.

theorem TauCeti.isConvexSeq_ite {s : Set ℕ} [DecidablePred fun (x : ℕ) => x ∈ s] {f : ℕ → ℝ} (hs : s.OrdConnected) (hf : MonotoneOn (fun (n : ℕ) => f (n + 1) - f n) {n : ℕ | n ∈ s ∧ n + 1 ∈ s}) : IsConvexSeq fun (n : ℕ) => if n ∈ s then ↑(f n) else ⊤

Extending a real sequence by infinity outside an integer interval is convex when its increments on that interval are nondecreasing.

@[simp]

theorem TauCeti.isConvexSeq_top : IsConvexSeq ⊤

The all-infinite height sequence, representing the empty polygon, is convex.

theorem TauCeti.isConvexSeq_affine (c m : ℝ) : IsConvexSeq fun (n : ℕ) => ↑(c + m * ↑n)

Real affine heights form a convex sequence on the whole natural line.

theorem TauCeti.isConvexSeq_affine_ite {s : Set ℕ} [DecidablePred fun (x : ℕ) => x ∈ s] (hs : s.OrdConnected) (c m : ℝ) : IsConvexSeq fun (n : ℕ) => if n ∈ s then ↑(c + m * ↑n) else ⊤

Real affine heights on an order-connected index set, extended by infinity, are convex.

def TauCeti.IsAdmissible (a : ℕ → WithTop ℝ) : Prop

A height sequence is admissible if it has a real affine lower bound. This is the existence condition for a lower convex envelope; the all-infinite sequence, the empty point set, is admissible.

theorem TauCeti.isAdmissible_iff {a : ℕ → WithTop ℝ} : IsAdmissible a ↔ ∃ (c : ℝ) (m : ℝ), ∀ (n : ℕ), ↑(c + m * ↑n) ≤ a n

Admissibility is the existence of a real affine lower bound.

@[simp]

theorem TauCeti.isAdmissible_top : IsAdmissible ⊤

The empty point set is admissible.

theorem TauCeti.IsAdmissible.mono {a b : ℕ → WithTop ℝ} (hb : IsAdmissible b) (hba : b ≤ a) : IsAdmissible a

A sequence lying above an admissible sequence is admissible.

theorem TauCeti.IsAdmissible.inf {a b : ℕ → WithTop ℝ} (ha : IsAdmissible a) (hb : IsAdmissible b) : IsAdmissible (a ⊓ b)

The pointwise minimum of two admissible sequences is admissible: on ℕ, the smaller intercept and the smaller slope give a common real affine lower bound.

@[simp]

theorem TauCeti.isAdmissible_inf_iff {a b : ℕ → WithTop ℝ} : IsAdmissible (a ⊓ b) ↔ IsAdmissible a ∧ IsAdmissible b

A pointwise minimum is admissible exactly when both sequences are.

theorem TauCeti.isAdmissible_of_forall_gt {a : ℕ → WithTop ℝ} {p : ℕ} (hp : ∀ (n : ℕ), p < n → a n = ⊤) : IsAdmissible a

A sequence whose heights are infinite after some index is admissible: a constant below its finitely many finite heights bounds it from below.

theorem TauCeti.IsConvexSeq.ne_top_of_le_of_le {h : ℕ → WithTop ℝ} (hh : IsConvexSeq h) {i j k : ℕ} (hi : h i ≠ ⊤) (hk : h k ≠ ⊤) (hij : i ≤ j) (hjk : j ≤ k) : h j ≠ ⊤

Finiteness propagates between any two finite heights.

theorem TauCeti.IsConvexSeq.mul_slope_le_sub {h : ℕ → WithTop ℝ} (hh : IsConvexSeq h) {i j m : ℕ} (hi : h i ≠ ⊤) (hj : h j ≠ ⊤) (hm : h m ≠ ⊤) (hm' : h (m + 1) ≠ ⊤) (hij : i ≤ j) (hmi : m ≤ i) : ↑(j - i) * unitSlope h m ≤ (h j).untop₀ - (h i).untop₀

Every later secant is bounded below by the slope of a finite edge that precedes it. The length-zero case is included.

theorem TauCeti.IsConvexSeq.sub_le_mul_slope {h : ℕ → WithTop ℝ} (hh : IsConvexSeq h) {i j m : ℕ} (hi : h i ≠ ⊤) (hj : h j ≠ ⊤) (hm : h m ≠ ⊤) (hm' : h (m + 1) ≠ ⊤) (hij : i ≤ j) (hjm : j ≤ m + 1) : (h j).untop₀ - (h i).untop₀ ≤ ↑(j - i) * unitSlope h m

Every earlier secant is bounded above by the slope of a finite edge that follows its last edge. The length-zero case is included.

theorem TauCeti.IsConvexSeq.supportingLine_le {h : ℕ → WithTop ℝ} (hh : IsConvexSeq h) {n : ℕ} (hn : h n ≠ ⊤) (hn' : h (n + 1) ≠ ⊤) (k : ℕ) : ↑((h n).untop₀ + (↑k - ↑n) * unitSlope h n) ≤ h k

The affine line through a finite edge lies below the entire height sequence, including indices outside its finite domain.

theorem TauCeti.IsConvexSeq.chord_inequality {h : ℕ → WithTop ℝ} (hh : IsConvexSeq h) {i j k : ℕ} (hi : h i ≠ ⊤) (hk : h k ≠ ⊤) (hij : i ≤ j) (hjk : j ≤ k) : (↑k - ↑i) * (h j).untop₀ ≤ (↑k - ↑j) * (h i).untop₀ + (↑j - ↑i) * (h k).untop₀

The discrete chord inequality in division-free form. An intermediate finite height lies below the chord joining any two finite endpoints.

theorem TauCeti.IsConvexSeq.eq_affine_of_affine_le {h : ℕ → WithTop ℝ} (hh : IsConvexSeq h) {i j k : ℕ} {c m : ℝ} (hi : h i = ↑(c + m * ↑i)) (hk : h k = ↑(c + m * ↑k)) (hij : i ≤ j) (hjk : j ≤ k) (hj : ↑(c + m * ↑j) ≤ h j) : h j = ↑(c + m * ↑j)

If a convex height sequence passes through two points of a real affine line, then at every intermediate index where it lies on or above that line it lies on the line.

theorem TauCeti.IsConvexSeq.succ_add_succ_le_add {h : ℕ → WithTop ℝ} (hh : IsConvexSeq h) {i k : ℕ} (hik : i ≤ k) : h (i + 1) + h (k + 1) ≤ h i + h (k + 2)

Moving two indices one step towards each other does not increase the sum of their heights: for i ≤ k, the inner pair i + 1, k + 1 has sum at most that of the outer pair i, k + 2. If either outer height is infinite, the bound is trivial.

theorem TauCeti.IsConvexSeq.le_max {h : ℕ → WithTop ℝ} (hh : IsConvexSeq h) {i j k : ℕ} (hij : i ≤ j) (hjk : j ≤ k) : h j ≤ max (h i) (h k)

An intermediate height is at most the larger of two outer heights. If either outer height is infinite, the bound is trivial.

theorem TauCeti.IsConvexSeq.exists_affine_minorant_eq {h : ℕ → WithTop ℝ} (hh : IsConvexSeq h) {n : ℕ} (hn : h n ≠ ⊤) : ∃ (c : ℝ) (σ : ℝ), (∀ (k : ℕ), ↑(c + σ * ↑k) ≤ h k) ∧ c + σ * ↑n = (h n).untop₀

At a finite height of a convex sequence, some real affine minorant passes through that height. This includes isolated finite heights.

theorem TauCeti.IsConvexSeq.isAdmissible {h : ℕ → WithTop ℝ} (hh : IsConvexSeq h) : IsAdmissible h

Every convex height sequence has a real affine lower bound, including the empty and singleton cases.

theorem TauCeti.IsConvexSeq.coe_le_iff_exists_affine_minorant {h : ℕ → WithTop ℝ} (hh : IsConvexSeq h) (n : ℕ) (r : ℝ) : ↑r ≤ h n ↔ ∃ (c : ℝ) (σ : ℝ), (∀ (k : ℕ), ↑(c + σ * ↑k) ≤ h k) ∧ r ≤ c + σ * ↑n

Every real number below a convex height is bounded above by the value of some affine minorant there. Infinite heights are recovered by arbitrarily high minorants, including outside the finite domain and for the empty sequence.

theorem TauCeti.IsConvexSeq.update_of_le {h : ℕ → WithTop ℝ} (hh : IsConvexSeq h) {n : ℕ} {y : ℝ} (hn : h n ≠ ⊤) (hn₂ : h (n + 2) ≠ ⊤) (hy : (h (n + 1)).untop₀ ≤ y) (hbound : 2 * y ≤ (h n).untop₀ + (h (n + 2)).untop₀) : IsConvexSeq (Function.update h (n + 1) ↑y)

Raising an interior height preserves convexity provided the new height stays below the average of its finite neighbors.

theorem TauCeti.IsConvexSeq.ite_le_of_le_of_eq {g h : ℕ → WithTop ℝ} (hg : IsConvexSeq g) (hh : IsConvexSeq h) {p : ℕ} (hle : ∀ n ≤ p, h n ≤ g n) (heq : g p = h p) : IsConvexSeq fun (n : ℕ) => if n ≤ p then g n else h n

Splice two convex sequences where their heights agree, taking the prefix from the sequence lying higher on that prefix. This comparison ensures convexity across the join; no finiteness assumption on the joining height is needed.

theorem TauCeti.IsConvexSeq.ite_le_of_le_of_eq_right {g h : ℕ → WithTop ℝ} (hh : IsConvexSeq h) (hg : IsConvexSeq g) {p : ℕ} (hle : ∀ (n : ℕ), p ≤ n → h n ≤ g n) (heq : h p = g p) : IsConvexSeq fun (n : ℕ) => if n ≤ p then h n else g n

Splice two convex sequences where their heights agree, taking the suffix from the sequence lying higher on that suffix. The comparison preserves convexity across the join, including when the joining height is infinite.

theorem TauCeti.exists_convexSeq_le_iff {a : ℕ → WithTop ℝ} : (∃ (h : ℕ → WithTop ℝ), IsConvexSeq h ∧ h ≤ a) ↔ IsAdmissible a

A height sequence admits a convex minorant exactly when it is admissible, that is, when it admits a real affine lower bound. No nonempty-support hypothesis is needed.

Changes of height scale

@[simp]

theorem TauCeti.finiteEdges_map {h : ℕ → WithTop ℝ} (f : ℝ → ℝ) : (finiteEdges fun (n : ℕ) => WithTop.map f (h n)) = finiteEdges h

Changing the height scale leaves the finite unit edges unchanged.

@[simp]

theorem TauCeti.unitSlope_map {h : ℕ → WithTop ℝ} {F : Type u_1} [FunLike F ℝ ℝ] [AddMonoidHomClass F ℝ ℝ] (f : F) (n : ℕ) : unitSlope (fun (n : ℕ) => WithTop.map (⇑f) (h n)) n = f (unitSlope h n)

Unit increments transform additively with the height scale. This also respects the zero default at infinite heights; only finite edges represent geometric slopes.

theorem TauCeti.IsConvexSeq.map {h : ℕ → WithTop ℝ} (hh : IsConvexSeq h) {F : Type u_1} [FunLike F ℝ ℝ] [AddMonoidHomClass F ℝ ℝ] [OrderHomClass F ℝ ℝ] (f : F) : IsConvexSeq fun (n : ℕ) => WithTop.map (⇑f) (h n)

An ordered additive change of height scale preserves convexity.

@[simp]

theorem TauCeti.isConvexSeq_map_iff {h : ℕ → WithTop ℝ} (e : ℝ ≃+o ℝ) : (IsConvexSeq fun (n : ℕ) => WithTop.map (⇑e) (h n)) ↔ IsConvexSeq h

An ordered additive change of height scale preserves and reflects convexity.

Affine covariance

theorem WithTop.add_affine_add_neg_affine (u : WithTop ℝ) (c m : ℝ) (n : ℕ) : u + ↑(c + m * ↑n) + ↑(-c + -m * ↑n) = u

Adding the affine function with parameters -c and -m undoes adding the one with parameters c and m.

theorem TauCeti.IsConvexSeq.add_affine {h : ℕ → WithTop ℝ} (hh : IsConvexSeq h) (c m : ℝ) : IsConvexSeq fun (n : ℕ) => h n + ↑(c + m * ↑n)

Adding a real affine function preserves convexity. With m = 0 this is a height translation; with c = 0 it is a shear.

@[simp]

theorem TauCeti.isConvexSeq_add_affine_iff {h : ℕ → WithTop ℝ} (c m : ℝ) : (IsConvexSeq fun (n : ℕ) => h n + (↑c + ↑m * ↑n)) ↔ IsConvexSeq h

Adding a real affine function does not change convexity. The affine function is written with its coercions pushed outward, which is the simp normal form.

theorem TauCeti.IsAdmissible.add_affine {a : ℕ → WithTop ℝ} (ha : IsAdmissible a) (c m : ℝ) : IsAdmissible fun (n : ℕ) => a n + ↑(c + m * ↑n)

Adding a real affine function preserves admissibility.

@[simp]

theorem TauCeti.isAdmissible_add_affine_iff {a : ℕ → WithTop ℝ} (c m : ℝ) : (IsAdmissible fun (n : ℕ) => a n + (↑c + ↑m * ↑n)) ↔ IsAdmissible a

Adding a real affine function does not change admissibility. The affine function is written with its coercions pushed outward, which is the simp normal form.

theorem TauCeti.finiteEdges_add_affine (h : ℕ → WithTop ℝ) (c m : ℝ) : (finiteEdges fun (n : ℕ) => h n + ↑(c + m * ↑n)) = finiteEdges h

Adding a real affine function does not change the finite unit edges.

theorem TauCeti.unitSlope_add_affine {h : ℕ → WithTop ℝ} {n : ℕ} (hn : n ∈ finiteEdges h) (c m : ℝ) : unitSlope (fun (n : ℕ) => h n + ↑(c + m * ↑n)) n = unitSlope h n + m

Adding the real affine function with slope m adds m to the slope of every finite unit edge.

Scaling of heights

theorem TauCeti.IsConvexSeq.map_mul {h : ℕ → WithTop ℝ} (hh : IsConvexSeq h) {c : ℝ} (hc : 0 ≤ c) : IsConvexSeq fun (n : ℕ) => WithTop.map (fun (x : ℝ) => c * x) (h n)

Scaling the heights by a nonnegative real factor preserves convexity.

theorem TauCeti.IsAdmissible.map_mul {a : ℕ → WithTop ℝ} (ha : IsAdmissible a) {c : ℝ} (hc : 0 ≤ c) : IsAdmissible fun (n : ℕ) => WithTop.map (fun (x : ℝ) => c * x) (a n)

Scaling the heights by a nonnegative real factor preserves admissibility.

Translation of indices

theorem TauCeti.IsConvexSeq.comp_add_right {h : ℕ → WithTop ℝ} (hh : IsConvexSeq h) (k : ℕ) : IsConvexSeq fun (n : ℕ) => h (n + k)

Dropping the first k heights preserves convexity.

theorem TauCeti.IsConvexSeq.shift {h : ℕ → WithTop ℝ} (hh : IsConvexSeq h) (k : ℕ) : IsConvexSeq fun (n : ℕ) => if k ≤ n then h (n - k) else ⊤

Shifting heights k places to the right, with infinite heights at the first k indices, preserves convexity.

theorem TauCeti.isAdmissible_shift_iff {a : ℕ → WithTop ℝ} (k : ℕ) : (IsAdmissible fun (n : ℕ) => if k ≤ n then a (n - k) else ⊤) ↔ IsAdmissible a

Shifting a sequence k places to the right, with infinite heights at the first k indices, does not change admissibility.

theorem TauCeti.finiteEdges_shift (h : ℕ → WithTop ℝ) (k : ℕ) : (finiteEdges fun (n : ℕ) => if k ≤ n then h (n - k) else ⊤) = (fun (x : ℕ) => x + k) '' finiteEdges h

Shifting heights k places to the right, with infinite heights at the first k indices, shifts the finite unit edges k places to the right.

@[simp]

theorem TauCeti.unitSlope_shift (h : ℕ → WithTop ℝ) (k n : ℕ) : unitSlope (fun (n : ℕ) => if k ≤ n then h (n - k) else ⊤) (n + k) = unitSlope h n

Shifting heights k places to the right, with infinite heights at the first k indices, moves every unit slope k places to the right.

Reflection of indices

theorem TauCeti.IsConvexSeq.reflect {h : ℕ → WithTop ℝ} (hh : IsConvexSeq h) (N : ℕ) : IsConvexSeq fun (n : ℕ) => if n ≤ N then h (N - n) else ⊤

Reflecting heights in N, with infinite heights beyond N, preserves convexity. The heights of h beyond N are discarded.

theorem TauCeti.finiteEdges_reflect {h : ℕ → WithTop ℝ} {N : ℕ} (hh : ∀ (n : ℕ), N < n → h n = ⊤) : (finiteEdges fun (n : ℕ) => if n ≤ N then h (N - n) else ⊤) = (fun (x : ℕ) => N - 1 - x) '' finiteEdges h

Reflecting heights in N, when they are infinite beyond N, reverses the finite unit edges: the edge [m, m + 1] moves to [N - 1 - m, N - m].

@[simp]

theorem TauCeti.unitSlope_reflect (h : ℕ → WithTop ℝ) {N n : ℕ} (hn : n < N) : unitSlope (fun (n : ℕ) => if n ≤ N then h (N - n) else ⊤) n = -unitSlope h (N - 1 - n)

Reflecting heights in N negates the unit slopes and reverses their order.