From 6651c0852a75ec0cf24cbfe960e28e28469ea93b Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Wed, 11 Sep 2024 10:24:45 +0200 Subject: [PATCH] =?UTF-8?q?Working=E2=80=A6?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Nevanlinna/holomorphicAt.lean | 17 +++ Nevanlinna/holomorphic_JensenFormula2.lean | 144 +++++++++--------- ...pecialFunctions_CircleIntegral_affine.lean | 13 ++ 3 files changed, 98 insertions(+), 76 deletions(-) diff --git a/Nevanlinna/holomorphicAt.lean b/Nevanlinna/holomorphicAt.lean index ba34592..2749587 100644 --- a/Nevanlinna/holomorphicAt.lean +++ b/Nevanlinna/holomorphicAt.lean @@ -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} diff --git a/Nevanlinna/holomorphic_JensenFormula2.lean b/Nevanlinna/holomorphic_JensenFormula2.lean index 99bb368..b33433b 100644 --- a/Nevanlinna/holomorphic_JensenFormula2.lean +++ b/Nevanlinna/holomorphic_JensenFormula2.lean @@ -7,72 +7,12 @@ 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 +lemma h₁U : IsPreconnected (Metric.closedBall (0 : ℂ) 1) := + (convex_closedBall (0 : ℂ) 1).isPreconnected +lemma h₂U : IsCompact (Metric.closedBall (0 : ℂ) 1) := + isCompact_closedBall 0 1 -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 : ℂ → ℂ) @@ -81,19 +21,15 @@ theorem jensen_case_R_eq_one (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) := - (convex_closedBall (0 : ℂ) 1).isPreconnected - - 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 + intro z h₁z + apply AnalyticAt.holomorphicAt + exact h₁F z h₁z 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‖ @@ -149,7 +85,7 @@ theorem jensen_case_R_eq_one exact h₂F z h₁z - have : ∫ (x : ℝ) in (0)..2 * π, log ‖f (circleMap 0 1 x)‖ = ∫ (x : ℝ) in (0)..2 * π, G (circleMap 0 1 x) := by + 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] @@ -184,7 +120,7 @@ theorem jensen_case_R_eq_one -- This is hard. Need to invoke specialFunctions_CircleIntegral_affine. sorry - have : ∫ (x : ℝ) in (0)..2 * π, G (circleMap 0 1 x) + 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] @@ -290,9 +226,65 @@ theorem jensen_case_R_eq_one 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 + 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 - sorry + rw [int_logAbs_f_eq_int_G] + rw [decompose_int_G] + rw [h₃F] + simp + 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 + + rw [finsum_eq_sum_of_support_subset _ (s := (finiteZeros h₁U h₂U h'₁f h'₂f).toFinset)] + simp + simp + intro x ⟨h₁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 diff --git a/Nevanlinna/specialFunctions_CircleIntegral_affine.lean b/Nevanlinna/specialFunctions_CircleIntegral_affine.lean index 17a43ee..09160fc 100644 --- a/Nevanlinna/specialFunctions_CircleIntegral_affine.lean +++ b/Nevanlinna/specialFunctions_CircleIntegral_affine.lean @@ -360,3 +360,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