contMDiff_denom_zpow — Mathlib

English

The family of functions τ ↦ denom(g, τ) raised to an integer power k is ContMDiff of class n on the upper half-plane.

Русский

Семейство функций τ ↦ denom(g, τ)^k, где k ∈ ℤ, является ContMDiff класса n на верхней полуплоскости.

LaTeX

$$$ContMDiff 𝓘(ℂ) 𝓘(ℂ) n (denom g \cdot ^ k : ℍ → ℂ)$$$

Lean4

theorem contMDiff_denom_zpow (g : GL (Fin 2) ℝ) (k : ℤ) : ContMDiff 𝓘(ℂ) 𝓘(ℂ) n (denom g · ^ k : ℍ → ℂ) := fun τ ↦
  by
  have : AnalyticAt ℂ (· ^ k) (denom g τ) :=
    (differentiableOn_zpow k _ (by tauto)).analyticOnNhd isOpen_compl_singleton _ (denom_ne_zero g τ)
  exact this.contDiffAt.contMDiffAt.comp τ (contMDiff_denom g τ)

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