Finite sums in the semi-closed upper half-plane

This file extends the neutral phase-geometry API in Analysis/Complex/PhaseGeometry.lean from binary sums to nonempty finite sums, and records the determinant formulations the HN-polygon proofs use.

Nothing here is categorical or stability-theoretic -- which is exactly why it is not under CategoryTheory/Abelian/Stability/, where MO1.08 (#1319) placed the rest of that directory. It sat under StabilityCondition/Weak/Foundation/StabilityFunction/ until MO1.13 (#1324), which moved it so that the Euclidean core of the mass-subadditivity proof could reach these bounds without reaching stability. Declaration names and the CategoryTheory.Triangulated namespace are unchanged.

theorem CategoryTheory.Triangulated.mem_semiClosedUpperHalfPlane_of_arg_pos {z : ℂ} (hz : 0 < z.arg) : z ∈ semiClosedUpperHalfPlane

Positive argument places a complex number in the semi-closed upper half-plane.

theorem CategoryTheory.Triangulated.sum_mem_semiClosedUpperHalfPlane {ι : Type u_1} {s : Finset ι} (hs : s.Nonempty) {f : ι → ℂ} (hf : ∀ i ∈ s, f i ∈ semiClosedUpperHalfPlane) : ∑ i ∈ s, f i ∈ semiClosedUpperHalfPlane

A nonempty finite sum of upper-half-plane vectors stays in that half-plane.

theorem CategoryTheory.Triangulated.arg_sum_le_sup_of_semiClosedUpperHalfPlane {ι : Type u_1} {s : Finset ι} (hs : s.Nonempty) {f : ι → ℂ} (hf : ∀ i ∈ s, f i ∈ semiClosedUpperHalfPlane) : (∑ i ∈ s, f i).arg ≤ s.sup' hs (Complex.arg ∘ f)

The argument of a nonempty upper-half-plane sum is at most the largest summand argument.

theorem CategoryTheory.Triangulated.inf_le_arg_sum_of_semiClosedUpperHalfPlane {ι : Type u_1} {s : Finset ι} (hs : s.Nonempty) {f : ι → ℂ} (hf : ∀ i ∈ s, f i ∈ semiClosedUpperHalfPlane) : s.inf' hs (Complex.arg ∘ f) ≤ (∑ i ∈ s, f i).arg

The argument of a nonempty upper-half-plane sum is at least the smallest summand argument.

theorem CategoryTheory.Triangulated.cross_nonneg_of_arg_le {z w : ℂ} (hzIm : 0 ≤ z.im) (hz : z ≠ 0) (hw : w ≠ 0) (harg : z.arg ≤ w.arg) : 0 ≤ z.re * w.im - z.im * w.re

Nondecreasing arguments give a nonnegative planar cross product.

theorem CategoryTheory.Triangulated.arg_le_of_cross_nonneg {z w : ℂ} (hz : z ≠ 0) (hw : w ≠ 0) (hwArg : 0 < w.arg) (hcross : 0 ≤ z.re * w.im - z.im * w.re) : z.arg ≤ w.arg

A nonnegative cross product recovers the argument order in the upper half-plane.

theorem CategoryTheory.Triangulated.cross_pos_of_arg_lt {z w : ℂ} (hzArg : 0 < z.arg) (hz : z ≠ 0) (hw : w ≠ 0) (harg : z.arg < w.arg) : 0 < z.re * w.im - z.im * w.re

Strictly increasing positive arguments give a positive planar cross product.