Working…
This commit is contained in:
Stefan Kebekus
parent
8e5ada9a01
commit
745e614016
|
|
@ -357,6 +357,53 @@ theorem AnalyticOnCompact.eliminateZeros
|
||||||
· exact inter
|
· exact inter
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
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 ∈ (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
|
||||||
|
|
||||||
|
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₁
|
theorem AnalyticOnCompact.eliminateZeros₁
|
||||||
{f : ℂ → ℂ}
|
{f : ℂ → ℂ}
|
||||||
{U : Set ℂ}
|
{U : Set ℂ}
|
||||||
|
|
@ -364,8 +411,7 @@ theorem AnalyticOnCompact.eliminateZeros₁
|
||||||
(h₂U : IsCompact U)
|
(h₂U : IsCompact U)
|
||||||
(h₁f : AnalyticOn ℂ f U)
|
(h₁f : AnalyticOn ℂ f U)
|
||||||
(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, (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
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -1,449 +0,0 @@
|
||||||
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
|
|
||||||
|
|
@ -77,16 +77,29 @@ noncomputable def order
|
||||||
theorem jensen_case_R_eq_one
|
theorem jensen_case_R_eq_one
|
||||||
(f : ℂ → ℂ)
|
(f : ℂ → ℂ)
|
||||||
(h₁f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt f z)
|
(h₁f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt f z)
|
||||||
(h'₁f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, AnalyticAt ℂ f z)
|
(h'₁f : AnalyticOn ℂ f (Metric.closedBall (0 : ℂ) 1))
|
||||||
(h₂f : f 0 ≠ 0) :
|
(h₂f : f 0 ≠ 0) :
|
||||||
log ‖f 0‖ = -∑ s : (ZeroFinset h₁f h₂f), order s * log (‖s.1‖⁻¹) + (2 * π )⁻¹ * ∫ (x : ℝ) in (0)..2 * π, log ‖f (circleMap 0 1 x)‖ := by
|
log ‖f 0‖ = -∑ᶠ s, (h'₁f.order s).toNat * log (‖s.1‖⁻¹) + (2 * π)⁻¹ * ∫ (x : ℝ) in (0)..(2 * π), log ‖f (circleMap 0 1 x)‖ := by
|
||||||
|
|
||||||
have F : ℂ → ℂ := by sorry
|
have h₁U : IsPreconnected (Metric.closedBall (0 : ℂ) 1) := by
|
||||||
have h₁F : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt F z := by sorry
|
apply IsConnected.isPreconnected
|
||||||
have h₂F : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, F z ≠ 0 := by sorry
|
apply Convex.isConnected
|
||||||
have h₃F : f = fun z ↦ (F z) * ∏ s : ZeroFinset h₁f h₂f, (z - s) ^ (order s) := by sorry
|
exact convex_closedBall 0 1
|
||||||
|
exact Set.nonempty_of_nonempty_subtype
|
||||||
|
|
||||||
let G := fun z ↦ log ‖F z‖ + ∑ s : ZeroFinset h₁f h₂f, (order s) * log ‖z - s‖
|
have h₂U : IsCompact (Metric.closedBall (0 : ℂ) 1) := isCompact_closedBall 0 1
|
||||||
|
|
||||||
|
have h'₂f : ∃ u ∈ (Metric.closedBall (0 : ℂ) 1), f u ≠ 0 := by
|
||||||
|
use 0
|
||||||
|
simp
|
||||||
|
exact h₂f
|
||||||
|
|
||||||
|
obtain ⟨F, h₁F, h₂F, h₃F⟩ := AnalyticOnCompact.eliminateZeros₂ h₁U h₂U h'₁f h'₂f
|
||||||
|
|
||||||
|
have h'₁F : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt F z := by
|
||||||
|
sorry
|
||||||
|
|
||||||
|
let G := fun z ↦ log ‖F z‖ + ∑ s ∈ (finiteZeros h₁U h₂U h'₁f h'₂f).toFinset, (h'₁f.order s).toNat * log ‖z - s‖
|
||||||
|
|
||||||
have decompose_f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, f z ≠ 0 → log ‖f z‖ = G z := by
|
have decompose_f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, f z ≠ 0 → log ‖f z‖ = G z := by
|
||||||
intro z h₁z h₂z
|
intro z h₁z h₂z
|
||||||
|
|
@ -95,9 +108,10 @@ theorem jensen_case_R_eq_one
|
||||||
left
|
left
|
||||||
arg 1
|
arg 1
|
||||||
rw [h₃F]
|
rw [h₃F]
|
||||||
|
rw [smul_eq_mul]
|
||||||
rw [norm_mul]
|
rw [norm_mul]
|
||||||
rw [norm_prod]
|
rw [norm_prod]
|
||||||
right
|
left
|
||||||
arg 2
|
arg 2
|
||||||
intro b
|
intro b
|
||||||
rw [norm_pow]
|
rw [norm_pow]
|
||||||
|
|
@ -106,13 +120,15 @@ theorem jensen_case_R_eq_one
|
||||||
rw [Real.log_prod]
|
rw [Real.log_prod]
|
||||||
conv =>
|
conv =>
|
||||||
left
|
left
|
||||||
right
|
left
|
||||||
arg 2
|
arg 2
|
||||||
intro s
|
intro s
|
||||||
rw [Real.log_pow]
|
rw [Real.log_pow]
|
||||||
dsimp [G]
|
dsimp [G]
|
||||||
|
abel
|
||||||
|
|
||||||
-- ∀ x ∈ (ZeroFinset h₁f).attach, Complex.abs (z - ↑x) ^ order x ≠ 0
|
-- ∀ x ∈ (ZeroFinset h₁f).attach, Complex.abs (z - ↑x) ^ order x ≠ 0
|
||||||
|
|
||||||
simp
|
simp
|
||||||
intro s hs
|
intro s hs
|
||||||
rw [ZeroFinset_mem_iff h₁f s] at hs
|
rw [ZeroFinset_mem_iff h₁f s] at hs
|
||||||
|
|
@ -153,6 +169,7 @@ theorem jensen_case_R_eq_one
|
||||||
apply finiteZeros
|
apply finiteZeros
|
||||||
|
|
||||||
-- IsPreconnected (Metric.closedBall (0 : ℂ) 1)
|
-- IsPreconnected (Metric.closedBall (0 : ℂ) 1)
|
||||||
|
|
||||||
apply IsConnected.isPreconnected
|
apply IsConnected.isPreconnected
|
||||||
apply Convex.isConnected
|
apply Convex.isConnected
|
||||||
exact convex_closedBall 0 1
|
exact convex_closedBall 0 1
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue