norm_qParam_lt_iff — Mathlib

English

Assume h > 0. Then for real A and z ∈ ℂ, ‖qParam(h,z)‖ < exp(-2π A / h) iff A < im z.

Русский

Пусть h > 0. Тогда для вещественного A и z ∈ ℂ, ‖qParam(h,z)‖ < exp(-2π A / h) эквивалентно A < im z.

LaTeX

$$$h>0\quad\Rightarrow\quad \|\mathrm{qParam}(h,z)\| < \exp\left(-\frac{2\pi A}{h}\right) \iff A < \operatorname{Im}(z)$$$

Lean4

theorem norm_qParam_lt_iff (hh : 0 < h) (A : ℝ) (z : ℂ) : ‖qParam h z‖ < Real.exp (-2 * π * A / h) ↔ A < im z :=
  by
  rw [norm_qParam, Real.exp_lt_exp, div_lt_div_iff_of_pos_right hh, mul_lt_mul_left_of_neg]
  simpa using Real.pi_pos

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