English
A real conformal map on the plane is either the restriction of a complex-linear map or the restriction of a map composed with complex conjugation.
Русский
Реальное конформное отображение на плоскости есть либо ограничение комплексно-линейной карты, либо ограничение карты после сопряжения.
LaTeX
$$IsConformalMap g → ((\exists map, map.restrictScalars ℝ = g) ∨ (\exists map, map.restrictScalars ℝ = g ∘ conjCLE))$$
Lean4
/-- The **Cauchy-Riemann Equation**: A real-differentiable function `f` on `ℂ` is complex-differentiable
at `x` within `s` iff the derivative `fderivWithin ℝ f s x` maps `I` to
`I • (fderivWithin ℝ f s x) 1`.
-/
theorem differentiableWithinAt_complex_iff_differentiableWithinAt_real (hs : UniqueDiffWithinAt ℝ s x) :
DifferentiableWithinAt ℂ f s x ↔
DifferentiableWithinAt ℝ f s x ∧ (fderivWithin ℝ f s x I = I • fderivWithin ℝ f s x 1) :=
by
refine ⟨fun h ↦ ⟨h.restrictScalars ℝ, ?_⟩, fun ⟨h₁, h₂⟩ ↦ ?_⟩
· simp only [← h.restrictScalars_fderivWithin ℝ hs, ContinuousLinearMap.coe_restrictScalars']
rw [(by simp : I = I • 1), (fderivWithin ℂ f s x).map_smul]
simp
· apply (differentiableWithinAt_iff_restrictScalars ℝ h₁ hs).2
use (fderivWithin ℝ f s x).complexOfReal h₂
rfl
