Cauchy-Riemann

Stream: general

[Henry Goodell]

I am trying to formalize very basic complex analysis, and the Cauchy-Riemann equation is pretty important for that. I found that in Mathlib 3 they were formalized (or at least work was done on formalizing them), but it seems that they have not been formalized in mathlib 4. Is it possible to prove, and define the cauchy-riemann equation using the line derivative function?
I am relatively new here, so Im not sure if this is the right channel (if it is not, please point me to the correct one).

[Johan Commelin]

Welcome! Everything in mathlib 3 was ported to mathlib 4. Do you have a link to the formalization you found?

[Henry Goodell]

It looks like there was some work being done on it, evidenced by this thread, but I can not find any actual results, nor any mention of using the line derivative in relation to the Cauchy-Riemann equations.

[Yaël Dillies]

If you grep (Ctrl + F mathlib-wide) for "Cauchy-Riemann", then you will relevant results :wink:

[Henry Goodell]

It looks like there are equivalent statements, but no explicit statement of the conditions, nor proofs of their equivalence to the stated equivalents. Does this statement appear to be an accurate description of the Cauchy-Riemann conditions? :

theorem HenryCauchyRiemann  (f: ℂ → ℂ)(u v : (ℝ × ℝ) → ℝ )(z : ℂ )(x y :ℝ)[NontriviallyNormedField (ℝ × ℝ)][NormedSpace (ℝ×ℝ) ℝ]
(h1:f z = u (x,y) + Complex.I * (v (x,y))):
let I := ((0 : ℝ ),(1 : ℝ ))
let E := ((1 : ℝ) , (0 : ℝ ))
LineDifferentiableAt (ℝ × ℝ) u (x , y) E
∧ LineDifferentiableAt (ℝ × ℝ) v (x , y) E
∧ LineDifferentiableAt (ℝ × ℝ) u (x , y) I
∧ LineDifferentiableAt (ℝ × ℝ) v (x , y) I
∧ lineDeriv (ℝ × ℝ) u (x , y) E = lineDeriv (ℝ × ℝ) v (x , y) I
∧ lineDeriv (ℝ × ℝ) u (x , y) I =(-1) * lineDeriv (ℝ × ℝ) v (x , y) E ↔ AnalyticAt ℂ f z := sorry

[Mitchell Lee]

Get rid of the NontriviallyNormedField condition; $\mathbb{R} \times \mathbb{R}$ isn't a nontrivially normed field.

You need the hypothesis that $z = x + iy$. Also, your hypothesis h1 states only that $f(z) = u(x, y) + iv(x,y)$ at a particular point $(x,y)$, whereas you need equality of functions.

You need the hypothesis that $f$ is Fréchet differentiable over $\mathbb{R}$ at $z$ for the forward direction. The existence of partial derivatives that satisfy the Cauchy-Riemann equations is not enough to conclude that the function is complex differentiable.
Also, the conclusion should be that $f$ is complex differentiable at $z$, not analytic. (A holomorphic function on an open subset of $\mathbb{C}$ is analytic, but a function can be complex differentiable at a point without being analytic at that point.)

[Henry Goodell]

Does the fact that \R \x \R is not a nontrivially normed field mean that you can not take the line derivatives I am trying to take here?

[Mitchell Lee]

You should take the line derivatives over $\mathbb{R}$. You can remove both hypotheses about $\mathbb{R} \times \mathbb{R}$.

Traditionally, a statement like this would be written in terms of the matrix entries of the Fréchet derivative of $f$, rather than in terms of the partial derivatives of $u$ and $v$. I recommend this approach because $f$ needs to be Fréchet differentiable anyway.

[Henry Goodell]

Ok thank you, I greatly appreciate your patience with my very lacking understanding of these structures.

[Mitchell Lee]

Also, it is worth noting that the basic theory of complex functions can (and should) be developed without ever using the Cauchy–Riemann equations. This is the approach that mathlib already takes.

[Henry Goodell]

I initially approached this with the intent of proving the Cauchy Integral theorem, and the proof that I am familiar with for this theorem involves using the Cauchy-Riemann equation in conjunction with Green's theorem. After realizing that (as far as I can tell) Green's theorem has not been formalized, I temporarily abandoned my initial goal, but I would still like produce some kind of formalization of the Cauchy-Riemann equation.

[Henry Goodell]

Is this formulation (even if not optimal) accurate? :

theorem HenryCauchyRiemann  (f: ℂ → ℂ)(u v : (ℝ × ℝ) → ℝ )(z : ℂ )(x y :ℝ)
(g1:∀ (a:ℂ), (f a = u (a.re,a.im) + Complex.I * (v (a.re,a.im)))):
let I := ((0 : ℝ ),(1 : ℝ ))
let E := ((1 : ℝ) , (0 : ℝ ))
DifferentiableAt ℝ u (z.re , z.im)
∧ DifferentiableAt ℝ v (z.re , z.im)
∧ LineDifferentiableAt ℝ  u (z.re , z.im) E
∧ LineDifferentiableAt ℝ  v (z.re , z.im) E
∧ LineDifferentiableAt ℝ  u (z.re , z.im) I
∧ LineDifferentiableAt ℝ v (z.re , z.im) I
∧ lineDeriv ℝ u (z.re , z.im) E = lineDeriv ℝ v (z.re , z.im) I
∧ lineDeriv ℝ  u (z.re , z.im) I =(-1) * lineDeriv ℝ v (z.re , z.im) E
↔ DifferentiableAt ℂ f z := sorry

[Mitchell Lee]

I think it's true now. The LineDifferentiableAt hypotheses are not necessary because they follow from the Fréchet differentiability. You can also get rid of x,y if you want.

[Henry Goodell]

Thank you so much, you have been very helpful!

[Mitchell Lee]

You're welcome

[Patrick Massot]

Of course you can work on this as an exercise, but all this is already in Mathlib in a suitably abstract way.

[Henry Goodell]

Yeah, I am currently a sophmore, and I started studying LEAN thinking I could just prove homework problems from my undergraduate Complex/Real Analysis, Algebra, and Number Theory courses. I have now realized that the extreme generality of the theorems in mathlib makes it very difficult for an undergraduate to approach and use (at least it has been for me, and my advisor generally agrees with that sentiment), so I have been attempting to formalize the basics of complex analysis in a way that is much more digestible for people who lack the knowledge necessarily to appreciate the generalized formalizations that can be found in mathlib. It has proven to be very time consuming, but I believe I am making some meaningful progress.

[Winston Yin (尹維晨)]

It’s normal to spend 10x the time to formalise a result than it takes to prove it informally, if not more. If your goal is to become familiar with Lean and formalisation, it’s probably more helpful to start with the easiest informal proofs and work your way up. On the other hand, spending some time studying the general formulation in mathlib can be a great opportunity for learning additional mathematics, beyond the typical undergraduate approach. Good luck, and do ask any questions here, including “why is this thing formalised this way?” It’s definitely not meant to be self-evident.

[Oliver Nash]

A while back while trying to persuade someone about Mathlib, I made a script showing how to "see" the classical form of the Cauchy-Riemann equations. It's not very pretty but it does contain valid Lean which reads:

    ∂u/∂y = - ∂v/∂x ∧
    ∂v/∂y =   ∂u/∂x := by

[Oliver Nash]

Since it was easy to get it working again, I'll share it here:

import Mathlib.Analysis.Complex.CauchyIntegral

open Complex

variable {E F : Type*} [NormedAddCommGroup E] [NormedAddCommGroup F]

@[simp] lemma DifferentiableAt.comp_ofReal_iff [NormedSpace ℝ E] {f : E → ℝ} {e : E} :
    DifferentiableAt ℝ (ofReal ∘ f) e ↔ DifferentiableAt ℝ f e := by
  sorry

@[simp] lemma fderiv_ofReal_comp [NormedSpace ℝ E] {f : E → ℝ} {e : E} :
    fderiv ℝ (ofReal ∘ f) e = ofReal ∘ fderiv ℝ f e := by
  sorry

@[simp] lemma fderiv_ofReal_comp' [NormedSpace ℝ E] {f : E → ℝ} {e : E} :
    fderiv ℝ (fun e' ↦ (f e' : ℂ)) e = ofReal ∘ fderiv ℝ f e :=
  fderiv_ofReal_comp

variable [NormedSpace ℂ E] [NormedSpace ℂ F]

/-- Abstract form of Cauchy-Riemann equations -/
lemma cauchy_riemann {f : E → F} {e : E} (hf : DifferentiableAt ℂ f e) :
    (fderiv ℝ f e).comp (ContinuousLinearMap.lsmul ℝ ℂ I) =
    (ContinuousLinearMap.lsmul ℝ ℂ I).comp (fderiv ℝ f e) := by
  rw [hf.fderiv_restrictScalars ℝ]; ext; simp

local notation "∂"f"/∂x" => fun z ↦ fderiv ℝ f z 1
local notation "∂"f"/∂y" => fun z ↦ fderiv ℝ f z I
local notation "𝓒¹"f:max => ContDiff ℝ 1 f

/-- Elementary form of Cauchy-Riemann equations (demonstration only: not suitable for Mathlib). -/
example (u v : ℂ → ℝ) (h : Differentiable ℂ (fun z ↦ u z + I * v z)) :
    𝓒¹ u ∧
    𝓒¹ v ∧
    ∂u/∂y = - ∂v/∂x ∧
    ∂v/∂y =   ∂u/∂x := by
  have hu : ContDiff ℝ 1 u := by
    convert reCLM.contDiff.comp (h.contDiff.restrict_scalars ℝ); ext; simp
  have hv : ContDiff ℝ 1 v := by
    convert imCLM.contDiff.comp (h.contDiff.restrict_scalars ℝ); ext; simp
  refine ⟨hu, hv, ?_⟩
  simp_rw [funext_iff, ← forall_and]
  intro z
  have := DFunLike.congr_fun (cauchy_riemann (h z)) 1
  replace hu : DifferentiableAt ℝ (fun w ↦ (u w : ℂ)) z :=
    DifferentiableAt.comp_ofReal_iff.mpr <| hu.differentiable (le_refl 1) z
  replace hv : DifferentiableAt ℝ (fun w ↦ (v w : ℂ)) z :=
    DifferentiableAt.comp_ofReal_iff.mpr <| hv.differentiable (le_refl 1) z
  rw [ContinuousLinearMap.comp_apply, ContinuousLinearMap.comp_apply,
    ContinuousLinearMap.lsmul_apply, ContinuousLinearMap.lsmul_apply,
    fderiv_add hu (hv.const_mul I), ContinuousLinearMap.add_apply,
    ContinuousLinearMap.add_apply, smul_add, fderiv_const_mul hv,
    ContinuousLinearMap.smul_apply, ContinuousLinearMap.smul_apply] at this
  simpa [← mul_assoc, Complex.ext_iff] using this

[Tainnor]

Hi @Henry Goodell - a bit late, but just been meaning to write that I understand your struggles, I'm in a very similar boat. I've also been attempting to formalise complex analysis and also only have an undergraduate background. :) I have put off the CR equations for now and am currently trying to define complex integration.

[Johan Commelin]

Is there something specific about complex integration that you are trying to do?

[Eric Wieser]

Oliver Nash said:

A while back while trying to persuade someone about Mathlib, I made a script showing how to "see" the classical form of the Cauchy-Riemann equations. It's not very pretty but it does contain valid Lean which reads:

    ∂u/∂y = - ∂v/∂x ∧
    ∂v/∂y =   ∂u/∂x := by

How about we put this in Archive so that we can point others to it too?

[Tainnor]

Johan Commelin said:

Is there something specific about complex integration that you are trying to do?

I'm trying to define complex contour integrals "from scratch". I assume there's something like that already in mathlib, but it's meant as an educational exercise. After that, I want to attempt proving things such as integrability criteria, the Goursat lemma, Cauchy's integral theorem and formulas, etc. I'm a bit worried that I'll struggle with the more geometric aspects of it, but I'll see...

The last thing that I proved was the standard inequality

$$\left|\int_\gamma f\right| \le \lVert f \rVert_{|\gamma|} \cdot L(\gamma)$$

[Henry Goodell]

After many many many hours of work, I have completed the proof outlined by @Oliver Nash . I am in the process of writing my undergraduate thesis on this proof, and its formalization, and I would love feedback on the proof itself. I finished it literally minutes ago, so it is very messy and unrefined, but it works.

import Mathlib
import Mathlib.Analysis.Complex.CauchyIntegral
open Complex
--I got the differentiablity ofReal from https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Differentiability.20of.20the.20natural.20map.20.E2.84.9D.20.E2.86.92.20.E2.84.82/near/418076119
--I got the outline for the main proof from https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Cauchy-Riemann/near/486690839

lemma differentiable_ofReal : Differentiable ℝ ofReal' := by
  intro x
  have H : HasDerivAt ofReal' 1 x
  · refine hasDerivAt_iff_tendsto.mpr ?_
    simp only [Real.norm_eq_abs, real_smul, ofReal_sub, mul_one, sub_self, norm_zero, mul_zero,
      tendsto_const_nhds_iff]
  exact ⟨_, H.hasFDerivAt⟩

variable {E F : Type*} [NormedAddCommGroup E] [NormedAddCommGroup F]



@[simp]
lemma DifferentiableAt.comp_ofReal_iff [NormedSpace ℝ E] {f : E → ℝ} {e : E} :
   DifferentiableAt ℝ f e ↔ DifferentiableAt ℝ (ofReal' ∘ f) e  := by
apply Iff.intro
intro h1
have h2: DifferentiableAt ℝ ofReal (f e)
apply Differentiable.differentiableAt
apply differentiable_ofReal
apply DifferentiableAt.comp
apply h2
exact h1
intro h3
have h8: DifferentiableAt ℝ  RCLike.reCLM (ofReal' (f e))
apply ContinuousLinearMap.differentiableAt
have h9: DifferentiableAt ℝ f e ↔ DifferentiableAt ℝ (RCLike.reCLM ∘  ofReal' ∘ f) e
exact Eq.to_iff rfl
rw[h9]
exact comp e h8 h3

@[simp]
lemma fderiv_ofReal_comp [NormedSpace ℝ E] {f : E → ℝ} {e : E} :
    fderiv ℝ (ofReal' ∘ f) e = ofReal' ∘ fderiv ℝ f e := by
have h1: (DifferentiableAt ℝ f e) ∨ ¬(DifferentiableAt ℝ f e)
exact Classical.em (DifferentiableAt ℝ f e)
cases h1
have h2: DifferentiableAt ℝ ofReal' (f e)
apply differentiable_ofReal
rw[fderiv.comp]
have h3: HasDerivAt ofReal' 1 (f e)
· refine hasDerivAt_iff_tendsto.mpr ?_
  simp only [Real.norm_eq_abs, real_smul, ofReal_sub, mul_one, sub_self, norm_zero, mul_zero,
       tendsto_const_nhds_iff]
have h4: HasFDerivAt ofReal' ofRealCLM (f e)
exact hasFDerivAt_iff_hasDerivAt.mpr h3
have h5: fderiv ℝ ofReal' (f e) = ofRealCLM
exact HasFDerivAt.fderiv h4
rw[h5]
simp
exact rfl
exact h2
trivial
have h6: fderiv ℝ f e=0
have h0: ¬DifferentiableAt ℝ f e
trivial
exact fderiv_zero_of_not_differentiableAt h0
have h7: ¬(DifferentiableAt ℝ (ofReal' ∘ f) e)
rw[←DifferentiableAt.comp_ofReal_iff]
trivial
have h8: fderiv ℝ (ofReal' ∘ f) e=0
exact fderiv_zero_of_not_differentiableAt h7
rw[h6,h8]
exact rfl

@[simp]
lemma fderiv_ofReal_comp' [NormedSpace ℝ E] {f : E → ℝ} {e : E} :
    fderiv ℝ (fun e' ↦ (f e' : ℂ)) e = ofReal' ∘ fderiv ℝ f e :=
  fderiv_ofReal_comp

variable [NormedSpace ℂ E] [NormedSpace ℂ F](u v : ℂ → ℝ)


local notation "∂"f"/∂x" => fun z ↦ fderiv ℝ f z 1
local notation "∂"f"/∂y" => fun z ↦ fderiv ℝ f z I
local notation "𝓒¹"f:max => ContDiff ℝ 1 f
local notation "g" => (fun z ↦ u z + I * v z)

lemma cauchy_riemann {f : E → F} {e : E} (hf : DifferentiableAt ℂ f e) :
    (fderiv ℝ f e).comp (ContinuousLinearMap.lsmul ℝ ℂ I) =
    (ContinuousLinearMap.lsmul ℝ ℂ I).comp (fderiv ℝ f e) := by
  rw [hf.fderiv_restrictScalars ℝ]; ext; simp


theorem HenryCR (h : Differentiable ℂ g) :
    𝓒¹ u ∧
    𝓒¹ v ∧
    ∂u/∂y = - ∂v/∂x ∧
    ∂v/∂y =   ∂u/∂x := by

have hu : ContDiff ℝ 1 u := by
    convert reCLM.contDiff.comp (h.contDiff.restrict_scalars ℝ); ext; simp
have hv : ContDiff ℝ 1 v := by
    convert imCLM.contDiff.comp (h.contDiff.restrict_scalars ℝ); ext; simp
refine ⟨hu, hv, ?_⟩
simp_rw [funext_iff, ← forall_and]
intro z
have := DFunLike.congr_fun (cauchy_riemann (h z)) 1
apply And.intro
simp
any_goals simp at this
any_goals have h2: Differentiable ℝ u
any_goals apply ContDiff.differentiable
trivial
trivial
any_goals have h3:Differentiable ℝ v
any_goals apply ContDiff.differentiable
any_goals trivial
any_goals have h4: DifferentiableAt ℝ (fun w ↦ (u w : ℂ)) z
refine DifferentiableAt.comp' ?h4.hg (h2 z)
any_goals apply differentiable_ofReal
rotate_left
apply DifferentiableAt.comp'
apply differentiable_ofReal
apply h2
any_goals have h5: DifferentiableAt ℝ (fun w ↦ (v w : ℂ)) z
any_goals apply DifferentiableAt.comp'
any_goals apply differentiable_ofReal
any_goals apply h3
any_goals repeat rw[fderiv_add] at this
any_goals repeat rw[fderiv_mul] at this
any_goals simp at this
have h6: DifferentiableAt ℝ (ofReal' ∘ u) z
trivial
have h7: DifferentiableAt ℝ (ofReal' ∘ v) z
trivial
any_goals have h8: ofReal' ((fderiv ℝ u z) I) =((fderiv ℝ (ofReal' ∘ u) z) I)
any_goals simp
any_goals rw[h8] at this
any_goals have h9: ofReal' ((fderiv ℝ v z) I) =((fderiv ℝ (ofReal' ∘ v) z) I)
any_goals simp
any_goals rw[h9] at this
any_goals have h10: ofReal' ((fderiv ℝ u z) 1) =((fderiv ℝ (ofReal' ∘ u) z) 1)
any_goals simp
any_goals rw[h10] at this
any_goals have h11: ofReal' ((fderiv ℝ v z) 1) =((fderiv ℝ (ofReal' ∘ v) z) 1)
any_goals simp
any_goals rw[h11] at this
any_goals have h12:  I * ((fderiv ℝ (ofReal' ∘ u) z) 1 + I * (fderiv ℝ (ofReal' ∘ v) z) 1)
=I*((fderiv ℝ (ofReal' ∘ u) z) 1)-((fderiv ℝ (ofReal' ∘ v) z) 1)
any_goals rw[mul_add]
any_goals rw[←mul_assoc]
any_goals simp
any_goals trivial
any_goals rw[h12] at this
rotate_left
rotate_left
any_goals rw[Complex.ext_iff] at this
any_goals rw[Complex.add_re,Complex.sub_re,Complex.add_im,Complex.sub_im,Complex.mul_re,Complex.I_re] at this
any_goals simp at this
apply this.left
rotate_left
apply this.right
apply DifferentiableAt.comp'
apply DifferentiableAt.comp
rotate_left
simp
apply h5
apply DifferentiableAt.comp'
rotate_left
apply h5
any_goals apply DifferentiableAt.mul
any_goals exact differentiableAt_const I
exact differentiableAt_id'
exact differentiableAt_id'

[Michael Rothgang]

It's great to see this! I have some style feedback for you to get you started.

Style is always a matter of taste. The following is about making your code conform better to mathlib's style --- that'd be a requirement for PRing to the mathlib archive anyway. (In my opinion and experience, these also make code more readable, but YMMV.) So, here comes a first batch of comments.

• At some point, your proofs create multiple goals. You'll be making your proofs easier to read (and maintain) if you focus them as needed. You can use focusing dots and indentation for this. #style contains an example (search for "When new goals arise as side conditions or steps, they are indented and preceded by a focusing dot · (inserted as \.); the dot is not indented.") --- if that example is not clear enough, feel free to ask again!
• Mathlib style also uses indentation consciously: the proof of a lemma is indented by two spaces; proofs of sub-goals are indented by two further spaces (for each level).
• You're using "old-style have": mathlib has moved away from that. In short, instead of

have h8: DifferentiableAt ℝ  RCLike.reCLM (ofReal' (f e))
apply ContinuousLinearMap.differentiableAt

you'd write

have h8: DifferentiableAt ℝ  RCLike.reCLM (ofReal' (f e)) := by
  apply ContinuousLinearMap.differentiableAt

(Looking closer, you could perhaps even replace apply by exact, and then by exact ... is usually superfluous.)

• Finally, have you learned about dot notation already? That's another trick to make your code shorter. (If you haven't, people will be happy to explain.)

[Michael Rothgang]

As a meta-comment: eventually, commenting on your code will be easier if you create a PR. The contribution guidelines explain how that process works.

[Michael Rothgang]

Oh, and let me add: mathlib has style linters for some of these points. set_option linter.style.multiGoal true should enforce the first bullet I mentioned; if you minimize your imports (put #min_imports at the end of your files) and make sure Mathlib.Tactic.Have is not imported), you will ensure "old-style have" is not used.

[Henry Goodell]

I greatly appreciate the feedback on style, throughout the proof I was pretty much only focused on getting something functional, and really had no clue what standard practices were for style, but having that reference, I will update the proof as I work on my thesis. Currently I have a lot of time pressures involving my thesis, and other studies, so I will likely not create a pull request for some time, but if and when I do, I will be sure to keep this thread updated, as well as posting the correctly stylized proof once I complete that.