From 9a7c8b82a4573e482b30a3cc0db12168ec074419 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Wed, 31 Jul 2024 15:59:43 +0200
Subject: [PATCH] working

---
 Nevanlinna/holomorphicAt.lean             | 15 ++++++++
 Nevanlinna/holomorphic_JensenFormula.lean | 44 ++++++++++++++++++++---
 2 files changed, 54 insertions(+), 5 deletions(-)

diff --git a/Nevanlinna/holomorphicAt.lean b/Nevanlinna/holomorphicAt.lean
index b7d7cdd..198c848 100644
--- a/Nevanlinna/holomorphicAt.lean
+++ b/Nevanlinna/holomorphicAt.lean
@@ -33,6 +33,21 @@ theorem HolomorphicAt_iff
     · assumption
 
 
+theorem Differentiable.holomorphicAt
+  {f : E → F}
+  (hf : Differentiable ℂ f)
+  {x : E} :
+  HolomorphicAt f x := by
+  apply HolomorphicAt_iff.2
+  use Set.univ
+  constructor
+  · exact isOpen_univ
+  · constructor
+    · exact trivial
+    · intro z _
+      exact hf z
+
+
 theorem HolomorphicAt_isOpen
   (f : E → F) :
   IsOpen { x : E | HolomorphicAt f x } := by
diff --git a/Nevanlinna/holomorphic_JensenFormula.lean b/Nevanlinna/holomorphic_JensenFormula.lean
index 33ccc26..7f30fd6 100644
--- a/Nevanlinna/holomorphic_JensenFormula.lean
+++ b/Nevanlinna/holomorphic_JensenFormula.lean
@@ -12,7 +12,7 @@ theorem jensen_case_R_eq_one
   (F : ℂ → ℂ)
   (h₁F : Differentiable ℂ F)
   (h₂F : ∀ z, F z ≠ 0)
-  (h₃F : f = fun z ↦ (F z) * ∑ s : S, (z - a s))
+  (h₃F : f = fun z ↦ (F z) * ∏ s : S, (z - a s))
   :
   Real.log ‖f 0‖ = -∑ s, Real.log (‖a s‖⁻¹) + (2 * Real.pi)⁻¹ * ∫ (x : ℝ) in (0)..2 * Real.pi, Real.log ‖f (circleMap 0 1 x)‖ := by
 
@@ -21,29 +21,63 @@ theorem jensen_case_R_eq_one
   have t₀ : ∀ z, HarmonicAt logAbsF z := by
     intro z
     apply logabs_of_holomorphicAt_is_harmonic
-    sorry
+    apply h₁F.holomorphicAt
     exact h₂F z
 
   have t₁ : (∫ (x : ℝ) in (0)..2 * Real.pi, logAbsF (circleMap 0 1 x)) = 2 * Real.pi * logAbsF 0 := by
     apply harmonic_meanValue t₀ 1
     exact Real.zero_lt_one
 
+  have t₂ : ∀ s, f (a s) = 0 := by
+    intro s
+    rw [h₃F]
+    simp
+    right
+    apply Finset.prod_eq_zero_iff.2
+    use s
+    simp
+
   let logAbsf := fun w ↦ Real.log ‖f w‖
   have s₀ : ∀ z, f z ≠ 0 → logAbsf z = logAbsF z + ∑ s, Real.log ‖z - a s‖ := by
-    sorry
+    intro z hz
+    dsimp [logAbsf]
+    rw [h₃F]
+    simp_rw [Complex.abs.map_mul]
+    rw [Complex.abs_prod]
+    rw [Real.log_mul]
+    rw [Real.log_prod]
+    rfl
+    intro s hs
+    simp
+    by_contra ha'
+    rw [ha'] at hz
+    exact hz (t₂ s)
+    -- Complex.abs (F z) ≠ 0
+    simp
+    exact h₂F z
+    -- ∏ I : { x // x ∈ S }, Complex.abs (z - a I) ≠ 0
+    by_contra h'
+    obtain ⟨s, h's, h''⟩ := Finset.prod_eq_zero_iff.1 h'
+    simp at h''
+    rw [h''] at hz
+    let A := t₂ s
+    exact hz A
+
   have s₁ : ∀ z, f z ≠ 0 → logAbsF z = logAbsf z - ∑ s, Real.log ‖z - a s‖ := by
     sorry
 
   rw [s₁ 0 h₂f] at t₁
 
-  have {x : ℝ} : f (circleMap 0 1 x) ≠ 0 := by sorry
+  have {x : ℝ} : f (circleMap 0 1 x) ≠ 0 := by
+    sorry
+
   simp_rw [s₁ (circleMap 0 1 _) this] at t₁
   rw [intervalIntegral.integral_sub] at t₁
   rw [intervalIntegral.integral_finset_sum] at t₁
 
   have {i : S} : ∫ (x : ℝ) in (0)..2 * Real.pi, Real.log ‖circleMap 0 1 x - a i‖ = 0 := by
-
     sorry
+
   simp_rw [this] at t₁
   simp at t₁
   rw [t₁]