nevanlinna/Nevanlinna/harmonicAt_examples.lean

import Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
import Nevanlinna.complexHarmonic
import Nevanlinna.holomorphicAt

variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F]


theorem holomorphicAt_is_harmonicAt
  {f : ℂ → F}
  {z : ℂ}
  (hf : HolomorphicAt f z) :
  HarmonicAt f z := by

  let t := {x | HolomorphicAt f x}
  have ht : IsOpen t := HolomorphicAt_isOpen f
  have hz : z ∈ t := by exact hf

  constructor
  · -- ContDiffAt ℝ 2 f z
    exact hf.contDiffAt

  · -- Δ f =ᶠ[nhds z] 0
    apply Filter.eventuallyEq_iff_exists_mem.2
    use t
    constructor
    · exact IsOpen.mem_nhds ht hz
    · intro w hw
      unfold Complex.laplace
      simp
      rw [partialDeriv_eventuallyEq ℝ hw.CauchyRiemannAt Complex.I]
      rw [partialDeriv_smul'₂]
      simp

      rw [partialDeriv_commAt hw.contDiffAt Complex.I 1]
      rw [partialDeriv_eventuallyEq ℝ hw.CauchyRiemannAt 1]
      rw [partialDeriv_smul'₂]
      simp

      rw [← smul_assoc]
      simp


theorem re_of_holomorphicAt_is_harmonicAr
  {f : ℂ → ℂ}
  {z : ℂ}
  (h : HolomorphicAt f z) :
  HarmonicAt (Complex.reCLM ∘ f) z := by
  apply harmonicAt_comp_CLM_is_harmonicAt
  exact holomorphicAt_is_harmonicAt h


theorem im_of_holomorphicAt_is_harmonicAt
  {f : ℂ → ℂ}
  {z : ℂ}
  (h : HolomorphicAt f z) :
  HarmonicAt (Complex.imCLM ∘ f) z := by
  apply harmonicAt_comp_CLM_is_harmonicAt
  exact holomorphicAt_is_harmonicAt h


theorem antiholomorphicAt_is_harmonicAt
  {f : ℂ → ℂ}
  {z : ℂ}
  (h : HolomorphicAt f z) :
  HarmonicAt (Complex.conjCLE ∘ f) z := by
  apply harmonicAt_iff_comp_CLE_is_harmonicAt.1
  exact holomorphicAt_is_harmonicAt h


theorem log_normSq_of_holomorphicAt_is_harmonicAt
  {f : ℂ → ℂ}
  {z : ℂ}
  (h₁f : HolomorphicAt f z)
  (h₂f : f z ≠ 0) :
  HarmonicAt (Real.log ∘ Complex.normSq ∘ f) z := by

  -- For later use
  have slitPlaneLemma {z : ℂ} (hz : z ≠ 0) : z ∈ Complex.slitPlane ∨ -z ∈ Complex.slitPlane := by
    rw [Complex.mem_slitPlane_iff, Complex.mem_slitPlane_iff]
    simp at hz
    rw [Complex.ext_iff] at hz
    push_neg at hz
    simp at hz
    simp
    by_contra contra
    push_neg at contra
    exact hz (le_antisymm contra.1.1 contra.2.1) contra.1.2

  -- First prove the theorem for functions with image in the slitPlane
  have lem₁ : ∀ g : ℂ → ℂ, (HolomorphicAt g z) → (g z ≠ 0) → (g z ∈ Complex.slitPlane) → HarmonicAt (Real.log ∘ Complex.normSq ∘ g) z := by
    intro g h₁g h₂g h₃g

    -- Rewrite the log |g|² as Complex.log (g * gc)
    suffices hyp : HarmonicAt (Complex.log ∘ ((Complex.conjCLE ∘ g) * g)) z from by
      have : Real.log ∘ Complex.normSq ∘ g = Complex.reCLM ∘ Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ g := by
        funext x
        simp
      rw [this]

      have : Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ g = Complex.log ∘ ((Complex.conjCLE ∘ g) * g) := by
        funext x
        simp
        rw [Complex.ofReal_log]
        rw [Complex.normSq_eq_conj_mul_self]
        exact Complex.normSq_nonneg (g x)
      rw [← this] at hyp
      apply harmonicAt_comp_CLM_is_harmonicAt hyp

    -- Locally around z, rewrite Complex.log (g * gc) as Complex.log g + Complex.log.gc
    -- This uses the assumption that g z is in Complex.slitPlane
    have : (Complex.log ∘ (Complex.conjCLE ∘ g * g)) =ᶠ[nhds z] (Complex.log ∘ Complex.conjCLE ∘ g + Complex.log ∘ g) := by
      apply Filter.eventuallyEq_iff_exists_mem.2
      use g⁻¹' (Complex.slitPlane ∩ {0}ᶜ)
      constructor
      · apply ContinuousAt.preimage_mem_nhds
        · exact h₁g.differentiableAt.continuousAt
        · apply IsOpen.mem_nhds
          apply IsOpen.inter Complex.isOpen_slitPlane isOpen_ne
          constructor
          · exact h₃g
          · exact h₂g
      · intro x hx
        simp
        rw [Complex.log_mul_eq_add_log_iff _ hx.2]
        rw [Complex.arg_conj]
        simp [Complex.slitPlane_arg_ne_pi hx.1]
        constructor
        · exact Real.pi_pos
        · exact Real.pi_nonneg
        simp
        apply hx.2

    -- Locally around z, rewrite Complex.log (g * gc) as Complex.log g + Complex.log.gc
    -- This uses the assumption that g z is in Complex.slitPlane
    have : (Complex.log ∘ (Complex.conjCLE ∘ g * g)) =ᶠ[nhds z] (Complex.conjCLE ∘ Complex.log ∘ g + Complex.log ∘ g) := by
      apply Filter.eventuallyEq_iff_exists_mem.2
      use g⁻¹' (Complex.slitPlane ∩ {0}ᶜ)
      constructor
      · apply ContinuousAt.preimage_mem_nhds
        · exact h₁g.differentiableAt.continuousAt
        · apply IsOpen.mem_nhds
          apply IsOpen.inter Complex.isOpen_slitPlane isOpen_ne
          constructor
          · exact h₃g
          · exact h₂g
      · intro x hx
        simp
        rw [← Complex.log_conj]
        rw [Complex.log_mul_eq_add_log_iff _ hx.2]
        rw [Complex.arg_conj]
        simp [Complex.slitPlane_arg_ne_pi hx.1]
        constructor
        · exact Real.pi_pos
        · exact Real.pi_nonneg
        simp
        apply hx.2
        apply Complex.slitPlane_arg_ne_pi hx.1

    rw [HarmonicAt_eventuallyEq this]
    apply harmonicAt_add_harmonicAt_is_harmonicAt
    · rw [← harmonicAt_iff_comp_CLE_is_harmonicAt]
      apply holomorphicAt_is_harmonicAt
      apply HolomorphicAt_comp
      use Complex.slitPlane
      constructor
      · apply IsOpen.mem_nhds
        exact Complex.isOpen_slitPlane
        assumption
      · exact fun z a => Complex.differentiableAt_log a
      exact h₁g
    · apply holomorphicAt_is_harmonicAt
      apply HolomorphicAt_comp
      use Complex.slitPlane
      constructor
      · apply IsOpen.mem_nhds
        exact Complex.isOpen_slitPlane
        assumption
      · exact fun z a => Complex.differentiableAt_log a
      exact h₁g

  by_cases h₃f : f z ∈ Complex.slitPlane
  · exact lem₁ f h₁f h₂f h₃f
  · have : Complex.normSq ∘ f = Complex.normSq ∘ (-f) := by funext; simp
    rw [this]
    apply lem₁ (-f)
    · exact HolomorphicAt_neg h₁f
    · simpa
    · exact (slitPlaneLemma h₂f).resolve_left h₃f


theorem logabs_of_holomorphicAt_is_harmonic
  {f : ℂ → ℂ}
  {z : ℂ}
  (h₁f : HolomorphicAt f z)
  (h₂f : f z ≠ 0) :
  HarmonicAt (fun w ↦ Real.log ‖f w‖) z := by

  -- Suffices: Harmonic (2⁻¹ • Real.log ∘ ⇑Complex.normSq ∘ f)
  have : (fun z ↦ Real.log ‖f z‖) = (2 : ℝ)⁻¹ • (Real.log ∘ Complex.normSq ∘ f) := by
    funext z
    simp
    unfold Complex.abs
    simp
    rw [Real.log_sqrt]
    rw [div_eq_inv_mul (Real.log (Complex.normSq (f z))) 2]
    exact Complex.normSq_nonneg (f z)
  rw [this]

  -- Suffices: Harmonic (Real.log ∘ ⇑Complex.normSq ∘ f)
  apply (harmonicAt_iff_smul_const_is_harmonicAt (inv_ne_zero two_ne_zero)).1
  exact log_normSq_of_holomorphicAt_is_harmonicAt h₁f h₂f