nevanlinna/Nevanlinna/holomorphic_examples.lean

import Nevanlinna.complexHarmonic
import Nevanlinna.holomorphicAt
import Nevanlinna.holomorphic_primitive


theorem CauchyRiemann₆
  {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] 
  {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] 
  {f : E → F}
  {z : E} : 
  (DifferentiableAt ℂ f z) ↔ (DifferentiableAt ℝ f z) ∧ ∀ e, partialDeriv ℝ (Complex.I • e) f z = Complex.I • partialDeriv ℝ e f z := by
  constructor

  · -- Direction "→" 
    intro h
    constructor
    · exact DifferentiableAt.restrictScalars ℝ h
    · unfold partialDeriv
      conv =>
        intro e
        left
        rw [DifferentiableAt.fderiv_restrictScalars ℝ h]
        simp
        rw [← mul_one Complex.I]
        rw [← smul_eq_mul]
      conv =>
        intro e
        right
        right
        rw [DifferentiableAt.fderiv_restrictScalars ℝ h]
      simp

  · -- Direction "←" 
    intro ⟨h₁, h₂⟩
    apply (differentiableAt_iff_restrictScalars ℝ h₁).2

    use {
      toFun := fderiv ℝ f z
      map_add' := fun x y => ContinuousLinearMap.map_add (fderiv ℝ f z) x y
      map_smul' := by
        simp
        intro m x
        have : m = m.re + m.im • Complex.I := by simp
        rw [this, add_smul, add_smul, ContinuousLinearMap.map_add]
        congr
        simp
        rw [smul_assoc, smul_assoc, ContinuousLinearMap.map_smul (fderiv ℝ f z) m.2]
        congr
        exact h₂ x
    }
    rfl


theorem CauchyRiemann₇
  {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] 
  {f : ℂ → F}
  {z : ℂ} : 
  (DifferentiableAt ℂ f z) ↔ (DifferentiableAt ℝ f z) ∧ partialDeriv ℝ Complex.I f z = Complex.I • partialDeriv ℝ 1 f z := by
  constructor
  · intro hf
    constructor
    · exact (CauchyRiemann₆.1 hf).1
    · let A := (CauchyRiemann₆.1 hf).2 1
      simp at A
      exact A
  · intro ⟨h₁, h₂⟩
    apply CauchyRiemann₆.2
    constructor
    · exact h₁
    · intro e
      have : Complex.I • e = e • Complex.I := by 
        rw [smul_eq_mul, smul_eq_mul]
        exact CommMonoid.mul_comm Complex.I e
      rw [this]
      have : e = e.re + e.im • Complex.I := by simp
      rw [this, add_smul, partialDeriv_add₁, partialDeriv_add₁]
      simp
      rw [← smul_eq_mul]
      have : partialDeriv ℝ ((e.re : ℝ) • Complex.I) f = partialDeriv ℝ ((e.re : ℂ) • Complex.I) f := by rfl
      rw [← this, partialDeriv_smul₁ ℝ]
      have : (e.re : ℂ) = (e.re : ℝ) • (1 : ℂ) := by simp
      rw [this, partialDeriv_smul₁ ℝ]
      have : partialDeriv ℝ ((e.im : ℂ) * Complex.I) f = partialDeriv ℝ ((e.im : ℝ) • Complex.I) f := by rfl
      rw [this, partialDeriv_smul₁ ℝ]
      simp
      rw [h₂]
      rw [smul_comm]
      congr
      rw [mul_assoc]
      simp
      nth_rw 2 [smul_comm]
      rw [← smul_assoc]
      simp
      have : - (e.im : ℂ) = (-e.im : ℝ) • (1 : ℂ) := by simp
      rw [this, partialDeriv_smul₁ ℝ]
      simp
  


/-

A harmonic, real-valued function on ℂ is the real part of a suitable holomorphic function.

-/

theorem harmonic_is_realOfHolomorphic
  {f : ℂ → ℝ}
  (hf : ∀ z, HarmonicAt f z) :
  ∃ F : ℂ → ℂ, ∀ z, HolomorphicAt F z ∧ (Complex.reCLM ∘ F = f) := by

  let f_1 : ℂ → ℂ := Complex.ofRealCLM ∘ (partialDeriv ℝ 1 f)
  let f_I : ℂ → ℂ := Complex.ofRealCLM ∘ (partialDeriv ℝ Complex.I f)

  let g : ℂ → ℂ := f_1 - Complex.I • f_I

  have reg₂f : ContDiff ℝ 2 f := by
    apply contDiff_iff_contDiffAt.mpr 
    intro z
    exact (hf z).1

  have reg₁f_1 : ContDiff ℝ 1 f_1 := by
    apply contDiff_iff_contDiffAt.mpr 
    intro z
    dsimp [f_1]
    apply ContDiffAt.continuousLinearMap_comp
    exact partialDeriv_contDiffAt ℝ (hf z).1 1

  have reg₁f_I : ContDiff ℝ 1 f_I := by
    apply contDiff_iff_contDiffAt.mpr 
    intro z
    dsimp [f_I]
    apply ContDiffAt.continuousLinearMap_comp
    exact partialDeriv_contDiffAt ℝ (hf z).1 Complex.I

  have reg₁g : ContDiff ℝ 1 g := by 
    dsimp [g]
    apply ContDiff.sub
    exact reg₁f_1
    have : Complex.I • f_I = fun x ↦ Complex.I • f_I x := rfl
    rw [this]
    apply ContDiff.const_smul
    exact reg₁f_I
  
  have reg₁ : Differentiable ℂ g := by 
    intro z
    apply CauchyRiemann₇.2
    constructor
    · apply Differentiable.differentiableAt
      apply ContDiff.differentiable
      exact reg₁g
      rfl
    · dsimp [g]
      rw [partialDeriv_sub₂, partialDeriv_sub₂]
      simp
      dsimp [f_1, f_I]
      rw [partialDeriv_smul'₂, partialDeriv_smul'₂]
      rw [partialDeriv_compContLin, partialDeriv_compContLin, partialDeriv_compContLin, partialDeriv_compContLin]
      rw [mul_sub]
      simp
      rw [← mul_assoc]
      simp
      rw [add_comm, sub_eq_add_neg]
      congr 1
      · rw [partialDeriv_comm reg₂f Complex.I 1]
      · let A := Filter.EventuallyEq.eq_of_nhds (hf z).2
        simp at A
        unfold Complex.laplace at A
        conv =>
          right
          right
          rw [← sub_zero (partialDeriv ℝ 1 (partialDeriv ℝ 1 f) z)]
          rw [← A]
        simp

      --Differentiable ℝ (partialDeriv ℝ _ f)
      repeat
        apply ContDiff.differentiable 
        apply contDiff_iff_contDiffAt.mpr 
        exact fun w ↦ partialDeriv_contDiffAt ℝ (hf w).1 _
        apply le_rfl
      -- Differentiable ℝ f_1
      exact reg₁f_1.differentiable le_rfl
      -- Differentiable ℝ (Complex.I • f_I)
      have : Complex.I • f_I = fun x ↦ Complex.I • f_I x := rfl
      rw [this]
      apply Differentiable.const_smul
      exact reg₁f_I.differentiable le_rfl
      -- Differentiable ℝ f_1
      exact reg₁f_1.differentiable le_rfl
      -- Differentiable ℝ (Complex.I • f_I)
      have : Complex.I • f_I = fun x ↦ Complex.I • f_I x := rfl
      rw [this]
      apply Differentiable.const_smul
      exact reg₁f_I.differentiable le_rfl
  
  let F := fun z ↦ (primitive 0 g) z + f 0
  have regF : Differentiable ℂ F := by 
    apply Differentiable.add
    intro x
    let A : HasDerivAt (primitive 0 g) (g x) x := primitive_fderiv g reg₁
    exact A.differentiableAt 
    simp

  have pF' : ∀ x, (fderiv ℂ F x) = ContinuousLinearMap.lsmul ℂ ℂ (g x) := by 
    intro x
    dsimp [F]
    rw [fderiv_add_const]
    let A : HasDerivAt (primitive 0 g) (g x) x := primitive_fderiv g reg₁
    let B : HasFDerivAt (primitive 0 g) (ContinuousLinearMap.lsmul ℂ ℂ (g x)) x := by
      rw [hasFDerivAt_iff_hasDerivAt]
      simp
      exact A
    exact HasFDerivAt.fderiv B

  have pF'' : ∀ x, (fderiv ℝ F x) = ContinuousLinearMap.lsmul ℝ ℂ (g x) := by 
    intro x
    rw [DifferentiableAt.fderiv_restrictScalars ℝ (regF x), pF' x]
    exact rfl

  use F
  intro z
  constructor
  · -- HolomorphicAt F z
    apply HolomorphicAt_iff.2
    use Set.univ
    constructor
    · exact isOpen_const
    · constructor
      · simp
      · intro w _
        exact regF w
  · -- (F z).re = f z
    have A := reg₂f.differentiable one_le_two
    have B : Differentiable ℝ (Complex.reCLM ∘ F) := by 
      apply Differentiable.comp
      exact ContinuousLinearMap.differentiable Complex.reCLM
      exact Differentiable.restrictScalars ℝ regF
    have C : (F 0).re = f 0 := by 
      dsimp [F]
      rw [primitive_zeroAtBasepoint]
      simp

    apply eq_of_fderiv_eq B A _ 0 C
    intro x
    rw [fderiv.comp]
    simp
    apply ContinuousLinearMap.ext
    intro w
    simp
    rw [pF'']
    dsimp [g, f_1, f_I, partialDeriv]
    simp
    have : w = w.re • 1 + w.im • Complex.I := by simp
    nth_rw 3 [this]
    rw [(fderiv ℝ f x).map_add]
    rw [(fderiv ℝ f x).map_smul, (fderiv ℝ f x).map_smul]
    rw [smul_eq_mul, smul_eq_mul]
    ring
    -- DifferentiableAt ℝ (⇑Complex.reCLM) (F x)
    exact ContinuousLinearMap.differentiableAt Complex.reCLM
    -- DifferentiableAt ℝ F x
    exact regF.restrictScalars ℝ x