Update complexHarmonic.lean

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)) :