From 4b6cdcc76a1e81eae06c24fcbcc3164f5e4b80ff Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Thu, 8 Aug 2024 15:04:41 +0200
Subject: [PATCH] Update harmonicAt_meanValue.lean

---
 Nevanlinna/harmonicAt_meanValue.lean | 35 +++++++++++++++++++++-------
 1 file changed, 27 insertions(+), 8 deletions(-)

diff --git a/Nevanlinna/harmonicAt_meanValue.lean b/Nevanlinna/harmonicAt_meanValue.lean
index 7b4f2cf..88c0bd1 100644
--- a/Nevanlinna/harmonicAt_meanValue.lean
+++ b/Nevanlinna/harmonicAt_meanValue.lean
@@ -65,24 +65,43 @@ theorem harmonic_meanValue
     apply inv_mul_cancel
     apply circleMap_ne_center
     exact Ne.symm (ne_of_lt hR)
-  simp_rw [t₁] at this
+  have t'₁  {θ : ℝ} : circleMap 0 R θ = circleMap z R θ - z := by
+    exact Eq.symm (circleMap_sub_center z R θ)
+  simp_rw [← t'₁, t₁] at this
   simp at this
 
-  have t₂ : Complex.reCLM (-Complex.I * (Complex.I * ∫ (x : ℝ) in (0)..2 * Real.pi, F (circleMap 0 R x))) = Complex.reCLM (-Complex.I * (2 * ↑Real.pi * Complex.I * F 0)) := by
+  have t₂ : Complex.reCLM (-Complex.I * (Complex.I * ∫ (x : ℝ) in (0)..2 * Real.pi, F (circleMap z R x))) = Complex.reCLM (-Complex.I * (2 * ↑Real.pi * Complex.I * F z)) := by
     rw [this]
   simp at t₂
-  have xx {z : ℂ} : (F z).re = f z := by
+  have xx {x : ℝ} : (F (circleMap z R x)).re = f (circleMap z R x) := by
     rw [← h₂F]
     simp
-  simp_rw [xx] at t₂
+    simp
+    rw [Complex.dist_eq]
+    rw [circleMap_sub_center]
+    simp
+    rwa [abs_of_nonneg (le_of_lt hR)]
   have x₁ {z : ℂ} : z.re = Complex.reCLM z := by rfl
   rw [x₁] at t₂
   rw [← ContinuousLinearMap.intervalIntegral_comp_comm] at t₂
   simp at t₂
   simp_rw [xx] at t₂
+  have x₁ {z : ℂ} : z.re = Complex.reCLM z := by rfl
+  rw [x₁] at t₂
+  have : Complex.reCLM (F z) = f z := by
+    apply h₂F
+    simp
+    exact gt_trans hρ hR
+  rw [this] at t₂
   exact t₂
+
   -- IntervalIntegrable (fun x => F (circleMap 0 1 x)) MeasureTheory.volume 0 (2 * Real.pi)
-  apply Continuous.intervalIntegrable
-  apply Continuous.comp
-  exact regF.continuous
-  exact continuous_circleMap 0 R
+  apply ContinuousOn.intervalIntegrable
+  apply ContinuousOn.comp reg₀F.continuousOn _
+  intro θ _
+  simp
+  rw [Complex.dist_eq, circleMap_sub_center]
+  simp
+  rwa [abs_of_nonneg (le_of_lt hR)]
+  apply Continuous.continuousOn
+  exact continuous_circleMap z R