Compare commits

..

24 Commits

Author SHA1 Message Date
Stefan Kebekus dba4e2d9c4 Rename file 2024-09-13 07:42:57 +02:00
Stefan Kebekus fe0d8a5f5e Delete holomorphic_JensenFormula.lean 2024-09-13 07:42:07 +02:00
Stefan Kebekus 712be956d0 Jensen's formula is done! 2024-09-12 08:56:01 +02:00
Stefan Kebekus 5a984253c6 Update holomorphic_JensenFormula2.lean 2024-09-12 07:52:26 +02:00
Stefan Kebekus 42c1c14edf Delete diffOpGrothendieck.lean 2024-09-12 07:13:35 +02:00
Stefan Kebekus b988031047 Update analyticAt.lean 2024-09-12 07:12:03 +02:00
Stefan Kebekus dbea68061b Update analyticAt.lean 2024-09-12 07:04:00 +02:00
Stefan Kebekus f83f772506 Update analyticAt.lean 2024-09-12 06:58:43 +02:00
Stefan Kebekus dbeb631178 Update analyticAt.lean 2024-09-11 16:57:16 +02:00
Stefan Kebekus 1e8c5bad0f working 2024-09-11 15:48:43 +02:00
Stefan Kebekus b91e3677c0 Update holomorphic_JensenFormula2.lean 2024-09-11 11:09:03 +02:00
Stefan Kebekus 47e1bfe35e working 2024-09-11 11:06:45 +02:00
Stefan Kebekus 6651c0852a Working… 2024-09-11 10:24:45 +02:00
Stefan Kebekus 3bead7a9bf Update holomorphic_JensenFormula2.lean 2024-09-11 09:07:49 +02:00
Stefan Kebekus e901f241cc Working… 2024-09-10 16:50:29 +02:00
Stefan Kebekus 745e614016 Working… 2024-09-10 15:29:30 +02:00
Stefan Kebekus 8e5ada9a01 working… 2024-09-10 14:43:28 +02:00
Stefan Kebekus ef7e1df191 Working… 2024-09-10 14:21:08 +02:00
Stefan Kebekus fa2e431f4c Update analyticOn_zeroSet.lean 2024-09-10 12:53:34 +02:00
Stefan Kebekus f732c82f92 Update analyticOn_zeroSet.lean 2024-09-10 11:30:27 +02:00
Stefan Kebekus cd58c18a78 Update analyticOn_zeroSet.lean 2024-09-10 11:21:49 +02:00
Stefan Kebekus 5dc437751b Update analyticOn_zeroSet.lean 2024-09-10 11:06:00 +02:00
Stefan Kebekus aa79fdb9eb Update analyticOn_zeroSet.lean 2024-09-10 10:55:53 +02:00
Stefan Kebekus e41a08f1d5 Create analyticAt.lean 2024-09-10 10:45:53 +02:00
8 changed files with 828 additions and 984 deletions

226
Nevanlinna/analyticAt.lean Normal file
View File

@ -0,0 +1,226 @@
import Mathlib.Analysis.Analytic.IsolatedZeros
import Mathlib.Analysis.Complex.Basic
import Mathlib.Analysis.Analytic.Linear
theorem AnalyticAt.order_mul
{f₁ f₂ : }
{z₀ : }
(hf₁ : AnalyticAt f₁ z₀)
(hf₂ : AnalyticAt f₂ z₀) :
(hf₁.mul 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 AnalyticAt.order_eq_zero_iff
{f : }
{z₀ : }
(hf : AnalyticAt f z₀) :
hf.order = 0 ↔ f z₀ ≠ 0 := by
have : (0 : ENat) = (0 : Nat) := by rfl
rw [this, AnalyticAt.order_eq_nat_iff hf 0]
constructor
· intro hz
obtain ⟨g, _, h₂g, h₃g⟩ := hz
simp at h₃g
rw [Filter.Eventually.self_of_nhds h₃g]
tauto
· intro hz
use f
constructor
· exact hf
· constructor
· exact hz
· simp
theorem AnalyticAt.order_pow
{f : }
{z₀ : }
{n : }
(hf : AnalyticAt f z₀) :
(hf.pow n).order = n * hf.order := by
induction' n with n hn
· simp; rw [AnalyticAt.order_eq_zero_iff]; simp
· simp
simp_rw [add_mul, pow_add]
simp
rw [AnalyticAt.order_mul (hf.pow n) hf]
rw [hn]
theorem AnalyticAt.supp_order_toNat
{f : }
{z₀ : }
(hf : AnalyticAt f z₀) :
hf.order.toNat ≠ 0 → f z₀ = 0 := by
contrapose
intro h₁f
simp [hf.order_eq_zero_iff.2 h₁f]
theorem ContinuousLinearEquiv.analyticAt
( : ≃L[] ) (z₀ : ) : AnalyticAt (⇑ℓ) z₀ := .toContinuousLinearMap.analyticAt z₀
theorem eventually_nhds_comp_composition
{f₁ f₂ : }
{z₀ : }
(hf : ∀ᶠ (z : ) in nhds ( z₀), f₁ z = f₂ z)
(h : Continuous ) :
∀ᶠ (z : ) in nhds z₀, (f₁ ∘ ) z = (f₂ ∘ ) z := by
obtain ⟨t, h₁t, h₂t, h₃t⟩ := eventually_nhds_iff.1 hf
apply eventually_nhds_iff.2
use ℓ⁻¹' t
constructor
· intro y hy
exact h₁t ( y) hy
· constructor
· apply IsOpen.preimage
exact h
exact h₂t
· exact h₃t
theorem AnalyticAt.order_congr
{f₁ f₂ : }
{z₀ : }
(hf₁ : AnalyticAt f₁ z₀)
(hf : f₁ =ᶠ[nhds z₀] f₂) :
hf₁.order = (hf₁.congr hf).order := by
by_cases h₁f₁ : hf₁.order =
rw [h₁f₁, eq_comm, AnalyticAt.order_eq_top_iff]
rw [AnalyticAt.order_eq_top_iff] at h₁f₁
exact Filter.EventuallyEq.rw h₁f₁ (fun x => Eq (f₂ x)) (id (Filter.EventuallyEq.symm hf))
--
let n := hf₁.order.toNat
have hn : hf₁.order = n := Eq.symm (ENat.coe_toNat h₁f₁)
rw [hn, eq_comm, AnalyticAt.order_eq_nat_iff]
rw [AnalyticAt.order_eq_nat_iff] at hn
obtain ⟨g, h₁g, h₂g, h₃g⟩ := hn
use g
constructor
· assumption
· constructor
· assumption
· exact Filter.EventuallyEq.rw h₃g (fun x => Eq (f₂ x)) (id (Filter.EventuallyEq.symm hf))
theorem AnalyticAt.order_comp_CLE
( : ≃L[] )
{f : }
{z₀ : }
(hf : AnalyticAt f ( z₀)) :
hf.order = (hf.comp (.analyticAt z₀)).order := by
by_cases h₁f : hf.order =
· rw [h₁f]
rw [AnalyticAt.order_eq_top_iff] at h₁f
let A := eventually_nhds_comp_composition h₁f .continuous
simp at A
rw [AnalyticAt.order_congr (hf.comp (.analyticAt z₀)) A]
have : AnalyticAt (0 : ) z₀ := by
apply analyticAt_const
have : this.order = := by
rw [AnalyticAt.order_eq_top_iff]
simp
rw [this]
· let n := hf.order.toNat
have hn : hf.order = n := Eq.symm (ENat.coe_toNat h₁f)
rw [hn]
rw [AnalyticAt.order_eq_nat_iff] at hn
obtain ⟨g, h₁g, h₂g, h₃g⟩ := hn
have A := eventually_nhds_comp_composition h₃g .continuous
have t₁ : AnalyticAt (fun z => z - z₀) z₀ := by
apply AnalyticAt.sub
exact ContinuousLinearEquiv.analyticAt z₀
exact analyticAt_const
have t₀ : AnalyticAt (fun z => ( z - z₀) ^ n) z₀ := by
exact pow t₁ n
have : AnalyticAt (fun z ↦ ( z - z₀) ^ n • g ( z) : ) z₀ := by
apply AnalyticAt.mul
exact t₀
apply AnalyticAt.comp h₁g
exact ContinuousLinearEquiv.analyticAt z₀
rw [AnalyticAt.order_congr (hf.comp (.analyticAt z₀)) A]
simp
rw [AnalyticAt.order_mul t₀ ((h₁g.comp (.analyticAt z₀)))]
have : t₁.order = (1 : ) := by
rw [AnalyticAt.order_eq_nat_iff]
use (fun _ ↦ 1)
simp
constructor
· exact analyticAt_const
· apply Filter.Eventually.of_forall
intro x
calc x - z₀
_ = (x - z₀) := by
exact Eq.symm (ContinuousLinearEquiv.map_sub x z₀)
_ = ((x - z₀) * 1) := by
simp
_ = (x - z₀) * 1 := by
rw [← smul_eq_mul, ← smul_eq_mul]
exact ContinuousLinearEquiv.map_smul (x - z₀) 1
have : t₀.order = n := by
rw [AnalyticAt.order_pow t₁, this]
simp
rw [this]
have : (comp h₁g (ContinuousLinearEquiv.analyticAt z₀)).order = 0 := by
rwa [AnalyticAt.order_eq_zero_iff]
rw [this]
simp

View File

@ -1,21 +1,25 @@
import Mathlib.Analysis.Analytic.Constructions
import Mathlib.Analysis.Analytic.IsolatedZeros
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
{f : }
{U : Set }
{z₀ : }
{z₀ : U}
(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
hf.order z₀ = ↑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
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
-- 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
intro hz₁
rw [eventually_nhds_iff]
use {z₀}ᶜ
use {z₀.1}ᶜ
constructor
· intro y hy
simp at hy
@ -87,59 +91,20 @@ theorem AnalyticOn.order_eq_nat_iff
-- direction ←
intro h
obtain ⟨g, h₁g, h₂g, h₃g⟩ := h
dsimp [AnalyticOn.order]
rw [AnalyticAt.order_eq_nat_iff]
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.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]
theorem AnalyticOn.eliminateZeros
@ -147,8 +112,8 @@ theorem AnalyticOn.eliminateZeros
{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
(n : U) :
(∀ 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)
@ -167,7 +132,7 @@ theorem AnalyticOn.eliminateZeros
rw [← hBinsert b₀ (Finset.mem_insert_self b₀ B)]
let φ := fun z ↦ (∏ a ∈ B, (z - a.1) ^ n a.1)
let φ := fun z ↦ (∏ a ∈ B, (z - a.1) ^ n a)
have : f = fun z ↦ φ z * g₀ z := by
funext z
@ -208,8 +173,7 @@ theorem AnalyticOn.eliminateZeros
rw [h₂φ]
simp
obtain ⟨g₁, h₁g₁, h₂g₁, h₃g₁⟩ := (AnalyticOn.order_eq_nat_iff h₁g₀ b₀.2 (n b₀)).1 this
obtain ⟨g₁, h₁g₁, h₂g₁, h₃g₁⟩ := (AnalyticOn.order_eq_nat_iff h₁g₀ (n b₀)).1 this
use g₁
constructor
@ -259,14 +223,14 @@ theorem discreteZeros
(hU : IsPreconnected U)
(h₁f : AnalyticOn f U)
(h₂f : ∃ u ∈ U, f u ≠ 0) :
DiscreteTopology ↑(U ∩ f⁻¹' {0}) := by
DiscreteTopology ((U.restrict 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
let A := XX hU h₁f h₂f z.1.2
rw [eq_comm] at A
rw [AnalyticAt.order_eq_nat_iff] at A
obtain ⟨g, h₁g, h₂g, h₃g⟩ := A
@ -311,9 +275,9 @@ theorem discreteZeros
_ < min ε₁ ε₂ := by assumption
_ ≤ ε₁ := by exact min_le_left ε₁ ε₂
have F := h₂ε₂ y.1 h₂y
rw [y.2.2] at F
have : f y = 0 := by exact y.2
rw [this] at F
simp at F
have : g y.1 ≠ 0 := by
@ -331,19 +295,19 @@ theorem finiteZeros
(h₂U : IsCompact U)
(h₁f : AnalyticOn f U)
(h₂f : ∃ u ∈ U, f u ≠ 0) :
Set.Finite ↑(U ∩ f⁻¹' {0}) := by
Set.Finite (U.restrict 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
have closedness : IsClosed (U.restrict f⁻¹' {0}) := by
apply IsClosed.preimage
apply continuousOn_iff_continuous_restrict.1
exact h₁f.continuousOn
exact isClosed_singleton
exact Set.inter_subset_left
apply hinter.finite
apply DiscreteTopology.of_subset (s := ↑(U ∩ f⁻¹' {0}))
have : CompactSpace U := by
exact isCompact_iff_compactSpace.mp h₂U
apply (IsClosed.isCompact closedness).finite
exact discreteZeros h₁U h₁f h₂f
rfl
theorem AnalyticOnCompact.eliminateZeros
@ -353,32 +317,20 @@ theorem AnalyticOnCompact.eliminateZeros
(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
∃ (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 ι : U → := Subtype.val
let A := (finiteZeros h₁U h₂U h₁f h₂f).toFinset
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
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]
simp
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
@ -386,11 +338,6 @@ theorem AnalyticOnCompact.eliminateZeros
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
@ -400,15 +347,115 @@ theorem AnalyticOnCompact.eliminateZeros
· 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
exact C
tauto
rw [inter z] at this
exact right_ne_zero_of_smul this
· 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₁
{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
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
· intro z
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
by_contra C
rw [C] at hx
simp at hx
simp [A]
exact AnalyticAt.supp_order_toNat (h₁f x x.2) this
rw [finprod_eq_prod_of_mulSupport_subset φ hφ]
rw [inter z]
rfl

View File

@ -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

View File

@ -1,9 +0,0 @@
import Mathlib.Analysis.Calculus.ContDiff.Basic
import Mathlib.Analysis.InnerProductSpace.PiL2
/-
Here we would like to define differential operators, following EGA 4-1, §20.
This is work to be done in the future.
-/

View File

@ -125,6 +125,23 @@ theorem HolomorphicAt.analyticAt
exact IsOpen.mem_nhds h₁s h₂s
theorem AnalyticAt.holomorphicAt
[CompleteSpace F]
{f : → F}
{x : } :
AnalyticAt f x → HolomorphicAt f x := by
intro hf
rw [HolomorphicAt_iff]
use {x : | AnalyticAt f x}
constructor
· exact isOpen_analyticAt f
· constructor
· simpa
· intro z hz
simp at hz
exact differentiableAt hz
theorem HolomorphicAt.contDiffAt
[CompleteSpace F]
{f : → F}

View File

@ -1,172 +1,449 @@
import Mathlib.Analysis.Complex.CauchyIntegral
import Mathlib.Analysis.Analytic.IsolatedZeros
import Nevanlinna.analyticOn_zeroSet
import Nevanlinna.harmonicAt_examples
import Nevanlinna.harmonicAt_meanValue
import Nevanlinna.specialFunctions_CircleIntegral_affine
open Real
theorem jensen_case_R_eq_one
(f : )
(h₁f : ∀ z ∈ Metric.closedBall (0 : ) 1, HolomorphicAt f z)
(h₂f : f 0 ≠ 0)
(S : Finset )
(a : S → )
(ha : ∀ s, a s ∈ Metric.ball 0 1)
(F : )
(h₁F : ∀ z ∈ Metric.closedBall (0 : ) 1, HolomorphicAt F z)
(h₂F : ∀ z ∈ Metric.closedBall (0 : ) 1, F z ≠ 0)
(h₃F : f = fun z ↦ (F z) * ∏ s : S, (z - a s)) :
Real.log ‖f 0‖ = -∑ s, Real.log (‖a s‖⁻¹) + (2 * Real.pi)⁻¹ * ∫ (x : ) in (0)..2 * Real.pi, Real.log ‖f (circleMap 0 1 x)‖ := by
(h₁f : AnalyticOn f (Metric.closedBall 0 1))
(h₂f : f 0 ≠ 0) :
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 h₁U : IsPreconnected (Metric.closedBall (0 : ) 1) := by sorry
have h₂U : IsCompact (Metric.closedBall (0 : ) 1) := by sorry
have h₁f : AnalyticOn f (Metric.closedBall (0 : ) 1) := by sorry
have h₂f : ∃ u ∈ (Metric.closedBall (0 : ) 1), f u ≠ 0 := by sorry
have h₁U : IsPreconnected (Metric.closedBall (0 : ) 1) :=
(convex_closedBall (0 : ) 1).isPreconnected
let α := AnalyticOnCompact.eliminateZeros h₁U h₂U h₁f h₂f
obtain ⟨g, A, h'₁g, h₂g, h₃g⟩ := α
have h₁g : ∀ z ∈ Metric.closedBall 0 1, HolomorphicAt F z := by sorry
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
let logAbsF := fun w ↦ Real.log ‖F w‖
have h'₁F : ∀ z ∈ Metric.closedBall (0 : ) 1, HolomorphicAt F z := by
intro z h₁z
apply AnalyticAt.holomorphicAt
exact h₁F z h₁z
have t₀ : ∀ z ∈ Metric.closedBall 0 1, HarmonicAt logAbsF z := by
intro z hz
apply logabs_of_holomorphicAt_is_harmonic
apply h₁F z hz
exact h₂F z hz
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 t₁ : (∫ (x : ) in (0)..2 * Real.pi, logAbsF (circleMap 0 1 x)) = 2 * Real.pi * logAbsF 0 := by
apply harmonic_meanValue₁ 1 Real.zero_lt_one t₀
have t₂ : ∀ s, f (a s) = 0 := by
intro s
rw [h₃F]
simp
right
apply Finset.prod_eq_zero_iff.2
use s
simp
let logAbsf := fun w ↦ Real.log ‖f w‖
have s₀ : ∀ z ∈ Metric.closedBall (0 : ) 1, f z ≠ 0 → logAbsf z = logAbsF z + ∑ s, Real.log ‖z - a s‖ := by
have decompose_f : ∀ z ∈ Metric.closedBall (0 : ) 1, f z ≠ 0 → log ‖f z‖ = G z := by
intro z h₁z h₂z
dsimp [logAbsf]
rw [h₃F]
simp_rw [Complex.abs.map_mul]
rw [Complex.abs_prod]
conv =>
left
arg 1
rw [h₃F]
rw [smul_eq_mul]
rw [norm_mul]
rw [norm_prod]
left
arg 2
intro b
rw [norm_pow]
simp only [Complex.norm_eq_abs, Finset.univ_eq_attach]
rw [Real.log_mul]
rw [Real.log_prod]
rfl
intro s hs
simp
by_contra ha'
rw [ha'] at h₂z
exact h₂z (t₂ s)
conv =>
left
left
arg 2
intro s
rw [Real.log_pow]
dsimp [G]
abel
-- ∀ x ∈ ⋯.toFinset, Complex.abs (z - ↑x) ^ (h'₁f.order x).toNat ≠ 0
have : ∀ x ∈ (finiteZeros h₁U h₂U h₁f h'₂f).toFinset, Complex.abs (z - ↑x) ^ (h₁f.order x).toNat ≠ 0 := by
intro s hs
simp at hs
simp
intro h₂s
rw [h₂s] at h₂z
tauto
exact this
-- ∏ x ∈ ⋯.toFinset, Complex.abs (z - ↑x) ^ (h'₁f.order x).toNat ≠ 0
have : ∀ x ∈ (finiteZeros h₁U h₂U h₁f h'₂f).toFinset, Complex.abs (z - ↑x) ^ (h₁f.order x).toNat ≠ 0 := by
intro s hs
simp at hs
simp
intro h₂s
rw [h₂s] at h₂z
tauto
rw [Finset.prod_ne_zero_iff]
exact this
-- Complex.abs (F z) ≠ 0
simp
exact h₂F z h₁z
-- ∏ I : { x // x ∈ S }, Complex.abs (z - a I) ≠ 0
by_contra h'
obtain ⟨s, h's, h''⟩ := Finset.prod_eq_zero_iff.1 h'
simp at h''
rw [h''] at h₂z
let A := t₂ s
exact h₂z A
have s₁ : ∀ z ∈ Metric.closedBall (0 : ) 1, f z ≠ 0 → logAbsF z = logAbsf z - ∑ s, Real.log ‖z - a s‖ := by
intro z h₁z h₂z
rw [s₀ z h₁z]
have int_logAbs_f_eq_int_G : ∫ (x : ) in (0)..2 * π, log ‖f (circleMap 0 1 x)‖ = ∫ (x : ) in (0)..2 * π, G (circleMap 0 1 x) := by
rw [intervalIntegral.integral_congr_ae]
rw [MeasureTheory.ae_iff]
apply Set.Countable.measure_zero
simp
assumption
have : 0 ∈ Metric.closedBall (0 : ) 1 := by simp
rw [s₁ 0 this h₂f] at t₁
have t₀ : {a | a ∈ Ι 0 (2 * π) ∧ ¬log ‖f (circleMap 0 1 a)‖ = G (circleMap 0 1 a)}
⊆ (circleMap 0 1)⁻¹' (Metric.closedBall 0 1 ∩ f⁻¹' {0}) := by
intro a ha
simp at ha
simp
by_contra C
have : (circleMap 0 1 a) ∈ Metric.closedBall 0 1 :=
circleMap_mem_closedBall 0 (zero_le_one' ) a
exact ha.2 (decompose_f (circleMap 0 1 a) this C)
have h₀ {x : } : f (circleMap 0 1 x) ≠ 0 := by
rw [h₃F]
apply Set.Countable.mono t₀
apply Set.Countable.preimage_circleMap
apply Set.Finite.countable
let A := finiteZeros h₁U h₂U h₁f h'₂f
have : (Metric.closedBall 0 1 ∩ f ⁻¹' {0}) = (Metric.closedBall 0 1).restrict f ⁻¹' {0} := by
ext z
simp
tauto
rw [this]
exact Set.Finite.image Subtype.val A
exact Ne.symm (zero_ne_one' )
have decompose_int_G : ∫ (x : ) in (0)..2 * π, G (circleMap 0 1 x)
= (∫ (x : ) in (0)..2 * π, log (Complex.abs (F (circleMap 0 1 x))))
+ ∑ x ∈ (finiteZeros h₁U h₂U h₁f h'₂f).toFinset, (h₁f.order x).toNat * ∫ (x_1 : ) in (0)..2 * π, log (Complex.abs (circleMap 0 1 x_1 - ↑x)) := by
dsimp [G]
rw [intervalIntegral.integral_add]
rw [intervalIntegral.integral_finset_sum]
simp_rw [intervalIntegral.integral_const_mul]
-- ∀ i ∈ (finiteZeros h₁U h₂U h'₁f h'₂f).toFinset,
-- IntervalIntegrable (fun x => (h'₁f.order i).toNat *
-- log (Complex.abs (circleMap 0 1 x - ↑i))) MeasureTheory.volume 0 (2 * π)
intro i _
apply IntervalIntegrable.const_mul
--simp at this
by_cases h₂i : ‖i.1‖ = 1
-- case pos
exact int'₂ h₂i
-- case neg
apply Continuous.intervalIntegrable
apply continuous_iff_continuousAt.2
intro x
have : (fun x => log (Complex.abs (circleMap 0 1 x - ↑i))) = log ∘ Complex.abs ∘ (fun x ↦ circleMap 0 1 x - ↑i) :=
rfl
rw [this]
apply ContinuousAt.comp
apply Real.continuousAt_log
simp
constructor
· have : (circleMap 0 1 x) ∈ Metric.closedBall (0 : ) 1 := by simp
exact h₂F (circleMap 0 1 x) this
· by_contra h'
obtain ⟨s, _, h₂s⟩ := Finset.prod_eq_zero_iff.1 h'
have : circleMap 0 1 x = a s := by
rw [← sub_zero (circleMap 0 1 x)]
nth_rw 2 [← h₂s]
simp
let A := ha s
rw [← this] at A
simp at A
have {θ} : (circleMap 0 1 θ) ∈ Metric.closedBall (0 : ) 1 := by simp
simp_rw [s₁ (circleMap 0 1 _) this h₀] at t₁
rw [intervalIntegral.integral_sub] at t₁
rw [intervalIntegral.integral_finset_sum] at t₁
by_contra ha'
conv at h₂i =>
arg 1
rw [← ha']
rw [Complex.norm_eq_abs]
rw [abs_circleMap_zero 1 x]
simp
tauto
apply ContinuousAt.comp
apply Complex.continuous_abs.continuousAt
fun_prop
-- IntervalIntegrable (fun x => log (Complex.abs (F (circleMap 0 1 x)))) MeasureTheory.volume 0 (2 * π)
apply Continuous.intervalIntegrable
apply continuous_iff_continuousAt.2
intro x
have : (fun x => log (Complex.abs (F (circleMap 0 1 x)))) = log ∘ Complex.abs ∘ F ∘ (fun x ↦ circleMap 0 1 x) :=
rfl
rw [this]
apply ContinuousAt.comp
apply Real.continuousAt_log
simp [h₂F]
-- ContinuousAt (⇑Complex.abs ∘ F ∘ fun x => circleMap 0 1 x) x
apply ContinuousAt.comp
apply Complex.continuous_abs.continuousAt
apply ContinuousAt.comp
apply DifferentiableAt.continuousAt (𝕜 := )
apply HolomorphicAt.differentiableAt
simp [h'₁F]
-- ContinuousAt (fun x => circleMap 0 1 x) x
apply Continuous.continuousAt
apply continuous_circleMap
simp_rw [int₀ (ha _)] at t₁
simp at t₁
rw [t₁]
have : (fun x => ∑ s ∈ (finiteZeros h₁U h₂U h₁f h'₂f).toFinset, (h₁f.order s).toNat * log (Complex.abs (circleMap 0 1 x - ↑s)))
= ∑ s ∈ (finiteZeros h₁U h₂U h₁f h'₂f).toFinset, (fun x => (h₁f.order s).toNat * log (Complex.abs (circleMap 0 1 x - ↑s))) := by
funext x
simp
rw [this]
apply IntervalIntegrable.sum
intro i _
apply IntervalIntegrable.const_mul
--have : i.1 ∈ Metric.closedBall (0 : ) 1 := i.2
--simp at this
by_cases h₂i : ‖i.1‖ = 1
-- case pos
exact int'₂ h₂i
-- case neg
--have : i.1 ∈ Metric.ball (0 : ) 1 := by sorry
apply Continuous.intervalIntegrable
apply continuous_iff_continuousAt.2
intro x
have : (fun x => log (Complex.abs (circleMap 0 1 x - ↑i))) = log ∘ Complex.abs ∘ (fun x ↦ circleMap 0 1 x - ↑i) :=
rfl
rw [this]
apply ContinuousAt.comp
apply Real.continuousAt_log
simp
by_contra ha'
conv at h₂i =>
arg 1
rw [← ha']
rw [Complex.norm_eq_abs]
rw [abs_circleMap_zero 1 x]
simp
tauto
apply ContinuousAt.comp
apply Complex.continuous_abs.continuousAt
fun_prop
have t₁ : (∫ (x : ) in (0)..2 * Real.pi, log ‖F (circleMap 0 1 x)‖) = 2 * Real.pi * log ‖F 0‖ := by
let logAbsF := fun w ↦ Real.log ‖F w‖
have t₀ : ∀ z ∈ Metric.closedBall 0 1, HarmonicAt logAbsF z := by
intro z hz
apply logabs_of_holomorphicAt_is_harmonic
apply h'₁F z hz
exact h₂F z hz
apply harmonic_meanValue₁ 1 Real.zero_lt_one t₀
simp_rw [← Complex.norm_eq_abs] at decompose_int_G
rw [t₁] at decompose_int_G
conv at decompose_int_G =>
right
right
arg 2
intro x
right
rw [int₃ x.2]
simp at decompose_int_G
rw [int_logAbs_f_eq_int_G]
rw [decompose_int_G]
rw [h₃F]
simp
have {w : } : Real.pi⁻¹ * 2⁻¹ * (2 * Real.pi * w) = w := by
ring_nf
simp [mul_inv_cancel₀ Real.pi_ne_zero]
have {l : } : π⁻¹ * 2⁻¹ * (2 * π * l) = l := by
calc π⁻¹ * 2⁻¹ * (2 * π * l)
_ = π⁻¹ * (2⁻¹ * 2) * π * l := by ring
_ = π⁻¹ * π * l := by ring
_ = (π⁻¹ * π) * l := by ring
_ = 1 * l := by
rw [inv_mul_cancel₀]
exact pi_ne_zero
_ = l := by simp
rw [this]
rw [log_mul]
rw [log_prod]
simp
rfl
-- ∀ i ∈ Finset.univ, IntervalIntegrable (fun x => Real.log ‖circleMap 0 1 x - a i‖) MeasureTheory.volume 0 (2 * Real.pi)
intro i _
apply Continuous.intervalIntegrable
apply continuous_iff_continuousAt.2
intro x
have : (fun x => Real.log ‖circleMap 0 1 x - a i‖) = Real.log ∘ Complex.abs ∘ (fun x ↦ circleMap 0 1 x - a i) :=
rfl
rw [this]
apply ContinuousAt.comp
apply Real.continuousAt_log
rw [finsum_eq_sum_of_support_subset _ (s := (finiteZeros h₁U h₂U h₁f h'₂f).toFinset)]
simp
by_contra ha'
let A := ha i
rw [← ha'] at A
simp
intro x ⟨h₁x, _⟩
simp
dsimp [AnalyticOn.order] at h₁x
simp only [Function.mem_support, ne_eq, Nat.cast_eq_zero, not_or] at h₁x
exact AnalyticAt.supp_order_toNat (AnalyticOn.order.proof_1 h₁f x) h₁x
--
intro x hx
simp at hx
simp
intro h₁x
nth_rw 1 [← h₁x] at h₂f
tauto
--
rw [Finset.prod_ne_zero_iff]
intro x hx
simp at hx
simp
intro h₁x
nth_rw 1 [← h₁x] at h₂f
tauto
--
simp
apply h₂F
simp
lemma const_mul_circleMap_zero
{R θ : } :
circleMap 0 R θ = R * circleMap 0 1 θ := by
rw [circleMap_zero, circleMap_zero]
simp
theorem jensen
{R : }
(hR : 0 < R)
(f : )
(h₁f : AnalyticOn f (Metric.closedBall 0 R))
(h₂f : f 0 ≠ 0) :
log ‖f 0‖ = -∑ᶠ s, (h₁f.order s).toNat * log (R * ‖s.1‖⁻¹) + (2 * π)⁻¹ * ∫ (x : ) in (0)..(2 * π), log ‖f (circleMap 0 R x)‖ := by
let : ≃L[] :=
{
toFun := fun x ↦ R * x
map_add' := fun x y => DistribSMul.smul_add R x y
map_smul' := fun m x => mul_smul_comm m (↑R) x
invFun := fun x ↦ R⁻¹ * x
left_inv := by
intro x
simp
rw [← mul_assoc, mul_comm, inv_mul_cancel₀, mul_one]
simp
exact ne_of_gt hR
right_inv := by
intro x
simp
rw [← mul_assoc, mul_inv_cancel₀, one_mul]
simp
exact ne_of_gt hR
continuous_toFun := continuous_const_smul R
continuous_invFun := continuous_const_smul R⁻¹
}
let F := f ∘
have h₁F : AnalyticOn F (Metric.closedBall 0 1) := by
apply AnalyticOn.comp (t := Metric.closedBall 0 R)
exact h₁f
intro x _
apply .toContinuousLinearMap.analyticAt x
intro x hx
have : x = R * x := by rfl
rw [this]
simp
simp at hx
rw [abs_of_pos hR]
calc R * Complex.abs x
_ ≤ R * 1 := by exact (mul_le_mul_iff_of_pos_left hR).mpr hx
_ = R := by simp
have h₂F : F 0 ≠ 0 := by
dsimp [F]
have : 0 = R * 0 := by rfl
rw [this]
simpa
let A := jensen_case_R_eq_one F h₁F h₂F
dsimp [F] at A
have {x : } : x = R * x := by rfl
repeat
simp_rw [this] at A
simp at A
apply ContinuousAt.comp
apply Complex.continuous_abs.continuousAt
fun_prop
-- IntervalIntegrable (fun x => logAbsf (circleMap 0 1 x)) MeasureTheory.volume 0 (2 * Real.pi)
apply Continuous.intervalIntegrable
apply continuous_iff_continuousAt.2
simp
rw [A]
simp_rw [← const_mul_circleMap_zero]
simp
let e : (Metric.closedBall (0 : ) 1) → (Metric.closedBall (0 : ) R) := by
intro ⟨x, hx⟩
have hy : R • x ∈ Metric.closedBall (0 : ) R := by
simp
simp at hx
have : R = |R| := by exact Eq.symm (abs_of_pos hR)
rw [← this]
norm_num
calc R * Complex.abs x
_ ≤ R * 1 := by exact (mul_le_mul_iff_of_pos_left hR).mpr hx
_ = R := by simp
exact ⟨R • x, hy⟩
let e' : (Metric.closedBall (0 : ) R) → (Metric.closedBall (0 : ) 1) := by
intro ⟨x, hx⟩
have hy : R⁻¹ • x ∈ Metric.closedBall (0 : ) 1 := by
simp
simp at hx
have : R = |R| := by exact Eq.symm (abs_of_pos hR)
rw [← this]
norm_num
calc R⁻¹ * Complex.abs x
_ ≤ R⁻¹ * R := by
apply mul_le_mul_of_nonneg_left hx
apply inv_nonneg.mpr
exact abs_eq_self.mp (id (Eq.symm this))
_ = 1 := by
apply inv_mul_cancel₀
exact Ne.symm (ne_of_lt hR)
exact ⟨R⁻¹ • x, hy⟩
apply finsum_eq_of_bijective e
apply Function.bijective_iff_has_inverse.mpr
use e'
constructor
· apply Function.leftInverse_iff_comp.mpr
funext x
dsimp only [e, e', id_eq, eq_mp_eq_cast, Function.comp_apply]
conv =>
left
arg 1
rw [← smul_assoc, smul_eq_mul]
rw [inv_mul_cancel₀ (Ne.symm (ne_of_lt hR))]
rw [one_smul]
· apply Function.rightInverse_iff_comp.mpr
funext x
dsimp only [e, e', id_eq, eq_mp_eq_cast, Function.comp_apply]
conv =>
left
arg 1
rw [← smul_assoc, smul_eq_mul]
rw [mul_inv_cancel₀ (Ne.symm (ne_of_lt hR))]
rw [one_smul]
intro x
have : (fun x => logAbsf (circleMap 0 1 x)) = Real.log ∘ Complex.abs ∘ f ∘ (fun x ↦ circleMap 0 1 x) :=
rfl
rw [this]
apply ContinuousAt.comp
simp
exact h₀
apply ContinuousAt.comp
apply Complex.continuous_abs.continuousAt
apply ContinuousAt.comp
apply ContDiffAt.continuousAt (f := f) (𝕜 := ) (n := 1)
apply HolomorphicAt.contDiffAt
apply h₁f
by_cases hx : x = (0 : )
rw [hx]
simp
let A := continuous_circleMap 0 1
apply A.continuousAt
-- IntervalIntegrable (fun x => ∑ s : { x // x ∈ S }, Real.log ‖circleMap 0 1 x - a s‖) MeasureTheory.volume 0 (2 * Real.pi)
apply Continuous.intervalIntegrable
apply continuous_finset_sum
intro i _
apply continuous_iff_continuousAt.2
intro x
have : (fun x => Real.log ‖circleMap 0 1 x - a i‖) = Real.log ∘ Complex.abs ∘ (fun x ↦ circleMap 0 1 x - a i) :=
rfl
rw [this]
apply ContinuousAt.comp
apply Real.continuousAt_log
rw [log_mul, log_mul, log_inv, log_inv]
have : R = |R| := by exact Eq.symm (abs_of_pos hR)
rw [← this]
simp
by_contra ha'
let A := ha i
rw [← ha'] at A
simp at A
apply ContinuousAt.comp
apply Complex.continuous_abs.continuousAt
fun_prop
left
congr 1
dsimp [AnalyticOn.order]
rw [← AnalyticAt.order_comp_CLE ]
--
simpa
--
have : R = |R| := by exact Eq.symm (abs_of_pos hR)
rw [← this]
apply inv_ne_zero
exact Ne.symm (ne_of_lt hR)
--
exact Ne.symm (ne_of_lt hR)
--
simp
constructor
· assumption
· exact Ne.symm (ne_of_lt hR)

View File

@ -1,287 +0,0 @@
import Mathlib.Analysis.Complex.CauchyIntegral
import Mathlib.Analysis.Analytic.IsolatedZeros
import Nevanlinna.analyticOn_zeroSet
import Nevanlinna.harmonicAt_examples
import Nevanlinna.harmonicAt_meanValue
import Nevanlinna.specialFunctions_CircleIntegral_affine
open Real
noncomputable def Zeroset
{f : }
{s : Set }
(hf : ∀ z ∈ s, HolomorphicAt f z) :
Set := by
exact f⁻¹' {0} ∩ s
noncomputable def ZeroFinset
{f : }
(h₁f : ∀ z ∈ Metric.closedBall (0 : ) 1, HolomorphicAt f z)
(h₂f : f 0 ≠ 0) :
Finset := by
let Z := f⁻¹' {0} ∩ Metric.closedBall (0 : ) 1
have hZ : Set.Finite Z := by
dsimp [Z]
rw [Set.inter_comm]
apply finiteZeros
-- Ball is preconnected
apply IsConnected.isPreconnected
apply Convex.isConnected
exact convex_closedBall 0 1
exact Set.nonempty_of_nonempty_subtype
--
exact isCompact_closedBall 0 1
--
intro x hx
have A := (h₁f x hx)
let B := HolomorphicAt_iff.1 A
obtain ⟨s, h₁s, h₂s, h₃s⟩ := B
apply DifferentiableOn.analyticAt (s := s)
intro z hz
apply DifferentiableAt.differentiableWithinAt
apply h₃s
exact hz
exact IsOpen.mem_nhds h₁s h₂s
--
use 0
constructor
· simp
· exact h₂f
exact hZ.toFinset
lemma ZeroFinset_mem_iff
{f : }
(h₁f : ∀ z ∈ Metric.closedBall (0 : ) 1, HolomorphicAt f z)
{h₂f : f 0 ≠ 0}
(z : ) :
z ∈ ↑(ZeroFinset h₁f h₂f) ↔ z ∈ Metric.closedBall 0 1 ∧ f z = 0 := by
dsimp [ZeroFinset]; simp
tauto
noncomputable def order
{f : }
{h₁f : ∀ z ∈ Metric.closedBall (0 : ) 1, HolomorphicAt f z}
{h₂f : f 0 ≠ 0} :
ZeroFinset h₁f h₂f → := by
intro i
let A := ((ZeroFinset_mem_iff h₁f i).1 i.2).1
let B := (h₁f i.1 A).analyticAt
exact B.order.toNat
theorem jensen_case_R_eq_one
(f : )
(h₁f : ∀ z ∈ Metric.closedBall (0 : ) 1, HolomorphicAt f z)
(h'₁f : ∀ z ∈ Metric.closedBall (0 : ) 1, AnalyticAt f z)
(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
have F : := by sorry
have h₁F : ∀ z ∈ Metric.closedBall (0 : ) 1, HolomorphicAt F z := by sorry
have h₂F : ∀ z ∈ Metric.closedBall (0 : ) 1, F z ≠ 0 := by sorry
have h₃F : f = fun z ↦ (F z) * ∏ s : ZeroFinset h₁f h₂f, (z - s) ^ (order s) := by sorry
let G := fun z ↦ log ‖F z‖ + ∑ s : ZeroFinset h₁f h₂f, (order s) * log ‖z - s‖
have decompose_f : ∀ z ∈ Metric.closedBall (0 : ) 1, f z ≠ 0 → log ‖f z‖ = G z := by
intro z h₁z h₂z
conv =>
left
arg 1
rw [h₃F]
rw [norm_mul]
rw [norm_prod]
right
arg 2
intro b
rw [norm_pow]
simp only [Complex.norm_eq_abs, Finset.univ_eq_attach]
rw [Real.log_mul]
rw [Real.log_prod]
conv =>
left
right
arg 2
intro s
rw [Real.log_pow]
dsimp [G]
-- ∀ x ∈ (ZeroFinset h₁f).attach, Complex.abs (z - ↑x) ^ order x ≠ 0
simp
intro s hs
rw [ZeroFinset_mem_iff h₁f s] at hs
rw [← hs.2] at h₂z
tauto
-- Complex.abs (F z) ≠ 0
simp
exact h₂F z h₁z
-- ∏ I : { x // x ∈ S }, Complex.abs (z - a I) ≠ 0
by_contra C
obtain ⟨s, h₁s, h₂s⟩ := Finset.prod_eq_zero_iff.1 C
simp at h₂s
rw [← ((ZeroFinset_mem_iff h₁f s).1 (Finset.coe_mem s)).2, h₂s.1] at h₂z
tauto
have : ∫ (x : ) in (0)..2 * π, log ‖f (circleMap 0 1 x)‖ = ∫ (x : ) in (0)..2 * π, G (circleMap 0 1 x) := by
rw [intervalIntegral.integral_congr_ae]
rw [MeasureTheory.ae_iff]
apply Set.Countable.measure_zero
simp
have t₀ : {a | a ∈ Ι 0 (2 * π) ∧ ¬log ‖f (circleMap 0 1 a)‖ = G (circleMap 0 1 a)}
⊆ (circleMap 0 1)⁻¹' (Metric.closedBall 0 1 ∩ f⁻¹' {0}) := by
intro a ha
simp at ha
simp
by_contra C
have : (circleMap 0 1 a) ∈ Metric.closedBall 0 1 := by
sorry
exact ha.2 (decompose_f (circleMap 0 1 a) this C)
apply Set.Countable.mono t₀
apply Set.Countable.preimage_circleMap
apply Set.Finite.countable
apply finiteZeros
-- IsPreconnected (Metric.closedBall (0 : ) 1)
apply IsConnected.isPreconnected
apply Convex.isConnected
exact convex_closedBall 0 1
exact Set.nonempty_of_nonempty_subtype
--
exact isCompact_closedBall 0 1
--
exact h'₁f
use 0
exact ⟨Metric.mem_closedBall_self (zero_le_one' ), h₂f⟩
exact Ne.symm (zero_ne_one' )
have h₁Gi : ∀ i ∈ (ZeroFinset h₁f h₂f).attach, IntervalIntegrable (fun x => log (Complex.abs (circleMap 0 1 x - ↑i))) MeasureTheory.volume 0 (2 * π) := by
-- This is hard. Need to invoke specialFunctions_CircleIntegral_affine.
sorry
have : ∫ (x : ) in (0)..2 * π, G (circleMap 0 1 x) = (∫ (x : ) in (0)..2 * π, log (Complex.abs (F (circleMap 0 1 x)))) + ∑ x ∈ (ZeroFinset h₁f h₂f).attach, ↑(order x) * ∫ (x_1 : ) in (0)..2 * π, log (Complex.abs (circleMap 0 1 x_1 - ↑x)) := by
dsimp [G]
rw [intervalIntegral.integral_add]
rw [intervalIntegral.integral_finset_sum]
simp_rw [intervalIntegral.integral_const_mul]
-- ∀ i ∈ (ZeroFinset h₁f).attach, IntervalIntegrable (fun x => ↑(order i) *
-- log (Complex.abs (circleMap 0 1 x - ↑i))) MeasureTheory.volume 0 (2 * π)
intro i hi
apply IntervalIntegrable.const_mul
have : i.1 ∈ Metric.closedBall (0 : ) 1 := by exact ((ZeroFinset_mem_iff h₁f i).1 i.2).1
simp at this
by_cases h₂i : ‖i.1‖ = 1
-- case pos
exact int'₂ h₂i
-- case neg
have : i.1 ∈ Metric.ball (0 : ) 1 := by sorry
apply Continuous.intervalIntegrable
apply continuous_iff_continuousAt.2
intro x
have : (fun x => log (Complex.abs (circleMap 0 1 x - ↑i))) = log ∘ Complex.abs ∘ (fun x ↦ circleMap 0 1 x - ↑i) :=
rfl
rw [this]
apply ContinuousAt.comp
apply Real.continuousAt_log
simp
by_contra ha'
conv at h₂i =>
arg 1
rw [← ha']
rw [Complex.norm_eq_abs]
rw [abs_circleMap_zero 1 x]
simp
tauto
apply ContinuousAt.comp
apply Complex.continuous_abs.continuousAt
fun_prop
-- IntervalIntegrable (fun x => log (Complex.abs (F (circleMap 0 1 x)))) MeasureTheory.volume 0 (2 * π)
apply Continuous.intervalIntegrable
apply continuous_iff_continuousAt.2
intro x
have : (fun x => log (Complex.abs (F (circleMap 0 1 x)))) = log ∘ Complex.abs ∘ F ∘ (fun x ↦ circleMap 0 1 x) :=
rfl
rw [this]
apply ContinuousAt.comp
apply Real.continuousAt_log
simp [h₂F]
--
apply ContinuousAt.comp
apply Complex.continuous_abs.continuousAt
apply ContinuousAt.comp
apply DifferentiableAt.continuousAt (𝕜 := )
apply HolomorphicAt.differentiableAt
simp [h₁F]
--
apply Continuous.continuousAt
apply continuous_circleMap
--
have : (fun x => ∑ s ∈ (ZeroFinset h₁f h₂f).attach, ↑(order s) * log (Complex.abs (circleMap 0 1 x - ↑s)))
= ∑ s ∈ (ZeroFinset h₁f h₂f).attach, (fun x => ↑(order s) * log (Complex.abs (circleMap 0 1 x - ↑s))) := by
funext x
simp
rw [this]
apply IntervalIntegrable.sum
intro i h₂i
apply IntervalIntegrable.const_mul
have : i.1 ∈ Metric.closedBall (0 : ) 1 := by exact ((ZeroFinset_mem_iff h₁f i).1 i.2).1
simp at this
by_cases h₂i : ‖i.1‖ = 1
-- case pos
exact int'₂ h₂i
-- case neg
have : i.1 ∈ Metric.ball (0 : ) 1 := by sorry
apply Continuous.intervalIntegrable
apply continuous_iff_continuousAt.2
intro x
have : (fun x => log (Complex.abs (circleMap 0 1 x - ↑i))) = log ∘ Complex.abs ∘ (fun x ↦ circleMap 0 1 x - ↑i) :=
rfl
rw [this]
apply ContinuousAt.comp
apply Real.continuousAt_log
simp
by_contra ha'
conv at h₂i =>
arg 1
rw [← ha']
rw [Complex.norm_eq_abs]
rw [abs_circleMap_zero 1 x]
simp
tauto
apply ContinuousAt.comp
apply Complex.continuous_abs.continuousAt
fun_prop
have t₁ : (∫ (x : ) in (0)..2 * Real.pi, log ‖F (circleMap 0 1 x)‖) = 2 * Real.pi * log ‖F 0‖ := by
let logAbsF := fun w ↦ Real.log ‖F w‖
have t₀ : ∀ z ∈ Metric.closedBall 0 1, HarmonicAt logAbsF z := by
intro z hz
apply logabs_of_holomorphicAt_is_harmonic
apply h₁F z hz
exact h₂F z hz
apply harmonic_meanValue₁ 1 Real.zero_lt_one t₀
simp_rw [← Complex.norm_eq_abs] at this
rw [t₁] at this
--let Z₁ := (ZeroFinset h₁f h₂f) ∩ (Metric.ball 0 1)
let Z₂ := { x : ZeroFinset h₁f h₂f | ‖x.1‖ = 1 }
sorry

View File

@ -8,10 +8,6 @@ import Nevanlinna.periodic_integrability
open scoped Interval Topology
open Real Filter MeasureTheory intervalIntegral
-- Integrability of periodic functions
-- Lemmas for the circleMap
@ -46,6 +42,20 @@ lemma l₂ {x : } : ‖(circleMap 0 1 x) - a‖ = ‖1 - (circleMap 0 1 (-x))
-- Integral of log ‖circleMap 0 1 x - a‖, for ‖a‖ < 1.
lemma int'₀
{a : }
(ha : a ∈ Metric.ball 0 1) :
IntervalIntegrable (fun x ↦ log ‖circleMap 0 1 x - a‖) volume 0 (2 * π) := by
apply Continuous.intervalIntegrable
apply Continuous.log
fun_prop
simp
intro x
by_contra h₁a
rw [← h₁a] at ha
simp at ha
lemma int₀
{a : }
(ha : a ∈ Metric.ball 0 1) :
@ -210,7 +220,6 @@ lemma int''₁ : -- Integrability of log ‖circleMap 0 1 x - 1‖ for arbitrary
rw [zero_add]
exact int'₁
lemma int₁ :
∫ x in (0)..(2 * π), log ‖circleMap 0 1 x - 1‖ = 0 := by
@ -360,3 +369,16 @@ lemma int₂
simp
simp_rw [this]
exact int₁
lemma int₃
{a : }
(ha : a ∈ Metric.closedBall 0 1) :
∫ x in (0)..(2 * π), log ‖circleMap 0 1 x - a‖ = 0 := by
by_cases h₁a : a ∈ Metric.ball 0 1
· exact int₀ h₁a
· apply int₂
simp at ha
simp at h₁a
simp
linarith