Update analyticOn_zeroSet.lean

This commit is contained in:
Stefan Kebekus 2024-09-10 10:55:53 +02:00
parent e41a08f1d5
commit aa79fdb9eb
1 changed files with 13 additions and 59 deletions

View File

@ -1,21 +1,25 @@
import Mathlib.Analysis.Analytic.Constructions import Mathlib.Analysis.Analytic.Constructions
import Mathlib.Analysis.Analytic.IsolatedZeros import Mathlib.Analysis.Analytic.IsolatedZeros
import Mathlib.Analysis.Complex.Basic import Mathlib.Analysis.Complex.Basic
import Nevanlinna.analyticAt
noncomputable def AnalyticOn.order
{f : } {U : Set } (hf : AnalyticOn f U) : U → ℕ∞ := fun u ↦ (hf u u.2).order
theorem AnalyticOn.order_eq_nat_iff theorem AnalyticOn.order_eq_nat_iff
{f : } {f : }
{U : Set } {U : Set }
{z₀ : } {z₀ : U}
(hf : AnalyticOn f U) (hf : AnalyticOn f U)
(hz₀ : z₀ ∈ U)
(n : ) : (n : ) :
(hf z₀ hz₀).order = ↑n ↔ ∃ (g : ), AnalyticOn g U ∧ g z₀ ≠ 0 ∧ ∀ z, f z = (z - z₀) ^ n • g z := by hf.order z₀ = ↑n ↔ ∃ (g : ), AnalyticOn g U ∧ g z₀ ≠ 0 ∧ ∀ z, f z = (z - z₀) ^ n • g z := by
constructor constructor
-- Direction → -- Direction →
intro hn intro hn
obtain ⟨gloc, h₁gloc, h₂gloc, h₃gloc⟩ := (AnalyticAt.order_eq_nat_iff (hf z₀ hz₀) n).1 hn obtain ⟨gloc, h₁gloc, h₂gloc, h₃gloc⟩ := (AnalyticAt.order_eq_nat_iff (hf z₀ z₀.2) n).1 hn
-- Define a candidate function; this is (f z) / (z - z₀) ^ n with the -- Define a candidate function; this is (f z) / (z - z₀) ^ n with the
-- removable singularity removed -- removable singularity removed
@ -44,7 +48,7 @@ theorem AnalyticOn.order_eq_nat_iff
have g_near_z₁ {z₁ : } : z₁ ≠ z₀ → ∀ᶠ (z : ) in nhds z₁, g z = f z / (z - z₀) ^ n := by have g_near_z₁ {z₁ : } : z₁ ≠ z₀ → ∀ᶠ (z : ) in nhds z₁, g z = f z / (z - z₀) ^ n := by
intro hz₁ intro hz₁
rw [eventually_nhds_iff] rw [eventually_nhds_iff]
use {z₀}ᶜ use {z₀.1}ᶜ
constructor constructor
· intro y hy · intro y hy
simp at hy simp at hy
@ -87,59 +91,10 @@ theorem AnalyticOn.order_eq_nat_iff
-- direction ← -- direction ←
intro h intro h
obtain ⟨g, h₁g, h₂g, h₃g⟩ := h obtain ⟨g, h₁g, h₂g, h₃g⟩ := h
dsimp [AnalyticOn.order]
rw [AnalyticAt.order_eq_nat_iff] rw [AnalyticAt.order_eq_nat_iff]
use g use g
exact ⟨h₁g z₀ hz₀, ⟨h₂g, Filter.Eventually.of_forall h₃g⟩⟩ exact ⟨h₁g z₀ z₀.2, ⟨h₂g, Filter.Eventually.of_forall h₃g⟩⟩
theorem AnalyticAt.order_mul
{f₁ f₂ : }
{z₀ : }
(hf₁ : AnalyticAt f₁ z₀)
(hf₂ : AnalyticAt f₂ z₀) :
(AnalyticAt.mul hf₁ hf₂).order = hf₁.order + hf₂.order := by
by_cases h₂f₁ : hf₁.order =
· simp [h₂f₁]
rw [AnalyticAt.order_eq_top_iff, eventually_nhds_iff]
rw [AnalyticAt.order_eq_top_iff, eventually_nhds_iff] at h₂f₁
obtain ⟨t, h₁t, h₂t, h₃t⟩ := h₂f₁
use t
constructor
· intro y hy
rw [h₁t y hy]
ring
· exact ⟨h₂t, h₃t⟩
· by_cases h₂f₂ : hf₂.order =
· simp [h₂f₂]
rw [AnalyticAt.order_eq_top_iff, eventually_nhds_iff]
rw [AnalyticAt.order_eq_top_iff, eventually_nhds_iff] at h₂f₂
obtain ⟨t, h₁t, h₂t, h₃t⟩ := h₂f₂
use t
constructor
· intro y hy
rw [h₁t y hy]
ring
· exact ⟨h₂t, h₃t⟩
· obtain ⟨g₁, h₁g₁, h₂g₁, h₃g₁⟩ := (AnalyticAt.order_eq_nat_iff hf₁ ↑hf₁.order.toNat).1 (eq_comm.1 (ENat.coe_toNat h₂f₁))
obtain ⟨g₂, h₁g₂, h₂g₂, h₃g₂⟩ := (AnalyticAt.order_eq_nat_iff hf₂ ↑hf₂.order.toNat).1 (eq_comm.1 (ENat.coe_toNat h₂f₂))
rw [← ENat.coe_toNat h₂f₁, ← ENat.coe_toNat h₂f₂, ← ENat.coe_add]
rw [AnalyticAt.order_eq_nat_iff (AnalyticAt.mul hf₁ hf₂) ↑(hf₁.order.toNat + hf₂.order.toNat)]
use g₁ * g₂
constructor
· exact AnalyticAt.mul h₁g₁ h₁g₂
· constructor
· simp; tauto
· obtain ⟨t₁, h₁t₁, h₂t₁, h₃t₁⟩ := eventually_nhds_iff.1 h₃g₁
obtain ⟨t₂, h₁t₂, h₂t₂, h₃t₂⟩ := eventually_nhds_iff.1 h₃g₂
rw [eventually_nhds_iff]
use t₁ ∩ t₂
constructor
· intro y hy
rw [h₁t₁ y hy.1, h₁t₂ y hy.2]
simp; ring
· constructor
· exact IsOpen.inter h₂t₁ h₂t₂
· exact Set.mem_inter h₃t₁ h₃t₂
theorem AnalyticOn.eliminateZeros theorem AnalyticOn.eliminateZeros
@ -148,7 +103,7 @@ theorem AnalyticOn.eliminateZeros
{A : Finset U} {A : Finset U}
(hf : AnalyticOn f U) (hf : AnalyticOn f U)
(n : ) : (n : ) :
(∀ a ∈ A, (hf a.1 a.2).order = n a) → ∃ (g : ), AnalyticOn g U ∧ (∀ a ∈ A, g a ≠ 0) ∧ ∀ z, f z = (∏ a ∈ A, (z - a) ^ (n a)) • g z := by (∀ a ∈ A, hf.order a = n a) → ∃ (g : ), AnalyticOn g U ∧ (∀ a ∈ A, g a ≠ 0) ∧ ∀ z, f z = (∏ a ∈ A, (z - a) ^ (n a)) • g z := by
apply Finset.induction (α := U) (p := fun A ↦ (∀ a ∈ A, (hf a.1 a.2).order = n a) → ∃ (g : ), AnalyticOn g U ∧ (∀ a ∈ A, g a ≠ 0) ∧ ∀ z, f z = (∏ a ∈ A, (z - a) ^ (n a)) • g z) apply Finset.induction (α := U) (p := fun A ↦ (∀ a ∈ A, (hf a.1 a.2).order = n a) → ∃ (g : ), AnalyticOn g U ∧ (∀ a ∈ A, g a ≠ 0) ∧ ∀ z, f z = (∏ a ∈ A, (z - a) ^ (n a)) • g z)
@ -208,8 +163,7 @@ theorem AnalyticOn.eliminateZeros
rw [h₂φ] rw [h₂φ]
simp simp
obtain ⟨g₁, h₁g₁, h₂g₁, h₃g₁⟩ := (AnalyticOn.order_eq_nat_iff h₁g₀ (n b₀)).1 this
obtain ⟨g₁, h₁g₁, h₂g₁, h₃g₁⟩ := (AnalyticOn.order_eq_nat_iff h₁g₀ b₀.2 (n b₀)).1 this
use g₁ use g₁
constructor constructor