From 05582e5d8321c25d4cbba93d2d3669fb14177ba3 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Wed, 5 Jun 2024 09:51:02 +0200
Subject: [PATCH] Update complexHarmonic.lean

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

diff --git a/Nevanlinna/complexHarmonic.lean b/Nevanlinna/complexHarmonic.lean
index 26de608..c5c2224 100644
--- a/Nevanlinna/complexHarmonic.lean
+++ b/Nevanlinna/complexHarmonic.lean
@@ -25,10 +25,42 @@ variable {G₁ : Type*} [NormedAddCommGroup G₁] [NormedSpace ℂ G₁] [Comple
 def Harmonic (f : ℂ → F) : Prop :=
   (ContDiff ℝ 2 f) ∧ (∀ z, Δ f z = 0)
 
+def HarmonicAt (f : ℂ → F) (x : ℂ) : Prop :=
+  (ContDiffAt ℝ 2 f x) ∧ (Δ f =ᶠ[nhds x] 0)
 
 def HarmonicOn (f : ℂ → F) (s : Set ℂ) : Prop :=
   (ContDiffOn ℝ 2 f s) ∧ (∀ z ∈ s, Δ f z = 0)
 
+theorem HarmonicAt_iff
+  {f : ℂ → F}
+  {x : ℂ} :
+  HarmonicAt f x ↔ ∃ s : Set ℂ, IsOpen s ∧ x ∈ s ∧ (ContDiffOn ℝ 2 f s) ∧ (∀ z ∈ s, Δ f z = 0) := by
+  constructor
+  · intro hf
+    obtain ⟨s₁, h₁s₁, h₂s₁, h₃s₁⟩ := hf.1.contDiffOn' le_rfl
+    simp at h₃s₁
+    obtain ⟨t₂, h₁t₂, h₂t₂⟩ := (Filter.eventuallyEq_iff_exists_mem.1 hf.2)
+    obtain ⟨s₂, h₁s₂, h₂s₂, h₃s₂⟩ := mem_nhds_iff.1 h₁t₂
+    let s := s₁ ∩ s₂
+    use s
+    constructor
+    · exact IsOpen.inter h₁s₁ h₂s₂
+    · constructor
+      · exact Set.mem_inter h₂s₁ h₃s₂
+      · constructor
+        · exact h₃s₁.mono (Set.inter_subset_left s₁ s₂)
+        · intro z hz
+          exact h₂t₂ (h₁s₂ hz.2)
+  · intro hyp
+    obtain ⟨s, h₁s, h₂s, h₁f, h₂f⟩ := hyp
+    constructor
+    · apply h₁f.contDiffAt
+      apply (IsOpen.mem_nhds_iff h₁s).2 h₂s
+    · apply Filter.eventuallyEq_iff_exists_mem.2
+      use s
+      constructor
+      · apply (IsOpen.mem_nhds_iff h₁s).2 h₂s
+      · exact h₂f
 
 
 theorem HarmonicOn_of_locally_HarmonicOn {f : ℂ → F} {s : Set ℂ} (h : ∀ x ∈ s, ∃ (u : Set ℂ), IsOpen u ∧ x ∈ u ∧ HarmonicOn f (s ∩ u)) :