Principal complex powers on a sector

This file records pointwise facts about symmetric angular sectors and principal complex powers. A closed symmetric sector can be described by a continuous linear inequality, the principal inverse power maps the corresponding open sector to the right half-plane, and raising that root back to the original power recovers the starting point.

Main results

• TauCeti.arg_mem_Icc_iff_norm_mul_cos_le_re characterizes a closed symmetric sector without referring to the discontinuous argument function on the target side.
• TauCeti.cpow_inv_re_pos_of_arg_mem_sector maps an open sector into the right half-plane.
• TauCeti.cpow_inv_cpow_of_sector recovers a point after taking its principal inverse power.

theorem TauCeti.arg_mem_Icc_iff_norm_mul_cos_le_re {z : ℂ} {a : ℝ} (ha : a ∈ Set.Icc 0 Real.pi) : z.arg ∈ Set.Icc (-a) a ↔ ‖z‖ * Real.cos a ≤ z.re

A complex number lies in the closed sector of half-opening a ≤ π around the positive real axis exactly when ‖z‖ * cos a ≤ z.re. The right-hand side is continuous in z, so this characterization passes to limits, unlike the argument itself. For a = π / 2 this specializes to Complex.abs_arg_le_pi_div_two_iff.

theorem TauCeti.cpow_inv_re_pos_of_arg_mem_sector {z : ℂ} {β : ℝ} (hβ : 0 < β) (hz : z ≠ 0) (harg : z.arg ∈ Set.Ioo (-(Real.pi * β / 2)) (Real.pi * β / 2)) : 0 < (z ^ ↑β⁻¹).re

The principal inverse power maps the sector of opening βπ into the open right half-plane.

theorem TauCeti.cpow_inv_cpow_of_sector {w : ℂ} {β : ℝ} (hβ : 0 < β) (hw : |w.arg| ≤ β * Real.pi / 2) : (w ^ ↑β⁻¹) ^ ↑β = w

On a sector of half-angle β * π / 2, the principal β-th root followed by the principal β-th power is the identity, including at zero.