kebekus/nevanlinna
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Update stronglyMeromorphicOn_ratlPolynomial.lean

Browse Source
This commit is contained in:
Stefan Kebekus 2024-11-26 11:20:02 +01:00
parent 0e88e97295
commit 092bfd85a3
1 changed files with 32 additions and 31 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

61
Nevanlinna/stronglyMeromorphicOn_ratlPolynomial.lean
View File

@ -82,8 +82,7 @@ theorem stronglyMeromorphicOn_divisor_ratlPolynomial₁
by_contra hCon by_contra hCon
let A := congrFun hCon u let A := congrFun hCon u
simp at A simp at A
have t₁ : (0 : ℂ) ^ d u ≠ 0 := by have t₁ : (0 : ℂ) ^ d u ≠ 0 := ne_zero_of_eq_one A
exact ne_zero_of_eq_one A
rw [zpow_ne_zero_iff h] at t₁ rw [zpow_ne_zero_iff h] at t₁
tauto tauto
@ -104,42 +103,44 @@ theorem stronglyMeromorphicOn_divisor_ratlPolynomial₁
tauto tauto
· apply Filter.Eventually.of_forall · apply Filter.Eventually.of_forall
intro x intro x
have t₀ : (Function.mulSupport fun u z => (z - u) ^ d u).Finite := by
rwa [h₂d]
rw [finprod_eq_prod _ t₀]
have t₁ : h₁d.toFinset = t₀.toFinset := by
simp simp
rwa [eq_comm]
rw [t₁]
simp
rw [eq_comm]
have : z ∉ h₁d.toFinset.erase z := Finset.not_mem_erase z h₁d.toFinset
by_cases hz : z ∈ h₁d.toFinset
· rw [t₁] at hz
conv =>
right
rw [← Finset.mul_prod_erase t₀.toFinset _ hz]
· have : t₀.toFinset = t₀.toFinset.erase z := by
rw [eq_comm]
apply Finset.erase_eq_of_not_mem
rwa [t₁] at hz
rw [this]
rw [← Finset.mul_prod_erase] have : (x - z) ^ d z = 1 := by
sorry simp at hz
rw [hz]
by_cases hz : z ∈ d.support simp
· sorry rw [this]
· use (∏ᶠ u, fun z ↦ (z - u) ^ d u) simp
constructor
·
apply?
simp [hz]
sorry
· rw [Function.nmem_support.mp fun a => hz (h₂d a)]
rw [MeromorphicOn.divisor]
simp [hz]
theorem stronglyMeromorphicOn_divisor_ratlPolynomial theorem stronglyMeromorphicOn_divisor_ratlPolynomial
{U : Set ℂ}
(d : ℂ → ℤ) (d : ℂ → ℤ)
(h₁d : Set.Finite d.support) (h₁d : Set.Finite d.support) :
(h₂d : d.support ⊆ U) : (stronglyMeromorphicOn_ratlPolynomial₃ d).meromorphicOn.divisor = d := by
(stronglyMeromorphicOn_ratlPolynomial₃ d (U := U)).meromorphicOn.divisor = d := by
funext z funext z
by_cases hz : z ∈ U
· rw [MeromorphicOn.divisor]
simp [hz]
sorry
· rw [Function.nmem_support.mp fun a => hz (h₂d a)]
rw [MeromorphicOn.divisor] rw [MeromorphicOn.divisor]
simp [hz] simp
rw [stronglyMeromorphicOn_divisor_ratlPolynomial₁ d h₁d]
simp
theorem makeStronglyMeromorphicOn_changeDiscrete' theorem makeStronglyMeromorphicOn_changeDiscrete'