Update meromorphicOn_integrability.lean

Nevanlinna/meromorphicOn_integrability.lean

@@ -106,18 +106,65 @@ theorem MeromorphicOn.integrable_log_abs_f
   (h₂f : ∃ u : (Metric.closedBall (0 : ℂ) r), (h₁f u u.2).order ≠ ⊤) :
   IntervalIntegrable (fun z ↦ log ‖f (circleMap 0 r z)‖) MeasureTheory.volume 0 (2 * π) := by
 
-  have h₁U : IsCompact (Metric.closedBall (0 : ℂ) r) := by sorry
-  have h₂U : IsConnected (Metric.closedBall (0 : ℂ) r) := by sorry
-  have h₃U : interior (Metric.closedBall (0 : ℂ) r) ≠ ∅ := by sorry
+  have h₁U : IsCompact (Metric.closedBall (0 : ℂ) r) := isCompact_closedBall 0 r
+
+  have h₂U : IsConnected (Metric.closedBall (0 : ℂ) r) := by
+    constructor
+    · exact Metric.nonempty_closedBall.mpr (le_of_lt hr)
+    · exact (convex_closedBall (0 : ℂ) r).isPreconnected
+
+  have h₃U : interior (Metric.closedBall (0 : ℂ) r) ≠ ∅ := by
+    rw [interior_closedBall, ← Set.nonempty_iff_ne_empty]
+    use 0; simp [hr];
+    repeat exact Ne.symm (ne_of_lt hr)
+
+  have h₃f : Set.Finite (Function.support h₁f.divisor) := by
+    exact Divisor.finiteSupport h₁U h₁f.divisor
 
   obtain ⟨g, h₁g, h₂g, h₃g⟩ := MeromorphicOn.decompose_log h₁U h₂U h₃U h₁f h₂f
   have : (fun z ↦ log ‖f (circleMap 0 r z)‖) = (fun z ↦ log ‖f z‖) ∘ (circleMap 0 r) := by
     rfl
   rw [this]
   have : Metric.sphere (0 : ℂ) |r| ⊆ Metric.closedBall (0 : ℂ) r := by
-    sorry
+    rw [abs_of_pos hr]
+    apply Metric.sphere_subset_closedBall
+
   rw [integrability_congr_changeDiscrete this h₃g]
 
   apply IntervalIntegrable.add
-  sorry
+  --
+  apply Continuous.intervalIntegrable
+  apply continuous_iff_continuousAt.2
+  intro x
+  have : (fun x => log ‖g (circleMap 0 r x)‖) = log ∘ Complex.abs ∘ g ∘ (fun x ↦ circleMap 0 r x) :=
+    rfl
+  rw [this]
+  apply ContinuousAt.comp
+  apply Real.continuousAt_log
+  · simp
+    have : (circleMap 0 r x) ∈ (Metric.closedBall (0 : ℂ) r) := by
+      apply circleMap_mem_closedBall
+      exact le_of_lt hr
+    exact h₂g ⟨(circleMap 0 r x), this⟩
+  apply ContinuousAt.comp
+  · apply Continuous.continuousAt Complex.continuous_abs
+  apply ContinuousAt.comp
+  · have : (circleMap 0 r x) ∈ (Metric.closedBall (0 : ℂ) r) := by
+      apply circleMap_mem_closedBall (0 : ℂ) (le_of_lt hr) x
+    apply (h₁g (circleMap 0 r x) this).continuousAt
+  apply Continuous.continuousAt (continuous_circleMap 0 r)
+  --
+  have h {x : ℝ} : (Function.support fun s => (h₁f.divisor s) * log ‖circleMap 0 r x - s‖) ⊆ h₃f.toFinset := by
+    intro x; simp; tauto
+  simp_rw [finsum_eq_sum_of_support_subset _ h]
+  --let A := IntervalIntegrable.sum h₃f.toFinset
+  --have h : ∀ s ∈ h₃f.toFinset, IntervalIntegrable (f i) volume 0 (2 * π) := by
+  --  sorry
+  have : (fun x => ∑ s ∈ h₃f.toFinset, (h₁f.divisor s) * log ‖circleMap 0 r x - s‖) = (∑ s ∈ h₃f.toFinset, fun x => (h₁f.divisor s) * log ‖circleMap 0 r x - s‖) := by
+    ext x; simp
+  rw [this]
+  apply IntervalIntegrable.sum h₃f.toFinset
+  intro s hs
+  apply IntervalIntegrable.const_mul
+
   sorry