differentiableAt_comp_ofComplex — Mathlib

English

If z has positive imaginary part, then the composition f ∘ ofComplex is differentiable at z for modular form f.

Русский

Если Im z > 0, то композиция f ∘ ofComplex дифференцируема в точке z для модулярной формы f.

LaTeX

$$$\text{If } 0 < \mathrm{Im}(z),\quad \text{DifferentiableAt}_{\mathbb{C}}(f \circ \mathrm{ofComplex}, z)$$$

Lean4

theorem differentiableAt_comp_ofComplex [ModularFormClass F Γ k] {z : ℂ} (hz : 0 < im z) :
    DifferentiableAt ℂ (f ∘ ofComplex) z :=
  mdifferentiableAt_iff_differentiableAt.mp ((holo f _).comp z (mdifferentiableAt_ofComplex hz))

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