From 47e1bfe35e125371105e091cef5da7ec9662f712 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Wed, 11 Sep 2024 11:06:45 +0200
Subject: [PATCH] working

---
 Nevanlinna/holomorphic_JensenFormula2.lean    | 11 +++--------
 ...pecialFunctions_CircleIntegral_affine.lean | 19 ++++++++++++++-----
 2 files changed, 17 insertions(+), 13 deletions(-)

diff --git a/Nevanlinna/holomorphic_JensenFormula2.lean b/Nevanlinna/holomorphic_JensenFormula2.lean
index b33433b..3030ca6 100644
--- a/Nevanlinna/holomorphic_JensenFormula2.lean
+++ b/Nevanlinna/holomorphic_JensenFormula2.lean
@@ -16,7 +16,6 @@ lemma h₂U : IsCompact (Metric.closedBall (0 : ℂ) 1) :=
 
 theorem jensen_case_R_eq_one
   (f : ℂ → ℂ)
-  (h₁f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt f z)
   (h'₁f : AnalyticOn ℂ f (Metric.closedBall (0 : ℂ) 1))
   (h₂f : f 0 ≠ 0) :
   log ‖f 0‖ = -∑ᶠ s, (h'₁f.order s).toNat * log (‖s.1‖⁻¹) + (2 * π)⁻¹ * ∫ (x : ℝ) in (0)..(2 * π), log ‖f (circleMap 0 1 x)‖ := by
@@ -116,10 +115,6 @@ theorem jensen_case_R_eq_one
     exact Ne.symm (zero_ne_one' ℝ)
 
 
-  have h₁Gi : ∀ i ∈ (finiteZeros h₁U h₂U h'₁f h'₂f).toFinset, 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 decompose_int_G : ∫ (x : ℝ) in (0)..2 * π, G (circleMap 0 1 x)
     = (∫ (x : ℝ) in (0)..2 * π, log (Complex.abs (F (circleMap 0 1 x))))
         + ∑ x ∈ (finiteZeros h₁U h₂U h'₁f h'₂f).toFinset, (h'₁f.order x).toNat * ∫ (x_1 : ℝ) in (0)..2 * π, log (Complex.abs (circleMap 0 1 x_1 - ↑x)) := by
@@ -131,7 +126,7 @@ theorem jensen_case_R_eq_one
     --  ∀ i ∈ (finiteZeros h₁U h₂U h'₁f h'₂f).toFinset,
     --  IntervalIntegrable (fun x => (h'₁f.order i).toNat *
     --    log (Complex.abs (circleMap 0 1 x - ↑i))) MeasureTheory.volume 0 (2 * π)
-    intro i hi
+    intro i _
     apply IntervalIntegrable.const_mul
     --simp at this
     by_cases h₂i : ‖i.1‖ = 1
@@ -186,7 +181,7 @@ theorem jensen_case_R_eq_one
       simp
     rw [this]
     apply IntervalIntegrable.sum
-    intro i h₂i
+    intro i _
     apply IntervalIntegrable.const_mul
     --have : i.1 ∈ Metric.closedBall (0 : ℂ) 1 := i.2
     --simp at this
@@ -260,7 +255,7 @@ theorem jensen_case_R_eq_one
   rw [finsum_eq_sum_of_support_subset _ (s := (finiteZeros h₁U h₂U h'₁f h'₂f).toFinset)]
   simp
   simp
-  intro x ⟨h₁x, h₂x⟩
+  intro x ⟨h₁x, _⟩
   simp
 
   dsimp [AnalyticOn.order] at h₁x
diff --git a/Nevanlinna/specialFunctions_CircleIntegral_affine.lean b/Nevanlinna/specialFunctions_CircleIntegral_affine.lean
index 09160fc..0f87b49 100644
--- a/Nevanlinna/specialFunctions_CircleIntegral_affine.lean
+++ b/Nevanlinna/specialFunctions_CircleIntegral_affine.lean
@@ -8,10 +8,6 @@ import Nevanlinna.periodic_integrability
 open scoped Interval Topology
 open Real Filter MeasureTheory intervalIntegral
 
--- Integrability of periodic functions
-
-
-
 
 
 -- Lemmas for the circleMap
@@ -46,6 +42,20 @@ lemma l₂ {x : ℝ} : ‖(circleMap 0 1 x) - a‖ = ‖1 - (circleMap 0 1 (-x))
 
 -- Integral of log ‖circleMap 0 1 x - a‖, for ‖a‖ < 1.
 
+lemma int'₀
+  {a : ℂ}
+  (ha : a ∈ Metric.ball 0 1) :
+  IntervalIntegrable (fun x ↦ log ‖circleMap 0 1 x - a‖) volume 0 (2 * π) := by
+  apply Continuous.intervalIntegrable
+  apply Continuous.log
+  fun_prop
+  simp
+  intro x
+  by_contra h₁a
+  rw [← h₁a] at ha
+  simp at ha
+
+
 lemma int₀
   {a : ℂ}
   (ha : a ∈ Metric.ball 0 1) :
@@ -210,7 +220,6 @@ lemma int''₁ : -- Integrability of log ‖circleMap 0 1 x - 1‖ for arbitrary
   rw [zero_add]
   exact int'₁
 
-
 lemma int₁ :
   ∫ x in (0)..(2 * π), log ‖circleMap 0 1 x - 1‖ = 0 := by