Update meromorphicAt.lean

Nevanlinna/meromorphicAt.lean

@@ -232,13 +232,14 @@ theorem MeromorphicAt.order_add
   {z₀ : ℂ}
   (hf₁ : MeromorphicAt f₁ z₀)
   (hf₂ : MeromorphicAt f₂ z₀) :
-  (hf₁.add hf₂).order ≤ min hf₁.order hf₂.order := by
+  min hf₁.order hf₂.order ≤ (hf₁.add hf₂).order := by
 
   -- Handle the trivial cases where one of the orders equals ⊤
   by_cases h₂f₁: hf₁.order = ⊤
   · rw [h₂f₁]; simp
     rw [hf₁.order_eq_top_iff] at h₂f₁
     have h : f₁ + f₂ =ᶠ[𝓝[≠] z₀] f₂ := by
+      -- Optimize this, here an elsewhere
       rw [eventuallyEq_nhdsWithin_iff, eventually_iff_exists_mem]
       rw [eventually_nhdsWithin_iff, eventually_iff_exists_mem] at h₂f₁
       obtain ⟨v, hv⟩ := h₂f₁
@@ -258,7 +259,7 @@ theorem MeromorphicAt.order_add
   obtain ⟨g₂, h₁g₂, h₂g₂, h₃g₂⟩ := hf₂.order_neg_zero_iff.1 h₂f₂
 
   let n₁ := WithTop.untop' 0 hf₁.order
-  let n₂ := WithTop.untop' 0 hf₁.order
+  let n₂ := WithTop.untop' 0 hf₂.order
   let n := min n₁ n₂
   have h₁n₁ : 0 ≤ n₁ - n := by
     rw [sub_nonneg]
@@ -277,7 +278,7 @@ theorem MeromorphicAt.order_add
     apply analyticAt_const
     exact h₁g₁
     apply AnalyticAt.mul
-    apply AnalyticAt.zpow_nonneg _ h₁n₁
+    apply AnalyticAt.zpow_nonneg _ h₁n₂
     apply AnalyticAt.sub
     apply analyticAt_id
     apply analyticAt_const
@@ -285,18 +286,37 @@ theorem MeromorphicAt.order_add
   have h₂g : 0 ≤ h₁g.meromorphicAt.order := h₁g.meromorphicAt_order_nonneg
 
   have : f₁ + f₂ =ᶠ[𝓝[≠] z₀] (fun z ↦ (z - z₀) ^ n) * g := by
-    sorry
+    rw [eventuallyEq_nhdsWithin_iff, eventually_nhds_iff]
+    obtain ⟨t, ht⟩ := eventually_nhds_iff.1 (eventually_nhdsWithin_iff.1 (h₃g₁.and h₃g₂))
+    use t
+    simp [ht]
+    intro y h₁y h₂y
+    rw [(ht.1 y h₁y h₂y).1, (ht.1 y h₁y h₂y).2]
+    unfold g; simp; rw [mul_add]
+    repeat rw [←mul_assoc, ← zpow_add' (by left; exact (sub_ne_zero_of_ne h₂y))]
+    simp
+
   rw [(hf₁.add hf₂).order_congr this]
 
   have t₀ : MeromorphicAt (fun z ↦ (z - z₀) ^ n) z₀ := by
-    sorry
+    apply MeromorphicAt.zpow
+    apply MeromorphicAt.sub
+    apply MeromorphicAt.id
+    apply MeromorphicAt.const
   rw [t₀.order_mul h₁g.meromorphicAt]
   have t₁ : t₀.order = n := by
-    sorry
+    rw [t₀.order_eq_int_iff]
+    use 1
+    constructor
+    · apply analyticAt_const
+    · simp
   rw [t₁]
-
+  unfold n n₁ n₂
-  -- Exercise in WithTop
+  have : hf₁.order ⊓ hf₂.order = (WithTop.untop' 0 hf₁.order ⊓ WithTop.untop' 0 hf₂.order) := by
-  sorry
+    rw [←untop'_of_ne_top (d := 0) h₂f₁, ←untop'_of_ne_top (d := 0) h₂f₂]
+    simp
+  rw [this]
+  exact le_add_of_nonneg_right h₂g
 
 
 theorem MeromorphicAt.order_add_of_ne_orders
@@ -305,7 +325,134 @@ theorem MeromorphicAt.order_add_of_ne_orders
   (hf₁ : MeromorphicAt f₁ z₀)
   (hf₂ : MeromorphicAt f₂ z₀)
   (hf₁₂ : hf₁.order ≠ hf₂.order) :
-  (hf₁.add hf₂).order ≤ hf₁.order + hf₂.order := by
+  min hf₁.order hf₂.order = (hf₁.add hf₂).order := by
-  sorry
+
+  -- Handle the trivial cases where one of the orders equals ⊤
+  by_cases h₂f₁: hf₁.order = ⊤
+  · rw [h₂f₁]; simp
+    rw [hf₁.order_eq_top_iff] at h₂f₁
+    have h : f₁ + f₂ =ᶠ[𝓝[≠] z₀] f₂ := by
+      -- Optimize this, here an elsewhere
+      rw [eventuallyEq_nhdsWithin_iff, eventually_iff_exists_mem]
+      rw [eventually_nhdsWithin_iff, eventually_iff_exists_mem] at h₂f₁
+      obtain ⟨v, hv⟩ := h₂f₁
+      use v; simp; trivial
+    rw [(hf₁.add hf₂).order_congr h]
+  by_cases h₂f₂: hf₂.order = ⊤
+  · rw [h₂f₂]; simp
+    rw [hf₂.order_eq_top_iff] at h₂f₂
+    have h : f₁ + f₂ =ᶠ[𝓝[≠] z₀] f₁ := by
+      rw [eventuallyEq_nhdsWithin_iff, eventually_iff_exists_mem]
+      rw [eventually_nhdsWithin_iff, eventually_iff_exists_mem] at h₂f₂
+      obtain ⟨v, hv⟩ := h₂f₂
+      use v; simp; trivial
+    rw [(hf₁.add hf₂).order_congr h]
+
+  obtain ⟨g₁, h₁g₁, h₂g₁, h₃g₁⟩ := hf₁.order_neg_zero_iff.1 h₂f₁
+  obtain ⟨g₂, h₁g₂, h₂g₂, h₃g₂⟩ := hf₂.order_neg_zero_iff.1 h₂f₂
+
+  let n₁ := WithTop.untop' 0 hf₁.order
+  let n₂ := WithTop.untop' 0 hf₂.order
+  have hn₁₂ : n₁ ≠ n₂ := by
+    unfold n₁ n₂
+    let A := WithTop.untop'_eq_untop'_iff (d := 0) (x := hf₁.order) (y := hf₂.order)
+    let B := A.not
+    simp
+    rw [B]
+    push_neg
+    constructor
+    · assumption
+    · tauto
+
+  let n := min n₁ n₂
+  have h₁n₁ : 0 ≤ n₁ - n := by
+    rw [sub_nonneg]
+    exact Int.min_le_left n₁ n₂
+  have h₁n₂ : 0 ≤ n₂ - n := by
+    rw [sub_nonneg]
+    exact Int.min_le_right n₁ n₂
+
+  let g := (fun z ↦ (z - z₀) ^ (n₁ - n)) * g₁ +  (fun z ↦ (z - z₀) ^ (n₂ - n)) * g₂
+  have h₁g : AnalyticAt ℂ g z₀ := by
+    apply AnalyticAt.add
+    apply AnalyticAt.mul
+    apply AnalyticAt.zpow_nonneg _ h₁n₁
+    apply AnalyticAt.sub
+    apply analyticAt_id
+    apply analyticAt_const
+    exact h₁g₁
+    apply AnalyticAt.mul
+    apply AnalyticAt.zpow_nonneg _ h₁n₂
+    apply AnalyticAt.sub
+    apply analyticAt_id
+    apply analyticAt_const
+    exact h₁g₂
+  have h₂g : 0 ≤ h₁g.meromorphicAt.order := h₁g.meromorphicAt_order_nonneg
+  have h₂'g : g z₀ ≠ 0 := by
+    unfold g
+    simp
+    have : n = n₁ ∨ n = n₂ := by
+      unfold n
+      simp
+      by_cases h : n₁ ≤ n₂
+      · left; assumption
+      · right
+        simp at h
+        exact le_of_lt h
+    rcases this with h|h
+    · rw [h]
+      have : n₂ - n₁ ≠ 0 := by
+        rw [sub_ne_zero, ne_comm]
+        apply hn₁₂
+      have : (0 : ℂ) ^ (n₂ - n₁) = 0 := by
+        rwa [zpow_eq_zero_iff]
+      simp [this]
+      exact h₂g₁
+    · rw [h]
+      have : n₁ - n₂ ≠ 0 := by
+        rw [sub_ne_zero]
+        apply hn₁₂
+      have : (0 : ℂ) ^ (n₁ - n₂) = 0 := by
+        rwa [zpow_eq_zero_iff]
+      simp [this]
+      exact h₂g₂
+  have h₃g : h₁g.meromorphicAt.order = 0 := by
+    let A := h₁g.meromorphicAt_order
+    let B := h₁g.order_eq_zero_iff.2 h₂'g
+    rw [B] at A
+    simpa
+
+  have : f₁ + f₂ =ᶠ[𝓝[≠] z₀] (fun z ↦ (z - z₀) ^ n) * g := by
+    rw [eventuallyEq_nhdsWithin_iff, eventually_nhds_iff]
+    obtain ⟨t, ht⟩ := eventually_nhds_iff.1 (eventually_nhdsWithin_iff.1 (h₃g₁.and h₃g₂))
+    use t
+    simp [ht]
+    intro y h₁y h₂y
+    rw [(ht.1 y h₁y h₂y).1, (ht.1 y h₁y h₂y).2]
+    unfold g; simp; rw [mul_add]
+    repeat rw [←mul_assoc, ← zpow_add' (by left; exact (sub_ne_zero_of_ne h₂y))]
+    simp
+
+  rw [(hf₁.add hf₂).order_congr this]
+
+  have t₀ : MeromorphicAt (fun z ↦ (z - z₀) ^ n) z₀ := by
+    apply MeromorphicAt.zpow
+    apply MeromorphicAt.sub
+    apply MeromorphicAt.id
+    apply MeromorphicAt.const
+  rw [t₀.order_mul h₁g.meromorphicAt]
+  have t₁ : t₀.order = n := by
+    rw [t₀.order_eq_int_iff]
+    use 1
+    constructor
+    · apply analyticAt_const
+    · simp
+  rw [t₁]
+  unfold n n₁ n₂
+  have : hf₁.order ⊓ hf₂.order = (WithTop.untop' 0 hf₁.order ⊓ WithTop.untop' 0 hf₂.order) := by
+    rw [←untop'_of_ne_top (d := 0) h₂f₁, ←untop'_of_ne_top (d := 0) h₂f₂]
+    simp
+  rw [this, h₃g]
+  simp
 
 -- might want theorem MeromorphicAt.order_zpow