Finite polygonal paths in the complex plane

The carrier for a finite polygonal path -- n edges presented as n + 1 vertices Fin (n + 1) → ℂ -- together with its Euclidean length, the two real continuous linear functionals on ℂ that the perimeter arguments support against, and the supporting-hyperplane form of strict clockwise convexity.

Main declarations

• crossFunctional r, the oriented area functional z ↦ r × z, and unitRay θ, the unit vector at angle θ.
• length, the Euclidean length of a finite path, and norm_last_sub_zero_le_length: the chord is no longer than the path.
• exists_strict_support_at_interior: at an interior vertex of a path whose upper-half-plane edge arguments strictly decrease, some real-linear functional attains a strict unique maximum there.

Placement

This is neutral planar geometry and imports no category theory and no stability -- which is why it is not under CategoryTheory/Abelian/Stability/, where MO1.08 (#1319) placed the rest of that directory. It was the ComplexPolygonalPath block of what is now CategoryTheory/Abelian/Stability/HNPolygon.lean until MO1.13 (#1324); nothing in it mentions an object, a filtration or a stability function, and the Harder--Narasimhan reading of these statements -- that the vertices are subobject charges and the edges are semistable-factor charges -- is the adapter that stayed behind in HNPolygon.lean.

The perimeter comparison built on this carrier is the sibling ComplexPolygonalPath/Perimeter.lean.

Analysis/ is a new top-level subject, added to KNOWN_SUBJECTS in scripts/check_layering.py as the conscious act rule 6 requires. The pinned Mathlib revision has no polygonal-chain length and no perimeter at all (Mathlib.Geometry.Polygon.Basic supplies a vertex tuple with edges and a boundary, and stops there), so there was no Mathlib owner to reuse; the convexity API these files do consume, convexHull, is owned at that revision by Mathlib/Analysis/Convex/Hull.lean, which is what names the subject.

Declaration names and the CategoryTheory.Triangulated.ComplexPolygonalPath namespace are unchanged, per standing decision 1 of the cutover ledger.

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

The oriented area functional z ↦ r × z, regarded as a continuous real-linear functional on the complex plane.

Equations

• CategoryTheory.Triangulated.ComplexPolygonalPath.crossFunctional r = r.re • Complex.imCLM - r.im • Complex.reCLM

@[simp]

theorem CategoryTheory.Triangulated.ComplexPolygonalPath.crossFunctional_apply (r z : ℂ) : (crossFunctional r) z = r.re * z.im - r.im * z.re

noncomputable def CategoryTheory.Triangulated.ComplexPolygonalPath.unitRay (θ : ℝ) : ℂ

The unit complex vector at angle θ.

Equations

• CategoryTheory.Triangulated.ComplexPolygonalPath.unitRay θ = ↑(Real.cos θ) + ↑(Real.sin θ) * Complex.I

@[simp]

theorem CategoryTheory.Triangulated.ComplexPolygonalPath.unitRay_re (θ : ℝ) : (unitRay θ).re = Real.cos θ

@[simp]

theorem CategoryTheory.Triangulated.ComplexPolygonalPath.unitRay_im (θ : ℝ) : (unitRay θ).im = Real.sin θ

theorem CategoryTheory.Triangulated.ComplexPolygonalPath.unitRay_mem_semiClosedUpperHalfPlane {θ : ℝ} (hθ₀ : 0 < θ) (hθπ : θ < Real.pi) : unitRay θ ∈ semiClosedUpperHalfPlane

A unit ray at an angle strictly between 0 and π lies in the open upper half-plane.

theorem CategoryTheory.Triangulated.ComplexPolygonalPath.arg_unitRay {θ : ℝ} (hθ₀ : 0 < θ) (hθπ : θ < Real.pi) : (unitRay θ).arg = θ

On the principal upper-half-plane branch, the argument of unitRay θ is literally θ.

theorem CategoryTheory.Triangulated.ComplexPolygonalPath.crossFunctional_pos_of_arg_lt {r z : ℂ} (hr : r ∈ semiClosedUpperHalfPlane) (hz : z ∈ semiClosedUpperHalfPlane) (harg : r.arg < z.arg) : 0 < (crossFunctional r) z

The cross functional is positive on a vector of strictly larger upper-half-plane argument.

theorem CategoryTheory.Triangulated.ComplexPolygonalPath.crossFunctional_neg_of_arg_lt {r z : ℂ} (hr : r ∈ semiClosedUpperHalfPlane) (hz : z ∈ semiClosedUpperHalfPlane) (harg : z.arg < r.arg) : (crossFunctional r) z < 0

The cross functional is negative on a vector of strictly smaller upper-half-plane argument.

theorem CategoryTheory.Triangulated.ComplexPolygonalPath.exists_strict_support_at_interior {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) : ∃ (l : ℂ →L[ℝ] ℝ), ∀ (j : Fin (n + 1)), j ≠ k → l (z j) < l (z k)

At every interior vertex of a finite path whose upper-half-plane edge arguments strictly decrease, some real-linear functional has a strict unique maximum among the path vertices. This is the supporting-hyperplane form of strict clockwise convexity.

theorem CategoryTheory.Triangulated.ComplexPolygonalPath.sum_edges_eq_last_sub_zero {n : ℕ} (z : Fin (n + 1) → ℂ) : ∑ i : Fin n, (z i.succ - z i.castSucc) = z (Fin.last n) - z 0

The sum of the directed edges of a finite path is its endpoint displacement.

theorem CategoryTheory.Triangulated.ComplexPolygonalPath.arg_last_sub_zero_le_arg_first {n : ℕ} (z : Fin (n + 1) → ℂ) (hn : 0 < n) (hedge : ∀ (i : Fin n), z i.succ - z i.castSucc ∈ semiClosedUpperHalfPlane) (harg : Antitone fun (i : Fin n) => (z i.succ - z i.castSucc).arg) : (z (Fin.last n) - z 0).arg ≤ (z ⟨0, hn⟩.succ - z ⟨0, hn⟩.castSucc).arg

For an upper-half-plane path with decreasing edge arguments, the argument of its total displacement is bounded above by the argument of its first edge.

theorem CategoryTheory.Triangulated.ComplexPolygonalPath.arg_last_edge_le_arg_last_sub_zero {n : ℕ} (z : Fin (n + 1) → ℂ) (hn : 0 < n) (hedge : ∀ (i : Fin n), z i.succ - z i.castSucc ∈ semiClosedUpperHalfPlane) (harg : Antitone fun (i : Fin n) => (z i.succ - z i.castSucc).arg) : (z ⟨n - 1, ⋯⟩.succ - z ⟨n - 1, ⋯⟩.castSucc).arg ≤ (z (Fin.last n) - z 0).arg

For an upper-half-plane path with decreasing edge arguments, the argument of its last edge is bounded above by the argument of its total displacement.

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

The Euclidean length of a finite path in the complex plane. A path with n edges is represented by its n + 1 vertices.

Equations

• CategoryTheory.Triangulated.ComplexPolygonalPath.length z = ∑ i : Fin n, ‖z i.succ - z i.castSucc‖

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

The straight chord between the endpoints of a finite complex path is no longer than the path. This is the metric primitive used when an HN polygonal boundary is refined by inserting further vertices.