English
There is an equivalence relating ContMDiffAt on the upper half-plane to ContDiffAt on the complex chart after composing with the inclusion; i.e., differentiability in the ambient complex model corresponds to chart-level differentiability on the upper half-plane.
Русский
Существует эквивалентность между ContMDiffAt на верхней половине плоскости и ContDiffAt на комплексной карте после композиции с включением; дифференцируемость в окружающей модели соответствует дифференцируемости в диаграмме на верхней половине плоскости.
LaTeX
$$$\forall n, \forall f, \forall \tau, ContMDiffAt( 𝓘(\mathbb{C}) , 𝓘(\mathbb{C}) , n, f, \tau) \iff ContDiffAt(\mathbb{C}, n, f \circ \text{ofComplex}, \tau)$$$
Lean4
theorem contMDiffAt_iff {f : ℍ → ℂ} {τ : ℍ} : ContMDiffAt 𝓘(ℂ) 𝓘(ℂ) n f τ ↔ ContDiffAt ℂ n (f ∘ ofComplex) τ :=
by
rw [← contMDiffAt_iff_contDiffAt]
refine ⟨fun hf ↦ ?_, fun hf ↦ ?_⟩
· exact (ofComplex_apply τ ▸ hf).comp _ (contMDiffAt_ofComplex τ.im_pos)
· simpa only [Function.comp_def, ofComplex_apply] using hf.comp τ (contMDiff_coe τ)
