From f65c84a14bee23f3944efcd2a6366e1f1e7e99da Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Thu, 1 Aug 2024 10:02:36 +0200
Subject: [PATCH] =?UTF-8?q?working=E2=80=A6?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Nevanlinna/holomorphic_JensenFormula.lean | 40 ++++++++++++++++-------
 lake-manifest.json                        | 16 ++++-----
 lean-toolchain                            |  2 +-
 3 files changed, 38 insertions(+), 20 deletions(-)

diff --git a/Nevanlinna/holomorphic_JensenFormula.lean b/Nevanlinna/holomorphic_JensenFormula.lean
index 7f30fd6..11dddf1 100644
--- a/Nevanlinna/holomorphic_JensenFormula.lean
+++ b/Nevanlinna/holomorphic_JensenFormula.lean
@@ -1,6 +1,13 @@
 import Nevanlinna.harmonicAt_examples
 import Nevanlinna.harmonicAt_meanValue
 
+lemma int₀
+  {a : ℂ}
+  (ha : a ∈ Metric.ball 0 1)
+  :
+  ∫ (x : ℝ) in (0)..2 * Real.pi, Real.log ‖circleMap 0 1 x - a‖ = 0 := by
+    sorry
+
 
 theorem jensen_case_R_eq_one
   (f : ℂ → ℂ)
@@ -64,21 +71,32 @@ theorem jensen_case_R_eq_one
     exact hz A
 
   have s₁ : ∀ z, f z ≠ 0 → logAbsF z = logAbsf z - ∑ s, Real.log ‖z - a s‖ := by
-    sorry
+    intro z hz
+    rw [s₀ z hz]
+    simp
 
   rw [s₁ 0 h₂f] at t₁
 
-  have {x : ℝ} : f (circleMap 0 1 x) ≠ 0 := by
-    sorry
+  have h₀ {x : ℝ} : f (circleMap 0 1 x) ≠ 0 := by
+    rw [h₃F]
+    simp
+    constructor
+    · exact h₂F (circleMap 0 1 x)
+    · by_contra h'
+      obtain ⟨s, _, h₂s⟩  := Finset.prod_eq_zero_iff.1 h'
+      have : circleMap 0 1 x = a s := by
+        rw [← sub_zero (circleMap 0 1 x)]
+        nth_rw 2 [← h₂s]
+        simp
+      let A := ha s
+      rw [← this] at A
+      simp at A
 
-  simp_rw [s₁ (circleMap 0 1 _) this] at t₁
+  simp_rw [s₁ (circleMap 0 1 _) h₀] 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_rw [int₀ (ha _)] at t₁
   simp at t₁
   rw [t₁]
   simp
@@ -89,7 +107,7 @@ theorem jensen_case_R_eq_one
   simp
   rfl
   -- ∀ i ∈ Finset.univ, IntervalIntegrable (fun x => Real.log ‖circleMap 0 1 x - a i‖) MeasureTheory.volume 0 (2 * Real.pi)
-  intro i hi
+  intro i _
   apply Continuous.intervalIntegrable
   apply continuous_iff_continuousAt.2
   intro x
@@ -115,7 +133,7 @@ theorem jensen_case_R_eq_one
   rw [this]
   apply ContinuousAt.comp
   simp
-  sorry
+  exact h₀
   apply ContinuousAt.comp
   apply Complex.continuous_abs.continuousAt
   apply ContinuousAt.comp
@@ -125,7 +143,7 @@ theorem jensen_case_R_eq_one
   -- IntervalIntegrable (fun x => ∑ s : { x // x ∈ S }, Real.log ‖circleMap 0 1 x - a s‖) MeasureTheory.volume 0 (2 * Real.pi)
   apply Continuous.intervalIntegrable
   apply continuous_finset_sum
-  intro i hi
+  intro i _
   apply continuous_iff_continuousAt.2
   intro x
   have : (fun x => Real.log ‖circleMap 0 1 x - a i‖) = Real.log ∘ Complex.abs ∘ (fun x ↦ circleMap 0 1 x - a i) :=
diff --git a/lake-manifest.json b/lake-manifest.json
index 7830064..85499dc 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d2b1546c5fc05a06426e3f6ee1cb020e71be5592",
+   "rev": "0f3e143dffdc3a591662f3401ce1d7a3405227c0",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "622d52c803db99ff4ea4fb442c1db9e91aed944c",
+   "rev": "209712c78b16c795453b6da7f7adbda4589a8f21",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -35,27 +35,27 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d1b33202c3a29a079f292de65ea438648123b635",
+   "rev": "c87908619cccadda23f71262e6898b9893bffa36",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.39",
+   "inputRev": "v0.0.40",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29",
+   "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/import-graph",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "68b518c9b352fbee16e6d632adcb7a6d0760e2b7",
+   "rev": "e7e90d90a62e6d12cbb27cbbfc31c094ee4ecc58",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "cc495260156b40dcbd55b947c047061e15344000",
+   "rev": "c96401c7496392a2200dc78c0b334df0561466dc",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
diff --git a/lean-toolchain b/lean-toolchain
index 6a4259f..7f0ea50 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.10.0-rc2
+leanprover/lean4:v4.10.0