norm_exp_two_pi_I_lt_one — Mathlib

English

For any τ in the upper half-plane, the norm of exp(2π i τ) is strictly less than 1.

Русский

Для любого τ в верхней полуплоскости нормa exp(2π i τ) строго меньше единицы.

LaTeX

$$$\forall \tau \in \mathbb{H}, \; \|\exp\bigl(2\pi i \tau\bigr)\| < 1$$$

Lean4

theorem norm_exp_two_pi_I_lt_one (τ : ℍ) : ‖(Complex.exp (2 * π * Complex.I * τ))‖ < 1 := by
  simpa [Function.Periodic.norm_qParam, Complex.norm_exp] using τ.norm_qParam_lt_one 1

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