Update holomorphic_zero.lean
This commit is contained in:
Stefan Kebekus
parent
a910bd6988
commit
5e7dd06d4c
|
|
@ -288,18 +288,21 @@ theorem AnalyticOn.order_eq_nat_iff
|
|||
(hf : AnalyticOn ℂ f U)
|
||||
(hz₀ : z₀ ∈ U)
|
||||
(n : ℕ) :
|
||||
(hf z₀ hz₀).order = ↑n → ∃ (g : ℂ → ℂ), AnalyticOn ℂ g U ∧ g z₀ ≠ 0 ∧ ∀ z ∈ U, f z = (z - z₀) ^ n • g z := by
|
||||
(hf z₀ hz₀).order = ↑n ↔ ∃ (g : ℂ → ℂ), AnalyticOn ℂ g U ∧ g z₀ ≠ 0 ∧ ∀ z, f z = (z - z₀) ^ n • g z := by
|
||||
|
||||
constructor
|
||||
-- Direction →
|
||||
intro hn
|
||||
|
||||
obtain ⟨gloc, h₁gloc, h₂gloc, h₃gloc⟩ := (AnalyticAt.order_eq_nat_iff (hf z₀ hz₀) n).1 hn
|
||||
|
||||
let g : ℂ → ℂ := fun z ↦ if hz : z = z₀ then gloc z₀ else (f z) / (z - z₀) ^ n
|
||||
-- Define a candidate function; this is (f z) / (z - z₀) ^ n with the
|
||||
-- removable singularity removed
|
||||
let g : ℂ → ℂ := fun z ↦ if z = z₀ then gloc z₀ else (f z) / (z - z₀) ^ n
|
||||
|
||||
have t₀ : ∀ᶠ (z : ℂ) in nhds z₀, g z = gloc z := by
|
||||
-- Describe g near z₀
|
||||
have g_near_z₀ : ∀ᶠ (z : ℂ) in nhds z₀, g z = gloc z := by
|
||||
rw [eventually_nhds_iff]
|
||||
rw [eventually_nhds_iff] at h₃gloc
|
||||
obtain ⟨t, h₁t, h₂t, h₃t⟩ := h₃gloc
|
||||
obtain ⟨t, h₁t, h₂t, h₃t⟩ := eventually_nhds_iff.1 h₃gloc
|
||||
use t
|
||||
constructor
|
||||
· intro y h₁y
|
||||
|
|
@ -315,19 +318,18 @@ theorem AnalyticOn.order_eq_nat_iff
|
|||
· assumption
|
||||
· assumption
|
||||
|
||||
have t₁ {z₁ : ℂ} : z₁ ≠ z₀ → ∀ᶠ (z : ℂ) in nhds z₁, g z = f z / (z - z₀) ^ n := by
|
||||
-- Describe g near points z₁ that are different from z₀
|
||||
have g_near_z₁ {z₁ : ℂ} : z₁ ≠ z₀ → ∀ᶠ (z : ℂ) in nhds z₁, g z = f z / (z - z₀) ^ n := by
|
||||
intro hz₁
|
||||
rw [eventually_nhds_iff]
|
||||
use {z₀}ᶜ
|
||||
constructor
|
||||
· intro y hy
|
||||
simp at hy
|
||||
dsimp [g]
|
||||
simp [hy]
|
||||
· constructor
|
||||
· exact isOpen_compl_singleton
|
||||
· tauto
|
||||
simp [g, hy]
|
||||
· exact ⟨isOpen_compl_singleton, hz₁⟩
|
||||
|
||||
-- Use g and show that it has all required properties
|
||||
use g
|
||||
constructor
|
||||
· -- AnalyticOn ℂ g U
|
||||
|
|
@ -335,18 +337,130 @@ theorem AnalyticOn.order_eq_nat_iff
|
|||
by_cases h₂z : z = z₀
|
||||
· rw [h₂z]
|
||||
apply AnalyticAt.congr h₁gloc
|
||||
exact Filter.EventuallyEq.symm t₀
|
||||
· simp_rw [eq_comm] at t₁
|
||||
apply AnalyticAt.congr _ (t₁ h₂z)
|
||||
exact Filter.EventuallyEq.symm g_near_z₀
|
||||
· simp_rw [eq_comm] at g_near_z₁
|
||||
apply AnalyticAt.congr _ (g_near_z₁ h₂z)
|
||||
apply AnalyticAt.div
|
||||
exact hf z h₁z
|
||||
apply AnalyticAt.pow
|
||||
apply AnalyticAt.sub
|
||||
apply analyticAt_id
|
||||
exact analyticAt_const
|
||||
apply analyticAt_const
|
||||
simp
|
||||
rw [sub_eq_zero]
|
||||
tauto
|
||||
· constructor
|
||||
· simp [g]; tauto
|
||||
· intro z
|
||||
by_cases h₂z : z = z₀
|
||||
· rw [h₂z, g_near_z₀.self_of_nhds]
|
||||
exact h₃gloc.self_of_nhds
|
||||
· rw [(g_near_z₁ h₂z).self_of_nhds]
|
||||
simp [h₂z]
|
||||
rw [div_eq_mul_inv, mul_comm, mul_assoc, inv_mul_cancel]
|
||||
simp; norm_num
|
||||
rw [sub_eq_zero]
|
||||
tauto
|
||||
|
||||
-- direction ←
|
||||
intro h
|
||||
obtain ⟨g, h₁g, h₂g, h₃g⟩ := h
|
||||
rw [AnalyticAt.order_eq_nat_iff]
|
||||
use g
|
||||
exact ⟨h₁g z₀ hz₀, ⟨h₂g, Filter.eventually_of_forall h₃g⟩⟩
|
||||
|
||||
|
||||
theorem AnalyticOn.order_eq_nat_iff'
|
||||
{f : ℂ → ℂ}
|
||||
{U : Set ℂ}
|
||||
{A : Finset U}
|
||||
(hf : AnalyticOn ℂ f U)
|
||||
(n : A → ℕ) :
|
||||
∀ a : A, (hf a (Subtype.coe_prop a.val)).order = n a → ∃ (g : ℂ → ℂ), AnalyticOn ℂ g U ∧ (∀ a, g a ≠ 0) ∧ ∀ z, f z = (∏ a, (z - a) ^ (n a)) • g z := by
|
||||
|
||||
apply Finset.induction
|
||||
|
||||
let a : A := by sorry
|
||||
let b : ℂ := by sorry
|
||||
let u : U := by sorry
|
||||
|
||||
let X := n a
|
||||
have : a = (3 : ℂ) := by sorry
|
||||
have : b ∈ ↑A := by sorry
|
||||
have : ↑a ∈ U := by exact Subtype.coe_prop a.val
|
||||
|
||||
let Y := ∀ a : A, (hf a (Subtype.coe_prop a.val)).order = n a
|
||||
|
||||
--∀ a : A, (hf (ha a)).order = ↑(n a) →
|
||||
|
||||
intro hn
|
||||
obtain ⟨gloc, h₁gloc, h₂gloc, h₃gloc⟩ := (AnalyticAt.order_eq_nat_iff (hf z₀ hz₀) n).1 hn
|
||||
|
||||
-- Define a candidate function
|
||||
let g : ℂ → ℂ := fun z ↦ if z = z₀ then gloc z₀ else (f z) / (z - z₀) ^ n
|
||||
|
||||
-- Describe g near z₀
|
||||
have g_near_z₀ : ∀ᶠ (z : ℂ) in nhds z₀, g z = gloc z := by
|
||||
rw [eventually_nhds_iff]
|
||||
obtain ⟨t, h₁t, h₂t, h₃t⟩ := eventually_nhds_iff.1 h₃gloc
|
||||
use t
|
||||
constructor
|
||||
· intro y h₁y
|
||||
by_cases h₂y : y = z₀
|
||||
· dsimp [g]; simp [h₂y]
|
||||
· dsimp [g]; simp [h₂y]
|
||||
rw [div_eq_iff_mul_eq, eq_comm, mul_comm]
|
||||
exact h₁t y h₁y
|
||||
norm_num
|
||||
rw [sub_eq_zero]
|
||||
tauto
|
||||
· constructor
|
||||
· assumption
|
||||
· assumption
|
||||
|
||||
-- Describe g near points z₁ different from z₀
|
||||
have g_near_z₁ {z₁ : ℂ} : z₁ ≠ z₀ → ∀ᶠ (z : ℂ) in nhds z₁, g z = f z / (z - z₀) ^ n := by
|
||||
intro hz₁
|
||||
rw [eventually_nhds_iff]
|
||||
use {z₀}ᶜ
|
||||
constructor
|
||||
· intro y hy
|
||||
simp at hy
|
||||
simp [g, hy]
|
||||
· exact ⟨isOpen_compl_singleton, hz₁⟩
|
||||
|
||||
-- Use g and show that it has all required properties
|
||||
use g
|
||||
constructor
|
||||
· -- AnalyticOn ℂ g U
|
||||
intro z h₁z
|
||||
by_cases h₂z : z = z₀
|
||||
· rw [h₂z]
|
||||
apply AnalyticAt.congr h₁gloc
|
||||
exact Filter.EventuallyEq.symm g_near_z₀
|
||||
· simp_rw [eq_comm] at g_near_z₁
|
||||
apply AnalyticAt.congr _ (g_near_z₁ h₂z)
|
||||
apply AnalyticAt.div
|
||||
exact hf z h₁z
|
||||
apply AnalyticAt.pow
|
||||
apply AnalyticAt.sub
|
||||
apply analyticAt_id
|
||||
apply analyticAt_const
|
||||
simp
|
||||
rw [sub_eq_zero]
|
||||
tauto
|
||||
· constructor
|
||||
· simp [g]; tauto
|
||||
· intro z
|
||||
by_cases h₂z : z = z₀
|
||||
· rw [h₂z, g_near_z₀.self_of_nhds]
|
||||
exact h₃gloc.self_of_nhds
|
||||
· rw [(g_near_z₁ h₂z).self_of_nhds]
|
||||
simp [h₂z]
|
||||
rw [div_eq_mul_inv, mul_comm, mul_assoc, inv_mul_cancel]
|
||||
simp; norm_num
|
||||
rw [sub_eq_zero]
|
||||
tauto
|
||||
|
||||
|
||||
noncomputable def zeroDivisorDegree
|
||||
|
|
|
|||
Loading…
Reference in New Issue