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) : ℂ → F :=
  partialDeriv ℝ 1 (partialDeriv ℝ 1 f) + partialDeriv ℝ Complex.I (partialDeriv ℝ Complex.I f)

notation "Δ" => Complex.laplace


theorem laplace_eventuallyEq {f₁ f₂ : ℂ → F} {x : ℂ} (h : f₁ =ᶠ[nhds x] f₂) : Δ f₁ x = Δ 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₂) :
  Δ (f₁ + f₂) = (Δ f₁) + (Δ 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, Δ (f₁ + f₂) x = (Δ f₁) x + (Δ 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_add_ContDiffAt
  {f₁ f₂ : ℂ → F}
  {x : ℂ}
  (h₁ : ContDiffAt ℝ 2 f₁ x)
  (h₂ : ContDiffAt ℝ 2 f₂ x) :
  Δ (f₁ + f₂) x = (Δ f₁) x + (Δ f₂) x := by

  unfold Complex.laplace
  simp

  have h₁₁ : ContDiffAt ℝ 1 f₁ x := h₁.of_le one_le_two
  have h₂₁ : ContDiffAt ℝ 1 f₂ x := h₂.of_le one_le_two
  repeat
    rw [partialDeriv_eventuallyEq ℝ (partialDeriv_add₂_contDiffAt ℝ h₁₁ h₂₁)]
    rw [partialDeriv_add₂_differentiableAt]

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

  repeat
    apply fun v ↦ (partialDeriv_contDiffAt ℝ h₁ v).differentiableAt le_rfl
    apply fun v ↦ (partialDeriv_contDiffAt ℝ h₂ v).differentiableAt le_rfl


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


theorem laplace_compCLMAt
  {f : ℂ → F}
  {l : F →L[ℝ] G}
  {x : ℂ}
  (h : ContDiffAt ℝ 2 f x) :
  Δ (l ∘ f) x = (l ∘ (Δ f)) x := by

  obtain ⟨v, hv₁, hv₂, hv₃, hv₄⟩ : ∃ v ∈ nhds x, (IsOpen v) ∧ (x ∈ v) ∧ (ContDiffOn ℝ 2 f v) := by
    obtain ⟨u, hu₁, hu₂⟩ : ∃ u ∈ nhds x, ContDiffOn ℝ 2 f u := by
      apply ContDiffAt.contDiffOn h
      rfl
    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₁

  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) le_rfl

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


theorem laplace_compCLM
  {f : ℂ → F}
  {l : F →L[ℝ] G}
  (h : ContDiff ℝ 2 f) :
  Δ (l ∘ f) = l ∘ (Δ f) := by
  funext z
  exact laplace_compCLMAt h.contDiffAt


theorem laplace_compCLE {f : ℂ → F} {l : F ≃L[ℝ] G} :
  Δ (l ∘ f) = l ∘ (Δ f) := by
  unfold Complex.laplace
  repeat
    rw [partialDeriv_compCLE]
  simp