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.Topology.Algebra.InfiniteSum.Module
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_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_smul {f : ℂ → F} (h : ContDiff ℝ 2 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

  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_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_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