Supporting faces of Minkowski sums

Supporting faces of a min-convolution are sums of supporting faces at the same slope. In particular, finite faces have additive absolute endpoints, and the minimising split at either endpoint is unique. These statements isolate the geometric input to the unique dominant-term arguments for coefficient products.

Convexity is not needed once supporting lines and their contact sets are given. Thus the results also apply directly to coefficient heights, before taking a convex envelope. Singleton faces are included; no assertion is made about endpoints of infinite faces.

References

• N. Koblitz, p-adic Numbers, p-adic Analysis, and Zeta-Functions, Chapter IV §3.
• M. Lazard, Les zéros d'une fonction analytique d'une variable sur un corps valué complet, §1, Proposition 1.

theorem TauCeti.IsSupportingLine.minkowskiSum {h g : ℕ → WithTop ℝ} {σ c d : ℝ} (hc : IsSupportingLine h σ c) (hd : IsSupportingLine g σ d) : IsSupportingLine (TauCeti.minkowskiSum h g) σ (c + d)

Supporting lines of a common slope add to a supporting line of the Minkowski sum.

theorem TauCeti.minkowskiSum_add_eq_add_iff_of_mem_supportingFace {h g : ℕ → WithTop ℝ} {σ c d : ℝ} (hc : IsSupportingLine h σ c) (hd : IsSupportingLine g σ d) {i j : ℕ} (hn : i + j ∈ supportingFace (minkowskiSum h g) σ (c + d)) : minkowskiSum h g (i + j) = h i + g j ↔ i ∈ supportingFace h σ c ∧ j ∈ supportingFace g σ d

At a contact index of the sum, a split is minimising exactly when both its indices are contacts with the given supporting lines.

@[simp]

theorem TauCeti.mem_supportingFace_minkowskiSum_iff {h g : ℕ → WithTop ℝ} {σ c d : ℝ} (hc : IsSupportingLine h σ c) (hd : IsSupportingLine g σ d) {n : ℕ} : n ∈ supportingFace (minkowskiSum h g) σ (c + d) ↔ ∃ (i : ℕ) (j : ℕ), i + j = n ∧ i ∈ supportingFace h σ c ∧ j ∈ supportingFace g σ d

A supporting face of the Minkowski sum consists exactly of sums of contact indices for the two supporting lines of the same slope.

theorem TauCeti.IsFiniteFace.minkowskiSum {h g : ℕ → WithTop ℝ} {σ : ℝ} {l u l' u' : ℕ} (hf : IsFiniteFace h σ l u) (hg : IsFiniteFace g σ l' u') : IsFiniteFace (TauCeti.minkowskiSum h g) σ (l + l') (u + u')

Finite faces at a common slope add, with both absolute endpoints adding.

theorem TauCeti.IsFiniteFace.minkowskiSum_left_eq_iff {h g : ℕ → WithTop ℝ} {σ : ℝ} {l u l' u' : ℕ} (hf : IsFiniteFace h σ l u) (hg : IsFiniteFace g σ l' u') {i j : ℕ} (hij : i + j = l + l') : TauCeti.minkowskiSum h g (l + l') = h i + g j ↔ i = l ∧ j = l'

At the left endpoint of the sum face, the only minimising split uses the two left endpoints. All indices here are absolute, not measured from the polygon's anchor.

theorem TauCeti.IsFiniteFace.minkowskiSum_right_eq_iff {h g : ℕ → WithTop ℝ} {σ : ℝ} {l u l' u' : ℕ} (hf : IsFiniteFace h σ l u) (hg : IsFiniteFace g σ l' u') {i j : ℕ} (hij : i + j = u + u') : TauCeti.minkowskiSum h g (u + u') = h i + g j ↔ i = u ∧ j = u'

At the right endpoint of the sum face, the only minimising split uses the two right endpoints. This also applies when one or both faces are singletons.