From 1918cc01398cb723a3dd4d7c40e7464d347753c6 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Fri, 26 Apr 2024 16:02:56 +0200
Subject: [PATCH] Update harmonic.lean

---
 nevanlinna/harmonic.lean | 231 ++++++++++++++++++++++++++++++++++++---
 1 file changed, 216 insertions(+), 15 deletions(-)

diff --git a/nevanlinna/harmonic.lean b/nevanlinna/harmonic.lean
index 658ff92..b387bfa 100644
--- a/nevanlinna/harmonic.lean
+++ b/nevanlinna/harmonic.lean
@@ -1,5 +1,7 @@
 import Mathlib.Analysis.Complex.Basic
 import Mathlib.Analysis.Calculus.LineDeriv.Basic
+import Mathlib.Analysis.SpecialFunctions.ExpDeriv
+import Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
 
 -- Harmonic functions on the plane
 
@@ -7,19 +9,187 @@ import Mathlib.Analysis.Calculus.LineDeriv.Basic
 noncomputable def laplace' : (ℂ → ℝ) → (ℂ → ℝ) := by
   intro f
 
-  let f₁ := fun x ↦ lineDeriv ℝ f x ⟨1, 0⟩
-  let g₁ := fun x ↦ lineDeriv ℝ f x ⟨1, 0⟩
-  let f₁₁ := fun x ↦ lineDeriv ℝ f₁ x ⟨1, 0⟩
-  let f₂ := fun x ↦ lineDeriv ℝ f x ⟨0, 1⟩
-  let f₂₂ := fun x ↦ lineDeriv ℝ f₂ x ⟨0, 1⟩
+  let f₁ := fun x ↦ lineDeriv ℝ f x 1
+  let f₁₁ := fun x ↦ lineDeriv ℝ f₁ x 1
+  let f₂ := fun x ↦ lineDeriv ℝ f x Complex.I
+  let f₂₂ := fun x ↦ lineDeriv ℝ f₂ x Complex.I
   exact f₁₁ + f₂₂
 
-example : ∀ z₀ : ℂ, laplace' (fun z ↦ z.re) z₀ = 0 := by
-  intro z₀ 
-
-  unfold laplace' lineDeriv
+example : laplace' (fun z ↦ z.re) = fun z ↦ 0 := by
+  
+  unfold laplace' lineDeriv  
   simp
 
+  conv =>
+    lhs
+    intro x
+    arg 1
+    intro t
+    rw [deriv_add] <;> tactic => try fun_prop
+  simp
+  rfl
+
+example : laplace' (fun z ↦ (z*z).re) = fun z ↦ 0 := by
+  
+  unfold laplace' lineDeriv  
+  simp
+
+  conv =>
+    lhs
+    intro x
+    simp
+    arg 1
+    arg 1
+    intro t
+    rw [deriv_sub] <;> tactic => try fun_prop
+    simp
+    rw [deriv_mul] <;> tactic => try fun_prop
+    simp
+    rw [deriv_add] <;> tactic => try fun_prop
+    simp
+  
+  conv =>
+    lhs
+    intro x
+    arg 1
+    rw [deriv_add] <;> tactic => try fun_prop
+    rw [deriv_add] <;> tactic => try fun_prop
+    simp
+    rw [one_add_one_eq_two]
+
+
+  conv =>
+    lhs
+    intro x
+    arg 2
+    conv =>
+      arg 1
+      intro t
+      rw [deriv_sub] <;> tactic => try fun_prop
+      rw [deriv_mul] <;> tactic => try fun_prop
+      simp
+      rw [deriv_mul] <;> tactic => try fun_prop
+      simp
+      rw [deriv_add] <;> tactic => try fun_prop
+      rw [deriv_add] <;> tactic => try fun_prop
+      simp
+    
+  conv =>
+    lhs
+    intro x
+    rw [deriv_add] <;> tactic => try fun_prop
+    rw [deriv_add] <;> tactic => try fun_prop
+    simp
+
+  group
+
+example : laplace' (fun z ↦ (Complex.exp z).re) = fun z ↦ 0 := by
+  
+  unfold laplace' lineDeriv  
+  simp
+  
+  conv =>
+    lhs
+    arg 1
+    intro x
+    arg 1
+    intro t
+    arg 1
+    intro t₁
+    rw [Complex.exp_add]
+    rw [Complex.exp_add]
+  
+  conv =>
+    lhs
+    arg 1
+    intro x
+    arg 1
+    intro t
+    simp
+    conv =>
+      rhs
+      arg 1
+      intro x₁
+      rw [Complex.exp_re]
+      simp
+    rw [Real.deriv_exp]
+    simp
+  
+  conv =>
+    lhs
+    arg 1
+    intro x
+    simp
+    rhs
+    arg 1
+    intro x
+    rw [Complex.exp_re]
+  
+  conv =>
+    lhs
+    lhs
+    intro x
+    rhs
+    lhs
+    intro x₁
+    simp
+  
+  simp
+
+  conv =>
+    lhs
+    rhs
+    intro x
+    lhs
+    intro t
+    arg 1
+    intro t₁
+    rw [Complex.exp_add]
+    rw [Complex.exp_add]
+    simp
+    rw [Complex.exp_re]
+    rw [Complex.exp_im]
+    simp
+
+  conv =>
+    lhs
+    rhs
+    intro x
+    lhs
+    intro t
+    
+    simp
+    
+  
+
+    
+
+    
+    -- oops
+
+
+
+
+        conv =>
+          lhs
+
+          rw [Complex.exp_add]
+                  
+        rw [deriv_mul] <;> tactic => try fun_prop
+
+
+
+  sorry
+
+  rw [deriv_add] <;> tactic => try fun_prop
+
+      
+
+
+
+
+
+
   sorry
 
 noncomputable def laplace : (ℂ → ℝ) → (ℂ → ℝ) := by
@@ -39,13 +209,33 @@ noncomputable def laplace : (ℂ → ℝ) → (ℂ → ℝ) := by
 
 
 example : ∀ z₀ : ℂ, laplace (fun z ↦ (z*z).re) z₀ = 0 := by
-  intro z₀ 
-
+  intro z₀
   unfold laplace
   dsimp [lineDeriv]
   simp
-
-  sorry
+  conv =>
+    lhs
+    lhs
+    arg 1
+    intro t
+    rw [deriv_sub] <;> tactic => try fun_prop
+    rw [deriv_mul] <;> tactic => try fun_prop
+    rw [deriv_const_add]
+    simp
+    ring_nf
+  conv =>
+    lhs
+    rhs
+    arg 1
+    intro t
+    rw [deriv_sub] <;> tactic => try fun_prop
+    rw [deriv_const]
+    rw [deriv_mul] <;> tactic => try fun_prop
+    rw [deriv_const_add]
+    simp
+    ring_nf
+  rw [deriv_const_add, deriv_sub] <;> try fun_prop
+  simp
 
 example : ∀ z₀ : ℂ, laplace (fun z ↦ (Complex.exp z).re) z₀ = 0 := by
   intro z₀ 
@@ -57,8 +247,19 @@ example : ∀ z₀ : ℂ, laplace (fun z ↦ (Complex.exp z).re) z₀ = 0 := by
   sorry
 
 example : deriv (fun (t : ℝ) ↦ 2 + t) = fun (t : ℝ) ↦ 1 := by
-  -- Does not work: simp [deriv.add]            
-  sorry
+  -- in my experience with the library, more results are stated about
+  -- `HasDerivAt` than about equality of `deriv`
+  rw [deriv_eq] 
+  
+  intro x
+  
+  -- I guessed the name `HasDerivAt.add`, which didn't work, but the
+  -- autocomplete dropdown showed `add_const` and `const_add` too
+  apply HasDerivAt.const_add 
+
+  -- I assumed this was in the library, and `apply?` found it
+  exact hasDerivAt_id' x 
+
 
 example : laplace (fun z ↦ (Complex.exp z).re) = 0 := by
   have : (fun z => (Complex.exp z).re) = (fun z => Real.exp z.re * Real.cos z.im) := by