14.16. Deformation: PhasePerturbation🔗

14.16.1. wPhaseOf_perturbation_generic🔗

Generic phase perturbation bound. If w = m \cdot e^{i\pi\phi} \cdot (1 + u) with m > 0, \phi \in (\alpha - 1/2, \alpha + 1/2), and \|u\| < \sin(\pi\varepsilon) with 0 < \varepsilon \le 1/2, then |\operatorname{wPhaseOf}(w, \alpha) - \phi| < \varepsilon.

Proof: Split \arg of the product using \arg(z_1 z_2) = \arg(z_1) + \arg(z_2) (valid when the sum stays in (-\pi, \pi]). Compute \arg(m \cdot e^{i\pi(\phi - \alpha)}) = \pi(\phi - \alpha), and bound |\arg(1 + u)| < \pi\varepsilon from the pure complex analysis lemma abs_arg_one_add_lt.

theorem

CategoryTheory.Triangulated.wPhaseOf_perturbation_generic {m φ α ε : ℝ}
  {u : ℂ} (hm : 0 < m) (hφ : φ ∈ Set.Ioo (α - 1 / 2) (α + 1 / 2))
  (hε : 0 < ε) (hε2 : ε ≤ 1 / 2) (hu : ‖u‖ < Real.sin (Real.pi * ε)) :
  |CategoryTheory.Triangulated.wPhaseOf
          (↑m * Complex.exp (↑(Real.pi * φ) * Complex.I) * (1 + u)) α -
        φ| <
    ε
CategoryTheory.Triangulated.wPhaseOf_perturbation_generic
  {m φ α ε : ℝ} {u : ℂ} (hm : 0 < m)
  (hφ :
    φ ∈ Set.Ioo (α - 1 / 2) (α + 1 / 2))
  (hε : 0 < ε) (hε2 : ε ≤ 1 / 2)
  (hu : ‖u‖ < Real.sin (Real.pi * ε)) :
  |CategoryTheory.Triangulated.wPhaseOf
          (↑m *
              Complex.exp
                (↑(Real.pi * φ) *
                  Complex.I) *
            (1 + u))
          α -
        φ| <
    ε

Something wrong, better idea? Suggest a change