Working…

Nevanlinna/analyticOn_zeroSet.lean

@@ -357,8 +357,6 @@ theorem AnalyticOnCompact.eliminateZeros
     · exact inter
 
 
-
-
 theorem AnalyticOnCompact.eliminateZeros₂
   {f : ℂ → ℂ}
   {U : Set ℂ}

Nevanlinna/holomorphic_JensenFormula2.lean

@@ -81,18 +81,14 @@ theorem jensen_case_R_eq_one
   (h₂f : f 0 ≠ 0) :
   log ‖f 0‖ = -∑ᶠ s, (h'₁f.order s).toNat * log (‖s.1‖⁻¹) + (2 * π)⁻¹ * ∫ (x : ℝ) in (0)..(2 * π), log ‖f (circleMap 0 1 x)‖ := by
 
-  have h₁U : IsPreconnected (Metric.closedBall (0 : ℂ) 1) := by
-    apply IsConnected.isPreconnected
-    apply Convex.isConnected
-    exact convex_closedBall 0 1
-    exact Set.nonempty_of_nonempty_subtype
+  have h₁U : IsPreconnected (Metric.closedBall (0 : ℂ) 1) :=
+    (convex_closedBall (0 : ℂ) 1).isPreconnected
 
-  have h₂U : IsCompact (Metric.closedBall (0 : ℂ) 1) := isCompact_closedBall 0 1
+  have h₂U : IsCompact (Metric.closedBall (0 : ℂ) 1) :=
+    isCompact_closedBall 0 1
 
   have h'₂f : ∃ u ∈ (Metric.closedBall (0 : ℂ) 1), f u ≠ 0 := by
-    use 0
-    simp
-    exact h₂f
+    use 0; simp; exact h₂f
 
   obtain ⟨F, h₁F, h₂F, h₃F⟩ := AnalyticOnCompact.eliminateZeros₂ h₁U h₂U h'₁f h'₂f
 
@@ -127,24 +123,31 @@ theorem jensen_case_R_eq_one
     dsimp [G]
     abel
 
-    -- ∀ x ∈ (ZeroFinset h₁f).attach, Complex.abs (z - ↑x) ^ order x ≠ 0
-
-    simp
+    -- ∀ x ∈ ⋯.toFinset, Complex.abs (z - ↑x) ^ (h'₁f.order x).toNat ≠ 0
+    have : ∀ x ∈ (finiteZeros h₁U h₂U h'₁f h'₂f).toFinset, Complex.abs (z - ↑x) ^ (h'₁f.order x).toNat ≠ 0 := by
       intro s hs
-    rw [ZeroFinset_mem_iff h₁f s] at hs
-    rw [← hs.2] at h₂z
+      simp at hs
+      simp
+      intro h₂s
+      rw [h₂s] at h₂z
       tauto
+    exact this
+
+    -- ∏ x ∈ ⋯.toFinset, Complex.abs (z - ↑x) ^ (h'₁f.order x).toNat ≠ 0
+    have : ∀ x ∈ (finiteZeros h₁U h₂U h'₁f h'₂f).toFinset, Complex.abs (z - ↑x) ^ (h'₁f.order x).toNat ≠ 0 := by
+      intro s hs
+      simp at hs
+      simp
+      intro h₂s
+      rw [h₂s] at h₂z
+      tauto
+    rw [Finset.prod_ne_zero_iff]
+    exact this
 
     -- Complex.abs (F z) ≠ 0
     simp
     exact h₂F z h₁z
 
-    -- ∏ I : { x // x ∈ S }, Complex.abs (z - a I) ≠ 0
-    by_contra C
-    obtain ⟨s, h₁s, h₂s⟩ := Finset.prod_eq_zero_iff.1 C
-    simp at h₂s
-    rw [← ((ZeroFinset_mem_iff h₁f s).1 (Finset.coe_mem s)).2, h₂s.1] at h₂z
-    tauto
 
   have : ∫ (x : ℝ) in (0)..2 * π, log ‖f (circleMap 0 1 x)‖ = ∫ (x : ℝ) in (0)..2 * π, G (circleMap 0 1 x) := by
 
@@ -159,29 +162,24 @@ theorem jensen_case_R_eq_one
       simp at ha
       simp
       by_contra C
-      have : (circleMap 0 1 a) ∈ Metric.closedBall 0 1 := by
-        sorry
+      have : (circleMap 0 1 a) ∈ Metric.closedBall 0 1 :=
+        circleMap_mem_closedBall 0 (zero_le_one' ℝ) a
       exact ha.2 (decompose_f (circleMap 0 1 a) this C)
 
     apply Set.Countable.mono t₀
     apply Set.Countable.preimage_circleMap
     apply Set.Finite.countable
-    apply finiteZeros
+    let A := finiteZeros h₁U h₂U h'₁f h'₂f
 
-    -- IsPreconnected (Metric.closedBall (0 : ℂ) 1)
-
-    apply IsConnected.isPreconnected
-    apply Convex.isConnected
-    exact convex_closedBall 0 1
-    exact Set.nonempty_of_nonempty_subtype
-    --
-    exact isCompact_closedBall 0 1
-    --
-    exact h'₁f
-    use 0
-    exact ⟨Metric.mem_closedBall_self (zero_le_one' ℝ), h₂f⟩
+    have : (Metric.closedBall 0 1 ∩ f ⁻¹' {0}) = (Metric.closedBall 0 1).restrict f ⁻¹' {0} := by
+      ext z
+      simp
+      tauto
+    rw [this]
+    exact Set.Finite.image Subtype.val A
     exact Ne.symm (zero_ne_one' ℝ)
 
+
   have h₁Gi : ∀ i ∈ (ZeroFinset h₁f h₂f).attach, IntervalIntegrable (fun x => log (Complex.abs (circleMap 0 1 x - ↑i))) MeasureTheory.volume 0 (2 * π) := by
     -- This is hard. Need to invoke specialFunctions_CircleIntegral_affine.
     sorry