norm_qParam_le_of_one_half_le_im — Mathlib

English

If ξ ∈ ℂ satisfies Im(ξ) ≥ 1/2, then the modulus of qParam(1, ξ) is at most e^{-π}.

Русский

Пусть ξ ∈ ℂ такой, что Im(ξ) ≥ 1/2. Тогда модуль qParam(1, ξ) не превосходит e^{-π}.

LaTeX

$$$\forall \xi \in \mathbb{C}, \ \Im(\xi) \ge \tfrac{1}{2} ; \|\mathsf{qParam}(1, \xi)\| \le e^{-\pi}$$$

Lean4

theorem norm_qParam_le_of_one_half_le_im {ξ : ℂ} (hξ : 1 / 2 ≤ ξ.im) : ‖𝕢 1 ξ‖ ≤ rexp (-π) := by
  rwa [Periodic.qParam, ofReal_one, div_one, Complex.norm_exp, Real.exp_le_exp, mul_right_comm, mul_I_re,
    neg_le_neg_iff, ← ofReal_ofNat, ← ofReal_mul, im_ofReal_mul, mul_comm _ π, mul_assoc,
    le_mul_iff_one_le_right Real.pi_pos, ← div_le_iff₀' two_pos]

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