Derivative of Holomorphic Functions

Stream: Is there code for X?

[Yongxi Lin (Aaron)]

Suppose we have a holomorphic function cg : ℂ -> ℂsuch that its restriction to the real axis g is a real valued function. Do we have a theorem that can help me to prove that the complex derivative of cg on the real axis is the same as the real derivative of g? I actually also want to prove this result for higher order derivatives. That is,

import Mathlib

open Complex

variable {cg : ℂ → ℂ} {g : ℝ → ℝ}

lemma cgiteratedDeriv_eq_giteratedDeriv (t : ℝ) (n : ℕ) (hcg: Differentiable ℂ cg)
  (ht : ∀ x : ℝ, cg (x : ℂ) = g x) : iteratedDeriv n cg (t : ℂ) = iteratedDeriv n g t := by sorry

I am aware of HasDerivAt.ofReal_comp, but I have some trouble applying this result.

[Yury G. Kudryashov]

Proof by Aristotle https://aristotle.harmonic.fun/:

lemma cgiteratedDeriv_eq_giteratedDeriv {cg : ℂ → ℂ} {g : ℝ → ℝ} (t : ℝ) (n : ℕ)
    (hcg: Differentiable ℂ cg) (ht : ∀ x : ℝ, cg (x : ℂ) = g x) :
    iteratedDeriv n cg (t : ℂ) = iteratedDeriv n g t := by
  induction' n with n ih generalizing t <;> simp_all +decide [ iteratedDeriv_succ ];
  -- Since $cg$ is differentiable, its $n$-th derivative is also differentiable. The same applies to $g$.
  have h_diff : Differentiable ℂ (iteratedDeriv n cg) := by
    -- Since $cg$ is differentiable, its $n$-th derivative is also differentiable by induction.
    have h_diff_ind : ∀ n, Differentiable ℂ (iteratedDeriv n cg) := by
      -- We proceed by induction on $n$.
      intro n
      induction' n with n ih;
      · exact hcg;
      · rw [ iteratedDeriv_succ ];
        -- The derivative of a differentiable function is differentiable.
        have h_deriv_diff : AnalyticOn ℂ (iteratedDeriv n cg) Set.univ := by
          exact?;
        simp +zetaDelta at *;
        exact fun x => ( h_deriv_diff x ( Set.mem_univ x ) ) |> fun h => h.deriv.differentiableAt;
    exact h_diff_ind n;
  have h_diff_real : Differentiable ℝ (iteratedDeriv n g) := by
    -- Since the n-th derivative of cg is differentiable, its restriction to the real line is also differentiable.
    have h_restrict : Differentiable ℝ (fun t : ℝ => iteratedDeriv n cg (t : ℂ)) := by
      exact h_diff.restrictScalars ℝ |> Differentiable.comp <| Complex.ofRealCLM.differentiable;
    simpa only [ ih ] using Complex.reCLM.differentiable.comp h_restrict;
  -- Since $cg$ is differentiable, its iterated derivative is also differentiable. The derivative of a function at a point is the same as the derivative of its restriction to the real line.
  have h_deriv_eq : deriv (iteratedDeriv n cg) (t : ℂ) = deriv (fun x : ℝ => iteratedDeriv n cg (x : ℂ)) t := by
    have h_chain : deriv (iteratedDeriv n cg ∘ (fun x : ℝ => x : ℝ → ℂ)) t = deriv (iteratedDeriv n cg) (t : ℂ) * deriv (fun x : ℝ => x : ℝ → ℂ) t := by
      exact deriv_comp t h_diff.differentiableAt ( Complex.ofRealCLM.differentiableAt )
    convert h_chain.symm using 1;
    erw [ Complex.ofRealCLM.deriv ] ; norm_num;
  convert HasDerivAt.deriv ( HasDerivAt.ofReal_comp <| hasDerivAt_deriv_iff.mpr h_diff_real.differentiableAt ) using 1 ; aesop

[Yury G. Kudryashov]

Probably, it can be golfed a lot. I haven't tried.

[Yongxi Lin (Aaron)]

Thanks for your help. Aristotle is indeed useful! I clean up the code it generates very easily to get the result I want.