Working…

Nevanlinna/specialFunctions_CircleIntegral_affine.lean

@@ -394,7 +394,13 @@ lemma int₄
   have h₁a : a / R ∈ Metric.closedBall 0 1 := by
     simp
     simp at ha
-    sorry
+    rw [div_le_comm₀]
+    simp
+    have : R = |R| := by
+      exact Eq.symm (abs_of_pos hR)
+    rwa [this] at ha
+    rwa [abs_of_pos hR]
+    simp
 
   have t₀ {x : ℝ} : circleMap 0 R x = R * circleMap 0 1 x := by
     unfold circleMap

Nevanlinna/stronglyMeromorphic_JensenFormula.lean

@@ -304,16 +304,17 @@ theorem jensen
     simp at hs
     simp [hs.1]
   rw [finsum_eq_sum_of_support_subset _ h₁G'] at decompose_int_G
-  have : ∑ s ∈ h₃f.toFinset, (h₁f.meromorphicOn.divisor s) * ∫ (x_1 : ℝ) in (0)..(2 * π), log ‖circleMap 0 R x_1 - s‖ = 0 := by
-    apply Finset.sum_eq_zero
-    intro x hx
-    rw [int₃ _]
-    simp
-    simp at hx
-    let ZZ := h₁f.meromorphicOn.divisor.supportInU
-    simp at ZZ
-    let UU := ZZ x hx
-    simpa
+  have : ∑ s ∈ h₃f.toFinset, (h₁f.meromorphicOn.divisor s) * ∫ (x_1 : ℝ) in (0)..(2 * π), log ‖circleMap 0 R x_1 - s‖ = ∑ s ∈ h₃f.toFinset, (h₁f.meromorphicOn.divisor s) * (2 * π) * log R := by
+    apply Finset.sum_congr rfl
+    intro s hs
+    have : s ∈ Metric.closedBall 0 R := by
+      let A := h₁f.meromorphicOn.divisor.supportInU
+      have : s ∈ Function.support h₁f.meromorphicOn.divisor := by
+        simp at hs
+        exact hs
+      exact A this
+    rw [int₄ hR this]
+    linarith
   rw [this] at decompose_int_G
 
 
@@ -324,20 +325,42 @@ theorem jensen
   let X := h₄F
   nth_rw 1 [h₄F]
   simp
-  have {l : ℝ} : π⁻¹ * 2⁻¹ * (2 * π * l) = l := by
-    calc π⁻¹ * 2⁻¹ * (2 * π * l)
-    _ = π⁻¹ * (2⁻¹ * 2) * π * l := by ring
-    _ = π⁻¹ * π * l := by ring
-    _ = (π⁻¹ * π) * l := by ring
-    _ = 1 * l := by
+  have : π⁻¹ * 2⁻¹ * (2 * π) = 1 := by
+    calc π⁻¹ * 2⁻¹ * (2 * π)
+    _ = π⁻¹ * (2⁻¹ * 2) * π := by ring
+    _ = π⁻¹ * π := by ring
+    _ = (π⁻¹ * π) := by ring
+    _ = 1 := by
       rw [inv_mul_cancel₀]
       exact pi_ne_zero
-    _ = l := by simp
-  rw [this]
+  --rw [this]
   rw [log_mul]
   rw [log_prod]
   simp
   rw [add_comm]
+  rw [mul_add]
+  rw [← mul_assoc (π⁻¹ * 2⁻¹), this]
+  simp
+  rw [add_comm]
+  nth_rw 2 [add_comm]
+  rw [add_assoc]
+  congr
+  rw [Finset.mul_sum]
+  rw [← sub_eq_add_neg]
+  rw [← Finset.sum_sub_distrib]
+  rw [Finset.sum_congr rfl]
+  intro s hs
+  rw [log_mul, log_inv]
+  rw [← mul_assoc (π⁻¹ * 2⁻¹)]
+  rw [mul_comm _ (2 * π)]
+  rw [← mul_assoc (π⁻¹ * 2⁻¹)]
+  rw [this]
+  simp
+  rw [mul_add]
+  ring
+  --
+
+
   --
   intro x hx
   simp at hx