From 42a6c439a9baa757c4556bb3bac4daf366f3ca81 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Thu, 22 Aug 2024 14:52:52 +0200
Subject: [PATCH] Update holomorphic_JensenFormula2.lean

---
 Nevanlinna/holomorphic_JensenFormula2.lean | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/Nevanlinna/holomorphic_JensenFormula2.lean b/Nevanlinna/holomorphic_JensenFormula2.lean
index 96aa242..6402001 100644
--- a/Nevanlinna/holomorphic_JensenFormula2.lean
+++ b/Nevanlinna/holomorphic_JensenFormula2.lean
@@ -8,6 +8,14 @@ import Nevanlinna.specialFunctions_CircleIntegral_affine
 open Real
 
 
+noncomputable def Zeroset
+  {f : ℂ → ℂ}
+  {s : Set ℂ}
+  (hf : ∀ z ∈ s, HolomorphicAt f z) :
+  Set ℂ := by
+  exact f⁻¹' {0} ∩ s
+
+
 noncomputable def ZeroFinset
   {f : ℂ → ℂ}
   (h₁f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt f z)
@@ -272,7 +280,9 @@ theorem jensen_case_R_eq_one
   simp_rw [← Complex.norm_eq_abs] at this
   rw [t₁] at this
 
+  --let Z₁ := (ZeroFinset h₁f h₂f) ∩ (Metric.ball 0 1)
 
+  let Z₂ := { x : ZeroFinset h₁f h₂f | ‖x.1‖ = 1 }
 
 
   sorry