English
The weight-k slash action of GL(2,ℝ) preserves the property of MDifferentiability for holomorphic functions on the upper half-plane.
Русский
Действие слеша веса k сохраняет свойство MDifferentiable для голоморфных функций на верхней полуплоскости.
LaTeX
$$$\forall f:\mathbb{H}\to\mathbb{C},\; \mathrm{MDifferentiable}_{\mathcal{I}(\mathbb{C})\mathcal{I}(\mathbb{C})}(f) \Rightarrow \forall k\in\mathbb{Z},\; \forall g\in GL(2,\mathbb{R}),\; \mathrm{MDifferentiable}_{\mathcal{I}(\mathbb{C})\mathcal{I}(\mathbb{C})}(f|[k]g).$$$
Lean4
/-- The weight `k` slash action of `GL(2, ℝ)` preserves holomorphic functions. -/
theorem slash {f : ℍ → ℂ} (hf : MDifferentiable 𝓘(ℂ) 𝓘(ℂ) f) (k : ℤ) (g : GL (Fin 2) ℝ) :
MDifferentiable 𝓘(ℂ) 𝓘(ℂ) (f ∣[k] g) :=
by
refine g.det_ne_zero.lt_or_gt.elim (fun hg ↦ ?_) (hf.slash_of_pos k)
rw [show g = J * (J * g) by simp [← mul_assoc, ← sq], SlashAction.slash_mul]
exact (hf.slashJ k).slash_of_pos _ (by simpa using hg)
