Update holomorphic_JensenFormula.lean

Nevanlinna/holomorphic_JensenFormula.lean

@@ -5,31 +5,27 @@ import Nevanlinna.specialFunctions_CircleIntegral_affine
 
 theorem jensen_case_R_eq_one
   (f : ℂ → ℂ)
-  (h₁f : Differentiable ℂ f)
+  (h₁f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt f z)
   (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))
-  :
+  (h₁F : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt F z)
+  (h₂F : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, 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 ∈ Metric.ball 0 2, HarmonicAt logAbsF z := by
-    intro z _
+  have t₀ : ∀ z ∈ Metric.closedBall 0 1, HarmonicAt logAbsF z := by
+    intro z hz
     apply logabs_of_holomorphicAt_is_harmonic
-    apply h₁F.holomorphicAt
-    exact h₂F z
+    apply h₁F z hz
+    exact h₂F z hz
 
   have t₁ : (∫ (x : ℝ) in (0)..2 * Real.pi, logAbsF (circleMap 0 1 x)) = 2 * Real.pi * logAbsF 0 := by
-    have hR : (0 : ℝ) < (1 : ℝ) := by apply Real.zero_lt_one
-    have hρ : (1 : ℝ) < (2 : ℝ) := by linarith
-    apply harmonic_meanValue 2 1 hR hρ t₀
-
+    apply harmonic_meanValue₁ 1 Real.zero_lt_one t₀
 
   have t₂ : ∀ s, f (a s) = 0 := by
     intro s
@@ -41,8 +37,8 @@ theorem jensen_case_R_eq_one
     simp
 
   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
-    intro z hz
+  have s₀ : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, f z ≠ 0 → logAbsf z = logAbsF z + ∑ s, Real.log ‖z - a s‖ := by
+    intro z h₁z h₂z
     dsimp [logAbsf]
     rw [h₃F]
     simp_rw [Complex.abs.map_mul]
@@ -53,31 +49,34 @@ theorem jensen_case_R_eq_one
     intro s hs
     simp
     by_contra ha'
-    rw [ha'] at hz
-    exact hz (t₂ s)
+    rw [ha'] at h₂z
+    exact h₂z (t₂ s)
     -- Complex.abs (F z) ≠ 0
     simp
-    exact h₂F z
+    exact h₂F z h₁z
     -- ∏ I : { x // x ∈ S }, Complex.abs (z - a I) ≠ 0
     by_contra h'
     obtain ⟨s, h's, h''⟩ := Finset.prod_eq_zero_iff.1 h'
     simp at h''
-    rw [h''] at hz
+    rw [h''] at h₂z
     let A := t₂ s
-    exact hz A
+    exact h₂z A
 
-  have s₁ : ∀ z, f z ≠ 0 → logAbsF z = logAbsf z - ∑ s, Real.log ‖z - a s‖ := by
-    intro z hz
-    rw [s₀ z hz]
+  have s₁ : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, f z ≠ 0 → logAbsF z = logAbsf z - ∑ s, Real.log ‖z - a s‖ := by
+    intro z h₁z h₂z
+    rw [s₀ z h₁z]
     simp
+    assumption
 
-  rw [s₁ 0 h₂f] at t₁
+  have : 0 ∈ Metric.closedBall (0 : ℂ) 1 := by simp
+  rw [s₁ 0 this h₂f] at t₁
 
   have h₀ {x : ℝ} : f (circleMap 0 1 x) ≠ 0 := by
     rw [h₃F]
     simp
     constructor
-    · exact h₂F (circleMap 0 1 x)
+    · have : (circleMap 0 1 x) ∈ Metric.closedBall (0 : ℂ) 1 := by simp
+      exact h₂F (circleMap 0 1 x) this
     · by_contra h'
       obtain ⟨s, _, h₂s⟩  := Finset.prod_eq_zero_iff.1 h'
       have : circleMap 0 1 x = a s := by
@@ -88,7 +87,8 @@ theorem jensen_case_R_eq_one
       rw [← this] at A
       simp at A
 
-  simp_rw [s₁ (circleMap 0 1 _) h₀] at t₁
+  have {θ} : (circleMap 0 1 θ) ∈ Metric.closedBall (0 : ℂ) 1 := by simp
+  simp_rw [s₁ (circleMap 0 1 _) this h₀] at t₁
   rw [intervalIntegral.integral_sub] at t₁
   rw [intervalIntegral.integral_finset_sum] at t₁
 
@@ -133,7 +133,10 @@ theorem jensen_case_R_eq_one
   apply ContinuousAt.comp
   apply Complex.continuous_abs.continuousAt
   apply ContinuousAt.comp
-  apply h₁f.continuous.continuousAt
+  apply ContDiffAt.continuousAt (f := f) (𝕜 := ℝ) (n := 1)
+  apply HolomorphicAt.contDiffAt
+  apply h₁f
+  simp
   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)