slash — Mathlib

English

Slash action by GL(2,R) on functions on the upper half-plane preserves various boundedness properties under suitable conditions.

Русский

Все действия slash GL(2,R) на функциях верхней полуплоскости сохраняют некоторые свойства ограниченности при подходящих условиях.

LaTeX

$$$\\text{SlashAction}: f \\mapsto f|[k]g$ defines a group action compatible with topological properties.$$

Lean4

theorem slash (hg : g 1 0 = 0) (hf : IsBoundedAtImInfty f) : IsBoundedAtImInfty (f ∣[k] g) :=
  by
  rw [IsBoundedAtImInfty, BoundedAtFilter, ← Asymptotics.isBigO_norm_left] at hf ⊢
  suffices (fun x ↦ (‖g.det.val ^ (k - 1)‖ * ‖g 1 1 ^ (-k)‖) * ‖f (g • x)‖) =O[atImInfty] 1 by
    simpa [ModularForm.slash_def, denom, hg, mul_assoc, mul_comm ‖f _‖]
  apply (hf.comp_tendsto (tendsto_smul_atImInfty hg)).const_mul_left

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