134 lines
3.8 KiB
Plaintext
134 lines
3.8 KiB
Plaintext
import Mathlib.Analysis.Analytic.Meromorphic
|
||
import Nevanlinna.analyticAt
|
||
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
|
||
|
||
|
||
theorem MeromorphicOn.decompose₁
|
||
{f : ℂ → ℂ}
|
||
{U : Set ℂ}
|
||
{z₀ : ℂ}
|
||
(hz₀ : z₀ ∈ U)
|
||
(h₁f : MeromorphicOn f U)
|
||
(h₂f : StronglyMeromorphicAt f z₀) :
|
||
∃ g : ℂ → ℂ, (MeromorphicOn g U)
|
||
∧ (AnalyticAt ℂ g z₀)
|
||
∧ (g z₀ ≠ 0)
|
||
∧ (f = g * fun z ↦ (z - z₀) ^ (h₁f.divisor z₀)) := by
|
||
|
||
let h₁ := fun z ↦ (z - z₀) ^ (-h₁f.divisor z₀)
|
||
have h₁h₁ : MeromorphicOn h₁ U := by
|
||
apply MeromorphicOn.zpow
|
||
apply AnalyticOnNhd.meromorphicOn
|
||
apply AnalyticOnNhd.sub
|
||
exact analyticOnNhd_id
|
||
exact analyticOnNhd_const
|
||
have h₂h₁ : (h₁h₁ z₀ hz₀).order = -h₁f.divisor z₀ := by
|
||
|
||
sorry
|
||
|
||
let g₁ := f * h₁
|
||
have h₁g₁ : MeromorphicOn g₁ U := by
|
||
apply h₁f.mul h₁h₁
|
||
have h₂g₁ : (h₁g₁ z₀ hz₀).order = 0 := by
|
||
let A := (h₁g₁ z₀ hz₀).order_mul (h₁h₁ z₀ hz₀)
|
||
|
||
sorry
|
||
let g := (h₁g₁ z₀ hz₀).makeStronglyMeromorphicAt
|
||
have h₁g : MeromorphicOn g U := by
|
||
sorry
|
||
have h₂g : StronglyMeromorphicAt g z₀ := by
|
||
sorry
|
||
use g
|
||
constructor
|
||
· exact h₁g
|
||
· constructor
|
||
· apply h₂g.analytic
|
||
|
||
sorry
|
||
· constructor
|
||
· sorry
|
||
· sorry
|
||
|
||
|
||
|
||
theorem MeromorphicOn.decompose
|
||
{f : ℂ → ℂ}
|
||
{U : Set ℂ}
|
||
(h₁U : IsConnected U)
|
||
(h₂U : IsCompact U)
|
||
(h₁f : MeromorphicOn f U)
|
||
(h₂f : ∃ z₀ ∈ U, f z₀ ≠ 0) :
|
||
∃ g : ℂ → ℂ, (AnalyticOnNhd ℂ g U)
|
||
∧ (∀ z ∈ U, g z ≠ 0)
|
||
∧ (Set.EqOn h₁f.makeStronglyMeromorphicOn ((∏ᶠ p, fun z ↦ (z - p) ^ (h₁f.divisor p)) * g) U) := by
|
||
|
||
let g₁ : ℂ → ℂ := f * (fun z ↦ ∏ᶠ p, (z - p) ^ (h₁f.divisor p))
|
||
have h₁g₁ : MeromorphicOn g₁ U := by
|
||
sorry
|
||
let g := h₁g₁.makeStronglyMeromorphicOn
|
||
have h₁g : MeromorphicOn g U := by
|
||
sorry
|
||
have h₂g : ∀ z : U, (h₁g z.1 z.2).order = 0 := by
|
||
sorry
|
||
have h₃g : StronglyMeromorphicOn g U := by
|
||
sorry
|
||
have h₄g : AnalyticOnNhd ℂ g U := by
|
||
intro z hz
|
||
apply StronglyMeromorphicAt.analytic (h₃g z hz)
|
||
rw [h₂g ⟨z, hz⟩]
|
||
use g
|
||
constructor
|
||
· exact h₄g
|
||
· constructor
|
||
· intro z hz
|
||
rw [← (h₄g z hz).order_eq_zero_iff]
|
||
have A := (h₄g z hz).meromorphicAt_order
|
||
rw [h₂g ⟨z, hz⟩] at A
|
||
have t₀ : (h₄g z hz).order ≠ ⊤ := by
|
||
by_contra hC
|
||
rw [hC] at A
|
||
tauto
|
||
have t₁ : ∃ n : ℕ, (h₄g z hz).order = n := by
|
||
exact Option.ne_none_iff_exists'.mp t₀
|
||
obtain ⟨n, hn⟩ := t₁
|
||
rw [hn] at A
|
||
apply WithTopCoe
|
||
rw [eq_comm]
|
||
rw [hn]
|
||
exact A
|
||
· intro z hz
|
||
have t₀ : ∀ᶠ x in 𝓝[≠] z, AnalyticAt ℂ f x := by
|
||
sorry
|
||
have t₂ : ∀ᶠ x in 𝓝[≠] z, h₁f.divisor z = 0 := by
|
||
sorry
|
||
have t₁ : ∀ᶠ x in 𝓝[≠] z, AnalyticAt ℂ (fun z => ∏ᶠ (p : ℂ), (z - p) ^ h₁f.divisor p * g z) x := by
|
||
sorry
|
||
apply Filter.EventuallyEq.eq_of_nhds
|
||
apply StronglyMeromorphicAt.localIdentity
|
||
· exact StronglyMeromorphicOn_of_makeStronglyMeromorphic h₁f z hz
|
||
· right
|
||
use h₁f.divisor z
|
||
use (∏ᶠ p : ({z}ᶜ : Set ℂ), (fun x ↦ (x - p.1) ^ h₁f.divisor p.1)) * g
|
||
constructor
|
||
· apply AnalyticAt.mul₁
|
||
· apply analyticAt_finprod
|
||
intro w
|
||
|
||
|
||
sorry
|
||
· apply (h₃g z hz).analytic
|
||
rw [h₂g ⟨z, hz⟩]
|
||
· constructor
|
||
· sorry
|
||
· sorry
|
||
|
||
sorry
|