Phase control under near-identity perturbations

This file develops the complex-analytic estimate that converts a norm-small relative change of central charge into a small change of its selected phase. It is independent of categories and of the retained deformation library.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.im_sq_le_norm_sub_one_sq_mul (z : ℂ) : z.im ^ 2 ≤ ‖z - 1‖ ^ 2 * ‖z‖ ^ 2

The imaginary coordinate is bounded by the product of the distance from one and the norm.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.abs_sin_arg_le_norm_sub_one {z : ℂ} (hz : z ≠ 0) : |Real.sin z.arg| ≤ ‖z - 1‖

The sine of the argument of a nonzero complex number is controlled by its distance from one.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.sin_abs_eq_abs_sin {x : ℝ} (hx : |x| < Real.pi / 2) : Real.sin |x| = |Real.sin x|

On the central half-period, taking sine commutes with absolute value.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.abs_arg_one_add_lt {u : ℂ} {ε : ℝ} (hε : 0 < ε) (hε2 : ε ≤ 1 / 2) (hu : ‖u‖ < Real.sin (Real.pi * ε)) : |(1 + u).arg| < Real.pi * ε

A perturbation smaller than sin (π ε) changes the argument of one by less than π ε.

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

A norm-small multiplicative perturbation changes the selected relative phase by less than ε.