Working…

Nevanlinna/firstMain.lean

@@ -67,16 +67,32 @@ theorem Nevanlinna_counting₁₁
     simp [h']
     clear h'
 
+    have A := (hf.restrict |r|).divisor_add_const₂ a h
+    have A' : 0 ≤ -((MeromorphicOn.add (MeromorphicOn.restrict hf |r|) (MeromorphicOn.const a)).divisor x) := by
+      apply Int.le_neg_of_le_neg
+      simp
+      exact Int.le_of_lt A
+    simp [A']
+    clear A A'
 
-
-
-    simp [h]
-
-    linarith
-
-
-
-  sorry
+    exact (hf.restrict |r|).divisor_add_const₃ a h
+  --
+  intro x
+  contrapose
+  simp
+  intro hx
+  rw [hx]
+  tauto
+  --
+  intro x
+  contrapose
+  simp
+  intro hx
+  have : 0 ≤ (hf.restrict |r|).divisor x := by
+    rw [hx]
+  have G := (hf.restrict |r|).divisor_add_const₁ a this
+  clear this
+  simp [G]
 
 
 theorem Nevanlinna_counting₀

Nevanlinna/meromorphicOn_divisor.lean

@@ -273,6 +273,55 @@ theorem MeromorphicOn.divisor_add_const₂
   rwa [this] at h
 
 
+theorem MeromorphicOn.divisor_add_const₃
+  {f : ℂ → ℂ}
+  {U : Set ℂ}
+  {z : ℂ}
+  (hf : MeromorphicOn f U)
+  (a : ℂ) :
+  hf.divisor z < 0 → (hf.add (MeromorphicOn.const a)).divisor z = hf.divisor z := by
+  intro h
+
+  by_cases hz : z ∉ U
+  · have : hf.divisor z = 0 := by
+      unfold MeromorphicOn.divisor
+      simp [hz]
+    rw [this] at h
+    tauto
+
+  simp at hz
+  unfold MeromorphicOn.divisor
+  simp [hz]
+  unfold MeromorphicOn.divisor at h
+  simp [hz] at h
+
+  have : (hf z hz).order = (((hf.add (MeromorphicOn.const a))) z hz).order := by
+    have t₀ : (hf z hz).order < (0 : ℤ) := by
+        by_contra hCon
+        simp only [not_lt] at hCon
+        rw [←WithTop.le_untop'_iff (b := 0)] at hCon
+        exact Lean.Omega.Int.le_lt_asymm hCon h
+        tauto
+    rw [← MeromorphicAt.order_add_of_ne_orders (hf z hz) (MeromorphicAt.const a z)]
+    simp
+
+    by_cases ha: (MeromorphicAt.const a z).order = ⊤
+    · simp [ha]
+    · calc (hf z hz).order
+      _ ≤ 0 := by exact le_of_lt t₀
+      _ ≤ (MeromorphicAt.const a z).order := by
+        apply AnalyticAt.meromorphicAt_order_nonneg
+        exact analyticAt_const
+
+    apply ne_of_lt
+    calc (hf z hz).order
+      _ < 0 := by exact t₀
+      _ ≤ (MeromorphicAt.const a z).order := by
+        apply AnalyticAt.meromorphicAt_order_nonneg
+        exact analyticAt_const
+  rw [this]
+
+
 theorem MeromorphicOn.divisor_of_makeStronglyMeromorphicOn
   {f : ℂ → ℂ}
   {U : Set ℂ}