working…

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) :=