Phase geometry of the semi-closed upper half-plane

The argument of a sum of two nonzero vectors in the semi-closed upper half-plane lies between their arguments. This is proved directly from the oriented planar determinant phaseCross, and the resulting see-saw bounds are the analytic input for Harder--Narasimhan arguments.

Nothing here is categorical, algebraic or stability-theoretic: every statement quantifies over complex numbers.

Placement

These declarations were the first half of what MO1.08 (#1319) has since renamed CategoryTheory/Abelian/Stability/PhaseGeometry.lean, whose second half -- the StabilityFunction see-saw for a short exact sequence -- needs an abelian category and stayed there, importing this file. MO1.13 (#1324) made the split because the Euclidean core of the mass-subadditivity proof rests on these bounds and is required to be importable with no category theory and no stability.

Declaration names and the CategoryTheory.Triangulated namespace are unchanged; see standing decision 1 of the cutover ledger, and the same note in Analysis/Complex/HalfPlane.lean.

theorem CategoryTheory.Triangulated.im_nonneg_of_mem_semiClosedUpperHalfPlane {z : ℂ} (hz : z ∈ semiClosedUpperHalfPlane) : 0 ≤ z.im

theorem CategoryTheory.Triangulated.add_mem_semiClosedUpperHalfPlane {z w : ℂ} (hz : z ∈ semiClosedUpperHalfPlane) (hw : w ∈ semiClosedUpperHalfPlane) : z + w ∈ semiClosedUpperHalfPlane

theorem CategoryTheory.Triangulated.neg_sum_mem_semiClosedUpperHalfPlane_of_im_eq_zero_of_re_pos {n : ℕ} (hn : 0 < n) (z : Fin n → ℂ) (him : ∀ (i : Fin n), (z i).im = 0) (hre : ∀ (i : Fin n), 0 < (z i).re) : -∑ i : Fin n, z i ∈ semiClosedUpperHalfPlane

The additive step of every boundary argument. A nonempty finite family of charges on the positive real axis has its negated sum on the negative real axis, hence in the semi-closed upper half-plane. Nothing here asks how each 0 < Re was obtained.

def CategoryTheory.Triangulated.phaseCross (z w : ℂ) : ℝ

The oriented determinant of two complex vectors.

Equations

• CategoryTheory.Triangulated.phaseCross z w = z.re * w.im - z.im * w.re

theorem CategoryTheory.Triangulated.phaseCross_eq_norm_mul_sin (z w : ℂ) : phaseCross z w = ‖z‖ * ‖w‖ * Real.sin (w.arg - z.arg)

theorem CategoryTheory.Triangulated.phaseCross_nonneg_of_arg_le {z w : ℂ} (hz_im : 0 ≤ z.im) (hz : z ≠ 0) (hw : w ≠ 0) (harg : z.arg ≤ w.arg) : 0 ≤ phaseCross z w

theorem CategoryTheory.Triangulated.arg_le_of_phaseCross_nonneg {z w : ℂ} (hz : z ≠ 0) (hw : w ≠ 0) (hw_arg : 0 < w.arg) (hcross : 0 ≤ phaseCross z w) : z.arg ≤ w.arg

theorem CategoryTheory.Triangulated.phaseCross_pos_of_arg_lt {z w : ℂ} (hz_arg : 0 < z.arg) (hz : z ≠ 0) (hw : w ≠ 0) (harg : z.arg < w.arg) : 0 < phaseCross z w

theorem CategoryTheory.Triangulated.arg_lt_of_phaseCross_pos {z w : ℂ} (hz : z ≠ 0) (hw : w ≠ 0) (hw_arg : 0 < w.arg) (hcross : 0 < phaseCross z w) : z.arg < w.arg

theorem CategoryTheory.Triangulated.arg_add_le_max {z w : ℂ} (hz : z ∈ semiClosedUpperHalfPlane) (hw : w ∈ semiClosedUpperHalfPlane) : (z + w).arg ≤ max z.arg w.arg

theorem CategoryTheory.Triangulated.min_arg_le_arg_add {z w : ℂ} (hz : z ∈ semiClosedUpperHalfPlane) (hw : w ∈ semiClosedUpperHalfPlane) : min z.arg w.arg ≤ (z + w).arg

theorem CategoryTheory.Triangulated.arg_add_lt_max {z w : ℂ} (hz : z ∈ semiClosedUpperHalfPlane) (hw : w ∈ semiClosedUpperHalfPlane) (hne : z.arg ≠ w.arg) : (z + w).arg < max z.arg w.arg