English
For z ∈ ℂ with im(z) > 0, ContMDiffAt equals ContDiffAt after composing with the complex inclusion; equivalently, the C^n differentiability transfers across the complex inclusion.
Русский
Для z ∈ ℂ с Im(z) > 0 сопоставление ContMDiffAt эквивалентно ContDiffAt после композиции с включением в комплекс; гладкость передаётся через включение.
LaTeX
$$$\forall z \in \mathbb{C}, \operatorname{Im}(z) > 0 \Rightarrow (\text{ContMDiffAt } 𝓘(\mathbb{C}) 𝓘(\mathbb{C}) n f z) \iff (\text{ContDiffAt } \mathbb{C} n (f \circ \text{ofComplex}) z)$$$
Lean4
theorem contMDiffAt_ofComplex {z : ℂ} (hz : 0 < z.im) : ContMDiffAt 𝓘(ℂ) 𝓘(ℂ) n ofComplex z :=
by
rw [contMDiffAt_iff]
constructor
· -- continuity at z
rw [ContinuousAt, nhds_induced, tendsto_comap_iff]
refine Tendsto.congr' (eventuallyEq_coe_comp_ofComplex hz).symm ?_
simpa [ofComplex_apply_of_im_pos hz] using tendsto_id
· -- smoothness in local chart
simpa using contDiffAt_id.congr_of_eventuallyEq (eventuallyEq_coe_comp_ofComplex hz)
