Lower convex envelopes of height sequences

Suprema of convex height sequences are convex, so every height sequence a with a real affine lower bound has a greatest convex minorant, its lower convex envelope. Newton polygons are the lower convex envelopes of coefficient valuations; this file contains the construction-independent geometry, with no coefficient data.

The predicate IsLowerConvexEnvelope a h says that h is convex, lies below a, and dominates every convex minorant of a. It determines h uniquely, and it is satisfied by some h exactly when a is admissible. The total function lowerConvexEnvelope a is the pointwise supremum of the convex minorants when a is admissible, and the all-infinite sequence otherwise. That fallback is not an envelope of the inadmissible input: geometric conclusions about lowerConvexEnvelope a assume IsAdmissible a.

Main results

• IsConvexSeq.of_isLUB: a least upper bound of a family of convex height sequences is convex; IsConvexSeq.sup and IsConvexSeq.iSup are the binary and indexed cases.
• isLowerConvexEnvelope_lowerConvexEnvelope: an admissible sequence has lowerConvexEnvelope a as its lower convex envelope.
• exists_isLowerConvexEnvelope_iff: a lower convex envelope exists exactly for admissible sequences.
• le_lowerConvexEnvelope_iff: a convex sequence lies below the envelope of a exactly when it lies below a.
• lowerConvexEnvelope_mono and lowerConvexEnvelope_idem: the envelope is monotone on admissible inputs and idempotent.
• lowerConvexEnvelope_inf_lowerConvexEnvelope: the envelope of the pointwise minimum of two admissible sequences depends only on their envelopes.
• lowerConvexEnvelope_ne_top_iff: the finite domain of an admissible envelope is the integer convex hull of the finite indices of the sequence.
• lowerConvexEnvelope_eq_of_forall_lt and lowerConvexEnvelope_eq_of_forall_gt: the envelope passes through the first point and, when there is one, the last point.
• lowerConvexEnvelope_add_affine: adding a real affine function to the sequence adds it to the envelope; lowerConvexEnvelope_const_add allows an infinite constant, and lowerConvexEnvelope_add_nsmul states the shear by a finite slope.
• lowerConvexEnvelope_map_mul: scaling the sequence by a positive real factor scales the envelope by the same factor.
• lowerConvexEnvelope_shift: shifting the sequence to the right, with infinite heights at the vacated indices, shifts the envelope in the same way.
• lowerConvexEnvelope_reflect: reflecting points that are infinite beyond N in the index N reflects their envelope in the same way.

References

• N. Koblitz, p-adic Numbers, p-adic Analysis, and Zeta-Functions, second edition, Graduate Texts in Mathematics 58, Springer, 1984, Chapter IV §3.

Suprema of convex height sequences

theorem TauCeti.IsConvexSeq.of_isLUB {S : Set (ℕ → WithTop ℝ)} {h : ℕ → WithTop ℝ} (hS : ∀ g ∈ S, IsConvexSeq g) (hh : IsLUB S h) : IsConvexSeq h

A least upper bound of a family of convex height sequences is convex. The empty family has no least upper bound, since height sequences have no least element.

theorem TauCeti.IsConvexSeq.sup {g h : ℕ → WithTop ℝ} (hg : IsConvexSeq g) (hh : IsConvexSeq h) : IsConvexSeq (g ⊔ h)

The pointwise maximum of two convex height sequences is convex.

theorem TauCeti.IsConvexSeq.iSup {ι : Sort u_1} {g : ι → ℕ → WithTop ℝ} (hg : ∀ (i : ι), IsConvexSeq (g i)) : IsConvexSeq fun (n : ℕ) => ⨆ (i : ι), g i n

The pointwise supremum of a family of convex height sequences is convex. For the empty family the supremum is the junk value sSup ∅ = 0 of WithTop ℝ, the constant sequence 0.

Lower convex envelopes

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

h is the lower convex envelope of a: it is a convex minorant of a that dominates every convex minorant of a.

• isConvexSeq : IsConvexSeq h

  The envelope is convex.

• le : h ≤ a

  The envelope lies below the point heights.

• greatest ⦃g : ℕ → WithTop ℝ⦄ : IsConvexSeq g → g ≤ a → g ≤ h

  The envelope dominates every convex minorant.

theorem TauCeti.isLowerConvexEnvelope_iff_isGreatest {a h : ℕ → WithTop ℝ} : IsLowerConvexEnvelope a h ↔ IsGreatest {g : ℕ → WithTop ℝ | IsConvexSeq g ∧ g ≤ a} h

Being the lower convex envelope means being the greatest convex minorant.

theorem TauCeti.IsLowerConvexEnvelope.unique {a h g : ℕ → WithTop ℝ} (hh : IsLowerConvexEnvelope a h) (hg : IsLowerConvexEnvelope a g) : h = g

The lower convex envelope is unique.

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

A sequence with a lower convex envelope is admissible.

theorem TauCeti.IsLowerConvexEnvelope.of_isConvexSeq {h : ℕ → WithTop ℝ} (hh : IsConvexSeq h) : IsLowerConvexEnvelope h h

A convex sequence is its own lower convex envelope.

noncomputable def TauCeti.lowerConvexEnvelope (a : ℕ → WithTop ℝ) : ℕ → WithTop ℝ

The lower convex envelope of a height sequence, as a total function. For an admissible sequence it is the pointwise supremum of all convex minorants. For an inadmissible sequence it is the all-infinite fallback, which is not an envelope of that sequence.

theorem TauCeti.isLUB_lowerConvexEnvelope {a : ℕ → WithTop ℝ} (ha : IsAdmissible a) (n : ℕ) : IsLUB ((fun (g : ℕ → WithTop ℝ) => g n) '' {g : ℕ → WithTop ℝ | IsConvexSeq g ∧ g ≤ a}) (lowerConvexEnvelope a n)

For an admissible sequence, each envelope height is the least upper bound of the heights of the convex minorants there.

theorem TauCeti.lowerConvexEnvelope_of_not_isAdmissible {a : ℕ → WithTop ℝ} (ha : ¬IsAdmissible a) : lowerConvexEnvelope a = ⊤

The envelope of an inadmissible sequence is the all-infinite fallback.

theorem TauCeti.isAdmissible_of_lowerConvexEnvelope_ne_top {a : ℕ → WithTop ℝ} {n : ℕ} (hn : lowerConvexEnvelope a n ≠ ⊤) : IsAdmissible a

A finite height of the total envelope excludes its inadmissible fallback.

theorem TauCeti.isLowerConvexEnvelope_lowerConvexEnvelope {a : ℕ → WithTop ℝ} (ha : IsAdmissible a) : IsLowerConvexEnvelope a (lowerConvexEnvelope a)

An admissible sequence has lowerConvexEnvelope a as its lower convex envelope.

theorem TauCeti.exists_isLowerConvexEnvelope_iff {a : ℕ → WithTop ℝ} : (∃ (h : ℕ → WithTop ℝ), IsLowerConvexEnvelope a h) ↔ IsAdmissible a

A lower convex envelope exists exactly for admissible sequences.

theorem TauCeti.IsLowerConvexEnvelope.eq_lowerConvexEnvelope {a h : ℕ → WithTop ℝ} (hh : IsLowerConvexEnvelope a h) : h = lowerConvexEnvelope a

Any lower convex envelope of a is the total function lowerConvexEnvelope a.

theorem TauCeti.isLowerConvexEnvelope_iff_eq {a h : ℕ → WithTop ℝ} (ha : IsAdmissible a) : IsLowerConvexEnvelope a h ↔ h = lowerConvexEnvelope a

For an admissible sequence, being its lower convex envelope is equality with lowerConvexEnvelope a.

theorem TauCeti.isConvexSeq_lowerConvexEnvelope (a : ℕ → WithTop ℝ) : IsConvexSeq (lowerConvexEnvelope a)

The total envelope is convex, including the all-infinite fallback.

theorem TauCeti.lowerConvexEnvelope_le {a : ℕ → WithTop ℝ} (ha : IsAdmissible a) : lowerConvexEnvelope a ≤ a

The envelope of an admissible sequence lies below it.

theorem TauCeti.le_lowerConvexEnvelope {a h : ℕ → WithTop ℝ} (hh : IsConvexSeq h) (hha : h ≤ a) : h ≤ lowerConvexEnvelope a

A convex minorant lies below the envelope. Admissibility is automatic.

theorem TauCeti.le_lowerConvexEnvelope_iff {a h : ℕ → WithTop ℝ} (ha : IsAdmissible a) (hh : IsConvexSeq h) : h ≤ lowerConvexEnvelope a ↔ h ≤ a

For an admissible sequence a, a convex sequence lies below the envelope of a exactly when it lies below a.

theorem TauCeti.IsConvexSeq.lowerConvexEnvelope_eq {h : ℕ → WithTop ℝ} (hh : IsConvexSeq h) : lowerConvexEnvelope h = h

A convex sequence is its own lower convex envelope.

@[simp]

theorem TauCeti.lowerConvexEnvelope_top : lowerConvexEnvelope ⊤ = ⊤

The envelope of the empty point set is the empty polygon.

@[simp]

theorem TauCeti.lowerConvexEnvelope_idem (a : ℕ → WithTop ℝ) : lowerConvexEnvelope (lowerConvexEnvelope a) = lowerConvexEnvelope a

Taking the lower convex envelope is idempotent.

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

The envelope is monotone on admissible inputs: a lower admissible bound b ≤ a, not necessarily convex, has envelope below that of a.

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

For admissible a and b, the envelope of the pointwise minimum of their envelopes is the envelope of a ⊓ b. So the greatest convex minorant of a ⊓ b depends only on the envelopes of a and b, and by le_lowerConvexEnvelope it lies above every common convex minorant of the two envelopes. The pointwise minimum of two envelopes need not itself be convex.

Finite domain and endpoints

theorem TauCeti.lowerConvexEnvelope_eq_top_of_forall_le {a : ℕ → WithTop ℝ} {n : ℕ} (hn : ∀ i ≤ n, a i = ⊤) : lowerConvexEnvelope a n = ⊤

The envelope is infinite at n if every point at or before n is infinite.

theorem TauCeti.lowerConvexEnvelope_eq_top_of_forall_ge {a : ℕ → WithTop ℝ} {n : ℕ} (hn : ∀ (k : ℕ), n ≤ k → a k = ⊤) : lowerConvexEnvelope a n = ⊤

The envelope is infinite at n if every point at or after n is infinite.

theorem TauCeti.lowerConvexEnvelope_ne_top_iff {a : ℕ → WithTop ℝ} (ha : IsAdmissible a) {n : ℕ} : lowerConvexEnvelope a n ≠ ⊤ ↔ ∃ i ≤ n, ∃ (k : ℕ), n ≤ k ∧ a i ≠ ⊤ ∧ a k ≠ ⊤

For an admissible sequence, the finite domain of the envelope is the integer convex hull of the finite domain of the sequence.

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

An admissible envelope passes through the first point of the sequence: if every point before p is infinite, the envelope agrees with the sequence at p.

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

The envelope passes through the last point of the sequence, when there is one: if every point after p is infinite, the envelope agrees with the sequence at p. Such a sequence has only finitely many finite points, so it is automatically admissible.

Affine covariance

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

Adding a real affine function to the points adds it to their lower convex envelope.

theorem TauCeti.lowerConvexEnvelope_add_affine (a : ℕ → WithTop ℝ) (c m : ℝ) : (lowerConvexEnvelope fun (n : ℕ) => a n + ↑(c + m * ↑n)) = fun (n : ℕ) => lowerConvexEnvelope a n + ↑(c + m * ↑n)

Adding a real affine function to a sequence adds it to the envelope. This holds for inadmissible sequences too, where both sides are the all-infinite fallback. With m = 0 it is a height translation; with c = 0 it is a shear.

theorem TauCeti.lowerConvexEnvelope_const_add (t : WithTop ℝ) (a : ℕ → WithTop ℝ) : (lowerConvexEnvelope fun (n : ℕ) => t + a n) = fun (n : ℕ) => t + lowerConvexEnvelope a n

Adding a constant height, possibly infinite, to a sequence adds it to the envelope. An infinite constant gives the empty polygon on both sides.

theorem TauCeti.lowerConvexEnvelope_add_nsmul (a : ℕ → WithTop ℝ) {t : WithTop ℝ} (ht : t ≠ ⊤) : (lowerConvexEnvelope fun (n : ℕ) => a n + n • t) = fun (n : ℕ) => lowerConvexEnvelope a n + n • t

Adding the shear n ↦ n • t of a finite slope t to a sequence adds it to the envelope. The finiteness hypothesis is needed: n • ⊤ is 0 at n = 0 and ⊤ elsewhere, which is not affine.

Scaling of heights

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

Scaling the points by a positive real factor scales their lower convex envelope by the same factor.

theorem TauCeti.lowerConvexEnvelope_map_mul (a : ℕ → WithTop ℝ) {c : ℝ} (hc : 0 < c) : (lowerConvexEnvelope fun (n : ℕ) => WithTop.map (fun (x : ℝ) => c * x) (a n)) = fun (n : ℕ) => WithTop.map (fun (x : ℝ) => c * x) (lowerConvexEnvelope a n)

Scaling a sequence by a positive real factor scales its lower convex envelope by the same factor. This holds for inadmissible sequences too, where both sides are the all-infinite fallback.

Translation of indices

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

Shifting the points k places to the right, with infinite heights at the first k indices, shifts their lower convex envelope in the same way.

theorem TauCeti.lowerConvexEnvelope_shift (a : ℕ → WithTop ℝ) (k : ℕ) : (lowerConvexEnvelope fun (n : ℕ) => if k ≤ n then a (n - k) else ⊤) = fun (n : ℕ) => if k ≤ n then lowerConvexEnvelope a (n - k) else ⊤

Shifting a sequence k places to the right, with infinite heights at the first k indices, shifts its lower convex envelope in the same way. This holds for inadmissible sequences too, where both sides are the all-infinite fallback.

Reflection of indices

theorem TauCeti.IsLowerConvexEnvelope.reflect {a h : ℕ → WithTop ℝ} (hh : IsLowerConvexEnvelope a h) {N : ℕ} (ha : ∀ (n : ℕ), N < n → a n = ⊤) : IsLowerConvexEnvelope (fun (n : ℕ) => if n ≤ N then a (N - n) else ⊤) fun (n : ℕ) => if n ≤ N then h (N - n) else ⊤

Reflecting points in N, when they are infinite beyond N, reflects their lower convex envelope in the same way. The hypothesis is needed, since reflection discards the points beyond N, which may affect the envelope on [0, N].

theorem TauCeti.lowerConvexEnvelope_reflect {a : ℕ → WithTop ℝ} {N : ℕ} (ha : ∀ (n : ℕ), N < n → a n = ⊤) : (lowerConvexEnvelope fun (n : ℕ) => if n ≤ N then a (N - n) else ⊤) = fun (n : ℕ) => if n ≤ N then lowerConvexEnvelope a (N - n) else ⊤

Reflecting points in N, when they are infinite beyond N, reflects their lower convex envelope in the same way.