Slope presentations of convex height sequences

A nonempty convex polygon is determined by its first point and the slopes of its unit edges. This file gives the two one-sided presentations of that kind.

• FiniteSlopeData Γ: a starting index, an initial height, a horizontal length d and nondecreasing slopes indexed by Fin d. Length zero is a singleton polygon; the empty polygon has no presentation.
• InfiniteSlopeData Γ: a starting index, an initial height and a nondecreasing sequence of slopes indexed by ℕ, describing a polygon whose finite domain is a half-line.

The slopes and the initial height lie in a preordered additive commutative monoid Γ, such as ℕ, ℚ or ℝ, rather than in a type containing slope sentinels. The represented heights are cumulative sums on the finite domain and ⊤ outside it, so every actual edge has horizontal length one.

Main results

• FiniteSlopeData.heights_injective, InfiniteSlopeData.heights_injective: slope data is determined by the heights it represents.
• FiniteSlopeData.heights_map, InfiniteSlopeData.heights_map: compatibility with order-preserving additive maps of value monoids, such as ℚ → ℝ.
• FiniteSlopeData.isConvexSeq_heights, FiniteSlopeData.unitSlope_heights: real slope data represents a convex height sequence whose unit slopes are the given ones.
• FiniteSlopeData.ofIsConvexSeq, FiniteSlopeData.heights_ofIsConvexSeq, FiniteSlopeData.ofIsConvexSeq_heights: extraction of slope data from a convex height sequence with a specified finite domain, and both round trips.
• FiniteSlopeData.exists_heights_eq_iff: a height sequence has finite real slope data exactly when it is convex with nonempty finite domain.
• The corresponding InfiniteSlopeData statements, for convex height sequences with infinite domain.

References

• N. Koblitz, p-adic Numbers, p-adic Analysis, and Zeta-Functions, Chapter IV §3.
• A cumulative-sum construction of heights from monotone slopes also appears in William Coram's PhD/Main/NewtonPolygons/OfSlopes.lean at revision eefb3d91f34b27d0bc7822140fa85fecae029884.

Finite slope data

structure TauCeti.FiniteSlopeData (Γ : Type u_3) [Preorder Γ] : Type u_3

The unit-slope presentation of a nonempty convex polygon with finite domain [start, start + length]. The edge from start + i to start + i + 1 has slope slope i. Length zero represents a singleton polygon and carries no slopes.

• start : ℕ

  The first index of the finite domain.

• initialHeight : Γ

  The height at the first index.

• length : ℕ

  The horizontal length of the polygon, which is also its number of unit edges.

• slope : Fin self.length → Γ

  The slope of the i-th unit edge, counted from the left.

• monotone : Monotone self.slope

  Slopes are nondecreasing from left to right.

theorem TauCeti.FiniteSlopeData.ext_of_slope {Γ : Type u_1} [Preorder Γ] {d e : FiniteSlopeData Γ} (hs : d.start = e.start) (hy : d.initialHeight = e.initialHeight) (hl : d.length = e.length) (hm : ∀ (i : Fin d.length), d.slope i = e.slope (Fin.cast hl i)) : d = e

Finite slope data is determined by its anchor, length and pointwise unit slopes, transported along the equality of lengths.

def TauCeti.FiniteSlopeData.heights {Γ : Type u_1} [Preorder Γ] [AddCommMonoid Γ] (d : FiniteSlopeData Γ) (n : ℕ) : WithTop Γ

The heights represented by finite slope data: cumulative slope sums on [start, start + length] and ⊤ elsewhere.

theorem TauCeti.FiniteSlopeData.heights_def {Γ : Type u_1} [Preorder Γ] [AddCommMonoid Γ] (d : FiniteSlopeData Γ) (n : ℕ) : d.heights n = if d.start ≤ n ∧ n ≤ d.start + d.length then ↑(d.initialHeight + prefixSum (n - d.start) d.slope) else ⊤

The defining formula of FiniteSlopeData.heights at an arbitrary index.

theorem TauCeti.FiniteSlopeData.heights_ne_top_iff {Γ : Type u_1} [Preorder Γ] [AddCommMonoid Γ] (d : FiniteSlopeData Γ) {n : ℕ} : d.heights n ≠ ⊤ ↔ d.start ≤ n ∧ n ≤ d.start + d.length

The represented heights are finite exactly on [start, start + length].

@[simp]

theorem TauCeti.FiniteSlopeData.heights_eq_top_iff {Γ : Type u_1} [Preorder Γ] [AddCommMonoid Γ] (d : FiniteSlopeData Γ) {n : ℕ} : d.heights n = ⊤ ↔ n < d.start ∨ d.start + d.length < n

The represented heights are infinite exactly outside [start, start + length].

theorem TauCeti.FiniteSlopeData.setOf_heights_ne_top {Γ : Type u_1} [Preorder Γ] [AddCommMonoid Γ] (d : FiniteSlopeData Γ) : {n : ℕ | d.heights n ≠ ⊤} = Set.Icc d.start (d.start + d.length)

The finite domain of the represented heights is [start, start + length].

@[simp]

theorem TauCeti.FiniteSlopeData.heights_start_add {Γ : Type u_1} [Preorder Γ] [AddCommMonoid Γ] (d : FiniteSlopeData Γ) {k : ℕ} (hk : k ≤ d.length) : d.heights (d.start + k) = ↑(d.initialHeight + prefixSum k d.slope)

On the finite domain, the height is the initial height plus a partial slope sum.

@[simp]

theorem TauCeti.FiniteSlopeData.heights_start {Γ : Type u_1} [Preorder Γ] [AddCommMonoid Γ] (d : FiniteSlopeData Γ) : d.heights d.start = ↑d.initialHeight

The height at the first index is the initial height.

theorem TauCeti.FiniteSlopeData.heights_start_add_length {Γ : Type u_1} [Preorder Γ] [AddCommMonoid Γ] (d : FiniteSlopeData Γ) : d.heights (d.start + d.length) = ↑(d.initialHeight + ∑ i : Fin d.length, d.slope i)

The height at the right endpoint exceeds the initial height by the sum of all slopes.

def TauCeti.FiniteSlopeData.map {Γ : Type u_1} {Γ' : Type u_2} [Preorder Γ] [Preorder Γ'] [AddCommMonoid Γ] [AddCommMonoid Γ'] (d : FiniteSlopeData Γ) (f : Γ →+o Γ') : FiniteSlopeData Γ'

Transport finite slope data along an order-preserving additive map of value monoids.

@[simp]

theorem TauCeti.FiniteSlopeData.map_start {Γ : Type u_1} {Γ' : Type u_2} [Preorder Γ] [Preorder Γ'] [AddCommMonoid Γ] [AddCommMonoid Γ'] (d : FiniteSlopeData Γ) (f : Γ →+o Γ') : (d.map f).start = d.start

@[simp]

theorem TauCeti.FiniteSlopeData.map_initialHeight {Γ : Type u_1} {Γ' : Type u_2} [Preorder Γ] [Preorder Γ'] [AddCommMonoid Γ] [AddCommMonoid Γ'] (d : FiniteSlopeData Γ) (f : Γ →+o Γ') : (d.map f).initialHeight = f d.initialHeight

@[simp]

theorem TauCeti.FiniteSlopeData.map_length {Γ : Type u_1} {Γ' : Type u_2} [Preorder Γ] [Preorder Γ'] [AddCommMonoid Γ] [AddCommMonoid Γ'] (d : FiniteSlopeData Γ) (f : Γ →+o Γ') : (d.map f).length = d.length

@[simp]

theorem TauCeti.FiniteSlopeData.map_slope {Γ : Type u_1} {Γ' : Type u_2} [Preorder Γ] [Preorder Γ'] [AddCommMonoid Γ] [AddCommMonoid Γ'] (d : FiniteSlopeData Γ) (f : Γ →+o Γ') (i : Fin (d.map f).length) : (d.map f).slope i = f (d.slope (Fin.cast ⋯ i))

@[simp]

theorem TauCeti.FiniteSlopeData.heights_map {Γ : Type u_1} {Γ' : Type u_2} [Preorder Γ] [Preorder Γ'] [AddCommMonoid Γ] [AddCommMonoid Γ'] (d : FiniteSlopeData Γ) (f : Γ →+o Γ') (n : ℕ) : (d.map f).heights n = WithTop.map (⇑f) (d.heights n)

The heights of transported slope data are the transported heights.

theorem TauCeti.FiniteSlopeData.heights_injective {Γ : Type u_1} [Preorder Γ] [AddCancelCommMonoid Γ] : Function.Injective heights

Finite slope data is determined by the heights it represents: the starting index, the initial height, the length and every slope agree.

Infinite slope data

structure TauCeti.InfiniteSlopeData (Γ : Type u_3) [Preorder Γ] : Type u_3

The unit-slope presentation of a convex polygon whose finite domain is the half-line [start, ∞). The edge from start + i to start + i + 1 has slope slope i. A terminal ray is an eventually constant slope sequence; no slope is infinite.

• start : ℕ

  The first index of the finite domain.

• initialHeight : Γ

  The height at the first index.

• slope : ℕ → Γ

  The slope of the i-th unit edge, counted from the left.

• monotone : Monotone self.slope

  Slopes are nondecreasing from left to right.

theorem TauCeti.InfiniteSlopeData.ext_iff {Γ : Type u_3} {inst✝ : Preorder Γ} {x y : InfiniteSlopeData Γ} : x = y ↔ x.start = y.start ∧ x.initialHeight = y.initialHeight ∧ x.slope = y.slope

theorem TauCeti.InfiniteSlopeData.ext {Γ : Type u_3} {inst✝ : Preorder Γ} {x y : InfiniteSlopeData Γ} (start : x.start = y.start) (initialHeight : x.initialHeight = y.initialHeight) (slope : x.slope = y.slope) : x = y

def TauCeti.InfiniteSlopeData.truncate {Γ : Type u_1} [Preorder Γ] (d : InfiniteSlopeData Γ) (n : ℕ) : FiniteSlopeData Γ

Keep the anchor and first n unit slopes of an infinite slope presentation. For n = 0 the truncation is the singleton at the anchor.

@[simp]

theorem TauCeti.InfiniteSlopeData.truncate_start {Γ : Type u_1} [Preorder Γ] (d : InfiniteSlopeData Γ) (n : ℕ) : (d.truncate n).start = d.start

@[simp]

theorem TauCeti.InfiniteSlopeData.truncate_initialHeight {Γ : Type u_1} [Preorder Γ] (d : InfiniteSlopeData Γ) (n : ℕ) : (d.truncate n).initialHeight = d.initialHeight

@[simp]

theorem TauCeti.InfiniteSlopeData.truncate_length {Γ : Type u_1} [Preorder Γ] (d : InfiniteSlopeData Γ) (n : ℕ) : (d.truncate n).length = n

@[simp]

theorem TauCeti.InfiniteSlopeData.truncate_slope {Γ : Type u_1} [Preorder Γ] (d : InfiniteSlopeData Γ) (n : ℕ) (i : Fin (d.truncate n).length) : (d.truncate n).slope i = d.slope ↑i

def TauCeti.InfiniteSlopeData.heights {Γ : Type u_1} [Preorder Γ] [AddCommMonoid Γ] (d : InfiniteSlopeData Γ) (n : ℕ) : WithTop Γ

The heights represented by infinite slope data: cumulative slope sums from start onwards and ⊤ before it.

theorem TauCeti.InfiniteSlopeData.heights_def {Γ : Type u_1} [Preorder Γ] [AddCommMonoid Γ] (d : InfiniteSlopeData Γ) (n : ℕ) : d.heights n = if d.start ≤ n then ↑(d.initialHeight + ∑ i ∈ Finset.range (n - d.start), d.slope i) else ⊤

The defining formula of InfiniteSlopeData.heights at an arbitrary index.

theorem TauCeti.InfiniteSlopeData.heights_ne_top_iff {Γ : Type u_1} [Preorder Γ] [AddCommMonoid Γ] (d : InfiniteSlopeData Γ) {n : ℕ} : d.heights n ≠ ⊤ ↔ d.start ≤ n

The represented heights are finite exactly on [start, ∞).

@[simp]

theorem TauCeti.InfiniteSlopeData.heights_eq_top_iff {Γ : Type u_1} [Preorder Γ] [AddCommMonoid Γ] (d : InfiniteSlopeData Γ) {n : ℕ} : d.heights n = ⊤ ↔ n < d.start

The represented heights are infinite exactly before start.

theorem TauCeti.InfiniteSlopeData.setOf_heights_ne_top {Γ : Type u_1} [Preorder Γ] [AddCommMonoid Γ] (d : InfiniteSlopeData Γ) : {n : ℕ | d.heights n ≠ ⊤} = Set.Ici d.start

The finite domain of the represented heights is [start, ∞).

@[simp]

theorem TauCeti.InfiniteSlopeData.heights_start_add {Γ : Type u_1} [Preorder Γ] [AddCommMonoid Γ] (d : InfiniteSlopeData Γ) (k : ℕ) : d.heights (d.start + k) = ↑(d.initialHeight + ∑ i ∈ Finset.range k, d.slope i)

On the finite domain, the height is the initial height plus a partial slope sum.

@[simp]

theorem TauCeti.InfiniteSlopeData.heights_truncate_start_add {Γ : Type u_1} [Preorder Γ] [AddCommMonoid Γ] (d : InfiniteSlopeData Γ) (n : ℕ) {k : ℕ} (hk : k ≤ n) : (d.truncate n).heights (d.start + k) = d.heights (d.start + k)

Truncation preserves heights on the interval from the anchor to its endpoint.

@[simp]

theorem TauCeti.InfiniteSlopeData.heights_start {Γ : Type u_1} [Preorder Γ] [AddCommMonoid Γ] (d : InfiniteSlopeData Γ) : d.heights d.start = ↑d.initialHeight

The height at the first index is the initial height.

def TauCeti.InfiniteSlopeData.map {Γ : Type u_1} {Γ' : Type u_2} [Preorder Γ] [Preorder Γ'] [AddCommMonoid Γ] [AddCommMonoid Γ'] (d : InfiniteSlopeData Γ) (f : Γ →+o Γ') : InfiniteSlopeData Γ'

Transport infinite slope data along an order-preserving additive map of value monoids.

@[simp]

theorem TauCeti.InfiniteSlopeData.map_start {Γ : Type u_1} {Γ' : Type u_2} [Preorder Γ] [Preorder Γ'] [AddCommMonoid Γ] [AddCommMonoid Γ'] (d : InfiniteSlopeData Γ) (f : Γ →+o Γ') : (d.map f).start = d.start

@[simp]

theorem TauCeti.InfiniteSlopeData.map_initialHeight {Γ : Type u_1} {Γ' : Type u_2} [Preorder Γ] [Preorder Γ'] [AddCommMonoid Γ] [AddCommMonoid Γ'] (d : InfiniteSlopeData Γ) (f : Γ →+o Γ') : (d.map f).initialHeight = f d.initialHeight

@[simp]

theorem TauCeti.InfiniteSlopeData.map_slope {Γ : Type u_1} {Γ' : Type u_2} [Preorder Γ] [Preorder Γ'] [AddCommMonoid Γ] [AddCommMonoid Γ'] (d : InfiniteSlopeData Γ) (f : Γ →+o Γ') (i : ℕ) : (d.map f).slope i = f (d.slope i)

@[simp]

theorem TauCeti.InfiniteSlopeData.heights_map {Γ : Type u_1} {Γ' : Type u_2} [Preorder Γ] [Preorder Γ'] [AddCommMonoid Γ] [AddCommMonoid Γ'] (d : InfiniteSlopeData Γ) (f : Γ →+o Γ') (n : ℕ) : (d.map f).heights n = WithTop.map (⇑f) (d.heights n)

The heights of transported slope data are the transported heights.

theorem TauCeti.InfiniteSlopeData.heights_injective {Γ : Type u_1} [Preorder Γ] [AddCancelCommMonoid Γ] : Function.Injective heights

Infinite slope data is determined by the heights it represents: the starting index, the initial height and every slope agree.

Real slope data and convex height sequences

@[simp]

theorem TauCeti.FiniteSlopeData.unitSlope_heights (d : FiniteSlopeData ℝ) (i : Fin d.length) : unitSlope d.heights (d.start + ↑i) = d.slope i

The unit slopes of the represented heights are the given slopes.

theorem TauCeti.FiniteSlopeData.isConvexSeq_heights (d : FiniteSlopeData ℝ) : IsConvexSeq d.heights

Real finite slope data represents a convex height sequence.

noncomputable def TauCeti.FiniteSlopeData.ofIsConvexSeq {h : ℕ → WithTop ℝ} (hh : IsConvexSeq h) {l k : ℕ} (hdom : ∀ (n : ℕ), h n ≠ ⊤ ↔ l ≤ n ∧ n ≤ l + k) : FiniteSlopeData ℝ

The finite slope data of a convex height sequence whose finite domain is [l, l + k].

@[simp]

theorem TauCeti.FiniteSlopeData.ofIsConvexSeq_start {h : ℕ → WithTop ℝ} (hh : IsConvexSeq h) {l k : ℕ} (hdom : ∀ (n : ℕ), h n ≠ ⊤ ↔ l ≤ n ∧ n ≤ l + k) : (ofIsConvexSeq hh hdom).start = l

@[simp]

theorem TauCeti.FiniteSlopeData.ofIsConvexSeq_initialHeight {h : ℕ → WithTop ℝ} (hh : IsConvexSeq h) {l k : ℕ} (hdom : ∀ (n : ℕ), h n ≠ ⊤ ↔ l ≤ n ∧ n ≤ l + k) : (ofIsConvexSeq hh hdom).initialHeight = (h l).untop₀

@[simp]

theorem TauCeti.FiniteSlopeData.ofIsConvexSeq_length {h : ℕ → WithTop ℝ} (hh : IsConvexSeq h) {l k : ℕ} (hdom : ∀ (n : ℕ), h n ≠ ⊤ ↔ l ≤ n ∧ n ≤ l + k) : (ofIsConvexSeq hh hdom).length = k

@[simp]

theorem TauCeti.FiniteSlopeData.ofIsConvexSeq_slope {h : ℕ → WithTop ℝ} (hh : IsConvexSeq h) {l k : ℕ} (hdom : ∀ (n : ℕ), h n ≠ ⊤ ↔ l ≤ n ∧ n ≤ l + k) (i : Fin (ofIsConvexSeq hh hdom).length) : (ofIsConvexSeq hh hdom).slope i = unitSlope h (l + ↑i)

@[simp]

theorem TauCeti.FiniteSlopeData.heights_ofIsConvexSeq {h : ℕ → WithTop ℝ} (hh : IsConvexSeq h) {l k : ℕ} (hdom : ∀ (n : ℕ), h n ≠ ⊤ ↔ l ≤ n ∧ n ≤ l + k) : (ofIsConvexSeq hh hdom).heights = h

Extracting slope data and reconstructing heights recovers the height sequence.

@[simp]

theorem TauCeti.FiniteSlopeData.ofIsConvexSeq_heights (d : FiniteSlopeData ℝ) : ofIsConvexSeq ⋯ ⋯ = d

Reconstructing heights and extracting slope data recovers the slope data.

theorem TauCeti.FiniteSlopeData.exists_heights_eq_iff {h : ℕ → WithTop ℝ} : (∃ (d : FiniteSlopeData ℝ), d.heights = h) ↔ IsConvexSeq h ∧ {n : ℕ | h n ≠ ⊤}.Nonempty ∧ {n : ℕ | h n ≠ ⊤}.Finite

A real height sequence is represented by finite slope data exactly when it is convex and its finite domain is nonempty and finite.

@[simp]

theorem TauCeti.InfiniteSlopeData.unitSlope_heights (d : InfiniteSlopeData ℝ) (i : ℕ) : unitSlope d.heights (d.start + i) = d.slope i

The unit slopes of the represented heights are the given slopes.

theorem TauCeti.InfiniteSlopeData.isConvexSeq_heights (d : InfiniteSlopeData ℝ) : IsConvexSeq d.heights

Real infinite slope data represents a convex height sequence.

noncomputable def TauCeti.InfiniteSlopeData.ofIsConvexSeq {h : ℕ → WithTop ℝ} (hh : IsConvexSeq h) {l : ℕ} (hdom : ∀ (n : ℕ), h n ≠ ⊤ ↔ l ≤ n) : InfiniteSlopeData ℝ

The infinite slope data of a convex height sequence whose finite domain is [l, ∞).

@[simp]

theorem TauCeti.InfiniteSlopeData.ofIsConvexSeq_start {h : ℕ → WithTop ℝ} (hh : IsConvexSeq h) {l : ℕ} (hdom : ∀ (n : ℕ), h n ≠ ⊤ ↔ l ≤ n) : (ofIsConvexSeq hh hdom).start = l

@[simp]

theorem TauCeti.InfiniteSlopeData.ofIsConvexSeq_initialHeight {h : ℕ → WithTop ℝ} (hh : IsConvexSeq h) {l : ℕ} (hdom : ∀ (n : ℕ), h n ≠ ⊤ ↔ l ≤ n) : (ofIsConvexSeq hh hdom).initialHeight = (h l).untop₀

@[simp]

theorem TauCeti.InfiniteSlopeData.ofIsConvexSeq_slope {h : ℕ → WithTop ℝ} (hh : IsConvexSeq h) {l : ℕ} (hdom : ∀ (n : ℕ), h n ≠ ⊤ ↔ l ≤ n) (i : ℕ) : (ofIsConvexSeq hh hdom).slope i = unitSlope h (l + i)

@[simp]

theorem TauCeti.InfiniteSlopeData.heights_ofIsConvexSeq {h : ℕ → WithTop ℝ} (hh : IsConvexSeq h) {l : ℕ} (hdom : ∀ (n : ℕ), h n ≠ ⊤ ↔ l ≤ n) : (ofIsConvexSeq hh hdom).heights = h

Extracting slope data and reconstructing heights recovers the height sequence.

@[simp]

theorem TauCeti.InfiniteSlopeData.ofIsConvexSeq_heights (d : InfiniteSlopeData ℝ) : ofIsConvexSeq ⋯ ⋯ = d

Reconstructing heights and extracting slope data recovers the slope data.

theorem TauCeti.InfiniteSlopeData.exists_heights_eq_iff {h : ℕ → WithTop ℝ} : (∃ (d : InfiniteSlopeData ℝ), d.heights = h) ↔ IsConvexSeq h ∧ {n : ℕ | h n ≠ ⊤}.Infinite

A real height sequence is represented by infinite slope data exactly when it is convex and its finite domain is infinite.