English
A complex function is conformal iff it is holomorphic or antiholomorphic with nonvanishing differential.
Русский
Отображение конформно тогда и только тогда, когда оно голоморфно или антиголоморфно и имеет ненулевую производную.
LaTeX
$$ConformalAt f z \iff (DifferentiableAt f z \\lor DifferentiableAt (f \circ conj) (conj z)) \land fderiv ℝ f z \neq 0$$
Lean4
/-- A complex function is conformal if and only if the function is holomorphic or antiholomorphic
with a nonvanishing differential. -/
theorem conformalAt_iff_differentiableAt_or_differentiableAt_comp_conj {f : ℂ → ℂ} {z : ℂ} :
ConformalAt f z ↔ (DifferentiableAt ℂ f z ∨ DifferentiableAt ℂ (f ∘ conj) (conj z)) ∧ fderiv ℝ f z ≠ 0 :=
by
rw [conformalAt_iff_isConformalMap_fderiv]
rw [isConformalMap_iff_is_complex_or_conj_linear]
apply and_congr_left
intro h
have h_diff := h.imp_symm fderiv_zero_of_not_differentiableAt
apply or_congr
· rw [differentiableAt_iff_restrictScalars ℝ h_diff]
rw [← conj_conj z] at h_diff
rw [differentiableAt_iff_restrictScalars ℝ (h_diff.comp _ conjCLE.differentiableAt)]
refine exists_congr fun g => rfl.congr ?_
have : fderiv ℝ conj (conj z) = _ := conjCLE.fderiv
simp [fderiv_comp _ h_diff conjCLE.differentiableAt, this]
