diff --git a/Nevanlinna/meromorphicOn.lean b/Nevanlinna/meromorphicOn.lean index a97d0d3..3e99437 100644 --- a/Nevanlinna/meromorphicOn.lean +++ b/Nevanlinna/meromorphicOn.lean @@ -93,7 +93,6 @@ theorem MeromorphicOn.open_of_order_neq_top · exact h₃t' - theorem MeromorphicOn.clopen_of_order_eq_top {f : ℂ → ℂ} {U : Set ℂ} @@ -104,3 +103,29 @@ theorem MeromorphicOn.clopen_of_order_eq_top · rw [← isOpen_compl_iff] exact open_of_order_neq_top h₁f · exact open_of_order_eq_top h₁f + + +theorem MeromorphicOn.order_ne_top + {U : Set ℂ} + (hU : IsConnected U) + (h₁f : StronglyMeromorphicOn f U) + (h₂f : ∃ u : U, f u ≠ 0) : + ∀ u : U, (h₁f u u.2).meromorphicAt.order ≠ ⊤ := by + + let A := h₁f.meromorphicOn.clopen_of_order_eq_top + have : PreconnectedSpace U := by + apply isPreconnected_iff_preconnectedSpace.mp + exact IsConnected.isPreconnected hU + rw [isClopen_iff] at A + rcases A with h|h + · intro u + have : u ∉ (∅ : Set U) := by exact fun a => a + rw [← h] at this + simp at this + tauto + · obtain ⟨u, hu⟩ := h₂f + have : u ∈ (Set.univ : Set U) := by trivial + rw [← h] at this + simp at this + rw [(h₁f u u.2).order_eq_zero_iff.2 hu] at this + tauto diff --git a/Nevanlinna/stronglyMeromorphicOn.lean b/Nevanlinna/stronglyMeromorphicOn.lean index 0a34c95..ae313d7 100644 --- a/Nevanlinna/stronglyMeromorphicOn.lean +++ b/Nevanlinna/stronglyMeromorphicOn.lean @@ -1,3 +1,4 @@ +import Nevanlinna.meromorphicOn_divisor import Nevanlinna.stronglyMeromorphicAt import Mathlib.Algebra.BigOperators.Finprod @@ -79,79 +80,74 @@ theorem makeStronglyMeromorphicOn_changeDiscrete · simp [h₂v] -theorem stronglyMeromorphicOn_ratlPolynomial +theorem analyticAt_ratlPolynomial₁ + {z : ℂ} + (d : ℂ → ℤ) + (P : Finset ℂ) : + z ∉ P → AnalyticAt ℂ (∏ u ∈ P, fun z ↦ (z - u) ^ d u) z := by + intro hz + rw [Finset.prod_fn] + apply Finset.analyticAt_prod + intro u hu + apply AnalyticAt.zpow + apply AnalyticAt.sub + apply analyticAt_id + apply analyticAt_const + rw [sub_ne_zero, ne_comm] + exact ne_of_mem_of_not_mem hu hz + + +theorem stronglyMeromorphicOn_ratlPolynomial₂ + {U : Set ℂ} + (d : ℂ → ℤ) + (P : Finset ℂ) : + StronglyMeromorphicOn (∏ u ∈ P, fun z ↦ (z - u) ^ d u) U := by + + intro z hz + by_cases h₂z : z ∈ P + · rw [← Finset.mul_prod_erase P _ h₂z] + right + use d z + use ∏ x ∈ P.erase z, fun z => (z - x) ^ d x + constructor + · have : z ∉ P.erase z := Finset.not_mem_erase z P + apply analyticAt_ratlPolynomial₁ d (P.erase z) this + · constructor + · simp only [Finset.prod_apply] + rw [Finset.prod_ne_zero_iff] + intro u hu + apply zpow_ne_zero + rw [sub_ne_zero] + by_contra hCon + rw [hCon] at hu + let A := Finset.not_mem_erase u P + tauto + · exact Filter.Eventually.of_forall (congrFun rfl) + · apply AnalyticAt.stronglyMeromorphicAt + exact analyticAt_ratlPolynomial₁ d P (z := z) h₂z + + + +theorem stronglyMeromorphicOn_ratlPolynomial₃ {U : Set ℂ} (d : ℂ → ℤ) : StronglyMeromorphicOn (∏ᶠ u, fun z ↦ (z - u) ^ d u) U := by by_cases hd : (Function.mulSupport fun u z => (z - u) ^ d u).Finite · rw [finprod_eq_prod _ hd] - intro z h₁z - by_cases h₂z : d z = 0 - · apply AnalyticAt.stronglyMeromorphicAt - rw [Finset.prod_fn] - apply Finset.analyticAt_prod - intro u hu - by_cases huz : u = z - · rw [← huz] at h₂z - rw [h₂z] - simp - exact analyticAt_const - · apply AnalyticAt.zpow - apply AnalyticAt.sub - apply analyticAt_id - apply analyticAt_const - rwa [sub_ne_zero, ne_comm] - · have : z ∈ hd.toFinset := by - simp - by_contra hCon - have A : 0 ≠ (1 : ℂ → ℂ) z := by simp - rw [← hCon] at A - simp only [sub_self] at A - rw [ne_comm] at A - rw [zpow_ne_zero_iff] at A - tauto - exact h₂z - rw [← Finset.mul_prod_erase hd.toFinset _ this] - right - use d z - use ∏ x ∈ hd.toFinset.erase z, fun z => (z - x) ^ d x - constructor - · rw [Finset.prod_fn] - apply Finset.analyticAt_prod - intro u hu - apply AnalyticAt.zpow - apply AnalyticAt.sub - apply analyticAt_id - apply analyticAt_const - rw [sub_ne_zero, ne_comm] - by_contra hCon - simp at hu - tauto - · constructor - · simp only [Finset.prod_apply] - rw [Finset.prod_ne_zero_iff] - intro u hu - rw [zpow_ne_zero_iff] - rw [sub_ne_zero] - by_contra hCon - rw [hCon] at hu - let A := Finset.not_mem_erase u hd.toFinset - tauto - -- - have : u ∈ hd.toFinset := by - exact Finset.mem_of_mem_erase hu - simp at this - by_contra hCon - rw [hCon] at this - simp at this - tauto - · exact Filter.Eventually.of_forall (congrFun rfl) - + apply stronglyMeromorphicOn_ratlPolynomial₂ (U := U) d hd.toFinset · rw [finprod_of_infinite_mulSupport hd] apply AnalyticOn.stronglyMeromorphicOn apply analyticOnNhd_const +theorem stronglyMeromorphicOn_divisor_ratlPolynomial + {U : Set ℂ} + (d : ℂ → ℤ) + (hd : Set.Finite d.support) : + (stronglyMeromorphicOn_ratlPolynomial₃ d (U := U)).meromorphicOn.divisor = d := by + sorry + + theorem makeStronglyMeromorphicOn_changeDiscrete' {f : ℂ → ℂ} {U : Set ℂ} diff --git a/Nevanlinna/stronglyMeromorphicOn_eliminate.lean b/Nevanlinna/stronglyMeromorphicOn_eliminate.lean index 40194f9..83d279d 100644 --- a/Nevanlinna/stronglyMeromorphicOn_eliminate.lean +++ b/Nevanlinna/stronglyMeromorphicOn_eliminate.lean @@ -8,7 +8,6 @@ import Nevanlinna.meromorphicOn_divisor import Nevanlinna.stronglyMeromorphicOn import Nevanlinna.mathlibAddOn - open scoped Interval Topology open Real Filter MeasureTheory intervalIntegral @@ -304,27 +303,10 @@ theorem MeromorphicOn.decompose₃ ∃ g : ℂ → ℂ, (MeromorphicOn g U) ∧ (AnalyticOn ℂ g U) ∧ (∀ u : U, g u ≠ 0) - ∧ (f = g * ∏ᶠ u : U, fun z ↦ (z - u.1) ^ (h₁f.meromorphicOn.divisor u.1)) := by + ∧ (f = g * ∏ᶠ u, fun z ↦ (z - u) ^ (h₁f.meromorphicOn.divisor u)) := by have h₃f : ∀ u : U, (h₁f u u.2).meromorphicAt.order ≠ ⊤ := by - let A := h₁f.meromorphicOn.clopen_of_order_eq_top - have : PreconnectedSpace U := by - apply isPreconnected_iff_preconnectedSpace.mp - exact IsConnected.isPreconnected h₂U - rw [isClopen_iff] at A - rcases A with h|h - · intro u - have : u ∉ (∅ : Set U) := by exact fun a => a - rw [← h] at this - simp at this - tauto - · obtain ⟨u, hu⟩ := h₂f - let A := (h₁f u u.2).order_eq_zero_iff.2 hu - have : u ∈ (Set.univ : Set U) := by trivial - rw [← h] at this - simp at this - rw [A] at this - tauto + apply MeromorphicOn.order_ne_top h₂U h₁f h₂f have h₄f : Set.Finite (Function.support h₁f.meromorphicOn.divisor) := by exact h₁f.meromorphicOn.divisor.finiteSupport h₁U @@ -336,34 +318,14 @@ theorem MeromorphicOn.decompose₃ apply h₃f obtain ⟨g, h₁g, h₂g, h₃g, h₄g⟩ := MeromorphicOn.decompose₂ h₁f (P := P) hP + let h := ∏ p ∈ P, fun z => (z - p.1) ^ h₁f.meromorphicOn.divisor p.1 + have h₂h : StronglyMeromorphicOn h U := by - -- WARNING: This is a general lemma we should add! - intro u hu - right - by_cases h₁u : ⟨u, hu⟩ ∈ P - · sorry - · use 0 - use h - simp only [zpow_zero, smul_eq_mul, one_mul, eventually_true, and_true] - constructor - · - sorry - · unfold h - simp only [Finset.prod_apply] - rw [Finset.prod_ne_zero_iff] - intro p hp - apply zpow_ne_zero - rw [sub_ne_zero] - by_contra hCon - have : ⟨u, hu⟩ = p := by - exact SetCoe.ext hCon - rw [← this] at hp - tauto - - + unfold h + apply stronglyMeromorphicOn_ratlPolynomial₂ have h₁h : MeromorphicOn h U := by - sorry + exact StronglyMeromorphicOn.meromorphicOn h₂h have h₃h : h₁h.divisor = h₁f.meromorphicOn.divisor := by sorry