Contact at vertices of a lower convex envelope

An interior vertex of a convex height sequence is a strict increase between two adjacent finite unit slopes. For a lower convex envelope, every such vertex is an original point of the sequence. Equivalently, at a noncontact interior index the two adjacent slopes agree. Thus subdividing a straight segment does not introduce geometric vertices, and a missing coefficient cannot be a vertex. The endpoints of every finite face, including a singleton, are original points as well, whether they are interior vertices or boundaries of the finite domain.

The stronger local characterization IsLowerConvexEnvelope.eq_min_of_finite_neighbors says that each interior height is the minimum of its coefficient height and the average of its two neighboring heights. All results allow unbounded finite domains and infinite coefficient heights.

theorem TauCeti.IsLowerConvexEnvelope.eq_min_of_finite_neighbors {a h : ℕ → WithTop ℝ} (hh : IsLowerConvexEnvelope a h) {n : ℕ} (hn : h n ≠ ⊤) (hn₂ : h (n + 2) ≠ ⊤) : h (n + 1) = min (a (n + 1)) ↑(((h n).untop₀ + (h (n + 2)).untop₀) / 2)

At an index with two finite neighbors, an envelope height is the minimum of the original point height and the neighboring average. In particular it can lie strictly below the original point only along a straight segment.

theorem TauCeti.IsLowerConvexEnvelope.eq_of_unitSlope_lt {a h : ℕ → WithTop ℝ} (hh : IsLowerConvexEnvelope a h) {n : ℕ} (hn : h n ≠ ⊤) (hn₂ : h (n + 2) ≠ ⊤) (hs : unitSlope h n < unitSlope h (n + 1)) : h (n + 1) = a (n + 1)

Every interior strict slope change of a lower convex envelope is an original point. Both slopes are genuine finite edges; there are no endpoint sentinels.

theorem TauCeti.IsLowerConvexEnvelope.unitSlope_eq_of_lt {a h : ℕ → WithTop ℝ} (hh : IsLowerConvexEnvelope a h) {n : ℕ} (ha : h (n + 1) < a (n + 1)) : unitSlope h n = unitSlope h (n + 1)

At a noncontact interior index the two neighboring finite slopes agree. This also applies when the original point height is infinite. The neighbors of a noncontact index are automatically finite.

theorem TauCeti.IsLowerConvexEnvelope.eq_left_of_isFiniteFace {a h : ℕ → WithTop ℝ} (hh : IsLowerConvexEnvelope a h) {σ : ℝ} {l u : ℕ} (hf : IsFiniteFace h σ l u) : h l = a l

The left endpoint of a finite face, including a singleton, is an original point. The finite domain of the envelope need not be bounded.

theorem TauCeti.IsLowerConvexEnvelope.eq_right_of_isFiniteFace {a h : ℕ → WithTop ℝ} (hh : IsLowerConvexEnvelope a h) {σ : ℝ} {l u : ℕ} (hf : IsFiniteFace h σ l u) : h u = a u

The right endpoint of a finite face, including a singleton, is an original point. An unbounded terminal ray is excluded by the finite-face hypothesis.

theorem TauCeti.IsLowerConvexEnvelope.exists_isSupportingLine_isLeast_isGreatest_of_isFiniteFace {a h : ℕ → WithTop ℝ} (hh : IsLowerConvexEnvelope a h) {σ : ℝ} {l u : ℕ} (hf : IsFiniteFace h σ l u) : ∃ (c : ℝ), IsSupportingLine a σ c ∧ IsLeast (supportingFace a σ c) l ∧ IsGreatest (supportingFace a σ c) u

The absolute endpoints of a finite envelope face are the first and last original points touching its supporting line. Interior original points need not lie on the line.