Supporting values of height sequences

The supporting value of a height sequence at slope σ is the infimum of its heights after subtracting σ * n. When finite, it is the greatest real intercept of an affine line of slope σ below the sequence. Its values lie in EReal: the empty sequence has supporting value ⊤, while a tilted sequence unbounded below has value ⊥. Thus supporting values are defined even when no convex envelope exists.

The affine-minorant characterization shows that an admissible sequence and its lower convex envelope have identical supporting values. Translation and shear of the heights give the corresponding translation and parameter shift of the supporting values. Convex heights, including infinite heights outside their finite domain, are reconstructed as the supremum of their supporting lines. Consequently a convex height sequence lies below another sequence exactly when its supporting values do.

The inclusion WithTop.toEReal regards heights in WithTop ℝ as extended reals without installing a new coercion.

References

• N. Koblitz, p-adic Numbers, p-adic Analysis, and Zeta-Functions, second edition, Graduate Texts in Mathematics 58, Springer, 1984, Chapter IV §3.
• K. S. Kedlaya, Newton polygons, MIT 18.787, fall 2007, §§1–3. Kedlaya plots coefficient points at negative indices; our convention uses positive indices, so the geometric slope has the opposite sign.

noncomputable def TauCeti.supportingValue (a : ℕ → WithTop ℝ) (σ : ℝ) : EReal

The infimum of the tilted heights at slope σ. The inclusion WithTop.toEReal regards a height in WithTop ℝ as an extended real, so missing heights contribute ⊤ and no individual height contributes ⊥.

theorem TauCeti.supportingValue_def (a : ℕ → WithTop ℝ) (σ : ℝ) : supportingValue a σ = ⨅ (n : ℕ), (a n).toEReal - ↑(σ * ↑n)

The supporting value is the extended-real infimum of the tilted heights.

theorem TauCeti.le_supportingValue_iff {a : ℕ → WithTop ℝ} {σ : ℝ} {r : EReal} : r ≤ supportingValue a σ ↔ ∀ (n : ℕ), r ≤ (a n).toEReal - ↑(σ * ↑n)

A lower bound on the supporting value is a lower bound on every tilted height.

theorem TauCeti.coe_le_supportingValue_iff {a : ℕ → WithTop ℝ} {c σ : ℝ} : ↑c ≤ supportingValue a σ ↔ ∀ (n : ℕ), ↑(c + σ * ↑n) ≤ a n

A real intercept lies below the supporting value exactly when its affine line lies below every height. No admissibility assumption is needed.

theorem TauCeti.coe_le_supportingValue_iff_untop₀ {a : ℕ → WithTop ℝ} {c σ : ℝ} : ↑c ≤ supportingValue a σ ↔ ∀ (n : ℕ), a n ≠ ⊤ → c + σ * ↑n ≤ (a n).untop₀

A real intercept lies below the supporting value exactly when its affine line lies below every finite height, compared as real numbers.

theorem TauCeti.supportingValue_le (a : ℕ → WithTop ℝ) (σ : ℝ) (n : ℕ) : supportingValue a σ ≤ (a n).toEReal - ↑(σ * ↑n)

The supporting value lies below each tilted height.

theorem TauCeti.supportingValue_mono {a b : ℕ → WithTop ℝ} (hab : a ≤ b) (σ : ℝ) : supportingValue a σ ≤ supportingValue b σ

Increasing the heights increases every supporting value.

theorem TauCeti.supportingValue_antitone (a : ℕ → WithTop ℝ) : Antitone (supportingValue a)

On natural-number indices the supporting value is antitone in the slope.

@[simp]

theorem TauCeti.supportingValue_top (σ : ℝ) : supportingValue ⊤ σ = ⊤

The empty point sequence has supporting value ⊤ at every slope.

@[simp]

theorem TauCeti.supportingValue_eq_top_iff {a : ℕ → WithTop ℝ} {σ : ℝ} : supportingValue a σ = ⊤ ↔ a = ⊤

A supporting value equals ⊤ exactly when the point sequence is empty.

theorem TauCeti.supportingValue_lt_top_iff {a : ℕ → WithTop ℝ} {σ : ℝ} : supportingValue a σ < ⊤ ↔ ∃ (n : ℕ), a n ≠ ⊤

A nonempty sequence has supporting value strictly below ⊤, even when the infimum is ⊥.

theorem TauCeti.supportingValue_ne_bot_iff {a : ℕ → WithTop ℝ} {σ : ℝ} : supportingValue a σ ≠ ⊥ ↔ ∃ (c : ℝ), ∀ (n : ℕ), ↑(c + σ * ↑n) ≤ a n

A supporting value is not ⊥ exactly when there is a real affine minorant with the specified slope.

theorem TauCeti.supportingValue_eq_bot_iff {a : ℕ → WithTop ℝ} {σ : ℝ} : supportingValue a σ = ⊥ ↔ ∀ (c : ℝ), ∃ (n : ℕ), a n < ↑(c + σ * ↑n)

The value ⊥ means that the tilted heights are unbounded below, equivalently that no real affine line of this slope lies below the sequence.

theorem TauCeti.isAdmissible_iff_exists_supportingValue_ne_bot {a : ℕ → WithTop ℝ} : IsAdmissible a ↔ ∃ (σ : ℝ), supportingValue a σ ≠ ⊥

Admissibility means that at least one slope has supporting value above ⊥.

theorem TauCeti.exists_coe_eq_supportingValue_iff {a : ℕ → WithTop ℝ} {σ : ℝ} : (∃ (r : ℝ), ↑r = supportingValue a σ) ↔ (∃ (n : ℕ), a n ≠ ⊤) ∧ ∃ (c : ℝ), ∀ (n : ℕ), ↑(c + σ * ↑n) ≤ a n

A finite supporting value is equivalent to nonempty support and a real minorant of the specified slope.

theorem TauCeti.IsLowerConvexEnvelope.supportingValue_eq {a h : ℕ → WithTop ℝ} (hh : IsLowerConvexEnvelope a h) (σ : ℝ) : supportingValue h σ = supportingValue a σ

A lower convex envelope has the same supporting values as the original sequence. This is independent of the chosen construction of the envelope.

theorem TauCeti.supportingValue_lowerConvexEnvelope {a : ℕ → WithTop ℝ} (ha : IsAdmissible a) : supportingValue (lowerConvexEnvelope a) = supportingValue a

Taking the lower convex envelope of an admissible sequence preserves its supporting-value function.

Reconstruction from supporting lines

theorem TauCeti.IsConvexSeq.iSup_supportingValue_add {h : ℕ → WithTop ℝ} (hh : IsConvexSeq h) (n : ℕ) : ⨆ (σ : ℝ), supportingValue h σ + ↑(σ * ↑n) = (h n).toEReal

A convex height sequence is the supremum of all its supporting lines. The equality holds also at infinite heights, for empty and singleton domains, and at indices outside the finite domain.

theorem TauCeti.IsConvexSeq.le_iff_forall_supportingValue_le {a h : ℕ → WithTop ℝ} (hh : IsConvexSeq h) : h ≤ a ↔ ∀ (σ : ℝ), supportingValue h σ ≤ supportingValue a σ

A convex height sequence lies below another height sequence exactly when its supporting values do. The second sequence need not be convex.

theorem TauCeti.iSup_supportingValue_add_eq_lowerConvexEnvelope {a : ℕ → WithTop ℝ} (ha : IsAdmissible a) (n : ℕ) : ⨆ (σ : ℝ), supportingValue a σ + ↑(σ * ↑n) = (lowerConvexEnvelope a n).toEReal

The lower convex envelope of an admissible sequence is reconstructed from the supporting values of the sequence itself.

theorem TauCeti.supportingValue_add_affine (a : ℕ → WithTop ℝ) (c m σ : ℝ) : supportingValue (fun (n : ℕ) => a n + ↑(c + m * ↑n)) σ = supportingValue a (σ - m) + ↑c

Adding a real affine height translates the supporting value and shifts its slope parameter. The statement includes both infinite supporting values.