From 1e28302c17fc38ef9328b37c7bcaf56e6430b153 Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Thu, 19 Dec 2024 21:24:13 +0100 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/firstMain.lean | 18 +++--- Nevanlinna/intervalIntegrability.lean | 68 ++++++++++++++++++--- Nevanlinna/meromorphicOn_integrability.lean | 48 ++++++++++++++- 3 files changed, 115 insertions(+), 19 deletions(-) diff --git a/Nevanlinna/firstMain.lean b/Nevanlinna/firstMain.lean index e45c3f7..202482a 100644 --- a/Nevanlinna/firstMain.lean +++ b/Nevanlinna/firstMain.lean @@ -77,7 +77,7 @@ theorem Nevanlinna_proximity₀ {f : ℂ → ℂ} {r : ℝ} (h₁f : MeromorphicOn f ⊤) - (hr : 0 < r ) : + (hr : 0 < r) : (2 * π)⁻¹ * ∫ x in (0)..(2 * π), log ‖f (circleMap 0 r x)‖ = (h₁f.m_infty r) - (h₁f.inv.m_infty r) := by unfold MeromorphicOn.m_infty @@ -88,10 +88,13 @@ theorem Nevanlinna_proximity₀ exact Eq.symm (IsAbsoluteValue.abv_inv Norm.norm (f (circleMap 0 r x))) -- apply MeromorphicOn.integrable_logpos_abs_f hr + intro z hx + exact h₁f z trivial + -- + apply MeromorphicOn.integrable_logpos_abs_f hr + exact MeromorphicOn.inv_iff.mpr fun x a => h₁f x trivial - sorry - theorem Nevanlinna_proximity {f : ℂ → ℂ} {r : ℝ} @@ -105,9 +108,8 @@ theorem Nevanlinna_proximity rw [← mul_sub]; congr exact loglogpos - - - have hr : 0 < r := by sorry + by_cases h₂r : 0 < r + · exact Nevanlinna_proximity₀ h₁f h₂r unfold MeromorphicOn.m_infty rw [← mul_sub]; congr @@ -116,8 +118,10 @@ theorem Nevanlinna_proximity simp_rw [loglogpos]; congr exact Eq.symm (IsAbsoluteValue.abv_inv Norm.norm (f (circleMap 0 r x))) -- - apply MeromorphicOn.integrable_logpos_abs_f hr + apply MeromorphicOn.integrable_logpos_abs_f + + sorry sorry noncomputable def MeromorphicOn.T_infty diff --git a/Nevanlinna/intervalIntegrability.lean b/Nevanlinna/intervalIntegrability.lean index 5f187f7..6948ac8 100644 --- a/Nevanlinna/intervalIntegrability.lean +++ b/Nevanlinna/intervalIntegrability.lean @@ -1,13 +1,5 @@ -import Mathlib.Analysis.Analytic.Meromorphic import Mathlib.MeasureTheory.Integral.CircleIntegral -import Mathlib.MeasureTheory.Integral.IntervalIntegral -import Nevanlinna.analyticAt -import Nevanlinna.divisor -import Nevanlinna.meromorphicAt -import Nevanlinna.meromorphicOn_divisor -import Nevanlinna.stronglyMeromorphicOn -import Nevanlinna.stronglyMeromorphicOn_eliminate -import Nevanlinna.mathlibAddOn +import Nevanlinna.periodic_integrability open scoped Interval Topology open Real Filter MeasureTheory intervalIntegral @@ -96,3 +88,61 @@ theorem integral_congr_changeDiscrete constructor · apply Set.Countable.measure_zero (d hr hU hf) · tauto + + +lemma circleMap_neg + {r x : ℝ} : + circleMap 0 (-r) x = circleMap 0 r (x + π) := by + unfold circleMap + simp + rw [add_mul] + rw [Complex.exp_add] + simp + + +theorem integrability_congr_negRadius + {f : ℂ → ℝ} + {r : ℝ} : + IntervalIntegrable (fun (θ : ℝ) ↦ f (circleMap 0 r θ)) MeasureTheory.volume 0 (2 * π) → + IntervalIntegrable (fun (θ : ℝ) ↦ f (circleMap 0 (-r) θ)) MeasureTheory.volume 0 (2 * π) := by + + intro h + simp_rw [circleMap_neg] + + let A := IntervalIntegrable.comp_add_right h π + + have t₀ : Function.Periodic (fun (θ : ℝ) ↦ f (circleMap 0 r θ)) (2 * π) := by + intro x + simp + congr 1 + exact periodic_circleMap 0 r x + rw [← zero_add (2 * π)] at h + have B := periodic_integrability4 (a₁ := π) (a₂ := 3 * π) t₀ two_pi_pos h + let A := IntervalIntegrable.comp_add_right B π + simp at A + have : 3 * π - π = 2 * π := by + ring + rw [this] at A + exact A + + +theorem integrabl_congr_negRadius + {f : ℂ → ℝ} + {r : ℝ} : + ∫ (x : ℝ) in (0)..(2 * π), f (circleMap 0 r x) = ∫ (x : ℝ) in (0)..(2 * π), f (circleMap 0 (-r) x) := by + + simp_rw [circleMap_neg] + have t₀ : Function.Periodic (fun (θ : ℝ) ↦ f (circleMap 0 r θ)) (2 * π) := by + intro x + simp + congr 1 + exact periodic_circleMap 0 r x + --rw [← zero_add (2 * π)] at h + --have B := periodic_integrability4 (a₁ := π) (a₂ := 3 * π) t₀ two_pi_pos h + have B := intervalIntegral.integral_comp_add_right (a := 0) (b := 2 * π) (fun θ => f (circleMap 0 r θ)) π + rw [B] + let X := t₀.intervalIntegral_add_eq 0 (0 + π) + simp at X + rw [X] + simp + rw [add_comm] diff --git a/Nevanlinna/meromorphicOn_integrability.lean b/Nevanlinna/meromorphicOn_integrability.lean index 271fc39..f0053d1 100644 --- a/Nevanlinna/meromorphicOn_integrability.lean +++ b/Nevanlinna/meromorphicOn_integrability.lean @@ -16,9 +16,10 @@ open scoped Interval Topology open Real Filter MeasureTheory intervalIntegral -theorem MeromorphicOn.integrable_log_abs_f +theorem MeromorphicOn.integrable_log_abs_f₀ {f : ℂ → ℂ} {r : ℝ} + -- WARNING: Not optimal. This needs to go (hr : 0 < r) -- WARNING: Not optimal. It suffices to be meromorphic on the Sphere (h₁f : MeromorphicOn f (Metric.closedBall (0 : ℂ) r)) : @@ -111,10 +112,51 @@ theorem MeromorphicOn.integrable_log_abs_f rw [integrability_congr_changeDiscrete hU this] have : ∀ x ∈ Metric.closedBall 0 r, F x = 0 := by - sorry + intro x hx + let A := h₂f ⟨x, hx⟩ + rw [← makeStronglyMeromorphicOn_changeOrder h₁f hx] at A + let B := ((stronglyMeromorphicOn_of_makeStronglyMeromorphicOn h₁f) x hx).order_eq_zero_iff.not.1 + simp [A] at B + assumption + have : (fun z => log ‖F z‖) ∘ circleMap 0 r = 0 := by + funext x + simp + left + apply this + simp [abs_of_pos hr] + simp_rw [this] + apply intervalIntegral.intervalIntegrable_const + + +theorem MeromorphicOn.integrable_log_abs_f + {f : ℂ → ℂ} + {r : ℝ} + -- WARNING: Not optimal. It suffices to be meromorphic on the Sphere + (h₁f : MeromorphicOn f (Metric.closedBall (0 : ℂ) |r|)) : + IntervalIntegrable (fun z ↦ log ‖f (circleMap 0 r z)‖) MeasureTheory.volume 0 (2 * π) := by + + by_cases h₁r : r = 0 + · rw [h₁r] + simp + · by_cases h₂r : 0 < r + · have : |r| = r := by + exact abs_of_pos h₂r + rw [this] at h₁f + exact MeromorphicOn.integrable_log_abs_f₀ h₂r h₁f + · have t₀ : 0 < -r := by + sorry + have : |r| = -r := by + apply abs_of_neg + exact Left.neg_pos_iff.mp t₀ + rw [this] at h₁f + let A := MeromorphicOn.integrable_log_abs_f₀ t₀ h₁f + + let B := integrability_congr_negRadius (f := fun z => log ‖f z‖) (r := -r) + let C := B A + simp at C + simpa - sorry theorem MeromorphicOn.integrable_logpos_abs_f {f : ℂ → ℂ}