Update laplace.lean

Nevanlinna/laplace.lean

@@ -16,10 +16,39 @@ import Nevanlinna.partialDeriv
 
 variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
 
-noncomputable def Complex.laplace : (ℂ → F) → (ℂ → F) := by
-  intro f
-  let fx  := partialDeriv ℝ 1 f
-  let fxx := partialDeriv ℝ 1 fx
-  let fy  := partialDeriv ℝ Complex.I f
-  let fyy := partialDeriv ℝ Complex.I fy
-  exact fxx + fyy
+
+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
+
+
+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