15.2. ForMathlib: Analysis.SpecialFunctions.Complex.PhasePerturbation🔗

15.2.1. im_sq_le_norm_sq_mul🔗

For any z \in \mathbb{C}, z.\mathrm{im}^2 \leq \|z - 1\|^2 \cdot \|z\|^2.

Proof: Expand both sides using \|w\|^2 = w.\mathrm{re}^2 + w.\mathrm{im}^2 and check the resulting polynomial inequality by nlinarith.

theorem

im_sq_le_norm_sq_mul (z : ℂ) : z.im ^ 2 ≤ ‖z - 1‖ ^ 2 * ‖z‖ ^ 2
im_sq_le_norm_sq_mul (z : ℂ) :
  z.im ^ 2 ≤ ‖z - 1‖ ^ 2 * ‖z‖ ^ 2

Something wrong, better idea? Suggest a change

15.2.2. abs_sin_arg_le_norm_sub_one🔗

For any nonzero z \in \mathbb{C}, |\sin(\arg z)| \leq \|z - 1\|.

Proof: Since \sin(\arg z) = z.\mathrm{im} / \|z\|, the inequality follows from the geometric estimate z.\mathrm{im}^2 \leq \|z-1\|^2 \cdot \|z\|^2 via im_sq_le_norm_sq_mul.

theorem

abs_sin_arg_le_norm_sub_one {z : ℂ} (hz : z ≠ 0) :
  |Real.sin z.arg| ≤ ‖z - 1‖
abs_sin_arg_le_norm_sub_one {z : ℂ}
  (hz : z ≠ 0) :
  |Real.sin z.arg| ≤ ‖z - 1‖

Something wrong, better idea? Suggest a change

15.2.3. sin_abs_eq_abs_sin🔗

For |x| < \pi/2, \sin|x| = |\sin x|.

Proof: Case split on the sign of x: if x \geq 0 both sides equal \sin x \geq 0; if x < 0, then |x| = -x and \sin x < 0, so \sin|x| = \sin(-x) = -\sin x = |\sin x|.

theorem

sin_abs_eq_abs_sin {x : ℝ} (hx : |x| < Real.pi / 2) :
  Real.sin |x| = |Real.sin x|
sin_abs_eq_abs_sin {x : ℝ}
  (hx : |x| < Real.pi / 2) :
  Real.sin |x| = |Real.sin x|

Something wrong, better idea? Suggest a change

15.2.4. abs_arg_one_add_lt🔗

Phase bound for near-identity perturbation: if \|u\| < \sin(\pi\varepsilon) with 0 < \varepsilon \leq 1/2, then |\arg(1 + u)| < \pi\varepsilon.

theorem

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

Something wrong, better idea? Suggest a change