Minkowski sums of height sequences

The Minkowski sum of two one-sided height sequences is their min-convolution minkowskiSum h g n = min_{i + j = n} (h i + g j). For convex sequences it is the height function of the Minkowski sum of the two polygons. This is the geometric operation that describes Newton polygons of products of polynomials and power series.

Under tropicalisation trop : WithTop ℝ → MinTropical (WithTop ℝ), min-convolution is the Cauchy product of power series over the tropical semiring. This identifies the algebraic laws (symmetry, associativity, the singleton at (0, 0) as identity and the empty polygon as absorbing element) with those of multiplication of power series.

Main results

• mk_trop_minkowskiSum: tropicalisation turns minkowskiSum into multiplication of power series over MinTropical (WithTop ℝ).
• minkowskiSum_comm, minkowskiSum_assoc, minkowskiSum_ite_eq_zero, minkowskiSum_top: the algebraic laws; minkowskiSum_ite_eq describes the sum with a single point, which translates the other sequence.
• ordConnected_minkowskiSum: order-connected finite domains have an order-connected sum.
• minkowskiSum_add_eq_of_forall_lt, minkowskiSum_add_eq_of_forall_gt: first points add, and so do last points when both finite domains are bounded above.
• IsConvexSeq.minkowskiSum: the Minkowski sum of convex height sequences is convex.
• supportingValue_minkowskiSum, supportingValue_minkowskiSum_of_ne_bot: supporting values add in EReal for nonempty sequences, or when neither supporting value is ⊥.
• minkowskiSum_add_eq_add_iff: a split n = i + j of convex sequences is minimising exactly when i and j lie on supporting faces of h and g with a common slope.

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, Proposition 1.

noncomputable def TauCeti.minkowskiSum (h g : ℕ → WithTop ℝ) (n : ℕ) : WithTop ℝ

The Minkowski sum of two height sequences, given by the min-convolution n ↦ min_{i + j = n} (h i + g j). A split with an infinite height contributes ⊤.

theorem TauCeti.minkowskiSum_def (h g : ℕ → WithTop ℝ) (n : ℕ) : minkowskiSum h g n = (Finset.antidiagonal n).inf fun (p : ℕ × ℕ) => h p.1 + g p.2

The Minkowski sum is the infimum over the antidiagonal of sums of heights.

theorem TauCeti.minkowskiSum_add_le (h g : ℕ → WithTop ℝ) (i j : ℕ) : minkowskiSum h g (i + j) ≤ h i + g j

Every split of an index bounds the Minkowski sum from above.

theorem TauCeti.minkowskiSum_le_add_of_add_eq {h g : ℕ → WithTop ℝ} {i j n : ℕ} (hij : i + j = n) : minkowskiSum h g n ≤ h i + g j

Every split n = i + j bounds the Minkowski sum at n from above.

theorem TauCeti.le_minkowskiSum_iff {h g : ℕ → WithTop ℝ} {n : ℕ} {r : WithTop ℝ} : r ≤ minkowskiSum h g n ↔ ∀ (i j : ℕ), i + j = n → r ≤ h i + g j

A lower bound for the Minkowski sum is a lower bound for every split.

theorem TauCeti.exists_minkowskiSum_eq (h g : ℕ → WithTop ℝ) (n : ℕ) : ∃ (i : ℕ) (j : ℕ), i + j = n ∧ minkowskiSum h g n = h i + g j

The Minkowski sum is attained by some split.

theorem TauCeti.minkowskiSum_ne_top_iff {h g : ℕ → WithTop ℝ} {n : ℕ} : minkowskiSum h g n ≠ ⊤ ↔ ∃ (i : ℕ) (j : ℕ), i + j = n ∧ h i ≠ ⊤ ∧ g j ≠ ⊤

The Minkowski sum is finite exactly at sums of finite indices.

theorem TauCeti.minkowskiSum_eq_top_iff {h g : ℕ → WithTop ℝ} {n : ℕ} : minkowskiSum h g n = ⊤ ↔ ∀ (i j : ℕ), i + j = n → h i = ⊤ ∨ g j = ⊤

The Minkowski sum is infinite exactly when every split meets an infinite height.

theorem TauCeti.minkowskiSum_mono {h g h' g' : ℕ → WithTop ℝ} (hh : h ≤ h') (hg : g ≤ g') : minkowskiSum h g ≤ minkowskiSum h' g'

The Minkowski sum is monotone in both height sequences.

Tropicalisation and the algebraic laws

theorem TauCeti.mk_trop_minkowskiSum (h g : ℕ → WithTop ℝ) : (PowerSeries.mk fun (n : ℕ) => MinTropical.trop (minkowskiSum h g n)) = (PowerSeries.mk fun (n : ℕ) => MinTropical.trop (h n)) * PowerSeries.mk fun (n : ℕ) => MinTropical.trop (g n)

Tropicalisation turns the Minkowski sum of height sequences into the product of the corresponding power series over the tropical semiring MinTropical (WithTop ℝ).

theorem TauCeti.minkowskiSum_comm (h g : ℕ → WithTop ℝ) : minkowskiSum h g = minkowskiSum g h

The Minkowski sum is symmetric.

theorem TauCeti.minkowskiSum_assoc (h g k : ℕ → WithTop ℝ) : minkowskiSum (minkowskiSum h g) k = minkowskiSum h (minkowskiSum g k)

The Minkowski sum is associative.

theorem TauCeti.minkowskiSum_ite_eq (h : ℕ → WithTop ℝ) (k : ℕ) (c : WithTop ℝ) (n : ℕ) : minkowskiSum h (fun (m : ℕ) => if m = k then c else ⊤) n = if k ≤ n then h (n - k) + c else ⊤

Adding a single point at (k, c) shifts the indices by k and the heights by c.

@[simp]

theorem TauCeti.minkowskiSum_ite_eq_zero (h : ℕ → WithTop ℝ) : (minkowskiSum h fun (m : ℕ) => if m = 0 then 0 else ⊤) = h

The singleton at (0, 0) is an identity for the Minkowski sum.

@[simp]

theorem TauCeti.ite_eq_zero_minkowskiSum (h : ℕ → WithTop ℝ) : minkowskiSum (fun (m : ℕ) => if m = 0 then 0 else ⊤) h = h

The singleton at (0, 0) is an identity for the Minkowski sum.

@[simp]

theorem TauCeti.minkowskiSum_top (h : ℕ → WithTop ℝ) : minkowskiSum h ⊤ = ⊤

The empty polygon is absorbing for the Minkowski sum.

@[simp]

theorem TauCeti.top_minkowskiSum (g : ℕ → WithTop ℝ) : minkowskiSum ⊤ g = ⊤

The empty polygon is absorbing for the Minkowski sum.

First and last points

theorem TauCeti.minkowskiSum_eq_top_of_lt_add {h g : ℕ → WithTop ℝ} {i j n : ℕ} (hi : ∀ k < i, h k = ⊤) (hj : ∀ k < j, g k = ⊤) (hn : n < i + j) : minkowskiSum h g n = ⊤

Before the sum of the first finite indices, the Minkowski sum is infinite.

theorem TauCeti.minkowskiSum_add_eq_of_forall_lt {h g : ℕ → WithTop ℝ} {i j : ℕ} (hi : ∀ k < i, h k = ⊤) (hj : ∀ k < j, g k = ⊤) : minkowskiSum h g (i + j) = h i + g j

First points add: if h and g are infinite before i and j, the Minkowski sum at i + j is h i + g j.

theorem TauCeti.minkowskiSum_eq_top_of_add_lt {h g : ℕ → WithTop ℝ} {i j n : ℕ} (hi : ∀ (k : ℕ), i < k → h k = ⊤) (hj : ∀ (k : ℕ), j < k → g k = ⊤) (hn : i + j < n) : minkowskiSum h g n = ⊤

After the sum of the last finite indices, the Minkowski sum is infinite.

theorem TauCeti.minkowskiSum_add_eq_of_forall_gt {h g : ℕ → WithTop ℝ} {i j : ℕ} (hi : ∀ (k : ℕ), i < k → h k = ⊤) (hj : ∀ (k : ℕ), j < k → g k = ⊤) : minkowskiSum h g (i + j) = h i + g j

Last points add: if h and g are infinite after i and j, the Minkowski sum at i + j is h i + g j.

Convexity

theorem TauCeti.ordConnected_minkowskiSum {h g : ℕ → WithTop ℝ} (hh : {n : ℕ | h n ≠ ⊤}.OrdConnected) (hg : {n : ℕ | g n ≠ ⊤}.OrdConnected) : {n : ℕ | minkowskiSum h g n ≠ ⊤}.OrdConnected

The finite domain of a Minkowski sum of sequences with order-connected finite domains is order connected.

theorem TauCeti.minkowskiSum_succ_add_succ_le {h g : ℕ → WithTop ℝ} (hh : IsConvexSeq h) (hg : IsConvexSeq g) (n : ℕ) : minkowskiSum h g (n + 1) + minkowskiSum h g (n + 1) ≤ minkowskiSum h g n + minkowskiSum h g (n + 2)

The second-difference inequality for the Minkowski sum of convex sequences, in WithTop ℝ.

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

The Minkowski sum of convex height sequences is convex.

Supporting values

theorem TauCeti.supportingValue_minkowskiSum {h g : ℕ → WithTop ℝ} (hh : h ≠ ⊤) (hg : g ≠ ⊤) (σ : ℝ) : supportingValue (minkowskiSum h g) σ = supportingValue h σ + supportingValue g σ

For nonempty height sequences, the supporting values of their Minkowski sum are the sums of their supporting values. The nonemptiness hypotheses are needed: if h = ⊤ and the supporting value of g is ⊥, the left side is ⊤ while ⊤ + ⊥ = ⊥ in EReal.

theorem TauCeti.supportingValue_minkowskiSum_of_ne_bot {h g : ℕ → WithTop ℝ} {σ : ℝ} (hh : supportingValue h σ ≠ ⊥) (hg : supportingValue g σ ≠ ⊥) : supportingValue (minkowskiSum h g) σ = supportingValue h σ + supportingValue g σ

Supporting values of a Minkowski sum add in EReal whenever neither summand has supporting value ⊥. Compared with supportingValue_minkowskiSum, this allows either sequence to be empty: then both sides are ⊤.

Minimising splits

theorem TauCeti.minkowskiSum_add_eq_of_mem_supportingFace {h g : ℕ → WithTop ℝ} {σ c d : ℝ} {i j : ℕ} (hc : IsSupportingLine h σ c) (hi : i ∈ supportingFace h σ c) (hd : IsSupportingLine g σ d) (hj : j ∈ supportingFace g σ d) : minkowskiSum h g (i + j) = h i + g j

A split n = i + j at which h and g touch supporting lines of a common slope attains the Minkowski sum.

theorem TauCeti.minkowskiSum_add_eq_add_iff {h g : ℕ → WithTop ℝ} (hh : IsConvexSeq h) (hg : IsConvexSeq g) {i j : ℕ} (hi : h i ≠ ⊤) (hj : g j ≠ ⊤) : minkowskiSum h g (i + j) = h i + g j ↔ ∃ (σ : ℝ) (c : ℝ) (d : ℝ), IsSupportingLine h σ c ∧ i ∈ supportingFace h σ c ∧ IsSupportingLine g σ d ∧ j ∈ supportingFace g σ d

For convex sequences with finite heights at i and j, the split i + j attains the Minkowski sum exactly when i and j lie on supporting faces of h and g of a common slope.