15.3. ForMathlib: Analysis.SpecialFunctions.Complex.SectorBound🔗

15.3.1. eq_of_pos_mul_exp_eq🔗

Ray rigidity: if m_1 \cdot e^{i\pi\varphi} = m_2 \cdot e^{i\pi\psi} with m_1, m_2 > 0 and |\varphi - \psi| < 2, then \varphi = \psi. This ensures that a semistable object's phase is uniquely determined by its central charge value.

Proof: Extract the argument equality, reduce to \pi\psi - \pi\varphi = n \cdot 2\pi for some n \in \mathbb{Z}, and show n = 0 using the bound |\varphi - \psi| < 2.

theorem

eq_of_pos_mul_exp_eq {m₁ m₂ φ ψ : ℝ} (hm₁ : 0 < m₁) (hm₂ : 0 < m₂)
  (habs : |φ - ψ| < 2)
  (heq :
    ↑m₁ * Complex.exp (↑(Real.pi * φ) * Complex.I) =
      ↑m₂ * Complex.exp (↑(Real.pi * ψ) * Complex.I)) :
  φ = ψ
eq_of_pos_mul_exp_eq {m₁ m₂ φ ψ : ℝ}
  (hm₁ : 0 < m₁) (hm₂ : 0 < m₂)
  (habs : |φ - ψ| < 2)
  (heq :
    ↑m₁ *
        Complex.exp
          (↑(Real.pi * φ) * Complex.I) =
      ↑m₂ *
        Complex.exp
          (↑(Real.pi * ψ) * Complex.I)) :
  φ = ψ

Something wrong, better idea? Suggest a change

15.3.2. re_mul_exp_neg_ge_cos_mul_norm🔗

Sector projection bound: if \arg(z) \in (\alpha, \alpha + w) with w < \pi, then \cos(w/2) \cdot \|z\| \leq \mathrm{Re}(z \cdot e^{-i(\alpha + w/2)}).

Proof: Using the polar form z = \|z\| e^{i\arg z}, compute \mathrm{Re}(z e^{-i\beta}) = \|z\| \cos(\arg z - \beta) where \beta = \alpha + w/2. Since |\arg z - \beta| < w/2 and cosine is decreasing, \cos(\arg z - \beta) \geq \cos(w/2).

theorem

re_mul_exp_neg_ge_cos_mul_norm {z : ℂ} {α w : ℝ} (hwπ : w < Real.pi)
  (harg : z.arg ∈ Set.Ioo α (α + w)) :
  Real.cos (w / 2) * ‖z‖ ≤
    (z * Complex.exp (-(↑(α + w / 2) * Complex.I))).re
re_mul_exp_neg_ge_cos_mul_norm {z : ℂ}
  {α w : ℝ} (hwπ : w < Real.pi)
  (harg : z.arg ∈ Set.Ioo α (α + w)) :
  Real.cos (w / 2) * ‖z‖ ≤
    (z *
        Complex.exp
          (-(↑(α + w / 2) *
              Complex.I))).re

Something wrong, better idea? Suggest a change

15.3.3. norm_sum_ge_cos_mul_sum_norm🔗

Sector norm bound: if all z_i have \arg(z_i) \in (\alpha, \alpha + w) with w < \pi, then \cos(w/2) \cdot \sum_i \|z_i\| \leq \bigl\|\sum_i z_i\bigr\|.

Proof: Sum the pointwise bound from re_mul_exp_neg_ge_cos_mul_norm, collect into the rotated sum's real part, and bound by the norm.

theorem

norm_sum_ge_cos_mul_sum_norm.{u_1} {ι : Type u_1} {s : Finset ι}
  {z : ι → ℂ} {α w : ℝ} (hwπ : w < Real.pi)
  (harg : ∀ i ∈ s, (z i).arg ∈ Set.Ioo α (α + w)) :
  Real.cos (w / 2) * ∑ i ∈ s, ‖z i‖ ≤ ‖∑ i ∈ s, z i‖
norm_sum_ge_cos_mul_sum_norm.{u_1}
  {ι : Type u_1} {s : Finset ι}
  {z : ι → ℂ} {α w : ℝ}
  (hwπ : w < Real.pi)
  (harg :
    ∀ i ∈ s,
      (z i).arg ∈ Set.Ioo α (α + w)) :
  Real.cos (w / 2) * ∑ i ∈ s, ‖z i‖ ≤
    ‖∑ i ∈ s, z i‖

Something wrong, better idea? Suggest a change

15.3.4. norm_sum_exp_ge_cos_mul_sum🔗

Sector norm bound (explicit form): if m_i \geq 0 and phases \theta_i \in [\alpha, \alpha + w] with w < \pi, then \cos(w/2) \cdot \sum_i m_i \leq \bigl\|\sum_i m_i e^{i\theta_i}\bigr\|.

Proof: Project each summand onto the bisector direction \beta = \alpha + w/2: pointwise \cos(w/2) \cdot m_i \leq \mathrm{Re}(m_i e^{i\theta_i} e^{-i\beta}) by the cosine bound on |\theta_i - \beta| \leq w/2. Sum, bound the real part by the norm, and cancel the unit exponential.

theorem

norm_sum_exp_ge_cos_mul_sum.{u_1} {ι : Type u_1} {s : Finset ι}
  {m θ : ι → ℝ} (hm : ∀ i ∈ s, 0 ≤ m i) {α w : ℝ} (hw0 : 0 ≤ w)
  (hwπ : w < Real.pi) (hθ : ∀ i ∈ s, θ i ∈ Set.Icc α (α + w)) :
  Real.cos (w / 2) * ∑ i ∈ s, m i ≤
    ‖∑ i ∈ s, ↑(m i) * Complex.exp (↑(θ i) * Complex.I)‖
norm_sum_exp_ge_cos_mul_sum.{u_1}
  {ι : Type u_1} {s : Finset ι}
  {m θ : ι → ℝ} (hm : ∀ i ∈ s, 0 ≤ m i)
  {α w : ℝ} (hw0 : 0 ≤ w)
  (hwπ : w < Real.pi)
  (hθ :
    ∀ i ∈ s, θ i ∈ Set.Icc α (α + w)) :
  Real.cos (w / 2) * ∑ i ∈ s, m i ≤
    ‖∑ i ∈ s,
        ↑(m i) *
          Complex.exp
            (↑(θ i) * Complex.I)‖

Something wrong, better idea? Suggest a change