Conformal maps between complex vector spaces

We prove the sufficient and necessary conditions for a real-linear map between complex vector spaces to be conformal.

Main results

• isConformalMap_complex_linear: a nonzero complex linear map into an arbitrary complex normed space is conformal.

• isConformalMap_complex_linear_conj: the composition of a nonzero complex linear map with conj is complex linear.

• isConformalMap_iff_is_complex_or_conj_linear: a real linear map between the complex plane is conformal iff it's complex linear or the composition of some complex linear map and conj.

• DifferentiableAt.conformalAt states that a real-differentiable function with a nonvanishing differential from the complex plane into an arbitrary complex-normed space is conformal at a point if it's holomorphic at that point. This is a version of Cauchy-Riemann equations.

• conformalAt_iff_differentiableAt_or_differentiableAt_comp_conj proves that a real-differential function with a nonvanishing differential between the complex plane is conformal at a point if and only if it's holomorphic or antiholomorphic at that point.

• differentiableWithinAt_complex_iff_differentiableWithinAt_real and differentiableAt_complex_iff_differentiableAt_real characterize complex differentiability in terms of the classic Cauchy-Riemann equation.

Warning

Antiholomorphic functions such as the complex conjugate are considered as conformal functions in this file.

TODO

• On a connected open set u, a function which is ConformalAt each point is either holomorphic throughout or antiholomorphic throughout.

theorem isConformalMap_conj : IsConformalMap ↑Complex.conjLIE.toContinuousLinearEquiv

theorem isConformalMap_complex_linear {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedSpace ℂ E] {map : ℂ →L[ℂ] E} (nonzero : map ≠ 0) : IsConformalMap (ContinuousLinearMap.restrictScalars ℝ map)

theorem isConformalMap_complex_linear_conj {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedSpace ℂ E] {map : ℂ →L[ℂ] E} (nonzero : map ≠ 0) : IsConformalMap ((ContinuousLinearMap.restrictScalars ℝ map).comp ↑Complex.conjCLE)

theorem IsConformalMap.is_complex_or_conj_linear {g : ℂ →L[ℝ] ℂ} (h : IsConformalMap g) : (∃ (map : ℂ →L[ℂ] ℂ), ContinuousLinearMap.restrictScalars ℝ map = g) ∨ ∃ (map : ℂ →L[ℂ] ℂ), ContinuousLinearMap.restrictScalars ℝ map = g.comp ↑Complex.conjCLE

theorem isConformalMap_iff_is_complex_or_conj_linear {g : ℂ →L[ℝ] ℂ} : IsConformalMap g ↔ ((∃ (map : ℂ →L[ℂ] ℂ), ContinuousLinearMap.restrictScalars ℝ map = g) ∨ ∃ (map : ℂ →L[ℂ] ℂ), ContinuousLinearMap.restrictScalars ℝ map = g.comp ↑Complex.conjCLE) ∧ g ≠ 0

A real continuous linear map on the complex plane is conformal if and only if the map or its conjugate is complex linear, and the map is nonvanishing.

Conformality of real-differentiable complex maps

theorem DifferentiableAt.conformalAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {z : ℂ} {f : ℂ → E} (h : DifferentiableAt ℂ f z) (hf' : deriv f z ≠ 0) : ConformalAt f z

A real differentiable function of the complex plane into some complex normed space E is conformal at a point z if it is holomorphic at that point with a nonvanishing differential. This is a version of the Cauchy-Riemann equations.

theorem conformalAt_iff_differentiableAt_or_differentiableAt_comp_conj {f : ℂ → ℂ} {z : ℂ} : ConformalAt f z ↔ (DifferentiableAt ℂ f z ∨ DifferentiableAt ℂ (f ∘ ⇑(starRingEnd ℂ)) ((starRingEnd ℂ) z)) ∧ fderiv ℝ f z ≠ 0

A complex function is conformal if and only if the function is holomorphic or antiholomorphic with a nonvanishing differential.

The Cauchy-Riemann Equation for Complex-Differentiable Functions

theorem real_linearMap_map_smul_complex {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {ℓ : ℂ →ₗ[ℝ] E} (h : ℓ Complex.I = Complex.I • ℓ 1) (a b : ℂ) : ℓ (a • b) = a • ℓ b

A real linear map ℓ : ℂ →ₗ[ℝ] E respects complex scalar multiplication if it maps I to I • ℓ 1.

def LinearMap.complexOfReal {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (ℓ : ℂ →ₗ[ℝ] E) (h : ℓ Complex.I = Complex.I • ℓ 1) : ℂ →ₗ[ℂ] E

Construct a complex-linear map from a real-linear map ℓ that maps I to I • ℓ 1.

Equations

• ℓ.complexOfReal h = { toAddHom := ℓ.toAddHom, map_smul' := ⋯ }

@[simp]

theorem LinearMap.coe_complexOfReal {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {ℓ : ℂ →ₗ[ℝ] E} (h : ℓ Complex.I = Complex.I • ℓ 1) : ⇑(ℓ.complexOfReal h) = ⇑ℓ

def ContinuousLinearMap.complexOfReal {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (ℓ : ℂ →L[ℝ] E) (h : ℓ Complex.I = Complex.I • ℓ 1) : ℂ →L[ℂ] E

Construct a continuous complex-linear map from a continuous real-linear map ℓ that maps I to I • ℓ 1.

Equations

• ℓ.complexOfReal h = { toAddHom := (↑ℓ).toAddHom, map_smul' := ⋯, cont := ⋯ }

@[simp]

theorem ContinuousLinearMap.coe_complexOfReal {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {ℓ : ℂ →L[ℝ] E} (h : ℓ Complex.I = Complex.I • ℓ 1) : ⇑(ℓ.complexOfReal h) = ⇑ℓ

theorem differentiableWithinAt_complex_iff_differentiableWithinAt_real {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {x : ℂ} {s : Set ℂ} (hs : UniqueDiffWithinAt ℝ s x) : DifferentiableWithinAt ℂ f s x ↔ DifferentiableWithinAt ℝ f s x ∧ (fderivWithin ℝ f s x) Complex.I = Complex.I • (fderivWithin ℝ f s x) 1

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 HasFDerivWithinAt.complexOfReal {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {x : ℂ} {s : Set ℂ} {f' : ℂ →L[ℝ] E} (h₁ : HasFDerivWithinAt f f' s x) (h₂ : f' Complex.I = Complex.I • f' 1) : HasFDerivWithinAt f (f'.complexOfReal h₂) s x

In cases where the Cauchy-Riemann Equation guarantees complex differentiability at x, the complex derivative equals ContinuousLinearMap.complexOfReal of the real derivative.

theorem complexOfReal_fderivWithin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {x : ℂ} {s : Set ℂ} (h₁ : DifferentiableWithinAt ℝ f s x) (h₂ : (fderivWithin ℝ f s x) Complex.I = Complex.I • (fderivWithin ℝ f s x) 1) (hs : UniqueDiffWithinAt ℝ s x) : fderivWithin ℂ f s x = (fderivWithin ℝ f s x).complexOfReal h₂

In cases where the Cauchy-Riemann Equation guarantees complex differentiability at x, the complex derivative equals ContinuousLinearMap.complexOfReal of the real derivative.

theorem complexOfReal_hasDerivWithinAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {x : ℂ} {s : Set ℂ} (h₁ : DifferentiableWithinAt ℝ f s x) (h₂ : (fderivWithin ℝ f s x) Complex.I = Complex.I • (fderivWithin ℝ f s x) 1) : HasDerivWithinAt f (((fderivWithin ℝ f s x).complexOfReal h₂) 1) s x

In cases where the Cauchy-Riemann Equation guarantees complex differentiability at x, the complex derivative equals ContinuousLinearMap.complexOfReal of the real derivative.

theorem complexOfReal_derivWithin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {x : ℂ} {s : Set ℂ} (h₁ : DifferentiableWithinAt ℝ f s x) (h₂ : (fderivWithin ℝ f s x) Complex.I = Complex.I • (fderivWithin ℝ f s x) 1) (hs : UniqueDiffWithinAt ℂ s x) : derivWithin f s x = (fderivWithin ℝ f s x) 1

In cases where the Cauchy-Riemann Equation guarantees complex differentiability at x, the complex derivative equals the real derivative.

theorem differentiableAt_complex_iff_differentiableAt_real {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {x : ℂ} : DifferentiableAt ℂ f x ↔ DifferentiableAt ℝ f x ∧ (fderiv ℝ f x) Complex.I = Complex.I • (fderiv ℝ f x) 1

The Cauchy-Riemann Equation: A real-differentiable function f on ℂ is complex-differentiable at x if and only if the derivative fderiv ℝ f x maps I to I • (fderiv ℝ f x) 1.

theorem HasFDerivAt.complexOfReal_hasFDerivAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {x : ℂ} {f' : ℂ →L[ℝ] E} (h₁ : HasFDerivAt f f' x) (h₂ : f' Complex.I = Complex.I • f' 1) : HasFDerivAt f (f'.complexOfReal h₂) x

In cases where the Cauchy-Riemann Equation guarantees complex differentiability at x, the complex derivative equals ContinuousLinearMap.complexOfReal of the real derivative.

theorem complexOfReal_hasDerivAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {x : ℂ} (h₁ : DifferentiableAt ℝ f x) (h₂ : (fderiv ℝ f x) Complex.I = Complex.I • (fderiv ℝ f x) 1) : HasDerivAt f (((fderiv ℝ f x).complexOfReal h₂) 1) x

In cases where the Cauchy-Riemann Equation guarantees complex differentiability at x, the complex derivative equals ContinuousLinearMap.complexOfReal of the real derivative.

theorem complexOfReal_deriv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {x : ℂ} (h₁ : DifferentiableAt ℝ f x) (h₂ : (fderiv ℝ f x) Complex.I = Complex.I • (fderiv ℝ f x) 1) : deriv f x = (fderiv ℝ f x) 1

In cases where the Cauchy-Riemann Equation guarantees complex differentiability at x, the complex derivative equals the real derivative.

theorem complexOfReal_fderiv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {x : ℂ} (h₁ : DifferentiableAt ℝ f x) (h₂ : (fderiv ℝ f x) Complex.I = Complex.I • (fderiv ℝ f x) 1) : (fderiv ℝ f x).complexOfReal h₂ = fderiv ℂ f x

In cases where the Cauchy-Riemann Equation guarantees complex differentiability at x, the complex derivative equals ContinuousLinearMap.complexOfReal of the real derivative.