From 5a984253c6e382a2b3bdeb49fbefdc2693889d33 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Thu, 12 Sep 2024 07:52:26 +0200
Subject: [PATCH] Update holomorphic_JensenFormula2.lean

---
 Nevanlinna/holomorphic_JensenFormula2.lean | 49 +++++++++++++++++++---
 1 file changed, 43 insertions(+), 6 deletions(-)

diff --git a/Nevanlinna/holomorphic_JensenFormula2.lean b/Nevanlinna/holomorphic_JensenFormula2.lean
index e1601e9..aa9c7ea 100644
--- a/Nevanlinna/holomorphic_JensenFormula2.lean
+++ b/Nevanlinna/holomorphic_JensenFormula2.lean
@@ -301,25 +301,62 @@ theorem jensen
   (h₂f : f 0 ≠ 0) :
   log ‖f 0‖ = -∑ᶠ s, (h₁f.order s).toNat * log (R * ‖s.1‖⁻¹) + (2 * π)⁻¹ * ∫ (x : ℝ) in (0)..(2 * π), log ‖f (circleMap 0 R x)‖ := by
 
-  let F := fun z ↦ f (R • z)
+
+  let ℓ : ℂ ≃L[ℂ] ℂ :=
+  {
+    toFun := fun x ↦ R * x
+    map_add' := fun x y => DistribSMul.smul_add R x y
+    map_smul' := fun m x => mul_smul_comm m (↑R) x
+    invFun := fun x ↦ R⁻¹ * x
+    left_inv := by
+      intro x
+      simp
+      rw [← mul_assoc, mul_comm, inv_mul_cancel₀, mul_one]
+      simp
+      exact ne_of_gt hR
+    right_inv := by
+      intro x
+      simp
+      rw [← mul_assoc, mul_inv_cancel₀, one_mul]
+      simp
+      exact ne_of_gt hR
+    continuous_toFun := continuous_const_smul R
+    continuous_invFun := continuous_const_smul R⁻¹
+  }
 
 
+  let F := f ∘ ℓ
 
   have h₁F : AnalyticOn ℂ F (Metric.closedBall 0 1) := by
     apply AnalyticOn.comp (t := Metric.closedBall 0 R)
     exact h₁f
+    intro x _
+    apply ℓ.toContinuousLinearMap.analyticAt x
 
+    intro x hx
+    have : ℓ x = R * x := by rfl
+    rw [this]
+    simp
+    simp at hx
+    rw [abs_of_pos hR]
+    calc R * Complex.abs x
+    _ ≤ R * 1 := by exact (mul_le_mul_iff_of_pos_left hR).mpr hx
+    _ = R := by simp
 
-
-    sorry
-  have h₂F : F 0 ≠ 0 := by sorry
+  have h₂F : F 0 ≠ 0 := by
+    dsimp [F]
+    have : ℓ 0 = R * 0 := by rfl
+    rw [this]
+    simpa
 
   let A := jensen_case_R_eq_one F h₁F h₂F
   dsimp [F] at A
+  have {x : ℂ} : ℓ x = R * x := by rfl
+  repeat
+    simp_rw [this] at A
+  simp at A
   simp
-  rw [mul_zero] at A
   rw [A]
-  simp
 
   simp_rw [← const_mul_circleMap_zero]
   simp