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

working…

This commit is contained in:
Stefan Kebekus 2024-09-10 14:43:28 +02:00
parent ef7e1df191
commit 8e5ada9a01
2 changed files with 18 additions and 14 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
Nevanlinna/analyticAt.lean
View File

@ -74,3 +74,14 @@ theorem AnalyticAt.order_eq_zero_iff
· constructor · constructor
· exact hz · exact hz
· simp · simp
theorem AnalyticAt.supp_order_toNat
{f : ℂ → ℂ}
{z₀ : ℂ}
(hf : AnalyticAt ℂ f z₀) :
hf.order.toNat ≠ 0 → f z₀ = 0 := by
contrapose
intro h₁f
simp [hf.order_eq_zero_iff.2 h₁f]

21
Nevanlinna/analyticOn_zeroSet.lean
View File

@ -107,16 +107,6 @@ theorem AnalyticOn.support_of_order₁
rw [not_iff_comm, (hf u u.2).order_eq_zero_iff] rw [not_iff_comm, (hf u u.2).order_eq_zero_iff]
theorem AnalyticOn.support_of_order₂
{f : ℂ → ℂ}
{U : Set ℂ}
(h₁U : IsPreconnected U)
(h₁f : AnalyticOn ℂ f U)
(h₂f : ∃ u ∈ U, f u ≠ 0) :
Function.support (ENat.toNat ∘ h₁f.order) = U.restrict f⁻¹' {0} := by
sorry
theorem AnalyticOn.eliminateZeros theorem AnalyticOn.eliminateZeros
{f : ℂ → ℂ} {f : ℂ → ℂ}
{U : Set ℂ} {U : Set ℂ}
@ -376,6 +366,7 @@ theorem AnalyticOnCompact.eliminateZeros₁
(h₂f : ∃ u ∈ U, f u ≠ 0) : (h₂f : ∃ u ∈ U, f u ≠ 0) :
∃ (g : ℂ → ℂ), AnalyticOn ℂ g U ∧ (∀ z ∈ U, g z ≠ 0) ∧ ∀ z, f z = (∏ᶠ a : U, (z - a) ^ (h₁f.order a).toNat) • g z := by ∃ (g : ℂ → ℂ), AnalyticOn ℂ g U ∧ (∀ z ∈ U, g z ≠ 0) ∧ ∀ z, f z = (∏ᶠ a : U, (z - a) ^ (h₁f.order a).toNat) • g z := by
let A := (finiteZeros h₁U h₂U h₁f h₂f).toFinset let A := (finiteZeros h₁U h₂U h₁f h₂f).toFinset
let n : U → ℕ := fun z ↦ (h₁f z z.2).order.toNat let n : U → ℕ := fun z ↦ (h₁f z z.2).order.toNat
@ -394,7 +385,6 @@ theorem AnalyticOnCompact.eliminateZeros₁
intro z intro z
rw [h₃g z] rw [h₃g z]
constructor constructor
· exact h₁g · exact h₁g
· constructor · constructor
@ -411,14 +401,17 @@ theorem AnalyticOnCompact.eliminateZeros₁
rw [inter z] at this rw [inter z] at this
exact right_ne_zero_of_smul this exact right_ne_zero_of_smul this
· intro z · intro z
let φ : U → ℂ := fun a ↦ (z - ↑a) ^ (h₁f.order a).toNat let φ : U → ℂ := fun a ↦ (z - ↑a) ^ (h₁f.order a).toNat
have hφ : Function.mulSupport φ ⊆ A := by have hφ : Function.mulSupport φ ⊆ A := by
intro x hx intro x hx
simp [φ] at hx simp [φ] at hx
have : (h₁f.order x).toNat ≠ 0 := by have : (h₁f.order x).toNat ≠ 0 := by
sorry by_contra C
rw [C] at hx
sorry simp at hx
simp [A]
exact AnalyticAt.supp_order_toNat (h₁f x x.2) this
rw [finprod_eq_prod_of_mulSupport_subset φ hφ] rw [finprod_eq_prod_of_mulSupport_subset φ hφ]
rw [inter z] rw [inter z]
rfl rfl