diff --git a/Nevanlinna/mathlibAddOn.lean b/Nevanlinna/mathlibAddOn.lean index e5957f6..0ab0aef 100644 --- a/Nevanlinna/mathlibAddOn.lean +++ b/Nevanlinna/mathlibAddOn.lean @@ -72,3 +72,20 @@ lemma Mnhds · simp at h₂y rwa [h₂y] · exact h₂t + +-- unclear where this should go + +lemma WithTopCoe + {n : WithTop ℕ} : + WithTop.map (Nat.cast : ℕ → ℤ) n = 0 → n = 0 := by + rcases n with h|h + · intro h + contradiction + · intro h₁ + simp only [WithTop.map, Option.map] at h₁ + have : (h : ℤ) = 0 := by + exact WithTop.coe_eq_zero.mp h₁ + have : h = 0 := by + exact Int.ofNat_eq_zero.mp this + rw [this] + rfl diff --git a/Nevanlinna/meromorphicOn_decompose.lean b/Nevanlinna/meromorphicOn_decompose.lean index bc04777..91ff55f 100644 --- a/Nevanlinna/meromorphicOn_decompose.lean +++ b/Nevanlinna/meromorphicOn_decompose.lean @@ -4,26 +4,12 @@ import Nevanlinna.divisor import Nevanlinna.meromorphicAt import Nevanlinna.meromorphicOn_divisor import Nevanlinna.stronglyMeromorphicOn +import Nevanlinna.mathlibAddOn open scoped Interval Topology open Real Filter MeasureTheory intervalIntegral -lemma WithTopCoe - {n : WithTop ℕ} : - WithTop.map (Nat.cast : ℕ → ℤ) n = 0 → n = 0 := by - rcases n with h|h - · intro h - contradiction - · intro h₁ - simp only [WithTop.map, Option.map] at h₁ - have : (h : ℤ) = 0 := by - exact WithTop.coe_eq_zero.mp h₁ - have : h = 0 := by - exact Int.ofNat_eq_zero.mp this - rw [this] - rfl - theorem MeromorphicOn.decompose {f : ℂ → ℂ} diff --git a/Nevanlinna/stronglyMeromorphicAt.lean b/Nevanlinna/stronglyMeromorphicAt.lean index bb65ec0..e320453 100644 --- a/Nevanlinna/stronglyMeromorphicAt.lean +++ b/Nevanlinna/stronglyMeromorphicAt.lean @@ -129,7 +129,45 @@ theorem StronglyMeromorphicAt.order_eq_zero_iff {z₀ : ℂ} (hf : StronglyMeromorphicAt f z₀) : hf.meromorphicAt.order = 0 ↔ f z₀ ≠ 0 := by - sorry + constructor + · intro h₁f + let A := hf.analytic (le_of_eq (id (Eq.symm h₁f))) + apply A.order_eq_zero_iff.1 + let B := A.meromorphicAt_order + rw [h₁f] at B + apply WithTopCoe + rw [eq_comm] + exact B + · intro h + have hf' := hf + rcases hf with h₁|h₁ + · have : f z₀ = 0 := by + apply Filter.EventuallyEq.eq_of_nhds h₁ + tauto + · obtain ⟨n, g, h₁g, h₂g, h₃g⟩ := h₁ + have : n = 0 := by + by_contra hContra + let A := Filter.EventuallyEq.eq_of_nhds h₃g + have : (0 : ℂ) ^ n = 0 := by + exact zero_zpow n hContra + simp at A + simp_rw [this] at A + simp at A + tauto + rw [this] at h₃g + simp at h₃g + + have : hf'.meromorphicAt.order = 0 := by + apply (hf'.meromorphicAt.order_eq_int_iff 0).2 + use g + constructor + · assumption + · constructor + · assumption + · simp + apply Filter.EventuallyEq.filter_mono h₃g + exact nhdsWithin_le_nhds + exact this theorem StronglyMeromorphicAt.localIdentity {f g : ℂ → ℂ}