Minkowski sums of finite slope data

The Minkowski sum of two nonempty convex polygons with finite domain is again such a polygon. This file transports minkowskiSum to the finite unit-slope presentation FiniteSlopeData ℝ. The first points add, the horizontal lengths add, and the finite slope multisets add. The last statement is the geometric input to the additivity of the slope multisets of Newton polygons of polynomials under multiplication.

The slope multiset is compared through face widths: at every real slope σ both polygons have a finite face, the face of the sum at σ is the sum of these faces, and the multiplicity of σ is the width of the face.

Main results

• FiniteSlopeData.minkowskiSum: the slope data of the Minkowski sum of the represented polygons, with FiniteSlopeData.heights_minkowskiSum.
• FiniteSlopeData.minkowskiSum_start, FiniteSlopeData.minkowskiSum_initialHeight, FiniteSlopeData.minkowskiSum_length: anchors and horizontal lengths add.
• FiniteSlopeData.slopeMultiset_minkowskiSum: finite slope multisets add.

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.FiniteSlopeData.minkowskiSum (d₁ d₂ : FiniteSlopeData ℝ) : FiniteSlopeData ℝ

The finite slope data of the Minkowski sum of the polygons represented by d₁ and d₂. Its heights are the min-convolution of their heights.

@[simp]

theorem TauCeti.FiniteSlopeData.heights_minkowskiSum (d₁ d₂ : FiniteSlopeData ℝ) : (d₁.minkowskiSum d₂).heights = TauCeti.minkowskiSum d₁.heights d₂.heights

The Minkowski sum of slope data represents the Minkowski sum of the heights.

theorem TauCeti.FiniteSlopeData.eq_minkowskiSum_iff (d₁ d₂ : FiniteSlopeData ℝ) {d : FiniteSlopeData ℝ} : d = d₁.minkowskiSum d₂ ↔ d.heights = TauCeti.minkowskiSum d₁.heights d₂.heights

Slope data represents a Minkowski sum exactly when it is the Minkowski sum of the slope data.

@[simp]

theorem TauCeti.FiniteSlopeData.minkowskiSum_start (d₁ d₂ : FiniteSlopeData ℝ) : (d₁.minkowskiSum d₂).start = d₁.start + d₂.start

The first index of a Minkowski sum is the sum of the first indices.

@[simp]

theorem TauCeti.FiniteSlopeData.minkowskiSum_length (d₁ d₂ : FiniteSlopeData ℝ) : (d₁.minkowskiSum d₂).length = d₁.length + d₂.length

The horizontal length of a Minkowski sum is the sum of the horizontal lengths.

@[simp]

theorem TauCeti.FiniteSlopeData.minkowskiSum_initialHeight (d₁ d₂ : FiniteSlopeData ℝ) : (d₁.minkowskiSum d₂).initialHeight = d₁.initialHeight + d₂.initialHeight

The initial height of a Minkowski sum is the sum of the initial heights.

theorem TauCeti.FiniteSlopeData.minkowskiSum_comm (d₁ d₂ : FiniteSlopeData ℝ) : d₁.minkowskiSum d₂ = d₂.minkowskiSum d₁

The Minkowski sum of finite slope data is commutative.

theorem TauCeti.FiniteSlopeData.minkowskiSum_assoc (d₁ d₂ d₃ : FiniteSlopeData ℝ) : (d₁.minkowskiSum d₂).minkowskiSum d₃ = d₁.minkowskiSum (d₂.minkowskiSum d₃)

The Minkowski sum of finite slope data is associative.

@[simp]

theorem TauCeti.FiniteSlopeData.slopeMultiset_minkowskiSum (d₁ d₂ : FiniteSlopeData ℝ) : (d₁.minkowskiSum d₂).slopeMultiset = d₁.slopeMultiset + d₂.slopeMultiset

The finite slope multiset of a Minkowski sum is the sum of the finite slope multisets.