differentiableAt_eta_of_mem_upperHalfPlaneSet

English

Differentiability of eta holds at points in the upper half-plane.

Русский

Дифференцируемость η сохраняется в верхней полуплоскости.

LaTeX

$$$DifferentiableAt(\\mathbb{C}, \\eta, z)$ for all $z \\in \\mathbb{H}$$$

Lean4

theorem differentiableAt_eta_of_mem_upperHalfPlaneSet {z : ℂ} (hz : z ∈ ℍₒ) : DifferentiableAt ℂ eta z :=
  by
  apply DifferentiableAt.mul (by fun_prop)
  refine
    (multipliableLocallyUniformlyOn_eta.hasProdLocallyUniformlyOn.differentiableOn ?_ isOpen_upperHalfPlaneSet z
          hz).differentiableAt
      (isOpen_upperHalfPlaneSet.mem_nhds hz)
  filter_upwards with b
  simpa [Finset.prod_fn] using DifferentiableOn.finset_prod (by fun_prop)

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