124 lines
3.3 KiB
Plaintext
124 lines
3.3 KiB
Plaintext
import Mathlib.Analysis.SpecialFunctions.Integrals
|
||
import Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
|
||
import Mathlib.Analysis.Convex.SpecificFunctions.Deriv
|
||
import Nevanlinna.analyticAt
|
||
import Nevanlinna.divisor
|
||
|
||
open scoped Interval Topology
|
||
open Real Filter MeasureTheory intervalIntegral
|
||
|
||
|
||
|
||
|
||
noncomputable def AnalyticOnNhd.zeroDivisor
|
||
{f : ℂ → ℂ}
|
||
{U : Set ℂ}
|
||
(hf : AnalyticOnNhd ℂ f U) :
|
||
Divisor U where
|
||
|
||
toFun := by
|
||
intro z
|
||
if hz : z ∈ U then
|
||
exact ((hf z hz).order.toNat : ℤ)
|
||
else
|
||
exact 0
|
||
|
||
supportInU := by
|
||
intro z hz
|
||
simp only [Function.mem_support] at hz
|
||
simp only [Function.mem_support, ne_eq, dite_eq_else, Nat.cast_eq_zero, ENat.toNat_eq_zero, not_forall, not_or] at hz
|
||
|
||
|
||
discreteSupport := by
|
||
simp_rw [← singletons_open_iff_discrete]
|
||
simp_rw [Metric.isOpen_singleton_iff]
|
||
simp
|
||
|
||
-- simp only [dite_eq_ite, gt_iff_lt, Subtype.forall, Function.mem_support, ne_eq, ite_eq_else, Classical.not_imp, not_or, Subtype.mk.injEq]
|
||
|
||
intro a ha ⟨h₁a, h₂a⟩
|
||
obtain ⟨g, h₁g, h₂g, h₃g⟩ := (AnalyticAt.order_neq_top_iff (hf a ha)).1 h₂a
|
||
rw [Metric.eventually_nhds_iff_ball] at h₃g
|
||
|
||
have : ∃ ε > 0, ∀ y ∈ Metric.ball (↑a) ε, g y ≠ 0 := by
|
||
have h₄g : ContinuousAt g a :=
|
||
AnalyticAt.continuousAt h₁g
|
||
have : {0}ᶜ ∈ nhds (g a) := 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 hy ⟨h₁y, h₂y⟩ h₃
|
||
|
||
have h'₂y : ↑y ∈ Metric.ball (↑a) ε₂ := by
|
||
simp
|
||
calc dist y a
|
||
_ < min ε₁ ε₂ := by assumption
|
||
_ ≤ ε₂ := by exact min_le_right ε₁ ε₂
|
||
|
||
have h₃y : ↑y ∈ Metric.ball (↑a) ε₁ := by
|
||
simp
|
||
calc dist y a
|
||
_ < min ε₁ ε₂ := by assumption
|
||
_ ≤ ε₁ := by exact min_le_left ε₁ ε₂
|
||
|
||
have F := h₂ε₂ y h'₂y
|
||
have : f y = 0 := by
|
||
rw [AnalyticAt.order_eq_zero_iff (hf y hy)] at h₁y
|
||
tauto
|
||
rw [this] at F
|
||
simp at F
|
||
|
||
have : g y ≠ 0 := by
|
||
exact h₁ε₁.2 y h₃y
|
||
simp [this] at F
|
||
rw [sub_eq_zero] at F
|
||
tauto
|
||
|
||
|
||
theorem AnalyticOnNhd.support_of_zeroDivisor
|
||
{f : ℂ → ℂ}
|
||
{U : Set ℂ}
|
||
(hf : AnalyticOnNhd ℂ f U) :
|
||
Function.support hf.zeroDivisor ⊆ U := by
|
||
|
||
intro z
|
||
contrapose
|
||
intro hz
|
||
dsimp [AnalyticOnNhd.zeroDivisor]
|
||
simp
|
||
tauto
|
||
|
||
|
||
theorem AnalyticOnNhd.support_of_zeroDivisor₂
|
||
{f : ℂ → ℂ}
|
||
{U : Set ℂ}
|
||
(hf : AnalyticOnNhd ℂ f U) :
|
||
Function.support hf.zeroDivisor ⊆ f⁻¹' {0} := by
|
||
|
||
intro z hz
|
||
dsimp [AnalyticOnNhd.zeroDivisor] at hz
|
||
have t₀ := hf.support_of_zeroDivisor hz
|
||
simp [hf.support_of_zeroDivisor hz] at hz
|
||
let A := hz.1
|
||
let C := (hf z t₀).order_eq_zero_iff
|
||
simp
|
||
rw [C] at A
|
||
tauto
|