Finite faces of convex height sequences

A supporting line of slope σ lies below every height of a sequence. Its supporting face is the set of indices where equality holds. A sequence with a finite nonempty domain, convex or not, touches a supporting line of every slope and has a least contact index with it. For a convex height sequence the contact set is order connected. Consequently, whenever it is finite and nonempty it has unique absolute endpoints and consists of every integer between them.

The predicate IsFiniteFace h σ l u records these endpoints while leaving the supporting intercept implicit. The intercept is nevertheless unique, and equals the supporting value at σ. In particular, every nonempty convex height sequence with bounded finite domain has a finite face at every real slope. Without convexity, a sequence with only finitely many finite heights still has no supporting value ⊥. A finite edge whose slope is strictly greater than σ also guarantees a finite face of slope σ, with both endpoints at or before that edge. Thus unbounded finite edge slopes guarantee finite faces at every real slope, even on an unbounded domain. Finite unit slopes before a finite face are strictly less than its slope, on the face they equal its slope, and after it they are strictly greater. Consequently, on a domain with a first finite index, a finite face's left and right endpoints count the unit slopes respectively below and at most the face slope, and the unit edges of the face slope are exactly those inside the face, so their number is its width. These absolute endpoints are the geometric interface later used to identify extremal coefficients and count slope multiplicities. A sequence lying above a line of slope τ meets every line of smaller slope only finitely often, which bounds the supporting faces of smaller slope.

A supporting line of a point set also supports its lower convex envelope, and every contact point with the points is a contact point with the envelope. The envelope touches the line no earlier than the points do, so both have the same least contact index. Their greatest contact indices can differ: the envelope may follow a ray that the points approach only in the limit.

References

• N. Koblitz, p-adic Numbers, p-adic Analysis, and Zeta-Functions, second edition, Graduate Texts in Mathematics 58, Springer, 1984, Chapter IV §3.
• M. Lazard, Les zéros d'une fonction analytique d'une variable sur un corps valué complet, Publications Mathématiques de l'IHÉS 14 (1962), §1.

def TauCeti.IsSupportingLine (h : ℕ → WithTop ℝ) (σ c : ℝ) : Prop

A real affine line of slope σ and intercept c supports h from below.

theorem TauCeti.isSupportingLine_iff_forall {h : ℕ → WithTop ℝ} {σ c : ℝ} : IsSupportingLine h σ c ↔ ∀ (n : ℕ), ↑(c + σ * ↑n) ≤ h n

A line supports a height sequence exactly when it lies below every height.

theorem TauCeti.isSupportingLine_iff {h : ℕ → WithTop ℝ} {σ c : ℝ} : IsSupportingLine h σ c ↔ ↑c ≤ supportingValue h σ

A line supports a height sequence exactly when its intercept is at most the supporting value.

theorem TauCeti.IsSupportingLine.isAdmissible {h : ℕ → WithTop ℝ} {σ c : ℝ} (hc : IsSupportingLine h σ c) : IsAdmissible h

A height sequence with a supporting line is admissible.

theorem TauCeti.IsConvexSeq.isSupportingLine_iff_unitSlope {h : ℕ → WithTop ℝ} (hh : IsConvexSeq h) {n : ℕ} (hn : h n ≠ ⊤) (σ : ℝ) : IsSupportingLine h σ ((h n).untop₀ - σ * ↑n) ↔ (∀ (i : ℕ), i + 1 = n → h i ≠ ⊤ → unitSlope h i ≤ σ) ∧ (h (n + 1) ≠ ⊤ → σ ≤ unitSlope h n)

A line through a finite height supports a convex sequence exactly when its slope lies between the adjacent finite unit slopes. A missing adjacent edge imposes no bound.

def TauCeti.supportingFace (h : ℕ → WithTop ℝ) (σ c : ℝ) : Set ℕ

The supporting face cut out by a specified affine supporting line.

@[simp]

theorem TauCeti.mem_supportingFace {h : ℕ → WithTop ℝ} {σ c : ℝ} {n : ℕ} : n ∈ supportingFace h σ c ↔ h n = ↑(c + σ * ↑n)

Membership in a supporting face means equality with its affine line.

theorem TauCeti.supportingValue_le_coe_of_mem_supportingFace {h : ℕ → WithTop ℝ} {σ c : ℝ} {n : ℕ} (hn : n ∈ supportingFace h σ c) : supportingValue h σ ≤ ↑c

The intercept of a line of slope σ through a point of a height sequence bounds its supporting value of slope σ. The line need not be a supporting line.

theorem TauCeti.supportingValue_eq_coe_of_mem_supportingFace {h : ℕ → WithTop ℝ} {σ c : ℝ} (hc : IsSupportingLine h σ c) {n : ℕ} (hn : n ∈ supportingFace h σ c) : supportingValue h σ = ↑c

Contact with a supporting line identifies its intercept with the supporting value.

theorem TauCeti.exists_isSupportingLine_isLeast_supportingFace {h : ℕ → WithTop ℝ} (hfinite : {n : ℕ | h n ≠ ⊤}.Finite) (hne : {n : ℕ | h n ≠ ⊤}.Nonempty) (σ : ℝ) : ∃ (c : ℝ) (i : ℕ), IsSupportingLine h σ c ∧ IsLeast (supportingFace h σ c) i

A height sequence with a finite nonempty domain touches a supporting line of every slope, and has a least contact index with it. The sequence need not be convex, so the contact set need not be an interval.

theorem TauCeti.supportingValue_ne_bot_of_finite {h : ℕ → WithTop ℝ} (hfin : {n : ℕ | h n ≠ ⊤}.Finite) (σ : ℝ) : supportingValue h σ ≠ ⊥

A height sequence with only finitely many finite heights has no supporting value ⊥.

theorem TauCeti.IsConvexSeq.ordConnected_supportingFace {h : ℕ → WithTop ℝ} (hh : IsConvexSeq h) {σ c : ℝ} (hc : IsSupportingLine h σ c) : (supportingFace h σ c).OrdConnected

The contact indices of a supporting line on a convex height sequence are order connected.

def TauCeti.IsFiniteFace (h : ℕ → WithTop ℝ) (σ : ℝ) (l u : ℕ) : Prop

A finite face of slope σ has absolute endpoints l ≤ u, and the contact set of its supporting line is exactly the integer interval [l, u].

theorem TauCeti.isFiniteFace_iff {h : ℕ → WithTop ℝ} {σ : ℝ} {l u : ℕ} : IsFiniteFace h σ l u ↔ l ≤ u ∧ ∃ (c : ℝ), IsSupportingLine h σ c ∧ supportingFace h σ c = Set.Icc l u

A finite face is given by ordered endpoints together with a supporting intercept whose contact set is exactly the endpoint interval.

theorem TauCeti.IsFiniteFace.left_le_right {h : ℕ → WithTop ℝ} {σ : ℝ} {l u : ℕ} (hf : IsFiniteFace h σ l u) : l ≤ u

The left endpoint of a finite face is at most its right endpoint.

theorem TauCeti.IsFiniteFace.exists_intercept {h : ℕ → WithTop ℝ} {σ : ℝ} {l u : ℕ} (hf : IsFiniteFace h σ l u) : ∃ (c : ℝ), IsSupportingLine h σ c ∧ supportingFace h σ c = Set.Icc l u

A finite face admits a supporting intercept whose full contact set is its endpoint interval.

theorem TauCeti.IsFiniteFace.isSupportingLine_untop₀_sub {h : ℕ → WithTop ℝ} {σ : ℝ} {l u : ℕ} (hf : IsFiniteFace h σ l u) {n : ℕ} (hn : n ∈ Set.Icc l u) : IsSupportingLine h σ ((h n).untop₀ - σ * ↑n)

The line of the face slope through any point of a finite face supports the sequence.

theorem TauCeti.IsFiniteFace.existsUnique_intercept {h : ℕ → WithTop ℝ} {σ : ℝ} {l u : ℕ} (hf : IsFiniteFace h σ l u) : ∃! c : ℝ, IsSupportingLine h σ c ∧ supportingFace h σ c = Set.Icc l u

The intercept cutting out a finite face is unique.

theorem TauCeti.IsFiniteFace.existsUnique_supportingValue_eq {h : ℕ → WithTop ℝ} {σ : ℝ} {l u : ℕ} (hf : IsFiniteFace h σ l u) : ∃! c : ℝ, supportingValue h σ = ↑c

A finite face's supporting value is its unique real intercept.

theorem TauCeti.IsFiniteFace.unique {h : ℕ → WithTop ℝ} {σ : ℝ} {l u : ℕ} (hf : IsFiniteFace h σ l u) {l' u' : ℕ} (hf' : IsFiniteFace h σ l' u') : l = l' ∧ u = u'

A finite face has unique absolute endpoints.

theorem TauCeti.IsFiniteFace.of_le_of_eq_endpoints {h : ℕ → WithTop ℝ} {σ : ℝ} {l u : ℕ} (hf : IsFiniteFace h σ l u) {g : ℕ → WithTop ℝ} (hg : IsConvexSeq g) (hhg : h ≤ g) (hl : g l = h l) (hu : g u = h u) : IsFiniteFace g σ l u

If a convex sequence g lies above h and agrees with it at both endpoints of a finite face of h, then that is also a finite face of g. No new contacts appear outside its interval.

theorem TauCeti.IsFiniteFace.left_ne_top {h : ℕ → WithTop ℝ} {σ : ℝ} {l u : ℕ} (hf : IsFiniteFace h σ l u) : h l ≠ ⊤

The height at the left endpoint of a finite face is finite.

theorem TauCeti.IsFiniteFace.right_ne_top {h : ℕ → WithTop ℝ} {σ : ℝ} {l u : ℕ} (hf : IsFiniteFace h σ l u) : h u ≠ ⊤

The height at the right endpoint of a finite face is finite.

theorem TauCeti.IsFiniteFace.mul_width_eq_sub {h : ℕ → WithTop ℝ} {σ : ℝ} {l u : ℕ} (hf : IsFiniteFace h σ l u) : σ * ↑(u - l) = (h u).untop₀ - (h l).untop₀

The slope times the width of a finite face is the difference of its endpoint heights. This includes the zero-width singleton case.

theorem TauCeti.IsFiniteFace.slope_eq_div {h : ℕ → WithTop ℝ} {σ : ℝ} {l u : ℕ} (hf : IsFiniteFace h σ l u) (hlu : l < u) : σ = ((h u).untop₀ - (h l).untop₀) / ↑(u - l)

A finite face of positive width has slope equal to its rise divided by its width.

theorem TauCeti.IsFiniteFace.unitSlope_lt {h : ℕ → WithTop ℝ} {σ : ℝ} {l u : ℕ} (hf : IsFiniteFace h σ l u) (hh : IsConvexSeq h) {i : ℕ} (hi : i ∈ finiteEdges h) (hil : i < l) : unitSlope h i < σ

A finite unit edge strictly before a finite face has slope strictly less than the face slope.

theorem TauCeti.IsFiniteFace.unitSlope_eq {h : ℕ → WithTop ℝ} {σ : ℝ} {l u : ℕ} (hf : IsFiniteFace h σ l u) {i : ℕ} (hli : l ≤ i) (hiu : i < u) : unitSlope h i = σ

Every unit edge contained in a finite face has slope equal to the face slope.

theorem TauCeti.IsFiniteFace.lt_unitSlope {h : ℕ → WithTop ℝ} {σ : ℝ} {l u : ℕ} (hf : IsFiniteFace h σ l u) (hh : IsConvexSeq h) {i : ℕ} (hi : i ∈ finiteEdges h) (hui : u ≤ i) : σ < unitSlope h i

A finite unit edge at or after the right endpoint of a finite face has slope strictly greater than the face slope.

theorem TauCeti.IsFiniteFace.left_eq_start_add_ncard_unitSlope_lt {h : ℕ → WithTop ℝ} {σ : ℝ} {l u : ℕ} (hf : IsFiniteFace h σ l u) (hh : IsConvexSeq h) {a : ℕ} (ha : h a ≠ ⊤) (hfirst : ∀ (n : ℕ), h n ≠ ⊤ → a ≤ n) : l = a + {i : ℕ | i ∈ finiteEdges h ∧ unitSlope h i < σ}.ncard

A finite face's left endpoint is the first finite index plus the number of finite unit slopes strictly below the face slope. The finite domain may be bounded or unbounded.

theorem TauCeti.IsFiniteFace.right_eq_start_add_ncard_unitSlope_le {h : ℕ → WithTop ℝ} {σ : ℝ} {l u : ℕ} (hf : IsFiniteFace h σ l u) (hh : IsConvexSeq h) {a : ℕ} (ha : h a ≠ ⊤) (hfirst : ∀ (n : ℕ), h n ≠ ⊤ → a ≤ n) : u = a + {i : ℕ | i ∈ finiteEdges h ∧ unitSlope h i ≤ σ}.ncard

A finite face's right endpoint is the first finite index plus the number of finite unit slopes at most the face slope. The finite domain may be bounded or unbounded.

theorem TauCeti.IsFiniteFace.setOf_unitSlope_eq {h : ℕ → WithTop ℝ} {σ : ℝ} {l u : ℕ} (hf : IsFiniteFace h σ l u) (hh : IsConvexSeq h) : {i : ℕ | i ∈ finiteEdges h ∧ unitSlope h i = σ} = Set.Ico l u

The finite unit edges of slope σ are exactly the unit edges inside the finite face of slope σ.

theorem TauCeti.IsFiniteFace.ncard_setOf_unitSlope_eq {h : ℕ → WithTop ℝ} {σ : ℝ} {l u : ℕ} (hf : IsFiniteFace h σ l u) (hh : IsConvexSeq h) : {i : ℕ | i ∈ finiteEdges h ∧ unitSlope h i = σ}.ncard = u - l

The number of finite unit edges of slope σ is the width u - l of the finite face of slope σ.

theorem TauCeti.IsFiniteFace.finite_setOf_unitSlope_le {h : ℕ → WithTop ℝ} {σ : ℝ} {l u : ℕ} (hf : IsFiniteFace h σ l u) (hh : IsConvexSeq h) : {i : ℕ | i ∈ finiteEdges h ∧ unitSlope h i ≤ σ}.Finite

Only finitely many finite unit edges have slope at most the slope of a finite face: all of them lie before its right endpoint.

theorem TauCeti.IsConvexSeq.exists_isFiniteFace_of_finite_supportingFace {h : ℕ → WithTop ℝ} (hh : IsConvexSeq h) {σ c : ℝ} (hc : IsSupportingLine h σ c) (hfinite : (supportingFace h σ c).Finite) (hne : (supportingFace h σ c).Nonempty) : ∃ (l : ℕ) (u : ℕ), IsFiniteFace h σ l u

A finite nonempty supporting face of a convex height sequence has absolute endpoints.

theorem TauCeti.IsConvexSeq.exists_isFiniteFace_of_finiteDomain_eq_Icc {h : ℕ → WithTop ℝ} (hh : IsConvexSeq h) {a b : ℕ} (hab : a ≤ b) (hdom : ∀ (n : ℕ), h n ≠ ⊤ ↔ a ≤ n ∧ n ≤ b) (σ : ℝ) : ∃ (l : ℕ) (u : ℕ), IsFiniteFace h σ l u

Every nonempty convex height sequence with a bounded finite domain has a finite face at each real slope. The resulting endpoints are absolute indices in the original sequence.

theorem TauCeti.IsConvexSeq.exists_isFiniteFace_of_finiteDomain {h : ℕ → WithTop ℝ} (hh : IsConvexSeq h) (hfinite : {n : ℕ | h n ≠ ⊤}.Finite) (hne : {n : ℕ | h n ≠ ⊤}.Nonempty) (σ : ℝ) : ∃ (l : ℕ) (u : ℕ), IsFiniteFace h σ l u

Every nonempty convex height sequence with finite domain has a finite face at each real slope. No endpoints for the finite domain need to be supplied.

theorem TauCeti.IsConvexSeq.supportingFace_subset_Iic_of_lt_unitSlope {h : ℕ → WithTop ℝ} (hh : IsConvexSeq h) {σ c : ℝ} (hc : IsSupportingLine h σ c) {m : ℕ} (hm : m ∈ finiteEdges h) (hσ : σ < unitSlope h m) : supportingFace h σ c ⊆ Set.Iic m

Contact with a supporting line of slope σ occurs at or before any finite edge whose slope is strictly greater than σ.

theorem TauCeti.IsConvexSeq.exists_isFiniteFace_of_lt_unitSlope {h : ℕ → WithTop ℝ} (hh : IsConvexSeq h) {σ : ℝ} {m : ℕ} (hm : m ∈ finiteEdges h) (hσ : σ < unitSlope h m) : ∃ (l : ℕ) (u : ℕ), IsFiniteFace h σ l u ∧ u ≤ m

A finite edge of slope strictly greater than σ guarantees a finite nonempty face of slope σ. Its right endpoint, and hence also its left endpoint, is at most the edge index. The finite domain itself need not be bounded.

theorem TauCeti.IsConvexSeq.exists_isFiniteFace_of_unbounded_unitSlope {h : ℕ → WithTop ℝ} (hh : IsConvexSeq h) (hunbounded : ¬BddAbove (unitSlope h '' finiteEdges h)) (σ : ℝ) : ∃ (l : ℕ) (u : ℕ), IsFiniteFace h σ l u

Unbounded slopes on the finite edges of a convex height sequence guarantee a finite nonempty face at every real slope.

theorem TauCeti.IsSupportingLine.finite_supportingFace {h : ℕ → WithTop ℝ} {τ d σ : ℝ} (hd : IsSupportingLine h τ d) (hστ : σ < τ) (c : ℝ) : (supportingFace h σ c).Finite

A height sequence lying above a line of slope τ meets every line of a smaller slope σ in only finitely many indices: at a contact index n, c + σ n ≥ d + τ n. No convexity is used.

Supporting faces of lower convex envelopes

theorem TauCeti.IsLowerConvexEnvelope.isSupportingLine_iff {a h : ℕ → WithTop ℝ} {σ c : ℝ} (hh : IsLowerConvexEnvelope a h) : IsSupportingLine h σ c ↔ IsSupportingLine a σ c

A height sequence and its lower convex envelope have the same supporting lines.

theorem TauCeti.IsLowerConvexEnvelope.supportingFace_subset {a h : ℕ → WithTop ℝ} {σ c : ℝ} (hh : IsLowerConvexEnvelope a h) (hc : IsSupportingLine a σ c) : supportingFace a σ c ⊆ supportingFace h σ c

Every contact point of a supporting line with the point heights is a contact point with their lower convex envelope.

theorem TauCeti.IsLowerConvexEnvelope.exists_le_mem_supportingFace {a h : ℕ → WithTop ℝ} {σ c : ℝ} (hh : IsLowerConvexEnvelope a h) (hc : IsSupportingLine a σ c) {n : ℕ} (hn : n ∈ supportingFace h σ c) : ∃ k ≤ n, k ∈ supportingFace a σ c

If a lower convex envelope touches a supporting line of its point heights at n, then the point heights touch that line at some index at most n. The envelope may touch the line at indices beyond every contact point, along a ray approached by the points only in the limit.

theorem TauCeti.IsLowerConvexEnvelope.isLeast_supportingFace_iff {a h : ℕ → WithTop ℝ} {σ c : ℝ} (hh : IsLowerConvexEnvelope a h) (hc : IsSupportingLine a σ c) {l : ℕ} : IsLeast (supportingFace h σ c) l ↔ IsLeast (supportingFace a σ c) l

A lower convex envelope and its point heights have the same least contact index with a supporting line of the points. No analogous statement holds for greatest contact indices.