From 89793b75d841eea2064a1592c85396ab814e0e82 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Mon, 3 Jun 2024 17:32:33 +0200
Subject: [PATCH] Update complexHarmonic.examples.lean

---
 Nevanlinna/complexHarmonic.examples.lean | 77 ++++++++++++++++++++++++
 1 file changed, 77 insertions(+)

diff --git a/Nevanlinna/complexHarmonic.examples.lean b/Nevanlinna/complexHarmonic.examples.lean
index 07935cb..177810d 100644
--- a/Nevanlinna/complexHarmonic.examples.lean
+++ b/Nevanlinna/complexHarmonic.examples.lean
@@ -11,6 +11,7 @@ import Mathlib.Data.Complex.Order
 import Mathlib.Data.Complex.Exponential
 import Mathlib.Data.Fin.Tuple.Basic
 import Mathlib.Topology.Algebra.InfiniteSum.Module
+import Mathlib.Topology.Defs.Filter
 import Mathlib.Topology.Instances.RealVectorSpace
 import Nevanlinna.cauchyRiemann
 import Nevanlinna.laplace
@@ -240,6 +241,82 @@ theorem log_normSq_of_holomorphicOn_is_harmonicOn'
   exact DifferentiableOn.clog h₁ h₃
 
 
+theorem log_normSq_of_holomorphicOn_is_harmonicOn
+  {f : ℂ → ℂ}
+  {s : Set ℂ}
+  (hs : IsOpen s)
+  (h₁ : DifferentiableOn ℂ f s)
+  (h₂ : ∀ z ∈ s, f z ≠ 0)
+  (h₃ : ∀ z ∈ s, f z ∈ Complex.slitPlane) :
+  HarmonicOn (Real.log ∘ Complex.normSq ∘ f) s := by
+
+  let s₁ : Set ℂ := { z | f z ∈ Complex.slitPlane} ∩ s
+
+  have hs₁ : IsOpen s₁ := by
+    let A := DifferentiableOn.continuousOn h₁
+    let B := continuousOn_iff'.1 A
+    obtain ⟨u, hu₁, hu₂⟩ := B Complex.slitPlane Complex.isOpen_slitPlane
+    have : u ∩ s = s₁ := by
+      rw [← hu₂]
+      tauto
+    rw [← this]
+    apply IsOpen.inter hu₁ hs
+
+  have harm₁ : HarmonicOn (Real.log ∘ Complex.normSq ∘ f) s₁ := by
+    apply log_normSq_of_holomorphicOn_is_harmonicOn'
+    exact hs₁
+    apply DifferentiableOn.mono h₁ (Set.inter_subset_right {z | f z ∈ Complex.slitPlane} s)
+    -- ∀ z ∈ s₁, f z ≠ 0
+    exact fun z hz ↦ h₂ z (Set.mem_of_mem_inter_right hz)
+    -- ∀ z ∈ s₁, f z ∈ Complex.slitPlane
+    exact fun z hz ↦ h₃ z (Set.mem_of_mem_inter_right hz)
+
+  let s₂ : Set ℂ := { z | -f z ∈ Complex.slitPlane} ∩ s
+
+  have h₁' : DifferentiableOn ℂ (-f) s := by
+    rw [← differentiableOn_neg_iff]
+    simp
+    exact h₁
+
+  have hs₂ : IsOpen s₂ := by
+    let A := DifferentiableOn.continuousOn h₁'
+    let B := continuousOn_iff'.1 A
+    obtain ⟨u, hu₁, hu₂⟩ := B Complex.slitPlane Complex.isOpen_slitPlane
+    have : u ∩ s = s₂ := by
+      rw [← hu₂]
+      tauto
+    rw [← this]
+    apply IsOpen.inter hu₁ hs
+
+  have harm₂ : HarmonicOn (Real.log ∘ Complex.normSq ∘ (-f)) s₂ := by
+    apply log_normSq_of_holomorphicOn_is_harmonicOn'
+    exact hs₂
+    apply DifferentiableOn.mono h₁' (Set.inter_subset_right {z | -f z ∈ Complex.slitPlane} s)
+    -- ∀ z ∈ s₁, f z ≠ 0
+    intro z hz
+    simp
+    exact h₂ z (Set.mem_of_mem_inter_right hz)
+    -- ∀ z ∈ s₁, f z ∈ Complex.slitPlane
+    intro z hz
+    apply hz.1
+
+  apply HarmonicOn_of_locally_HarmonicOn
+  intro z hz
+  by_cases hfz : f z ∈ Complex.slitPlane
+  · use s₁
+    constructor
+    · exact hs₁
+    · constructor
+      · tauto
+      · have : s₁ = s ∩ s₁ := by
+          apply Set.right_eq_inter.mpr
+          exact Set.inter_subset_right {z | f z ∈ Complex.slitPlane} s
+        rw [← this]
+        exact harm₁
+  · use s₂
+    sorry
+
+
 theorem log_normSq_of_holomorphic_is_harmonic
   {f : ℂ → ℂ}
   (h₁ : Differentiable ℂ f)