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 hf₁ : ∀ z ∈ s, DifferentiableAt ℝ f₁ z := by
    intro z hz
    convert DifferentiableOn.differentiableAt _ (IsOpen.mem_nhds hs hz)
    apply ContDiffOn.differentiableOn h₁ one_le_two
  have hf₂ : ∀ z ∈ s, DifferentiableAt ℝ f₂ z := by
    intro z hz
    convert DifferentiableOn.differentiableAt _ (IsOpen.mem_nhds hs hz)
    apply ContDiffOn.differentiableOn h₂ one_le_two
  have : partialDeriv ℝ 1 (f₁ + f₂) =ᶠ[nhds x] (partialDeriv ℝ 1 f₁) + (partialDeriv ℝ 1 f₂) := by
    apply Filter.eventuallyEq_iff_exists_mem.2
    use s
    constructor
    · exact IsOpen.mem_nhds hs hx
    · intro z hz
      apply partialDeriv_add₂_differentiableAt
      exact hf₁ z hz
      exact hf₂ z hz
  rw [partialDeriv_eventuallyEq ℝ this]
  have t₁ : DifferentiableAt ℝ (partialDeriv ℝ 1 f₁) x := by
    let B₀ := (h₁ x hx).contDiffAt (IsOpen.mem_nhds hs hx)
    let A₀ := partialDeriv_contDiffAt ℝ B₀ 1
    exact A₀.differentiableAt (Submonoid.oneLE.proof_2 ℕ∞)
  have t₂ : DifferentiableAt ℝ (partialDeriv ℝ 1 f₂) x := by
    let B₀ := (h₂ x hx).contDiffAt (IsOpen.mem_nhds hs hx)
    let A₀ := partialDeriv_contDiffAt ℝ B₀ 1
    exact A₀.differentiableAt (Submonoid.oneLE.proof_2 ℕ∞)
  rw [partialDeriv_add₂_differentiableAt ℝ t₁ t₂]

  have : partialDeriv ℝ Complex.I (f₁ + f₂) =ᶠ[nhds x] (partialDeriv ℝ Complex.I f₁) + (partialDeriv ℝ Complex.I f₂) := by
    apply Filter.eventuallyEq_iff_exists_mem.2
    use s
    constructor
    · exact IsOpen.mem_nhds hs hx
    · intro z hz
      apply partialDeriv_add₂_differentiableAt
      exact hf₁ z hz
      exact hf₂ z hz
  rw [partialDeriv_eventuallyEq ℝ this]
  have t₃ : DifferentiableAt ℝ (partialDeriv ℝ Complex.I f₁) x := by
    let B₀ := (h₁ x hx).contDiffAt (IsOpen.mem_nhds hs hx)
    let A₀ := partialDeriv_contDiffAt ℝ B₀ Complex.I
    exact A₀.differentiableAt (Submonoid.oneLE.proof_2 ℕ∞)
  have t₄ : DifferentiableAt ℝ (partialDeriv ℝ Complex.I f₂) x := by
    let B₀ := (h₂ x hx).contDiffAt (IsOpen.mem_nhds hs hx)
    let A₀ := partialDeriv_contDiffAt ℝ B₀ Complex.I
    exact A₀.differentiableAt (Submonoid.oneLE.proof_2 ℕ∞)
  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