nevanlinna/Nevanlinna/laplace.lean

import Mathlib.Data.Fin.Tuple.Basic
import Mathlib.Analysis.Complex.Basic
import Mathlib.Analysis.Complex.TaylorSeries
import Mathlib.Analysis.Calculus.LineDeriv.Basic
import Mathlib.Analysis.Calculus.ContDiff.Defs
import Mathlib.Analysis.Calculus.FDeriv.Basic
import Mathlib.Analysis.Calculus.FDeriv.Symmetric
import Mathlib.Data.Complex.Module
import Mathlib.Data.Complex.Order
import Mathlib.Data.Complex.Exponential
import Mathlib.Analysis.RCLike.Basic
import Mathlib.Order.Filter.Basic
import Mathlib.Topology.Algebra.InfiniteSum.Module
import Mathlib.Topology.Basic
import Mathlib.Topology.Instances.RealVectorSpace
import Nevanlinna.cauchyRiemann
import Nevanlinna.partialDeriv

variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
variable {G : Type*} [NormedAddCommGroup G] [NormedSpace ℝ G]


noncomputable def Complex.laplace : (ℂ → F) → (ℂ → F) :=
  fun f ↦ partialDeriv ℝ 1 (partialDeriv ℝ 1 f) + partialDeriv ℝ Complex.I (partialDeriv ℝ Complex.I f)


theorem laplace_eventuallyEq {f₁ f₂ : ℂ → F} {x : ℂ} (h : f₁ =ᶠ[nhds x] f₂) : Complex.laplace f₁ x = Complex.laplace f₂ x := by
  unfold Complex.laplace
  simp
  rw [partialDeriv_eventuallyEq ℝ (partialDeriv_eventuallyEq' ℝ h 1) 1]
  rw [partialDeriv_eventuallyEq ℝ (partialDeriv_eventuallyEq' ℝ h Complex.I) Complex.I]


theorem laplace_add {f₁ f₂ : ℂ → F} (h₁ : ContDiff ℝ 2 f₁) (h₂ : ContDiff ℝ 2 f₂): Complex.laplace (f₁ + f₂) = (Complex.laplace f₁) + (Complex.laplace f₂) := by
  unfold Complex.laplace
  rw [partialDeriv_add₂]
  rw [partialDeriv_add₂]
  rw [partialDeriv_add₂]
  rw [partialDeriv_add₂]
  exact
    add_add_add_comm (partialDeriv ℝ 1 (partialDeriv ℝ 1 f₁))
      (partialDeriv ℝ 1 (partialDeriv ℝ 1 f₂))
      (partialDeriv ℝ Complex.I (partialDeriv ℝ Complex.I f₁))
      (partialDeriv ℝ Complex.I (partialDeriv ℝ Complex.I f₂))

  exact (partialDeriv_contDiff ℝ h₁ Complex.I).differentiable le_rfl
  exact (partialDeriv_contDiff ℝ h₂ Complex.I).differentiable le_rfl
  exact h₁.differentiable one_le_two
  exact h₂.differentiable one_le_two
  exact (partialDeriv_contDiff ℝ h₁ 1).differentiable le_rfl
  exact (partialDeriv_contDiff ℝ h₂ 1).differentiable le_rfl
  exact h₁.differentiable one_le_two
  exact h₂.differentiable one_le_two


theorem laplace_add_ContDiffOn
  {f₁ f₂ : ℂ → F}
  {s : Set ℂ}
  (hs : IsOpen s)
  (h₁ : ContDiffOn ℝ 2 f₁ s)
  (h₂ : ContDiffOn ℝ 2 f₂ s) :
  ∀ x ∈ s, Complex.laplace (f₁ + f₂) x = (Complex.laplace f₁) x + (Complex.laplace f₂) x := by

  unfold Complex.laplace
  simp
  intro x hx

  have : partialDeriv ℝ 1 (f₁ + f₂) =ᶠ[nhds x] (partialDeriv ℝ 1 f₁) + (partialDeriv ℝ 1 f₂) := by
    sorry
  rw [partialDeriv_eventuallyEq ℝ this]
  have t₁ : DifferentiableAt ℝ (partialDeriv ℝ 1 f₁) x := by
    sorry
  have t₂ : DifferentiableAt ℝ (partialDeriv ℝ 1 f₂) x := by
    sorry
  rw [partialDeriv_add₂_differentiableAt ℝ t₁ t₂]

  have : partialDeriv ℝ Complex.I (f₁ + f₂) =ᶠ[nhds x] (partialDeriv ℝ Complex.I f₁) + (partialDeriv ℝ Complex.I f₂) := by
    sorry
  rw [partialDeriv_eventuallyEq ℝ this]
  have t₃ : DifferentiableAt ℝ (partialDeriv ℝ Complex.I f₁) x := by
    sorry
  have t₄ : DifferentiableAt ℝ (partialDeriv ℝ Complex.I f₂) x := by
    sorry
  rw [partialDeriv_add₂_differentiableAt ℝ t₃ t₄]

  -- I am super confused at this point because the tactic 'ring' does not work.
  -- I do not understand why. So, I need to do things by hand.
  rw [add_assoc]
  rw [add_assoc]
  rw [add_right_inj (partialDeriv ℝ 1 (partialDeriv ℝ 1 f₁) x)]
  rw [add_comm]
  rw [add_assoc]
  rw [add_right_inj (partialDeriv ℝ Complex.I (partialDeriv ℝ Complex.I f₁) x)]
  rw [add_comm]


theorem laplace_smul {f : ℂ → F} : ∀ v : ℝ, Complex.laplace (v • f) = v • (Complex.laplace f) := by
  intro v
  unfold Complex.laplace
  rw [partialDeriv_smul₂]
  rw [partialDeriv_smul₂]
  rw [partialDeriv_smul₂]
  rw [partialDeriv_smul₂]
  simp


theorem laplace_compContLin {f : ℂ → F} {l : F →L[ℝ] G} (h : ContDiff ℝ 2 f) :
  Complex.laplace (l ∘ f) = l ∘ (Complex.laplace f) := by
  unfold Complex.laplace
  rw [partialDeriv_compContLin]
  rw [partialDeriv_compContLin]
  rw [partialDeriv_compContLin]
  rw [partialDeriv_compContLin]
  simp

  exact (partialDeriv_contDiff ℝ h Complex.I).differentiable le_rfl
  exact h.differentiable one_le_two
  exact (partialDeriv_contDiff ℝ h 1).differentiable le_rfl
  exact h.differentiable one_le_two


theorem laplace_compContLinAt {f : ℂ → F} {l : F →L[ℝ] G} {x : ℂ} (h : ContDiffAt ℝ 2 f x) :
  Complex.laplace (l ∘ f) x = (l ∘ (Complex.laplace f)) x := by

  have A₂ : ∃ v ∈ nhds x, (IsOpen v) ∧ (x ∈ v) ∧ (ContDiffOn ℝ 2 f v) := by
    have : ∃ u ∈ nhds x, ContDiffOn ℝ 2 f u := by
      apply ContDiffAt.contDiffOn h
      rfl
    obtain ⟨u, hu₁, hu₂⟩ := this
    obtain ⟨v, hv₁, hv₂, hv₃⟩ := mem_nhds_iff.1 hu₁
    use v
    constructor
    · exact IsOpen.mem_nhds hv₂ hv₃
    · constructor
      exact hv₂
      constructor
      · exact hv₃
      · exact ContDiffOn.congr_mono hu₂ (fun x => congrFun rfl) hv₁
  obtain ⟨v, hv₁, hv₂, hv₃, hv₄⟩ := A₂

  have D : ∀ w : ℂ, partialDeriv ℝ w (l ∘ f) =ᶠ[nhds x] l ∘ partialDeriv ℝ w (f) := by
    intro w
    apply Filter.eventuallyEq_iff_exists_mem.2
    use v
    constructor
    · exact IsOpen.mem_nhds hv₂ hv₃
    · intro y hy
      apply partialDeriv_compContLinAt
      let V := ContDiffOn.differentiableOn hv₄ one_le_two
      apply DifferentiableOn.differentiableAt V
      apply IsOpen.mem_nhds
      assumption
      assumption

  unfold Complex.laplace
  simp

  rw [partialDeriv_eventuallyEq ℝ (D 1) 1]
  rw [partialDeriv_compContLinAt]
  rw [partialDeriv_eventuallyEq ℝ (D Complex.I) Complex.I]
  rw [partialDeriv_compContLinAt]
  simp

  -- DifferentiableAt ℝ (partialDeriv ℝ Complex.I f) x
  apply ContDiffAt.differentiableAt (partialDeriv_contDiffAt ℝ (ContDiffOn.contDiffAt hv₄ hv₁) Complex.I)
  rfl

  -- DifferentiableAt ℝ (partialDeriv ℝ 1 f) x
  apply ContDiffAt.differentiableAt (partialDeriv_contDiffAt ℝ (ContDiffOn.contDiffAt hv₄ hv₁) 1)
  rfl


theorem laplace_compCLE {f : ℂ → F} {l : F ≃L[ℝ] G} (h : ContDiff ℝ 2 f) :
  Complex.laplace (l ∘ f) = l ∘ (Complex.laplace f) := by
  let l' := (l : F →L[ℝ] G)
  have : Complex.laplace (l' ∘ f) = l' ∘ (Complex.laplace f) := by
    exact laplace_compContLin h
  exact this