Complex derivatives treated as a real derivatives

Stream: Is there code for X?

[Geoffrey Irving]

Do we have this? My guess is that it exists in some quite abstract form, but I don't know where:

import Mathlib

/-- A complex derivative, treated as `ℂ →L[ℝ] → ℂ` -/
lemma Complex.real_hasFDerivAt {f : ℂ → ℂ} {z : ℂ} {f' : ℂ} (h : HasDerivAt f f' z) :
    HasFDerivAt f (ContinuousLinearMap.lsmul ℝ ℂ f') z := by
  sorry

[Geoffrey Irving]

It's roughly

1. HasDerivAt.hasFDerivAt
2. Dropping a CLM over ℂ to one over ℝ, as these are an appropriate tower.
3. A bit of commutativity at the end to swap left and right.

(2) is the only bit I don't know how to do idiomatically. (Unless the whole thing already exists.)

[Jireh Loreaux]

(2) is docs#ContinuousLinearMap.restrictScalars

[Geoffrey Irving]

Great, thank you!

[Jireh Loreaux]

But notice we also have docs#HasFDerivAt.restrictScalars

[Geoffrey Irving]

Even better, that's everything but the (3) bit.

[Geoffrey Irving]

Ah, no, that's also just (2).

[Geoffrey Irving]

But in any case I'm set.

[Jireh Loreaux]

This works as a proof:

import Mathlib

/-- A complex derivative, treated as `ℂ →L[ℝ] → ℂ` -/
lemma Complex.real_hasFDerivAt {f : ℂ → ℂ} {z : ℂ} {f' : ℂ} (h : HasDerivAt f f' z) :
    HasFDerivAt f (ContinuousLinearMap.lsmul ℝ ℂ f') z := by
  convert h.hasFDerivAt.restrictScalars ℝ
  ext
  exact mul_comm _ _

[Geoffrey Irving]

Ha, nice. I was stuck trying to simplify things at that third line, and was blocked because (1) ContinuousLinearMap.restrictScalars_apply doesn't exist and (2) ContinuousLinearMap.coe_restrictScalars wasn't firing.

[Geoffrey Irving]

Excellent, and now I can do things like

/-- A complex derivative, treated as `ℂ →L[ℝ] → ℂ` -/
lemma Complex.real_hasFDerivAt {f : ℂ → ℂ} {z : ℂ} {f' : ℂ} (h : HasDerivAt f f' z) :
    HasFDerivAt f (ContinuousLinearMap.lsmul ℝ ℂ f') z := by
  convert h.hasFDerivAt.restrictScalars ℝ
  ext
  exact mul_comm _ _

/-- The derivative of `.im` -/
lemma hasFDerivAt_im {z : ℂ} : HasFDerivAt Complex.im imCLM z := by
  have e : Complex.im = (fun z ↦ imCLM z) := by ext z; simp only [Complex.imCLM_apply]
  rw [e]; apply ContinuousLinearMap.hasFDerivAt

/-- The derivative of `arg`, via `log` -/
lemma hasFDerivAt_arg {z : ℂ} (m : z ∈ slitPlane) :
    HasFDerivAt arg (imCLM ∘L ContinuousLinearMap.lsmul ℝ ℂ z⁻¹) z := by
  have e : arg = (fun z ↦ (log z).im) := by ext z; rw [Complex.log_im]
  rw [e]
  exact HasFDerivAt.comp _ hasDerivAt_im (Complex.real_hasFDerivAt (Complex.hasDerivAt_log m))

[Geoffrey Irving]

(Sorry, not a working example because of opens. :/)

[Geoffrey Irving]

I am using monotonicity of arg to show a region is star-shaped.