diff --git a/Nevanlinna/meromorphicAt.lean b/Nevanlinna/meromorphicAt.lean index d51034f..d1c3e19 100644 --- a/Nevanlinna/meromorphicAt.lean +++ b/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₁] - - -- Exercise in WithTop - sorry + 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] + 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 - sorry + 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₁ + 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