Experimenting…

nevanlinna/harmonic.lean

@@ -0,0 +1,148 @@
+import Mathlib.Analysis.Complex.Basic
+import Mathlib.Analysis.Calculus.LineDeriv.Basic
+
+-- Harmonic functions on the plane
+
+
+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⟩
+  exact f₁₁ + f₂₂
+
+example : ∀ z₀ : ℂ, laplace' (fun z ↦ z.re) z₀ = 0 := by
+  intro z₀ 
+
+  unfold laplace' lineDeriv
+  simp
+
+  sorry
+
+noncomputable def laplace : (ℂ → ℝ) → (ℂ → ℝ) := by
+  intro f
+
+  let F : ℝ × ℝ → ℝ := fun x ↦ f (x.1 + x.2 * Complex.I)
+
+  let e₁ : ℝ × ℝ := ⟨1, 0⟩ 
+  let e₂ : ℝ × ℝ := ⟨0, 1⟩ 
+
+  let F₁ := fun x ↦ lineDeriv ℝ F x e₁
+  let F₁₁ := fun x ↦ lineDeriv ℝ F₁ x e₁
+  let F₂ := fun x ↦ lineDeriv ℝ F x e₂
+  let F₂₂ := fun x ↦ lineDeriv ℝ F₂ x e₂
+
+  exact fun x ↦ F₁₁ ⟨x.1, x.2⟩ + F₂₂ ⟨x.1, x.2⟩
+
+
+example : ∀ z₀ : ℂ, laplace (fun z ↦ (z*z).re) z₀ = 0 := by
+  intro z₀ 
+
+  unfold laplace
+  dsimp [lineDeriv]
+  simp
+
+  sorry
+
+example : ∀ z₀ : ℂ, laplace (fun z ↦ (Complex.exp z).re) z₀ = 0 := by
+  intro z₀ 
+
+  unfold laplace
+  dsimp [lineDeriv]
+  simp
+
+  sorry
+
+example : deriv (fun (t : ℝ) ↦ 2 + t) = fun (t : ℝ) ↦ 1 := by
+  -- Does not work: simp [deriv.add]            
+  sorry
+
+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
+    funext z
+    rw [Complex.exp_re]
+  rw [this]
+
+  unfold laplace
+  simp
+
+  have F₁ : (fun (x : ℝ × ℝ) => lineDeriv ℝ (fun (t : ℝ × ℝ) => Real.exp t.1 * Real.cos t.2) x ⟨1, 0⟩) = ((fun (x : ℝ × ℝ) => (Real.exp x.1 * Real.cos x.2))) := by
+    funext x    
+    dsimp [lineDeriv]        
+    simp
+    left
+    have t₁ : (fun x_1 => Real.exp (x.1 + x_1)) = (fun x_1 => Real.exp x.1 * Real.exp x_1) := by
+      funext t
+      exact Real.exp_add x.1 t
+    rw [t₁]
+    simp
+
+  have F₂ : (fun (x : ℝ × ℝ) => lineDeriv ℝ (fun (t : ℝ × ℝ) => Real.exp t.1 * Real.sin t.2) x ⟨0, 1⟩) = ((fun (x : ℝ × ℝ) => (Real.exp x.1 * Real.cos x.2))) := by
+    funext x    
+    
+    dsimp [lineDeriv]
+    simp 
+
+    have t₁ : (fun t => Real.sin (x.2 + t)) = (Real.sin ∘ (fun t => x.2 + t)) := by
+      rfl
+    rw [t₁]
+    rw [deriv.comp]
+    simp
+
+    have : deriv (fun (t : ℝ) ↦ 2 + t) = fun (t : ℝ) ↦ 1 := by
+      simp [deriv.add]            
+      sorry
+      
+      
+
+    rw [this]
+    simp
+    · exact Real.differentiableAt_sin
+    · -- DifferentiableAt ℝ (fun t => x.2 + t) 0
+      sorry
+
+
+  rw [this]
+
+  sorry
+
+    have : deriv (fun x_1 => Real.exp (x_1 + x_1)) 0 = 2 := by
+      simp
+      group
+    
+    
+    rw [this]
+    simp
+    
+    have : deriv (fun t => Real.cos (x.2 + t * y.2)) = (fun t => -y.2 * Real.sin (x.2 + t * y.2)) := by
+      funext t₀
+      have t₁ : (fun t => Real.cos (x.2 + t * y.2)) = (Real.cos ∘ (fun t => x.2 + t * y.2)) := by
+        rfl
+      rw [t₁]
+      rw [deriv.comp]
+      simp
+      · group
+      · exact Real.differentiableAt_cos
+      · simp
+    
+    simp
+    simp
+
+    sorry
+  
+  let XX := fderiv ℝ (fun (x : ℝ × ℝ) => Real.exp x.1 * Real.cos x.2)
+  simp at XX
+
+  have : fderiv ℝ fun x => Real.exp x.1 * Real.cos x.2 = 0 := by
+
+    sorry
+
+  funext z
+  simp
+  funext 
+
+  let ZZ := Complex.exp_re z
+  sorry

nevanlinna/test.lean

@@ -84,6 +84,7 @@ theorem JensenFormula₂ :
     rw [this]
 
   
+
   have : ∀ z : ℂ, log (Complex.abs z) = 1/2 * Complex.log z + 1/2 * Complex.log (conj z) := by
     intro z