English
Let hk ≤ 0 and f be a SlashInvariantForm. Then for any τ in the upper half-plane and f, there exists ξ in the upper half-plane such that Im ξ ≥ 1/2 and the norm at τ is bounded by the norm at ξ: ∥f(τ)∥ ≤ ∥f(ξ)∥.
Русский
Пусть hk ≤ 0 и f — SlashInvariantForm. Тогда для любого τ в верхней полуплоскости существует ξ в верхней полуплоскости с Im ξ ≥ 1/2 и нормa ∥f(τ)∥ ≤ ∥f(ξ)∥.
LaTeX
$$$\exists \xi \in \mathbb{H},\; \tfrac{1}{2} \le \operatorname{Im}(\xi) \quad\land\quad \|f(\tau)\| \le \|f(\xi)\|$$$
Lean4
theorem exists_one_half_le_im_and_norm_le (hk : k ≤ 0) (f : F) (τ : ℍ) : ∃ ξ : ℍ, 1 / 2 ≤ ξ.im ∧ ‖f τ‖ ≤ ‖f ξ‖ :=
let ⟨γ, hγ, hdenom⟩ := exists_one_half_le_im_smul_and_norm_denom_le τ
⟨γ • τ, hγ, by
simpa only [slash_action_eqn_SL'' _ (mem_Gamma_one γ), norm_mul, norm_zpow] using
le_mul_of_one_le_left (norm_nonneg _) <| one_le_zpow_of_nonpos₀ (norm_pos_iff.2 (denom_ne_zero _ _)) hdenom hk⟩
