Coordinate Cauchy–Riemann equations

Real differentiability and the coordinate Cauchy–Riemann equations characterize holomorphy on an open finite-dimensional domain. The proof uses Mathlib's one-variable conversion theorem and Osgood, rather than constructing a second complex derivative theory.

The domain ι → ℂ is intentional: each Wirtinger derivative and each displayed Cauchy–Riemann equation singles out a coordinate. The codomain may be a complex normed space, with completeness assumed for the analyticity results. Coordinate-free holomorphy is expressed by the usual complex Fréchet derivative; these results describe it in coordinates and relate the real derivative to the existing partialDeriv interface.

noncomputable def CarlsonFunctions.SeveralComplexVariables.wirtingerDeriv {ι : Type u_1} {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] (i : ι) (f : (ι → ℂ) → F) (z : ι → ℂ) : F

The holomorphic Wirtinger derivative, defined from the real Fréchet derivative.

Equations

• CarlsonFunctions.SeveralComplexVariables.wirtingerDeriv i f z = (1 / 2) • ((fderiv ℝ f z) (Pi.single i 1) - Complex.I • (fderiv ℝ f z) (Pi.single i Complex.I))

noncomputable def CarlsonFunctions.SeveralComplexVariables.conjWirtingerDeriv {ι : Type u_1} {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] (i : ι) (f : (ι → ℂ) → F) (z : ι → ℂ) : F

The antiholomorphic Wirtinger derivative, defined from the real Fréchet derivative.

Equations

• CarlsonFunctions.SeveralComplexVariables.conjWirtingerDeriv i f z = (1 / 2) • ((fderiv ℝ f z) (Pi.single i 1) + Complex.I • (fderiv ℝ f z) (Pi.single i Complex.I))

theorem CarlsonFunctions.SeveralComplexVariables.hasFDerivAt_update_real {ι : Type u_1} {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] [Finite ι] {f : (ι → ℂ) → F} (z : ι → ℂ) (i : ι) (w : ℂ) (hf : DifferentiableAt ℝ f (Function.update z i w)) : HasFDerivAt (fun (v : ℂ) => f (Function.update z i v)) (fderiv ℝ f (Function.update z i w) ∘SL ContinuousLinearMap.restrictScalars ℝ (ContinuousLinearMap.single ℂ (fun (x : ι) => ℂ) i)) w

The real derivative of a coordinate slice is the restriction of the real derivative to that coordinate's complex plane.

theorem CarlsonFunctions.SeveralComplexVariables.analyticOnNhd_iff_differentiableAt_real_cauchyRiemann {ι : Type u_1} {F : Type u_2} [Fintype ι] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {U : Set (ι → ℂ)} (hU : IsOpen U) {f : (ι → ℂ) → F} : AnalyticOnNhd ℂ f U ↔ (∀ z ∈ U, DifferentiableAt ℝ f z) ∧ ∀ z ∈ U, ∀ (i : ι), (fderiv ℝ f z) (Pi.single i Complex.I) = Complex.I • (fderiv ℝ f z) (Pi.single i 1)

On an open set, holomorphy is equivalent to real differentiability together with the coordinate Cauchy–Riemann equations. Continuous real differentiability is not needed.

theorem AnalyticOnNhd.conjWirtingerDeriv_eq_zeroCarlson {ι : Type u_1} {F : Type u_2} [Fintype ι] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {U : Set (ι → ℂ)} {f : (ι → ℂ) → F} (hf : AnalyticOnNhd ℂ f U) (hU : IsOpen U) {z : ι → ℂ} (hz : z ∈ U) (i : ι) : CarlsonFunctions.SeveralComplexVariables.conjWirtingerDeriv i f z = 0

The antiholomorphic Wirtinger derivative vanishes for a holomorphic function.

theorem AnalyticOnNhd.wirtingerDeriv_eq_partialDerivCarlson {ι : Type u_1} {F : Type u_2} [Fintype ι] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {U : Set (ι → ℂ)} {f : (ι → ℂ) → F} (hf : AnalyticOnNhd ℂ f U) (hU : IsOpen U) {z : ι → ℂ} (hz : z ∈ U) (i : ι) : CarlsonFunctions.SeveralComplexVariables.wirtingerDeriv i f z = CarlsonFunctions.SeveralComplexVariables.partialDerivCarlson i f z

For holomorphic functions the holomorphic Wirtinger derivative agrees with the complex coordinate derivative partialDeriv.