nevanlinna/Nevanlinna/analyticOn_zeroSet.lean

462 lines
13 KiB
Plaintext
Raw Permalink Normal View History

2024-08-20 10:16:37 +02:00
import Mathlib.Analysis.Analytic.Constructions
2024-08-20 12:54:30 +02:00
import Mathlib.Analysis.Analytic.IsolatedZeros
import Mathlib.Analysis.Complex.Basic
2024-09-10 10:55:53 +02:00
import Nevanlinna.analyticAt
noncomputable def AnalyticOn.order
{f : } {U : Set } (hf : AnalyticOn f U) : U → ℕ∞ := fun u ↦ (hf u u.2).order
2024-08-20 07:46:18 +02:00
theorem AnalyticOn.order_eq_nat_iff
{f : }
{U : Set }
2024-09-10 10:55:53 +02:00
{z₀ : U}
2024-08-20 07:46:18 +02:00
(hf : AnalyticOn f U)
(n : ) :
2024-09-10 10:55:53 +02:00
hf.order z₀ = ↑n ↔ ∃ (g : ), AnalyticOn g U ∧ g z₀ ≠ 0 ∧ ∀ z, f z = (z - z₀) ^ n • g z := by
2024-08-20 07:46:18 +02:00
constructor
-- Direction →
intro hn
2024-09-10 10:55:53 +02:00
obtain ⟨gloc, h₁gloc, h₂gloc, h₃gloc⟩ := (AnalyticAt.order_eq_nat_iff (hf z₀ z₀.2) n).1 hn
2024-08-20 07:46:18 +02:00
-- 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
-- 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₁ 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]
2024-09-10 10:55:53 +02:00
use {z₀.1}ᶜ
2024-08-20 07:46:18 +02:00
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]
2024-08-23 09:26:58 +02:00
rw [div_eq_mul_inv, mul_comm, mul_assoc, inv_mul_cancel₀]
2024-08-20 07:46:18 +02:00
simp; norm_num
rw [sub_eq_zero]
tauto
-- direction ←
intro h
obtain ⟨g, h₁g, h₂g, h₃g⟩ := h
2024-09-10 10:55:53 +02:00
dsimp [AnalyticOn.order]
2024-08-20 07:46:18 +02:00
rw [AnalyticAt.order_eq_nat_iff]
use g
2024-09-10 10:55:53 +02:00
exact ⟨h₁g z₀ z₀.2, ⟨h₂g, Filter.Eventually.of_forall h₃g⟩⟩
2024-08-20 10:16:37 +02:00
2024-09-10 14:21:08 +02:00
theorem AnalyticOn.support_of_order₁
{f : }
{U : Set }
(hf : AnalyticOn f U) :
Function.support hf.order = U.restrict f⁻¹' {0} := by
ext u
simp [AnalyticOn.order]
rw [not_iff_comm, (hf u u.2).order_eq_zero_iff]
2024-08-20 11:06:24 +02:00
theorem AnalyticOn.eliminateZeros
2024-08-20 07:46:18 +02:00
{f : }
{U : Set }
{A : Finset U}
(hf : AnalyticOn f U)
2024-09-10 12:53:34 +02:00
(n : U → ) :
2024-09-10 10:55:53 +02:00
(∀ 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
2024-08-20 07:46:18 +02:00
2024-08-20 15:33:55 +02:00
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)
-- case empty
simp
use f
simp
exact hf
-- case insert
intro b₀ B hb iHyp
intro hBinsert
obtain ⟨g₀, h₁g₀, h₂g₀, h₃g₀⟩ := iHyp (fun a ha ↦ hBinsert a (Finset.mem_insert_of_mem ha))
have : (h₁g₀ b₀ b₀.2).order = n b₀ := by
rw [← hBinsert b₀ (Finset.mem_insert_self b₀ B)]
2024-09-10 12:53:34 +02:00
let φ := fun z ↦ (∏ a ∈ B, (z - a.1) ^ n a)
2024-08-20 15:33:55 +02:00
have : f = fun z ↦ φ z * g₀ z := by
funext z
rw [h₃g₀ z]
rfl
simp_rw [this]
have h₁φ : AnalyticAt φ b₀ := by
dsimp [φ]
apply Finset.analyticAt_prod
intro b _
apply AnalyticAt.pow
apply AnalyticAt.sub
apply analyticAt_id
exact analyticAt_const
have h₂φ : h₁φ.order = (0 : ) := by
rw [AnalyticAt.order_eq_nat_iff h₁φ 0]
use φ
constructor
· assumption
· constructor
· dsimp [φ]
push_neg
rw [Finset.prod_ne_zero_iff]
intro a ha
simp
have : ¬ (b₀.1 - a.1 = 0) := by
by_contra C
rw [sub_eq_zero] at C
rw [SetCoe.ext C] at hb
tauto
tauto
· simp
rw [AnalyticAt.order_mul h₁φ (h₁g₀ b₀ b₀.2)]
rw [h₂φ]
simp
2024-09-10 10:55:53 +02:00
obtain ⟨g₁, h₁g₁, h₂g₁, h₃g₁⟩ := (AnalyticOn.order_eq_nat_iff h₁g₀ (n b₀)).1 this
2024-08-20 15:33:55 +02:00
use g₁
constructor
· exact h₁g₁
· constructor
· intro a h₁a
by_cases h₂a : a = b₀
· rwa [h₂a]
· let A' := Finset.mem_of_mem_insert_of_ne h₁a h₂a
let B' := h₃g₁ a
let C' := h₂g₀ a A'
rw [B'] at C'
exact right_ne_zero_of_smul C'
· intro z
let A' := h₃g₀ z
rw [h₃g₁ z] at A'
rw [A']
rw [← smul_assoc]
congr
simp
rw [Finset.prod_insert]
ring
exact hb
theorem XX
{f : }
{U : Set }
(hU : IsPreconnected U)
(h₁f : AnalyticOn f U)
(h₂f : ∃ u ∈ U, f u ≠ 0) :
∀ (hu : u ∈ U), (h₁f u hu).order.toNat = (h₁f u hu).order := by
intro hu
apply ENat.coe_toNat
by_contra C
rw [(h₁f u hu).order_eq_top_iff] at C
rw [← (h₁f u hu).frequently_zero_iff_eventually_zero] at C
obtain ⟨u₁, h₁u₁, h₂u₁⟩ := h₂f
rw [(h₁f.eqOn_zero_of_preconnected_of_frequently_eq_zero hU hu C) h₁u₁] at h₂u₁
tauto
theorem discreteZeros
{f : }
{U : Set }
(hU : IsPreconnected U)
(h₁f : AnalyticOn f U)
(h₂f : ∃ u ∈ U, f u ≠ 0) :
2024-09-10 11:06:00 +02:00
DiscreteTopology ((U.restrict f)⁻¹' {0}) := by
2024-08-20 15:33:55 +02:00
simp_rw [← singletons_open_iff_discrete]
simp_rw [Metric.isOpen_singleton_iff]
intro z
2024-09-10 11:06:00 +02:00
let A := XX hU h₁f h₂f z.1.2
2024-08-20 15:33:55 +02:00
rw [eq_comm] at A
rw [AnalyticAt.order_eq_nat_iff] at A
obtain ⟨g, h₁g, h₂g, h₃g⟩ := A
rw [Metric.eventually_nhds_iff_ball] at h₃g
have : ∃ ε > 0, ∀ y ∈ Metric.ball (↑z) ε, g y ≠ 0 := by
have h₄g : ContinuousAt g z := AnalyticAt.continuousAt h₁g
have : {0}ᶜ ∈ nhds (g z) := by
exact compl_singleton_mem_nhds_iff.mpr h₂g
let F := h₄g.preimage_mem_nhds this
rw [Metric.mem_nhds_iff] at F
obtain ⟨ε, h₁ε, h₂ε⟩ := F
use ε
constructor; exact h₁ε
intro y hy
let G := h₂ε hy
simp at G
exact G
obtain ⟨ε₁, h₁ε₁⟩ := this
obtain ⟨ε₂, h₁ε₂, h₂ε₂⟩ := h₃g
use min ε₁ ε₂
constructor
· have : 0 < min ε₁ ε₂ := by
rw [lt_min_iff]
exact And.imp_right (fun _ => h₁ε₂) h₁ε₁
exact this
intro y
intro h₁y
have h₂y : ↑y ∈ Metric.ball (↑z) ε₂ := by
simp
calc dist y z
_ < min ε₁ ε₂ := by assumption
_ ≤ ε₂ := by exact min_le_right ε₁ ε₂
have h₃y : ↑y ∈ Metric.ball (↑z) ε₁ := by
simp
calc dist y z
_ < min ε₁ ε₂ := by assumption
_ ≤ ε₁ := by exact min_le_left ε₁ ε₂
have F := h₂ε₂ y.1 h₂y
2024-09-10 11:06:00 +02:00
have : f y = 0 := by exact y.2
rw [this] at F
2024-08-20 15:33:55 +02:00
simp at F
have : g y.1 ≠ 0 := by
exact h₁ε₁.2 y h₃y
simp [this] at F
ext
rw [sub_eq_zero] at F
tauto
theorem finiteZeros
{f : }
{U : Set }
(h₁U : IsPreconnected U)
(h₂U : IsCompact U)
(h₁f : AnalyticOn f U)
(h₂f : ∃ u ∈ U, f u ≠ 0) :
2024-09-10 11:21:49 +02:00
Set.Finite (U.restrict f⁻¹' {0}) := by
2024-08-20 15:33:55 +02:00
2024-09-10 11:21:49 +02:00
have closedness : IsClosed (U.restrict f⁻¹' {0}) := by
apply IsClosed.preimage
apply continuousOn_iff_continuous_restrict.1
exact h₁f.continuousOn
2024-08-20 15:33:55 +02:00
exact isClosed_singleton
2024-09-10 11:21:49 +02:00
have : CompactSpace U := by
exact isCompact_iff_compactSpace.mp h₂U
apply (IsClosed.isCompact closedness).finite
2024-08-20 15:33:55 +02:00
exact discreteZeros h₁U h₁f h₂f
theorem AnalyticOnCompact.eliminateZeros
{f : }
{U : Set }
(h₁U : IsPreconnected U)
(h₂U : IsCompact U)
(h₁f : AnalyticOn f U)
(h₂f : ∃ u ∈ U, f u ≠ 0) :
2024-09-10 12:53:34 +02:00
∃ (g : ) (A : Finset U), AnalyticOn g U ∧ (∀ z ∈ U, g z ≠ 0) ∧ ∀ z, f z = (∏ a ∈ A, (z - a) ^ (h₁f.order a).toNat) • g z := by
let A := (finiteZeros h₁U h₂U h₁f h₂f).toFinset
let n : U → := fun z ↦ (h₁f z z.2).order.toNat
have hn : ∀ a ∈ A, (h₁f a a.2).order = n a := by
intro a _
dsimp [n, AnalyticOn.order]
rw [eq_comm]
apply XX h₁U
exact h₂f
obtain ⟨g, h₁g, h₂g, h₃g⟩ := AnalyticOn.eliminateZeros (A := A) h₁f n hn
use g
use A
have inter : ∀ (z : ), f z = (∏ a ∈ A, (z - ↑a) ^ (h₁f (↑a) a.property).order.toNat) • g z := by
intro z
rw [h₃g z]
constructor
· exact h₁g
· constructor
· intro z h₁z
by_cases h₂z : ⟨z, h₁z⟩ ∈ ↑A.toSet
· exact h₂g ⟨z, h₁z⟩ h₂z
· have : f z ≠ 0 := by
by_contra C
have : ⟨z, h₁z⟩ ∈ ↑A.toSet := by
dsimp [A]
simp
exact C
tauto
rw [inter z] at this
exact right_ne_zero_of_smul this
· exact inter
2024-09-10 15:29:30 +02:00
theorem AnalyticOnCompact.eliminateZeros₂
2024-09-10 12:53:34 +02:00
{f : }
{U : Set }
(h₁U : IsPreconnected U)
(h₂U : IsCompact U)
(h₁f : AnalyticOn f U)
(h₂f : ∃ u ∈ U, f u ≠ 0) :
2024-09-10 15:29:30 +02:00
∃ (g : ), AnalyticOn g U ∧ (∀ z ∈ U, g z ≠ 0) ∧ ∀ z, f z = (∏ a ∈ (finiteZeros h₁U h₂U h₁f h₂f).toFinset, (z - a) ^ (h₁f.order a).toNat) • g z := by
let A := (finiteZeros h₁U h₂U h₁f h₂f).toFinset
let n : U → := fun z ↦ (h₁f z z.2).order.toNat
2024-08-20 10:16:37 +02:00
2024-09-10 15:29:30 +02:00
have hn : ∀ a ∈ A, (h₁f a a.2).order = n a := by
intro a _
dsimp [n, AnalyticOn.order]
rw [eq_comm]
apply XX h₁U
exact h₂f
obtain ⟨g, h₁g, h₂g, h₃g⟩ := AnalyticOn.eliminateZeros (A := A) h₁f n hn
use g
have inter : ∀ (z : ), f z = (∏ a ∈ A, (z - ↑a) ^ (h₁f (↑a) a.property).order.toNat) • g z := by
intro z
rw [h₃g z]
constructor
· exact h₁g
· constructor
· intro z h₁z
by_cases h₂z : ⟨z, h₁z⟩ ∈ ↑A.toSet
· exact h₂g ⟨z, h₁z⟩ h₂z
· have : f z ≠ 0 := by
by_contra C
have : ⟨z, h₁z⟩ ∈ ↑A.toSet := by
dsimp [A]
simp
exact C
tauto
rw [inter z] at this
exact right_ne_zero_of_smul this
· exact h₃g
theorem AnalyticOnCompact.eliminateZeros₁
{f : }
{U : Set }
(h₁U : IsPreconnected U)
(h₂U : IsCompact U)
(h₁f : AnalyticOn f U)
(h₂f : ∃ u ∈ U, f u ≠ 0) :
∃ (g : ), AnalyticOn g U ∧ (∀ z ∈ U, g z ≠ 0) ∧ ∀ z, f z = (∏ᶠ a, (z - a) ^ (h₁f.order a).toNat) • g z := by
2024-09-10 14:43:28 +02:00
2024-09-10 11:30:27 +02:00
let A := (finiteZeros h₁U h₂U h₁f h₂f).toFinset
2024-08-20 11:06:24 +02:00
2024-09-10 14:21:08 +02:00
let n : U → := fun z ↦ (h₁f z z.2).order.toNat
2024-08-20 10:16:37 +02:00
2024-08-20 16:56:25 +02:00
have hn : ∀ a ∈ A, (h₁f a a.2).order = n a := by
2024-08-20 17:45:42 +02:00
intro a _
2024-09-10 14:21:08 +02:00
dsimp [n, AnalyticOn.order]
2024-08-20 17:45:42 +02:00
rw [eq_comm]
apply XX h₁U
exact h₂f
2024-08-20 09:14:54 +02:00
2024-08-20 16:56:25 +02:00
obtain ⟨g, h₁g, h₂g, h₃g⟩ := AnalyticOn.eliminateZeros (A := A) h₁f n hn
use g
2024-08-20 17:27:42 +02:00
2024-09-10 14:21:08 +02:00
have inter : ∀ (z : ), f z = (∏ a ∈ A, (z - ↑a) ^ (h₁f (↑a) a.property).order.toNat) • g z := by
2024-08-20 17:27:42 +02:00
intro z
rw [h₃g z]
2024-08-20 09:14:54 +02:00
constructor
2024-08-20 16:56:25 +02:00
· exact h₁g
2024-08-20 09:14:54 +02:00
· constructor
2024-08-20 17:27:42 +02:00
· intro z h₁z
by_cases h₂z : ⟨z, h₁z⟩ ∈ ↑A.toSet
· exact h₂g ⟨z, h₁z⟩ h₂z
· have : f z ≠ 0 := by
by_contra C
have : ⟨z, h₁z⟩ ∈ ↑A.toSet := by
dsimp [A]
simp
2024-09-10 11:30:27 +02:00
exact C
2024-08-20 17:27:42 +02:00
tauto
rw [inter z] at this
exact right_ne_zero_of_smul this
2024-09-10 14:21:08 +02:00
· intro z
2024-09-10 14:43:28 +02:00
2024-09-10 14:21:08 +02:00
let φ : U → := fun a ↦ (z - ↑a) ^ (h₁f.order a).toNat
have hφ : Function.mulSupport φ ⊆ A := by
intro x hx
simp [φ] at hx
have : (h₁f.order x).toNat ≠ 0 := by
2024-09-10 14:43:28 +02:00
by_contra C
rw [C] at hx
simp at hx
simp [A]
exact AnalyticAt.supp_order_toNat (h₁f x x.2) this
2024-09-10 14:21:08 +02:00
rw [finprod_eq_prod_of_mulSupport_subset φ hφ]
rw [inter z]
rfl