English
Let f be a map from the upper half-plane to the complex numbers. The notion of differentiability along the complex-analytic structure induced by the upper half-plane is equivalent to ordinary complex differentiability of the composition f with the standard complex inclusion at the corresponding point in the plane.
Русский
Пусть f: верхняя полуплоскость → ℂ. Тогда понятие дифференцируемости в пределах комплексной структуры верхней полуплоскости эквивалентно обычной комплексной дифференцируемости композиции f с включением в ℂ в соответствующей точке.
LaTeX
$$$MDifferentiableAt\, 𝓘(\mathbb{C})\, 𝓘(\mathbb{C})\, f\, τ \;\leftrightarrow\; DifferentiableAt\, \mathbb{C}\, (f \circ ofComplex)\, ↑τ$$$
Lean4
theorem mdifferentiableAt_iff {f : ℍ → ℂ} {τ : ℍ} :
MDifferentiableAt 𝓘(ℂ) 𝓘(ℂ) f τ ↔ DifferentiableAt ℂ (f ∘ ofComplex) ↑τ :=
by
rw [← mdifferentiableAt_iff_differentiableAt]
refine ⟨fun hf ↦ ?_, fun hf ↦ ?_⟩
· exact (ofComplex_apply τ ▸ hf).comp _ (mdifferentiableAt_ofComplex τ.im_pos)
· simpa only [Function.comp_def, ofComplex_apply] using hf.comp τ (mdifferentiable_coe τ)
