15.1. ForMathlib: Analysis.SpecialFunctions.Complex.ArgConvexity🔗

15.1.1. upperHalfPlaneUnion🔗

Bridgeland's semi-closed upper half plane: the set \{z \in \mathbb{C} \mid \mathrm{Im}(z) > 0\} \cup \{z \in \mathbb{C} \mid \mathrm{Im}(z) = 0,\ \mathrm{Re}(z) < 0\}. For z in this set, \arg(z) \in (0, \pi], matching Bridgeland's condition Z(E) \in \mathbb{H} \cup \mathbb{R}_{<0}.

Construction: The union of the open upper half plane and the open negative real axis, as a subset of \mathbb{C}.

def

CategoryTheory.upperHalfPlaneUnion : Set ℂ
CategoryTheory.upperHalfPlaneUnion : Set ℂ

Something wrong, better idea? Suggest a change

15.1.2. upperHalfPlaneUnion_ne_zero🔗

Every element of the semi-closed upper half plane is nonzero.

Proof: In the upper half plane case, \mathrm{Im}(z) > 0 \neq 0; on the negative real axis, \mathrm{Re}(z) < 0 \neq 0.

theorem

CategoryTheory.upperHalfPlaneUnion_ne_zero {z : ℂ}
  (hz : z ∈ CategoryTheory.upperHalfPlaneUnion) : z ≠ 0
CategoryTheory.upperHalfPlaneUnion_ne_zero
  {z : ℂ}
  (hz :
    z ∈
      CategoryTheory.upperHalfPlaneUnion) :
  z ≠ 0

Something wrong, better idea? Suggest a change

15.1.3. arg_pos_of_mem_upperHalfPlaneUnion🔗

Every element of the semi-closed upper half plane \{\mathrm{Im}(z) > 0\} \cup \{\mathrm{Im}(z) = 0, \mathrm{Re}(z) < 0\} has strictly positive argument \arg(z) > 0.

Proof: In the strict upper half plane, \arg \geq 0 and \arg = 0 \Rightarrow \mathrm{Im} = 0, contradiction. On the negative real axis, \arg = \pi > 0.

theorem

CategoryTheory.arg_pos_of_mem_upperHalfPlaneUnion {z : ℂ}
  (hz : z ∈ CategoryTheory.upperHalfPlaneUnion) : 0 < z.arg
CategoryTheory.arg_pos_of_mem_upperHalfPlaneUnion
  {z : ℂ}
  (hz :
    z ∈
      CategoryTheory.upperHalfPlaneUnion) :
  0 < z.arg

Something wrong, better idea? Suggest a change

15.1.4. im_nonneg_of_mem_upperHalfPlaneUnion🔗

Every element of the semi-closed upper half plane \{\mathrm{Im}(z) > 0\} \cup \{\mathrm{Im}(z) = 0, \mathrm{Re}(z) < 0\} has nonneg imaginary part.

Proof: Immediate from the two cases in the definition of upperHalfPlaneUnion.

theorem

CategoryTheory.im_nonneg_of_mem_upperHalfPlaneUnion {z : ℂ}
  (hz : z ∈ CategoryTheory.upperHalfPlaneUnion) : 0 ≤ z.im
CategoryTheory.im_nonneg_of_mem_upperHalfPlaneUnion
  {z : ℂ}
  (hz :
    z ∈
      CategoryTheory.upperHalfPlaneUnion) :
  0 ≤ z.im

Something wrong, better idea? Suggest a change

15.1.5. mem_upperHalfPlaneUnion_of_add🔗

The semi-closed upper half plane is closed under addition: if z_1, z_2 \in \overline{\mathbb{H}}, then z_1 + z_2 \in \overline{\mathbb{H}}.

Proof: Case split: if either \mathrm{Im}(z_j) > 0, the sum has positive imaginary part. Otherwise both lie on the negative real axis, so the sum has \mathrm{Im} = 0 and \mathrm{Re} < 0.

theorem

CategoryTheory.mem_upperHalfPlaneUnion_of_add {z₁ z₂ : ℂ}
  (h₁ : z₁ ∈ CategoryTheory.upperHalfPlaneUnion)
  (h₂ : z₂ ∈ CategoryTheory.upperHalfPlaneUnion) :
  z₁ + z₂ ∈ CategoryTheory.upperHalfPlaneUnion
CategoryTheory.mem_upperHalfPlaneUnion_of_add
  {z₁ z₂ : ℂ}
  (h₁ :
    z₁ ∈
      CategoryTheory.upperHalfPlaneUnion)
  (h₂ :
    z₂ ∈
      CategoryTheory.upperHalfPlaneUnion) :
  z₁ + z₂ ∈
    CategoryTheory.upperHalfPlaneUnion

Something wrong, better idea? Suggest a change

15.1.6. cross_eq_norm_mul_sin🔗

The 2D cross product satisfies z_1.\mathrm{re} \cdot z_2.\mathrm{im} - z_1.\mathrm{im} \cdot z_2.\mathrm{re} = \|z_1\| \cdot \|z_2\| \cdot \sin(\arg z_2 - \arg z_1).

Proof: Substitute the polar decompositions z_j = \|z_j\|(\cos(\arg z_j) + i\sin(\arg z_j)) and apply the sine subtraction formula.

theorem

CategoryTheory.cross_eq_norm_mul_sin (z₁ z₂ : ℂ) :
  z₁.re * z₂.im - z₁.im * z₂.re =
    ‖z₁‖ * ‖z₂‖ * Real.sin (z₂.arg - z₁.arg)
CategoryTheory.cross_eq_norm_mul_sin
  (z₁ z₂ : ℂ) :
  z₁.re * z₂.im - z₁.im * z₂.re =
    ‖z₁‖ * ‖z₂‖ *
      Real.sin (z₂.arg - z₁.arg)

Something wrong, better idea? Suggest a change

15.1.7. cross_nonneg_of_arg_le🔗

If z_1.\mathrm{im} \geq 0, z_1, z_2 \neq 0, and \arg z_1 \leq \arg z_2, then z_1.\mathrm{re} \cdot z_2.\mathrm{im} - z_1.\mathrm{im} \cdot z_2.\mathrm{re} \geq 0.

Proof: The cross product equals \|z_1\|\|z_2\|\sin(\arg z_2 - \arg z_1). Since \arg z_2 - \arg z_1 \in [0, \pi] (using \arg z_1 \geq 0 from z_1.\mathrm{im} \geq 0), \sin \geq 0.

theorem

CategoryTheory.cross_nonneg_of_arg_le {z₁ z₂ : ℂ} (him₁ : 0 ≤ z₁.im)
  (hz₁ : z₁ ≠ 0) (hz₂ : z₂ ≠ 0) (h : z₁.arg ≤ z₂.arg) :
  0 ≤ z₁.re * z₂.im - z₁.im * z₂.re
CategoryTheory.cross_nonneg_of_arg_le
  {z₁ z₂ : ℂ} (him₁ : 0 ≤ z₁.im)
  (hz₁ : z₁ ≠ 0) (hz₂ : z₂ ≠ 0)
  (h : z₁.arg ≤ z₂.arg) :
  0 ≤ z₁.re * z₂.im - z₁.im * z₂.re

Something wrong, better idea? Suggest a change

15.1.8. arg_le_of_cross_nonneg🔗

If z_1, z_2 \neq 0, \arg z_2 > 0, and the cross product z_1.\mathrm{re} \cdot z_2.\mathrm{im} - z_1.\mathrm{im} \cdot z_2.\mathrm{re} \geq 0, then \arg z_1 \leq \arg z_2.

Proof: Write the cross product as \|z_1\| \|z_2\| \sin(\arg z_2 - \arg z_1). If \arg z_1 > \arg z_2 then \arg z_2 - \arg z_1 < 0 and > -\pi, so \sin < 0, contradicting the nonnegativity.

theorem

CategoryTheory.arg_le_of_cross_nonneg {z₁ z₂ : ℂ} (hz₁ : z₁ ≠ 0)
  (hz₂ : z₂ ≠ 0) (harg₂ : 0 < z₂.arg)
  (hcross : 0 ≤ z₁.re * z₂.im - z₁.im * z₂.re) : z₁.arg ≤ z₂.arg
CategoryTheory.arg_le_of_cross_nonneg
  {z₁ z₂ : ℂ} (hz₁ : z₁ ≠ 0)
  (hz₂ : z₂ ≠ 0) (harg₂ : 0 < z₂.arg)
  (hcross :
    0 ≤ z₁.re * z₂.im - z₁.im * z₂.re) :
  z₁.arg ≤ z₂.arg

Something wrong, better idea? Suggest a change

15.1.9. cross_pos_of_arg_lt🔗

If \arg z_1 > 0, z_1, z_2 \neq 0, and \arg z_1 < \arg z_2, then the cross product z_1.\mathrm{re} \cdot z_2.\mathrm{im} - z_1.\mathrm{im} \cdot z_2.\mathrm{re} > 0.

Proof: The cross product equals \|z_1\|\|z_2\|\sin(\arg z_2 - \arg z_1) > 0 since \arg z_2 - \arg z_1 \in (0, \pi) (using \arg z_1 > 0 and \arg z_2 \leq \pi).

theorem

CategoryTheory.cross_pos_of_arg_lt {z₁ z₂ : ℂ} (harg₁ : 0 < z₁.arg)
  (hz₁ : z₁ ≠ 0) (hz₂ : z₂ ≠ 0) (h : z₁.arg < z₂.arg) :
  0 < z₁.re * z₂.im - z₁.im * z₂.re
CategoryTheory.cross_pos_of_arg_lt
  {z₁ z₂ : ℂ} (harg₁ : 0 < z₁.arg)
  (hz₁ : z₁ ≠ 0) (hz₂ : z₂ ≠ 0)
  (h : z₁.arg < z₂.arg) :
  0 < z₁.re * z₂.im - z₁.im * z₂.re

Something wrong, better idea? Suggest a change

15.1.10. arg_lt_of_cross_pos🔗

If z_1, z_2 \neq 0, \arg z_2 > 0, and the cross product z_1.\mathrm{re} \cdot z_2.\mathrm{im} - z_1.\mathrm{im} \cdot z_2.\mathrm{re} > 0, then \arg z_1 < \arg z_2.

Proof: The cross product equals \|z_1\|\|z_2\| \sin(\arg z_2 - \arg z_1) > 0, so \sin(\arg z_2 - \arg z_1) > 0, which forces \arg z_2 - \arg z_1 \in (0, \pi), i.e., \arg z_1 < \arg z_2.

theorem

CategoryTheory.arg_lt_of_cross_pos {z₁ z₂ : ℂ} (hz₁ : z₁ ≠ 0)
  (hz₂ : z₂ ≠ 0) (harg₂ : 0 < z₂.arg)
  (hcross : 0 < z₁.re * z₂.im - z₁.im * z₂.re) : z₁.arg < z₂.arg
CategoryTheory.arg_lt_of_cross_pos
  {z₁ z₂ : ℂ} (hz₁ : z₁ ≠ 0)
  (hz₂ : z₂ ≠ 0) (harg₂ : 0 < z₂.arg)
  (hcross :
    0 < z₁.re * z₂.im - z₁.im * z₂.re) :
  z₁.arg < z₂.arg

Something wrong, better idea? Suggest a change

15.1.11. arg_add_lt_max🔗

For z_1, z_2 in the semi-closed upper half plane with \arg z_1 \neq \arg z_2, the strict inequality \arg(z_1 + z_2) < \max(\arg z_1, \arg z_2) holds.

Proof: WLOG \arg z_1 < \arg z_2. Then the cross product z_1.\mathrm{re} \cdot z_2.\mathrm{im} - z_1.\mathrm{im} \cdot z_2.\mathrm{re} > 0 by cross_pos_of_arg_lt, and the self-cancellation identity shows the cross product of (z_1+z_2) with z_2 is the same positive quantity, giving \arg(z_1+z_2) < \arg z_2 via arg_lt_of_cross_pos.

theorem

CategoryTheory.arg_add_lt_max {z₁ z₂ : ℂ}
  (h₁ : z₁ ∈ CategoryTheory.upperHalfPlaneUnion)
  (h₂ : z₂ ∈ CategoryTheory.upperHalfPlaneUnion)
  (hne : z₁.arg ≠ z₂.arg) : (z₁ + z₂).arg < max z₁.arg z₂.arg
CategoryTheory.arg_add_lt_max {z₁ z₂ : ℂ}
  (h₁ :
    z₁ ∈
      CategoryTheory.upperHalfPlaneUnion)
  (h₂ :
    z₂ ∈
      CategoryTheory.upperHalfPlaneUnion)
  (hne : z₁.arg ≠ z₂.arg) :
  (z₁ + z₂).arg < max z₁.arg z₂.arg

Something wrong, better idea? Suggest a change

15.1.12. arg_add_le_max🔗

For z_1, z_2 in the semi-closed upper half plane, \arg(z_1 + z_2) \leq \max(\arg z_1, \arg z_2). This is the key analytical bound ensuring the phase of an extension is bounded by the phases of its subobjects.

Proof: WLOG \arg z_1 \leq \arg z_2. Show \arg(z_1+z_2) \leq \arg z_2 via the cross-product criterion arg_le_of_cross_nonneg: the cross product (z_1+z_2).\mathrm{re} \cdot z_2.\mathrm{im} - (z_1+z_2).\mathrm{im} \cdot z_2.\mathrm{re} equals z_1.\mathrm{re} \cdot z_2.\mathrm{im} - z_1.\mathrm{im} \cdot z_2.\mathrm{re} \geq 0 by cross_nonneg_of_arg_le.

theorem

CategoryTheory.arg_add_le_max {z₁ z₂ : ℂ}
  (h₁ : z₁ ∈ CategoryTheory.upperHalfPlaneUnion)
  (h₂ : z₂ ∈ CategoryTheory.upperHalfPlaneUnion) :
  (z₁ + z₂).arg ≤ max z₁.arg z₂.arg
CategoryTheory.arg_add_le_max {z₁ z₂ : ℂ}
  (h₁ :
    z₁ ∈
      CategoryTheory.upperHalfPlaneUnion)
  (h₂ :
    z₂ ∈
      CategoryTheory.upperHalfPlaneUnion) :
  (z₁ + z₂).arg ≤ max z₁.arg z₂.arg

Something wrong, better idea? Suggest a change

15.1.13. min_arg_le_arg_add🔗

For z_1, z_2 in the semi-closed upper half plane, \min(\arg z_1, \arg z_2) \leq \arg(z_1 + z_2). This is the lower companion to arg_add_le_max.

Proof: WLOG \arg z_1 \leq \arg z_2. Show \arg z_1 \leq \arg(z_1+z_2) via arg_le_of_cross_nonneg applied to the cross product of z_1 with z_1+z_2, which self-cancels to z_1.\mathrm{re} \cdot z_2.\mathrm{im} - z_1.\mathrm{im} \cdot z_2.\mathrm{re} \geq 0.

theorem

CategoryTheory.min_arg_le_arg_add {z₁ z₂ : ℂ}
  (h₁ : z₁ ∈ CategoryTheory.upperHalfPlaneUnion)
  (h₂ : z₂ ∈ CategoryTheory.upperHalfPlaneUnion) :
  min z₁.arg z₂.arg ≤ (z₁ + z₂).arg
CategoryTheory.min_arg_le_arg_add
  {z₁ z₂ : ℂ}
  (h₁ :
    z₁ ∈
      CategoryTheory.upperHalfPlaneUnion)
  (h₂ :
    z₂ ∈
      CategoryTheory.upperHalfPlaneUnion) :
  min z₁.arg z₂.arg ≤ (z₁ + z₂).arg

Something wrong, better idea? Suggest a change

15.1.14. min_arg_lt_arg_add🔗

For z_1, z_2 in the semi-closed upper half plane with \arg z_1 \neq \arg z_2, the strict lower bound \min(\arg z_1, \arg z_2) < \arg(z_1 + z_2) holds.

Proof: WLOG \arg z_1 < \arg z_2. The cross product of z_1 with z_1 + z_2 equals the original cross product > 0 by cross_pos_of_arg_lt, giving \arg z_1 < \arg(z_1+z_2) via arg_lt_of_cross_pos.

theorem

CategoryTheory.min_arg_lt_arg_add {z₁ z₂ : ℂ}
  (h₁ : z₁ ∈ CategoryTheory.upperHalfPlaneUnion)
  (h₂ : z₂ ∈ CategoryTheory.upperHalfPlaneUnion)
  (hne : z₁.arg ≠ z₂.arg) : min z₁.arg z₂.arg < (z₁ + z₂).arg
CategoryTheory.min_arg_lt_arg_add
  {z₁ z₂ : ℂ}
  (h₁ :
    z₁ ∈
      CategoryTheory.upperHalfPlaneUnion)
  (h₂ :
    z₂ ∈
      CategoryTheory.upperHalfPlaneUnion)
  (hne : z₁.arg ≠ z₂.arg) :
  min z₁.arg z₂.arg < (z₁ + z₂).arg

Something wrong, better idea? Suggest a change

15.1.15. sum_mem_upperHalfPlane🔗

A nonempty finite sum of elements of the semi-closed upper half plane again lies in the semi-closed upper half plane.

Proof: Induction on the finite set using mem_upperHalfPlaneUnion_of_add.

theorem

CategoryTheory.sum_mem_upperHalfPlane.{u_1} {ι : Type u_1}
  {s : Finset ι} (hs : s.Nonempty) {f : ι → ℂ}
  (hf : ∀ i ∈ s, f i ∈ CategoryTheory.upperHalfPlaneUnion) :
  ∑ i ∈ s, f i ∈ CategoryTheory.upperHalfPlaneUnion
CategoryTheory.sum_mem_upperHalfPlane.{u_1}
  {ι : Type u_1} {s : Finset ι}
  (hs : s.Nonempty) {f : ι → ℂ}
  (hf :
    ∀ i ∈ s,
      f i ∈
        CategoryTheory.upperHalfPlaneUnion) :
  ∑ i ∈ s, f i ∈
    CategoryTheory.upperHalfPlaneUnion

Something wrong, better idea? Suggest a change

15.1.16. arg_sum_le_sup'_of_upperHalfPlane🔗

If f(i) \in \overline{\mathbb{H}} for all i \in s, then \arg\bigl(\sum_{i \in s} f(i)\bigr) \leq \sup_{i \in s} \arg(f(i)).

Proof: Induction on s using Finset.Nonempty.cons_induction, applying arg_add_le_max at each step and using sum_mem_upperHalfPlane to maintain the membership condition.

theorem

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

Something wrong, better idea? Suggest a change

15.1.17. inf'_le_arg_sum_of_upperHalfPlane🔗

If f(i) \in \overline{\mathbb{H}} for all i \in s, then \inf_{i \in s} \arg(f(i)) \leq \arg\bigl(\sum_{i \in s} f(i)\bigr). This is the dual lower bound to arg_sum_le_sup'_of_upperHalfPlane.

Proof: Induction on s using Finset.Nonempty.cons_induction, applying min_arg_le_arg_add at each step.

theorem

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

Something wrong, better idea? Suggest a change