From eb4c9da6b58505cef7a7c3c2ff06b222c2a12ff8 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Wed, 31 Jul 2024 14:54:41 +0200
Subject: [PATCH] working

---
 Nevanlinna/holomorphic_JensenFormula.lean | 108 ++++++++++++++++++++++
 1 file changed, 108 insertions(+)
 create mode 100644 Nevanlinna/holomorphic_JensenFormula.lean

diff --git a/Nevanlinna/holomorphic_JensenFormula.lean b/Nevanlinna/holomorphic_JensenFormula.lean
new file mode 100644
index 0000000..e138191
--- /dev/null
+++ b/Nevanlinna/holomorphic_JensenFormula.lean
@@ -0,0 +1,108 @@
+import Nevanlinna.harmonicAt_examples
+import Nevanlinna.harmonicAt_meanValue
+
+
+theorem jensen_case_R_eq_one
+  (f : ℂ → ℂ)
+  (h₁f : Differentiable ℂ f)
+  (h₂f : f 0 ≠ 0)
+  (S : Finset ℕ)
+  (a : S → ℂ)
+  (ha : ∀ s, a s ∈ Metric.ball 0 1)
+  (F : ℂ → ℂ)
+  (h₁F : Differentiable ℂ F)
+  (h₂F : ∀ z, F z ≠ 0)
+  (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
+
+  let logAbsF := fun w ↦ Real.log ‖F w‖
+
+  have t₀ : ∀ z, HarmonicAt logAbsF z := by
+    intro z
+    apply logabs_of_holomorphicAt_is_harmonic
+    sorry
+    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
+
+  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
+  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
+  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₁]
+  simp
+  have : Real.pi⁻¹ * 2⁻¹ * (2 * Real.pi * (logAbsf 0 - ∑ x ∈ S.attach, Real.log (Complex.abs (a x)))) = logAbsf 0 - ∑ x ∈ S.attach, Real.log (Complex.abs (a x)) := by
+    sorry
+  rw [this]
+  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
+  apply Continuous.intervalIntegrable
+  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) :=
+    rfl
+  rw [this]
+  apply ContinuousAt.comp
+  apply Real.continuousAt_log
+  simp
+  by_contra ha'
+  let A := ha i
+  rw [← ha'] at A
+  simp at A
+  apply ContinuousAt.comp
+  apply Complex.continuous_abs.continuousAt
+  fun_prop
+  -- IntervalIntegrable (fun x => logAbsf (circleMap 0 1 x)) MeasureTheory.volume 0 (2 * Real.pi)
+  apply Continuous.intervalIntegrable
+  apply continuous_iff_continuousAt.2
+  intro x
+  have : (fun x => logAbsf (circleMap 0 1 x)) = Real.log ∘ Complex.abs ∘ f ∘ (fun x ↦ circleMap 0 1 x) :=
+    rfl
+  rw [this]
+  apply ContinuousAt.comp
+  simp
+  sorry
+  apply ContinuousAt.comp
+  apply Complex.continuous_abs.continuousAt
+  apply ContinuousAt.comp
+  apply h₁f.continuous.continuousAt
+  let A := continuous_circleMap 0 1
+  apply A.continuousAt
+  -- 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
+  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) :=
+    rfl
+  rw [this]
+  apply ContinuousAt.comp
+  apply Real.continuousAt_log
+  simp
+  by_contra ha'
+  let A := ha i
+  rw [← ha'] at A
+  simp at A
+  apply ContinuousAt.comp
+  apply Complex.continuous_abs.continuousAt
+  fun_prop