slash_apply — Mathlib

English

For any function f and g ∈ GL(2, ℝ), the slash operator is defined by (f ∣[k] g)(τ) = σ(g) f(g · τ) |det g|^{k−1} denom(g, τ)^{−k}.

Русский

Для любой функции f и матрицы g ∈ GL(2, ℝ) определяется slash-оператор: (f ∣[k] g)(τ) = σ(g) f(g·τ) |det g|^{k−1} denom(g, τ)^{−k}.

LaTeX

$$$ (f \lvert[k] g)(\tau) = \sigma(g) \; f(g \cdot \tau) \; |\det g|^{(k-1)} \; \text{denom}(g, \tau)^{(-k)} $$$

Lean4

theorem slash_apply (g : GL (Fin 2) ℝ) (τ : ℍ) :
    (f ∣[k] g) τ = σ g (f (g • τ)) * |g.det.val| ^ (k - 1) * denom g τ ^ (-k) :=
  rfl

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