angle_exp_exp — Mathlib

English

For real x,y, the angle between e^{i x} and e^{i y} equals the absolute value of a certain modular expression of x−y.

Русский

Для действительных x,y угол между e^{i x} и e^{i y} равен модулю некоторого модулярного выражения от x−y.

LaTeX

$$$$\angle\left(e^{i x}, e^{i y}\right) = \left| \operatorname{toIocMod}(2\pi_{pos})(-\pi)(x - y) \right|.$$$$

Lean4

theorem angle_exp_exp (x y : ℝ) : angle (exp (x * I)) (exp (y * I)) = |toIocMod Real.two_pi_pos (-π) (x - y)| := by
  simp_rw [angle_eq_abs_arg (exp_ne_zero _) (exp_ne_zero _), ← exp_sub, ← sub_mul, ← ofReal_sub, arg_exp_mul_I]

Похожие утверждения