Convex-polygon perimeter comparison

The Euclidean (t = 0) polygon comparison: if one nonempty upper-half-plane path turns with strictly decreasing edge arguments and its closed vertex hull sits inside another path's vertex hull, the first path is no longer than the second. The proof is finite-dimensional -- supporting functionals select a monotone subsequence of the outer boundary, and discrete integration by parts reduces the perimeter comparison to the triangle inequality.

Main declarations

• chainLength and closedLength, the open and closed perimeters, with closedLength_eq_sum_turning: a closed perimeter is its discrete support sum.
• closedLength_le_of_monotone_support, the finite support-fan comparison.
• length_le_of_convexHull_subset, the comparison itself.

Source

This is the t = 0 case of Ikeda, A phase limit formula and the space of stability conditions, Lemma 3.7, slightly strengthened: no decreasing-turn hypothesis is needed for the outer path, because the proof only selects a monotone subsequence of its support-maximizing vertices and any remaining turns can only increase the outer length. The Harder--Narasimhan reading of the comparison, and Ikeda's Lemma 3.8 built on it, are the stability adapter StabilityCondition/Mass/Subadditivity/HNPolygonComparison.lean.

Placement

Neutral planar geometry: this file imports no category theory and no stability, and every statement quantifies over vertices in ℂ. It was the first two-thirds of StabilityCondition/Metric/Mass/Subadditivity/PolygonPerimeter.lean -- a Euclidean perimeter argument living inside a mass-subadditivity proof directory -- until MO1.13 (#1324). See ComplexPolygonalPath/Basic.lean for why Analysis/ is the subject and why the namespace did not move with the path.

noncomputable def CategoryTheory.Triangulated.ComplexPolygonalPath.dotFunctional (r : ℂ) : ℂ →L[ℝ] ℝ

The Euclidean scalar product with r, bundled as a continuous real-linear functional.

Equations

• CategoryTheory.Triangulated.ComplexPolygonalPath.dotFunctional r = r.re • Complex.reCLM + r.im • Complex.imCLM

@[simp]

theorem CategoryTheory.Triangulated.ComplexPolygonalPath.dotFunctional_apply (r z : ℂ) : (dotFunctional r) z = r.re * z.re + r.im * z.im

noncomputable def CategoryTheory.Triangulated.ComplexPolygonalPath.unitDirection (z : ℂ) : ℂ

The direction of a vector, with the zero vector assigned direction zero.

Equations

• CategoryTheory.Triangulated.ComplexPolygonalPath.unitDirection z = ↑‖z‖⁻¹ * z

theorem CategoryTheory.Triangulated.ComplexPolygonalPath.norm_unitDirection_le_one (z : ℂ) : ‖unitDirection z‖ ≤ 1

theorem CategoryTheory.Triangulated.ComplexPolygonalPath.dotFunctional_unitDirection_self (z : ℂ) : (dotFunctional (unitDirection z)) z = ‖z‖

theorem CategoryTheory.Triangulated.ComplexPolygonalPath.unitDirection_eq_unitRay_arg {z : ℂ} (hz : z ≠ 0) : unitDirection z = unitRay z.arg

A nonzero vector's normalized direction is the unit ray at its principal argument.

theorem CategoryTheory.Triangulated.ComplexPolygonalPath.dotFunctional_le_norm_mul (r z : ℂ) : (dotFunctional r) z ≤ ‖r‖ * ‖z‖

Cauchy--Schwarz in the concrete scalar-product notation used below.

theorem CategoryTheory.Triangulated.ComplexPolygonalPath.dotFunctional_sub_left (r s z : ℂ) : (dotFunctional (r - s)) z = (dotFunctional r) z - (dotFunctional s) z

theorem CategoryTheory.Triangulated.ComplexPolygonalPath.dotFunctional_sub_right (r z w : ℂ) : (dotFunctional r) (z - w) = (dotFunctional r) z - (dotFunctional r) w

theorem CategoryTheory.Triangulated.ComplexPolygonalPath.dotFunctional_unitRay_sub (a b : ℝ) (z : ℂ) : (dotFunctional (unitRay a - unitRay b)) z = 2 * Real.sin ((a - b) / 2) * (crossFunctional (unitRay ((a + b) / 2))) z

The turn between two unit rays is a positive multiple of the cross functional at their angular bisector.

noncomputable def CategoryTheory.Triangulated.ComplexPolygonalPath.chainLength : List ℂ → ℝ

Length of a list viewed as a polygonal chain.

Equations

• CategoryTheory.Triangulated.ComplexPolygonalPath.chainLength [] = 0
• CategoryTheory.Triangulated.ComplexPolygonalPath.chainLength (y :: ys) = CategoryTheory.Triangulated.ComplexPolygonalPath.chainLengthFrom✝ y ys

@[simp]

theorem CategoryTheory.Triangulated.ComplexPolygonalPath.chainLength_nil : chainLength [] = 0

@[simp]

theorem CategoryTheory.Triangulated.ComplexPolygonalPath.chainLength_singleton (x : ℂ) : chainLength [x] = 0

@[simp]

theorem CategoryTheory.Triangulated.ComplexPolygonalPath.chainLength_cons_cons (x y : ℂ) (xs : List ℂ) : chainLength (x :: y :: xs) = ‖y - x‖ + chainLength (y :: xs)

theorem CategoryTheory.Triangulated.ComplexPolygonalPath.chainLength_mono_sublist {xs ys : List ℂ} (h : xs.Sublist ys) : chainLength xs ≤ chainLength ys

Polygonal-chain length is monotone under taking a sublist. This is the finite triangle inequality in the exact form needed for monotone support selectors.

theorem CategoryTheory.Triangulated.ComplexPolygonalPath.chainLength_comp_monotone_le {n m : ℕ} (w : Fin (m + 1) → ℂ) (q : Fin (n + 1) → Fin (m + 1)) (hq : Monotone q) : chainLength (List.ofFn fun (i : Fin (n + 1)) => w (q i)) ≤ chainLength (List.ofFn w)

A monotone choice of vertices gives a chain no longer than the original finite chain. Repeated choices are harmless and are removed by destutter.

theorem CategoryTheory.Triangulated.ComplexPolygonalPath.chainLength_ofFn_eq_length {n : ℕ} (z : Fin (n + 1) → ℂ) : chainLength (List.ofFn z) = length z

The list and Fin presentations of an open polygonal path have the same length.

def CategoryTheory.Triangulated.ComplexPolygonalPath.closedEdge {n : ℕ} (z : Fin (n + 1) → ℂ) (i : Fin (n + 1)) : ℂ

The cyclic edge leaving a vertex; the last vertex is joined back to the first by finRotate.

Equations

• CategoryTheory.Triangulated.ComplexPolygonalPath.closedEdge z i = z ((finRotate (n + 1)) i) - z i

noncomputable def CategoryTheory.Triangulated.ComplexPolygonalPath.closedLength {n : ℕ} (z : Fin (n + 1) → ℂ) : ℝ

The perimeter of the closed polygonal chain obtained by adjoining the last-to-first chord.

Equations

• CategoryTheory.Triangulated.ComplexPolygonalPath.closedLength z = ∑ i : Fin (n + 1), ‖CategoryTheory.Triangulated.ComplexPolygonalPath.closedEdge z i‖

noncomputable def CategoryTheory.Triangulated.ComplexPolygonalPath.closedTangent {n : ℕ} (z : Fin (n + 1) → ℂ) (i : Fin (n + 1)) : ℂ

The unit direction of a cyclic edge.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.Triangulated.ComplexPolygonalPath.turningFunctional {n : ℕ} (z : Fin (n + 1) → ℂ) (i : Fin (n + 1)) : ℂ →L[ℝ] ℝ

The outward turning functional at a cyclic vertex.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Triangulated.ComplexPolygonalPath.closedLength_eq_sum_turning {n : ℕ} (z : Fin (n + 1) → ℂ) : closedLength z = ∑ i : Fin (n + 1), (turningFunctional z i) (z i)

A closed perimeter is its discrete support sum. This is the finite integration-by-parts identity behind the comparison theorem.

theorem CategoryTheory.Triangulated.ComplexPolygonalPath.closedLength_eq_length_add_chord {n : ℕ} (z : Fin (n + 1) → ℂ) : closedLength z = length z + ‖z 0 - z (Fin.last n)‖

Closing an open path adds exactly its endpoint chord.

theorem CategoryTheory.Triangulated.ComplexPolygonalPath.length_snoc {n : ℕ} (z : Fin (n + 1) → ℂ) (a : ℂ) : length (Fin.snoc z a) = length z + ‖a - z (Fin.last n)‖

Appending one terminal vertex appends exactly one edge to an open polygonal path.

theorem CategoryTheory.Triangulated.ComplexPolygonalPath.closedLength_comp_monotone_le {n m : ℕ} (w : Fin (m + 1) → ℂ) (q : Fin (n + 1) → Fin (m + 1)) (hq : Monotone q) (hq₀ : q 0 = 0) (hq_last : q (Fin.last n) = Fin.last m) : (closedLength fun (i : Fin (n + 1)) => w (q i)) ≤ closedLength w

A monotone vertex selector preserving the two endpoints cannot increase closed perimeter.

theorem CategoryTheory.Triangulated.ComplexPolygonalPath.closedLength_le_of_monotone_support {n m : ℕ} (z : Fin (n + 1) → ℂ) (w : Fin (m + 1) → ℂ) (q : Fin (n + 1) → Fin (m + 1)) (hq : Monotone q) (hq₀ : q 0 = 0) (hq_last : q (Fin.last n) = Fin.last m) (hsupport : ∀ (i : Fin (n + 1)), (turningFunctional z i) (z i) ≤ (turningFunctional z i) (w (q i))) : closedLength z ≤ closedLength w

Finite support-fan perimeter comparison. If each turning functional of a closed inner chain is no larger at its inner vertex than at a monotone choice of outer vertices, then the inner perimeter is no larger than the outer perimeter.

theorem CategoryTheory.Triangulated.ComplexPolygonalPath.last_sub_zero_mem_semiClosedUpperHalfPlane {n : ℕ} (hn : 0 < n) (z : Fin (n + 1) → ℂ) (hedge : ∀ (i : Fin n), z i.succ - z i.castSucc ∈ semiClosedUpperHalfPlane) : z (Fin.last n) - z 0 ∈ semiClosedUpperHalfPlane

A nonempty path all of whose edges lie in the semi-closed upper half-plane has endpoint displacement in that half-plane.

theorem CategoryTheory.Triangulated.ComplexPolygonalPath.sub_mem_semiClosedUpperHalfPlane_of_lt {n : ℕ} (z : Fin (n + 1) → ℂ) (hedge : ∀ (i : Fin n), z i.succ - z i.castSucc ∈ semiClosedUpperHalfPlane) {a b : Fin (n + 1)} (hba : b < a) : z a - z b ∈ semiClosedUpperHalfPlane

Every forward chord of such a path remains in the semi-closed upper half-plane.

def CategoryTheory.Triangulated.ComplexPolygonalPath.interiorPrevEdge {n : ℕ} (z : Fin (n + 1) → ℂ) (k : Fin (n + 1)) (hk₀ : 0 < k) : ℂ

The incoming open edge at an interior vertex.

Equations

• CategoryTheory.Triangulated.ComplexPolygonalPath.interiorPrevEdge z k hk₀ = z ⟨↑k - 1, ⋯⟩.succ - z ⟨↑k - 1, ⋯⟩.castSucc

def CategoryTheory.Triangulated.ComplexPolygonalPath.interiorNextEdge {n : ℕ} (z : Fin (n + 1) → ℂ) (k : Fin (n + 1)) (hkn : k < Fin.last n) : ℂ

The outgoing open edge at a nonterminal vertex.

Equations

• CategoryTheory.Triangulated.ComplexPolygonalPath.interiorNextEdge z k hkn = z ⟨↑k, ⋯⟩.succ - z ⟨↑k, ⋯⟩.castSucc

noncomputable def CategoryTheory.Triangulated.ComplexPolygonalPath.interiorBisector {n : ℕ} (z : Fin (n + 1) → ℂ) (k : Fin (n + 1)) (hk₀ : 0 < k) (hkn : k < Fin.last n) : ℝ

The angular bisector of the two open edges at an interior vertex.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.Triangulated.ComplexPolygonalPath.interiorTurnScale {n : ℕ} (z : Fin (n + 1) → ℂ) (k : Fin (n + 1)) (hk₀ : 0 < k) (hkn : k < Fin.last n) : ℝ

The positive scale relating a turn to its bisector support.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Triangulated.ComplexPolygonalPath.turningFunctional_interior_eq_cross {n : ℕ} (z : Fin (n + 1) → ℂ) (hedge : ∀ (i : Fin n), z i.succ - z i.castSucc ∈ semiClosedUpperHalfPlane) (k : Fin (n + 1)) (hk₀ : 0 < k) (hkn : k < Fin.last n) (x : ℂ) : (turningFunctional z k) x = interiorTurnScale z k hk₀ hkn * (crossFunctional (unitRay (interiorBisector z k hk₀ hkn))) x

At an interior vertex, the cyclic turning functional is the positive bisector support functional used by the decreasing-argument proof.

theorem CategoryTheory.Triangulated.ComplexPolygonalPath.interiorTurnScale_pos {n : ℕ} (z : Fin (n + 1) → ℂ) (hedge : ∀ (i : Fin n), z i.succ - z i.castSucc ∈ semiClosedUpperHalfPlane) (harg : StrictAnti fun (i : Fin n) => (z i.succ - z i.castSucc).arg) (k : Fin (n + 1)) (hk₀ : 0 < k) (hkn : k < Fin.last n) : 0 < interiorTurnScale z k hk₀ hkn

theorem CategoryTheory.Triangulated.ComplexPolygonalPath.interiorBisector_mem_Ioo {n : ℕ} (z : Fin (n + 1) → ℂ) (hedge : ∀ (i : Fin n), z i.succ - z i.castSucc ∈ semiClosedUpperHalfPlane) (harg : StrictAnti fun (i : Fin n) => (z i.succ - z i.castSucc).arg) (k : Fin (n + 1)) (hk₀ : 0 < k) (hkn : k < Fin.last n) : interiorBisector z k hk₀ hkn ∈ Set.Ioo 0 Real.pi

theorem CategoryTheory.Triangulated.ComplexPolygonalPath.interiorBisector_strictAnti {n : ℕ} (z : Fin (n + 1) → ℂ) (harg : StrictAnti fun (i : Fin n) => (z i.succ - z i.castSucc).arg) {k l : Fin (n + 1)} (hk₀ : 0 < k) (hkn : k < Fin.last n) (hl₀ : 0 < l) (hln : l < Fin.last n) (hkl : k < l) : interiorBisector z l hl₀ hln < interiorBisector z k hk₀ hkn

noncomputable def CategoryTheory.Triangulated.ComplexPolygonalPath.crossMaxIndex {n : ℕ} (z : Fin (n + 1) → ℂ) (θ : ℝ) : Fin (n + 1)

A vertex where the cross support at angle θ is maximal.

Equations

• CategoryTheory.Triangulated.ComplexPolygonalPath.crossMaxIndex z θ = Classical.choose ⋯

theorem CategoryTheory.Triangulated.ComplexPolygonalPath.crossMaxIndex_max {n : ℕ} (z : Fin (n + 1) → ℂ) (θ : ℝ) (j : Fin (n + 1)) : (crossFunctional (unitRay θ)) (z j) ≤ (crossFunctional (unitRay θ)) (z (crossMaxIndex z θ))

theorem CategoryTheory.Triangulated.ComplexPolygonalPath.crossMaxIndex_mono_of_angle_gt {n : ℕ} (z : Fin (n + 1) → ℂ) (hedge : ∀ (i : Fin n), z i.succ - z i.castSucc ∈ semiClosedUpperHalfPlane) {θ₁ θ₂ : ℝ} (hθ₁ : θ₁ ∈ Set.Ioo 0 Real.pi) (hθ₂ : θ₂ ∈ Set.Ioo 0 Real.pi) (hθ : θ₂ < θ₁) : crossMaxIndex z θ₁ ≤ crossMaxIndex z θ₂

As the support angle turns clockwise, a maximizing vertex of a decreasing-argument upper-half-plane path can only move forward.

theorem CategoryTheory.Triangulated.ComplexPolygonalPath.length_le_of_convexHull_subset {n m : ℕ} (hn : 0 < n) (z : Fin (n + 1) → ℂ) (w : Fin (m + 1) → ℂ) (hzero : z 0 = w 0) (hlast : z (Fin.last n) = w (Fin.last m)) (hzedge : ∀ (i : Fin n), z i.succ - z i.castSucc ∈ semiClosedUpperHalfPlane) (hwedge : ∀ (i : Fin m), w i.succ - w i.castSucc ∈ semiClosedUpperHalfPlane) (hzarg : StrictAnti fun (i : Fin n) => (z i.succ - z i.castSucc).arg) (hcontain : (convexHull ℝ) (Set.range z) ⊆ (convexHull ℝ) (Set.range w)) : length z ≤ length w

Ikeda's polygon-perimeter comparison at t = 0. Two nonempty upper-half-plane paths have common endpoints. If the inner path turns with strictly decreasing edge arguments and its closed vertex hull is contained in the outer vertex hull, then its Euclidean length is no larger than the outer path length.

This slightly strengthens the literal t = 0 specialization of Ikeda's Lemma 3.7: no decreasing-turn hypothesis is needed for the outer path. The proof only selects a monotone subsequence of its support-maximizing vertices; any remaining turns can only increase the outer polygonal length.

The proof closes both paths by their common endpoint chord, chooses a maximal outer vertex for every inner bisector support, proves those choices are monotone, and applies closedLength_le_of_monotone_support.