nevanlinna/Nevanlinna/analyticOn_zeroSet2.lean

450 lines
12 KiB
Plaintext
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

import Mathlib.Analysis.Analytic.Constructions
import Mathlib.Analysis.Analytic.IsolatedZeros
import Mathlib.Analysis.Complex.Basic
theorem AnalyticOn.order_eq_nat_iff
{f : }
{U : Set }
{z₀ : }
(hf : AnalyticOn f U)
(hz₀ : z₀ ∈ U)
(n : ) :
(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
-- 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]
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
-- 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 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
{f : }
{U : Set }
{A : Finset U}
(hf : AnalyticOn f U)
(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
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)]
let φ := fun z ↦ (∏ a ∈ B, (z - a.1) ^ n a.1)
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
obtain ⟨g₁, h₁g₁, h₂g₁, h₃g₁⟩ := (AnalyticOn.order_eq_nat_iff h₁g₀ b₀.2 (n b₀)).1 this
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) :
DiscreteTopology ↑(U ∩ f⁻¹' {0}) := by
simp_rw [← singletons_open_iff_discrete]
simp_rw [Metric.isOpen_singleton_iff]
intro z
let A := XX hU h₁f h₂f z.2.1
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
rw [y.2.2] at F
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) :
Set.Finite ↑(U ∩ f⁻¹' {0}) := by
have hinter : IsCompact ↑(U ∩ f⁻¹' {0}) := by
apply IsCompact.of_isClosed_subset h₂U
apply h₁f.continuousOn.preimage_isClosed_of_isClosed
exact IsCompact.isClosed h₂U
exact isClosed_singleton
exact Set.inter_subset_left
apply hinter.finite
apply DiscreteTopology.of_subset (s := ↑(U ∩ f⁻¹' {0}))
exact discreteZeros h₁U h₁f h₂f
rfl
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 : ) (A : Finset U), AnalyticOn g U ∧ (∀ z ∈ U, g z ≠ 0) ∧ ∀ z, f z = (∏ a ∈ A, (z - a) ^ (h₁f a a.2).order.toNat) • g z := by
let ι : U → := Subtype.val
let A₁ := ι⁻¹' (U ∩ f⁻¹' {0})
have : A₁.Finite := by
apply Set.Finite.preimage
exact Set.injOn_subtype_val
exact finiteZeros h₁U h₂U h₁f h₂f
let A := this.toFinset
let n : := by
intro z
by_cases hz : z ∈ U
· exact (h₁f z hz).order.toNat
· exact 0
have hn : ∀ a ∈ A, (h₁f a a.2).order = n a := by
intro a _
dsimp [n]
simp
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]
congr
funext a
congr
dsimp [n]
simp [a.2]
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₁ := by
dsimp [A₁, ι]
simp
exact C
have : ⟨z, h₁z⟩ ∈ ↑A.toSet := by
dsimp [A]
simp
exact this
tauto
rw [inter z] at this
exact right_ne_zero_of_smul this
· exact inter
noncomputable def AnalyticOn.order
{f : }
{U : Set }
(hf : AnalyticOn f U) :
→ ℕ∞ := by
intro z
if hz : z ∈ U then
exact (hf z hz).order
else
exact 0
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 = (∏ᶠ u, (z - u) ^ (h₁f.order u).toNat) • g z := by
obtain ⟨g, A, h₁g, h₂g, h₃g⟩ := AnalyticOnCompact.eliminateZeros h₁U h₂U h₁f h₂f
use g
constructor
· exact h₁g
· constructor
· exact h₂g
· intro z
rw [h₃g z]
congr
sorry