diff --git a/Nevanlinna/holomorphic.lean b/Nevanlinna/holomorphic.lean
index eed131c..58f76d5 100644
--- a/Nevanlinna/holomorphic.lean
+++ b/Nevanlinna/holomorphic.lean
@@ -33,6 +33,20 @@ theorem HolomorphicAt_iff
     · assumption
 
 
+theorem HolomorphicAt_analyticAt
+  {f : ℂ → F}
+  {x : ℂ} :
+  HolomorphicAt f x → AnalyticAt ℂ f x := by
+  intro hf
+  obtain ⟨s, h₁s, h₂s, h₃s⟩ := HolomorphicAt_iff.1 hf
+  apply DifferentiableOn.analyticAt (s := s)
+  intro z hz
+  apply DifferentiableAt.differentiableWithinAt
+  apply h₃s
+  exact hz
+  exact IsOpen.mem_nhds h₁s h₂s
+
+
 theorem HolomorphicAt_differentiableAt
   {f : E → F}
   {x : E} :
diff --git a/Nevanlinna/holomorphicAt.lean b/Nevanlinna/holomorphicAt.lean
index 198c848..fe77785 100644
--- a/Nevanlinna/holomorphicAt.lean
+++ b/Nevanlinna/holomorphicAt.lean
@@ -1,4 +1,5 @@
-import Mathlib.Analysis.Complex.TaylorSeries
+import Mathlib.Analysis.Complex.CauchyIntegral
+--import Mathlib.Analysis.Complex.TaylorSeries
 import Nevanlinna.cauchyRiemann
 
 variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]
@@ -110,6 +111,21 @@ theorem HolomorphicAt_neg
     exact h₂UF z hz
 
 
+theorem HolomorphicAt.analyticAt
+  [CompleteSpace F]
+  {f : ℂ → F}
+  {x : ℂ} :
+  HolomorphicAt f x → AnalyticAt ℂ f x := by
+  intro hf
+  obtain ⟨s, h₁s, h₂s, h₃s⟩ := HolomorphicAt_iff.1 hf
+  apply DifferentiableOn.analyticAt (s := s)
+  intro z hz
+  apply DifferentiableAt.differentiableWithinAt
+  apply h₃s
+  exact hz
+  exact IsOpen.mem_nhds h₁s h₂s
+
+
 theorem HolomorphicAt.contDiffAt
   [CompleteSpace F]
   {f : ℂ → F}
diff --git a/Nevanlinna/holomorphic_JensenFormula2.lean b/Nevanlinna/holomorphic_JensenFormula2.lean
index 59c7a60..96aa242 100644
--- a/Nevanlinna/holomorphic_JensenFormula2.lean
+++ b/Nevanlinna/holomorphic_JensenFormula2.lean
@@ -8,28 +8,63 @@ import Nevanlinna.specialFunctions_CircleIntegral_affine
 open Real
 
 
-def ZeroFinset
+noncomputable def ZeroFinset
   {f : ℂ → ℂ}
-  (h₁f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt f z) :
+  (h₁f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt f z)
+  (h₂f : f 0 ≠ 0) :
   Finset ℂ := by
 
   let Z := f⁻¹' {0} ∩ Metric.closedBall (0 : ℂ) 1
-  have hZ : Set.Finite Z := by sorry
+  have hZ : Set.Finite Z := by
+    dsimp [Z]
+    rw [Set.inter_comm]
+    apply finiteZeros
+    -- Ball is preconnected
+    apply IsConnected.isPreconnected
+    apply Convex.isConnected
+    exact convex_closedBall 0 1
+    exact Set.nonempty_of_nonempty_subtype
+    --
+    exact isCompact_closedBall 0 1
+    --
+    intro x hx
+    have A := (h₁f x hx)
+    let B := HolomorphicAt_iff.1 A
+    obtain ⟨s, h₁s, h₂s, h₃s⟩ := B
+    apply DifferentiableOn.analyticAt (s := s)
+    intro z hz
+    apply DifferentiableAt.differentiableWithinAt
+    apply h₃s
+    exact hz
+    exact IsOpen.mem_nhds h₁s h₂s
+    --
+    use 0
+    constructor
+    · simp
+    · exact h₂f
   exact hZ.toFinset
 
 
-def order
-  {f : ℂ → ℂ}
-  {hf : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt f z} :
-  ZeroFinset hf → ℕ := by sorry
-
-
 lemma ZeroFinset_mem_iff
   {f : ℂ → ℂ}
-  (hf : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt f z)
+  (h₁f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt f z)
+  {h₂f : f 0 ≠ 0}
   (z : ℂ) :
-  z ∈ ↑(ZeroFinset hf) ↔ z ∈ Metric.closedBall 0 1 ∧ f z = 0 := by
-  sorry
+  z ∈ ↑(ZeroFinset h₁f h₂f) ↔ z ∈ Metric.closedBall 0 1 ∧ f z = 0 := by
+  dsimp [ZeroFinset]; simp
+  tauto
+
+
+noncomputable def order
+  {f : ℂ → ℂ}
+  {h₁f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt f z}
+  {h₂f : f 0 ≠ 0} :
+  ZeroFinset h₁f h₂f → ℕ := by
+  intro i
+  let A := ((ZeroFinset_mem_iff h₁f i).1 i.2).1
+  let B := (h₁f i.1 A).analyticAt
+  exact B.order.toNat
+
 
 
 theorem jensen_case_R_eq_one
@@ -37,14 +72,14 @@ theorem jensen_case_R_eq_one
   (h₁f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt f z)
   (h'₁f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, AnalyticAt ℂ f z)
   (h₂f : f 0 ≠ 0) :
-  log ‖f 0‖ = -∑ s : ZeroFinset h₁f, order s * log (‖s.1‖⁻¹) + (2 * π )⁻¹ * ∫ (x : ℝ) in (0)..2 * π, log ‖f (circleMap 0 1 x)‖ := by
+  log ‖f 0‖ = -∑ s : (ZeroFinset h₁f h₂f), order s * log (‖s.1‖⁻¹) + (2 * π )⁻¹ * ∫ (x : ℝ) in (0)..2 * π, log ‖f (circleMap 0 1 x)‖ := by
 
   have F : ℂ → ℂ := by sorry
   have h₁F : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt F z := by sorry
   have h₂F : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, F z ≠ 0 := by sorry
-  have h₃F : f = fun z ↦ (F z) * ∏ s : ZeroFinset h₁f, (z - s) ^ (order s) := by sorry
+  have h₃F : f = fun z ↦ (F z) * ∏ s : ZeroFinset h₁f h₂f, (z - s) ^ (order s) := by sorry
 
-  let G := fun z ↦ log ‖F z‖ + ∑ s : ZeroFinset h₁f, (order s) * log ‖z - s‖
+  let G := fun z ↦ log ‖F z‖ + ∑ s : ZeroFinset h₁f h₂f, (order s) * log ‖z - s‖
 
   have decompose_f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, f z ≠ 0 → log ‖f z‖ = G z := by
     intro z h₁z h₂z
@@ -123,11 +158,11 @@ theorem jensen_case_R_eq_one
     exact ⟨Metric.mem_closedBall_self (zero_le_one' ℝ), h₂f⟩
     exact Ne.symm (zero_ne_one' ℝ)
 
-  have h₁Gi : ∀ i ∈ (ZeroFinset h₁f).attach, IntervalIntegrable (fun x => log (Complex.abs (circleMap 0 1 x - ↑i))) MeasureTheory.volume 0 (2 * π) := by
+  have h₁Gi : ∀ i ∈ (ZeroFinset h₁f h₂f).attach, IntervalIntegrable (fun x => log (Complex.abs (circleMap 0 1 x - ↑i))) MeasureTheory.volume 0 (2 * π) := by
     -- This is hard. Need to invoke specialFunctions_CircleIntegral_affine.
     sorry
 
-  have : ∫ (x : ℝ) in (0)..2 * π, G (circleMap 0 1 x) = (∫ (x : ℝ) in (0)..2 * π, log (Complex.abs (F (circleMap 0 1 x)))) + ∑ x ∈ (ZeroFinset h₁f).attach, ↑(order x) * ∫ (x_1 : ℝ) in (0)..2 * π, log (Complex.abs (circleMap 0 1 x_1 - ↑x)) := by
+  have : ∫ (x : ℝ) in (0)..2 * π, G (circleMap 0 1 x) = (∫ (x : ℝ) in (0)..2 * π, log (Complex.abs (F (circleMap 0 1 x)))) + ∑ x ∈ (ZeroFinset h₁f h₂f).attach, ↑(order x) * ∫ (x_1 : ℝ) in (0)..2 * π, log (Complex.abs (circleMap 0 1 x_1 - ↑x)) := by
     dsimp [G]
     rw [intervalIntegral.integral_add]
     rw [intervalIntegral.integral_finset_sum]
@@ -188,8 +223,8 @@ theorem jensen_case_R_eq_one
     apply Continuous.continuousAt
     apply continuous_circleMap
     --
-    have : (fun x => ∑ s ∈ (ZeroFinset h₁f).attach, ↑(order s) * log (Complex.abs (circleMap 0 1 x - ↑s)))
-      = ∑ s ∈ (ZeroFinset h₁f).attach, (fun x => ↑(order s) * log (Complex.abs (circleMap 0 1 x - ↑s))) := by
+    have : (fun x => ∑ s ∈ (ZeroFinset h₁f h₂f).attach, ↑(order s) * log (Complex.abs (circleMap 0 1 x - ↑s)))
+      = ∑ s ∈ (ZeroFinset h₁f h₂f).attach, (fun x => ↑(order s) * log (Complex.abs (circleMap 0 1 x - ↑s))) := by
       funext x
       simp
     rw [this]
@@ -225,5 +260,19 @@ theorem jensen_case_R_eq_one
     apply Complex.continuous_abs.continuousAt
     fun_prop
 
+  have t₁ : (∫ (x : ℝ) in (0)..2 * Real.pi, log ‖F (circleMap 0 1 x)‖) = 2 * Real.pi * log ‖F 0‖ := by
+    let logAbsF := fun w ↦ Real.log ‖F w‖
+    have t₀ : ∀ z ∈ Metric.closedBall 0 1, HarmonicAt logAbsF z := by
+      intro z hz
+      apply logabs_of_holomorphicAt_is_harmonic
+      apply h₁F z hz
+      exact h₂F z hz
+
+    apply harmonic_meanValue₁ 1 Real.zero_lt_one t₀
+  simp_rw [← Complex.norm_eq_abs] at this
+  rw [t₁] at this
+
+
+
 
   sorry