eisSummand_extension_differentiableOn

English

The extension of eisSummand to the complex domain is differentiable on {Im(z) > 0}, compatible with the linear z → (c z + d) mapping of SL(2,Z).

Русский

Расширение eisSummand в комплексную область дифференцируемо на {Im(z) > 0} и совместимо с отображением SL(2,Z): z ↦ (c z + d).

LaTeX

$$$\text{eisSummand\_extension\_differentiableOn}(k,a):\ DifferentiableOn_{\mathbb{C}}(\uparrow_{h} \mathrm{eisSummand}(k,a))\{ z : 0 < \operatorname{Im} z\}.$$$

Lean4

/-- Auxiliary lemma showing that for any `k : ℤ` and `(a : Fin 2 → ℤ)`
the extension of `eisSummand` is differentiable on `{z : ℂ | 0 < z.im}`. -/
theorem eisSummand_extension_differentiableOn (k : ℤ) (a : Fin 2 → ℤ) :
    DifferentiableOn ℂ (↑ₕeisSummand k a) {z : ℂ | 0 < z.im} :=
  by
  apply DifferentiableOn.congr (div_linear_zpow_differentiableOn k a)
  intro z hz
  lift z to ℍ using hz
  apply comp_ofComplex

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