Update mathlib and work on Jensen Formula

Nevanlinna/stronglyMeromorphic_JensenFormula.lean

@@ -76,35 +76,32 @@ theorem jensen_case_R_eq_one
     rw [finsum_eq_sum_of_support_subset _ h₁G]
     --
     intro x hx
-    simp at hx
+    have : z ≠ x := by
-
+      by_contra hCon
-
+      rw [← hCon] at hx
-    abel
+      simp at hx
-
+      rw [← StronglyMeromorphicAt.order_eq_zero_iff] at h₂z
-    -- ∀ x ∈ ⋯.toFinset, Complex.abs (z - ↑x) ^ (h'₁f.order x).toNat ≠ 0
+      unfold MeromorphicOn.divisor at hx
-    have : ∀ x ∈ (finiteZeros h₁U h₂U h₁f h'₂f).toFinset, Complex.abs (z - ↑x) ^ (h₁f.order x).toNat ≠ 0 := by
+      simp [h₁z] at hx
-      intro s hs
-      simp at hs
-      simp
-      intro h₂s
-      rw [h₂s] at h₂z
       tauto
-    exact this
+    apply zpow_ne_zero
-
+    simpa
-    -- ∏ 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
+    exact h₃F ⟨z, h₁z⟩
+    --
+    rw [Finset.prod_ne_zero_iff]
+    intro x hx
+    have : z ≠ x := by
+      by_contra hCon
+      rw [← hCon] at hx
+      simp at hx
+      rw [← StronglyMeromorphicAt.order_eq_zero_iff] at h₂z
+      unfold MeromorphicOn.divisor at hx
+      simp [h₁z] at hx
+      tauto
+    apply zpow_ne_zero
+    simpa
 
 
   have int_logAbs_f_eq_int_G : ∫ (x : ℝ) in (0)..2 * π, log ‖f (circleMap 0 1 x)‖ = ∫ (x : ℝ) in (0)..2 * π, G (circleMap 0 1 x) := by
@@ -115,27 +112,39 @@ theorem jensen_case_R_eq_one
     simp
 
     have t₀ : {a | a ∈ Ι 0 (2 * π) ∧ ¬log ‖f (circleMap 0 1 a)‖ = G (circleMap 0 1 a)}
-      ⊆ (circleMap 0 1)⁻¹' (Metric.closedBall 0 1 ∩ f⁻¹' {0}) := by
+      ⊆ (circleMap 0 1)⁻¹' (h₃f.toFinset) := by
       intro a ha
       simp at ha
       simp
       by_contra C
-      have : (circleMap 0 1 a) ∈ Metric.closedBall 0 1 :=
+      have t₀ : (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)
+      have t₁ : f (circleMap 0 1 a) ≠ 0 := by
+        let A := h₁f (circleMap 0 1 a) t₀
+        rw [← A.order_eq_zero_iff]
+        unfold MeromorphicOn.divisor at C
+        simp [t₀] at C
+        rcases C with C₁|C₂
+        · assumption
+        · let B := h₁f.meromorphicOn.order_ne_top' h₁U
+          let C := fun q ↦ B q ⟨(circleMap 0 1 a), t₀⟩
+          rw [C₂] at C
+          have : ∃ u : (Metric.closedBall (0 : ℂ) 1), (h₁f u u.2).meromorphicAt.order ≠ ⊤ := by
+            use ⟨(0 : ℂ), (by simp)⟩
+            let H := h₁f 0 (by simp)
+            let K := H.order_eq_zero_iff.2 h₂f
+            rw [K]
+            simp
+          let D := C this
+          tauto
+      exact ha.2 (decompose_f (circleMap 0 1 a) t₀ t₁)
 
     apply Set.Countable.mono t₀
     apply Set.Countable.preimage_circleMap
     apply Set.Finite.countable
-    let A := finiteZeros h₁U h₂U h₁f h'₂f
+    exact Finset.finite_toSet h₃f.toFinset
-
+    --
-    have : (Metric.closedBall 0 1 ∩ f ⁻¹' {0}) = (Metric.closedBall 0 1).restrict f ⁻¹' {0} := by
+    simp
-      ext z
-      simp
-      tauto
-    rw [this]
-    exact Set.Finite.image Subtype.val A
-    exact Ne.symm (zero_ne_one' ℝ)
 
 
   have decompose_int_G : ∫ (x : ℝ) in (0)..2 * π, G (circleMap 0 1 x)

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "7cf807751deab8d4943d867898dc1b31d61b746a",
+   "rev": "134c6ee3da5185da90b69d05697c85bfba57e82e",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,