From 4cc853a5d92bd29f8ab089b0e16f00bdad70df69 Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Thu, 19 Dec 2024 16:10:51 +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 | 49 +++- Nevanlinna/intervalIntegrability.lean | 98 +++++++ Nevanlinna/logpos.lean | 36 +++ Nevanlinna/meromorphicOn_integrability.lean | 246 ++++++++---------- ...pecialFunctions_CircleIntegral_affine.lean | 92 ++++--- lake-manifest.json | 2 +- 6 files changed, 330 insertions(+), 193 deletions(-) create mode 100644 Nevanlinna/intervalIntegrability.lean create mode 100644 Nevanlinna/logpos.lean diff --git a/Nevanlinna/firstMain.lean b/Nevanlinna/firstMain.lean index 7f12a34..e45c3f7 100644 --- a/Nevanlinna/firstMain.lean +++ b/Nevanlinna/firstMain.lean @@ -2,6 +2,7 @@ import Mathlib.MeasureTheory.Integral.CircleIntegral import Nevanlinna.divisor import Nevanlinna.stronglyMeromorphicOn import Nevanlinna.meromorphicOn_divisor +import Nevanlinna.meromorphicOn_integrability open Real @@ -63,17 +64,6 @@ theorem Nevanlinna_counting rw [hx] tauto -noncomputable def logpos : ℝ → ℝ := fun r ↦ max 0 (log r) - -theorem loglogpos {r : ℝ} : log r = logpos r - logpos r⁻¹ := by - unfold logpos - rw [log_inv] - by_cases h : 0 ≤ log r - · simp [h] - · simp at h - have : 0 ≤ -log r := Left.nonneg_neg_iff.2 (le_of_lt h) - simp [h, this] - exact neg_nonneg.mp this -- @@ -83,11 +73,13 @@ noncomputable def MeromorphicOn.m_infty ℝ → ℝ := fun r ↦ (2 * π)⁻¹ * ∫ x in (0)..(2 * π), logpos ‖f (circleMap 0 r x)‖ -theorem Nevanlinna_proximity +theorem Nevanlinna_proximity₀ {f : ℂ → ℂ} {r : ℝ} - (h₁f : MeromorphicOn f ⊤) : + (h₁f : MeromorphicOn f ⊤) + (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 rw [← mul_sub]; congr rw [← intervalIntegral.integral_sub]; congr @@ -95,6 +87,37 @@ 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 + + + sorry + +theorem Nevanlinna_proximity + {f : ℂ → ℂ} + {r : ℝ} + (h₁f : MeromorphicOn f ⊤) : + (2 * π)⁻¹ * ∫ x in (0)..(2 * π), log ‖f (circleMap 0 r x)‖ = (h₁f.m_infty r) - (h₁f.inv.m_infty r) := by + + by_cases h₁r : r = 0 + · unfold MeromorphicOn.m_infty + rw [← mul_sub]; congr + simp only [h₁r, circleMap_zero_radius, Function.const_apply, intervalIntegral.integral_const, sub_zero, smul_eq_mul, Pi.inv_apply, norm_inv] + rw [← mul_sub]; congr + exact loglogpos + + + + have hr : 0 < r := by sorry + + unfold MeromorphicOn.m_infty + rw [← mul_sub]; congr + rw [← intervalIntegral.integral_sub]; congr + funext x + simp_rw [loglogpos]; congr + exact Eq.symm (IsAbsoluteValue.abv_inv Norm.norm (f (circleMap 0 r x))) + -- + apply MeromorphicOn.integrable_logpos_abs_f hr + sorry noncomputable def MeromorphicOn.T_infty diff --git a/Nevanlinna/intervalIntegrability.lean b/Nevanlinna/intervalIntegrability.lean new file mode 100644 index 0000000..5f187f7 --- /dev/null +++ b/Nevanlinna/intervalIntegrability.lean @@ -0,0 +1,98 @@ +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 + +open scoped Interval Topology +open Real Filter MeasureTheory intervalIntegral + + +/- Integral and Integrability up to changes on codiscrete sets -/ + +theorem d + {U S : Set ℂ} + {c : ℂ} + {r : ℝ} + (hr : r ≠ 0) + (hU : Metric.sphere c |r| ⊆ U) + (hS : S ∈ Filter.codiscreteWithin U) : + Countable ((circleMap c r)⁻¹' Sᶜ) := by + + have : (circleMap c r)⁻¹' (S ∪ Uᶜ)ᶜ = (circleMap c r)⁻¹' Sᶜ := by + simp [(by simpa : (circleMap c r)⁻¹' U = ⊤)] + rw [← this] + + apply Set.Countable.preimage_circleMap _ c hr + have : DiscreteTopology ((S ∪ Uᶜ)ᶜ : Set ℂ) := by + rw [discreteTopology_subtype_iff] + rw [mem_codiscreteWithin] at hS; simp at hS + + intro x hx + rw [← mem_iff_inf_principal_compl, (by ext z; simp; tauto : S ∪ Uᶜ = (U \ S)ᶜ)] + rw [Set.compl_union, compl_compl] at hx + exact hS x hx.2 + + apply TopologicalSpace.separableSpace_iff_countable.1 + exact TopologicalSpace.SecondCountableTopology.to_separableSpace + + +theorem integrability_congr_changeDiscrete₀ + {f₁ f₂ : ℂ → ℝ} + {U : Set ℂ} + {r : ℝ} + (hU : Metric.sphere 0 |r| ⊆ U) + (hf : f₁ =ᶠ[Filter.codiscreteWithin U] f₂) : + IntervalIntegrable (f₁ ∘ (circleMap 0 r)) MeasureTheory.volume 0 (2 * π) → IntervalIntegrable (f₂ ∘ (circleMap 0 r)) MeasureTheory.volume 0 (2 * π) := by + intro hf₁ + + by_cases hr : r = 0 + · unfold circleMap + rw [hr] + simp + have : f₂ ∘ (fun (θ : ℝ) ↦ 0) = (fun r ↦ f₂ 0) := by + exact rfl + rw [this] + simp + + · apply IntervalIntegrable.congr hf₁ + rw [Filter.eventuallyEq_iff_exists_mem] + use (circleMap 0 r)⁻¹' {z | f₁ z = f₂ z} + constructor + · apply Set.Countable.measure_zero (d hr hU hf) + · tauto + + +theorem integrability_congr_changeDiscrete + {f₁ f₂ : ℂ → ℝ} + {U : Set ℂ} + {r : ℝ} + (hU : Metric.sphere (0 : ℂ) |r| ⊆ U) + (hf : f₁ =ᶠ[Filter.codiscreteWithin U] f₂) : + IntervalIntegrable (f₁ ∘ (circleMap 0 r)) MeasureTheory.volume 0 (2 * π) ↔ IntervalIntegrable (f₂ ∘ (circleMap 0 r)) MeasureTheory.volume 0 (2 * π) := by + + constructor + · exact integrability_congr_changeDiscrete₀ hU hf + · exact integrability_congr_changeDiscrete₀ hU (EventuallyEq.symm hf) + + +theorem integral_congr_changeDiscrete + {f₁ f₂ : ℂ → ℝ} + {U : Set ℂ} + {r : ℝ} + (hr : r ≠ 0) + (hU : Metric.sphere 0 |r| ⊆ U) + (hf : f₁ =ᶠ[Filter.codiscreteWithin U] f₂) : + ∫ (x : ℝ) in (0)..(2 * π), f₁ (circleMap 0 r x) = ∫ (x : ℝ) in (0)..(2 * π), f₂ (circleMap 0 r x) := by + + apply intervalIntegral.integral_congr_ae + rw [eventually_iff_exists_mem] + use (circleMap 0 r)⁻¹' {z | f₁ z = f₂ z} + constructor + · apply Set.Countable.measure_zero (d hr hU hf) + · tauto diff --git a/Nevanlinna/logpos.lean b/Nevanlinna/logpos.lean new file mode 100644 index 0000000..b89b3af --- /dev/null +++ b/Nevanlinna/logpos.lean @@ -0,0 +1,36 @@ +import Mathlib.MeasureTheory.Integral.CircleIntegral +import Nevanlinna.divisor +import Nevanlinna.stronglyMeromorphicOn +import Nevanlinna.meromorphicOn_divisor + +open Real + + +noncomputable def logpos : ℝ → ℝ := fun r ↦ max 0 (log r) + +theorem loglogpos {r : ℝ} : log r = logpos r - logpos r⁻¹ := by + unfold logpos + rw [log_inv] + by_cases h : 0 ≤ log r + · simp [h] + · simp at h + have : 0 ≤ -log r := Left.nonneg_neg_iff.2 (le_of_lt h) + simp [h, this] + exact neg_nonneg.mp this + + +theorem logpos_norm {r : ℝ} : logpos r = 2⁻¹ * (log r + ‖log r‖) := by + by_cases hr : 0 ≤ log r + · rw [norm_of_nonneg hr] + have : logpos r = log r := by + unfold logpos + simp [hr] + rw [this] + ring + · rw [norm_of_nonpos (le_of_not_ge hr)] + have : logpos r = 0 := by + unfold logpos + simp + exact le_of_not_ge hr + rw [this] + ring diff --git a/Nevanlinna/meromorphicOn_integrability.lean b/Nevanlinna/meromorphicOn_integrability.lean index 37fba7b..271fc39 100644 --- a/Nevanlinna/meromorphicOn_integrability.lean +++ b/Nevanlinna/meromorphicOn_integrability.lean @@ -3,8 +3,11 @@ import Mathlib.MeasureTheory.Integral.CircleIntegral import Mathlib.MeasureTheory.Integral.IntervalIntegral import Nevanlinna.analyticAt import Nevanlinna.divisor +import Nevanlinna.intervalIntegrability +import Nevanlinna.logpos import Nevanlinna.meromorphicAt import Nevanlinna.meromorphicOn_divisor +import Nevanlinna.specialFunctions_CircleIntegral_affine import Nevanlinna.stronglyMeromorphicOn import Nevanlinna.stronglyMeromorphicOn_eliminate import Nevanlinna.mathlibAddOn @@ -13,158 +16,121 @@ open scoped Interval Topology open Real Filter MeasureTheory intervalIntegral -/- Integral and Integrability up to changes on codiscrete sets -/ - -theorem d - {U S : Set ℂ} - {c : ℂ} - {r : ℝ} - (hr : r ≠ 0) - (hU : Metric.sphere c |r| ⊆ U) - (hS : S ∈ Filter.codiscreteWithin U) : - Countable ((circleMap c r)⁻¹' Sᶜ) := by - - have : (circleMap c r)⁻¹' (S ∪ Uᶜ)ᶜ = (circleMap c r)⁻¹' Sᶜ := by - simp [(by simpa : (circleMap c r)⁻¹' U = ⊤)] - rw [← this] - - apply Set.Countable.preimage_circleMap _ c hr - have : DiscreteTopology ((S ∪ Uᶜ)ᶜ : Set ℂ) := by - rw [discreteTopology_subtype_iff] - rw [mem_codiscreteWithin] at hS; simp at hS - - intro x hx - rw [← mem_iff_inf_principal_compl, (by ext z; simp; tauto : S ∪ Uᶜ = (U \ S)ᶜ)] - rw [Set.compl_union, compl_compl] at hx - exact hS x hx.2 - - apply TopologicalSpace.separableSpace_iff_countable.1 - exact TopologicalSpace.SecondCountableTopology.to_separableSpace - - -theorem integrability_congr_changeDiscrete₀ - {f₁ f₂ : ℂ → ℝ} - {U : Set ℂ} - {r : ℝ} - (hU : Metric.sphere 0 |r| ⊆ U) - (hf : f₁ =ᶠ[Filter.codiscreteWithin U] f₂) : - IntervalIntegrable (f₁ ∘ (circleMap 0 r)) MeasureTheory.volume 0 (2 * π) → IntervalIntegrable (f₂ ∘ (circleMap 0 r)) MeasureTheory.volume 0 (2 * π) := by - intro hf₁ - - by_cases hr : r = 0 - · unfold circleMap - rw [hr] - simp - have : f₂ ∘ (fun (θ : ℝ) ↦ 0) = (fun r ↦ f₂ 0) := by - exact rfl - rw [this] - simp - - · apply IntervalIntegrable.congr hf₁ - rw [Filter.eventuallyEq_iff_exists_mem] - use (circleMap 0 r)⁻¹' {z | f₁ z = f₂ z} - constructor - · apply Set.Countable.measure_zero (d hr hU hf) - · tauto - - -theorem integrability_congr_changeDiscrete - {f₁ f₂ : ℂ → ℝ} - {U : Set ℂ} - {r : ℝ} - (hU : Metric.sphere (0 : ℂ) |r| ⊆ U) - (hf : f₁ =ᶠ[Filter.codiscreteWithin U] f₂) : - IntervalIntegrable (f₁ ∘ (circleMap 0 r)) MeasureTheory.volume 0 (2 * π) ↔ IntervalIntegrable (f₂ ∘ (circleMap 0 r)) MeasureTheory.volume 0 (2 * π) := by - - constructor - · exact integrability_congr_changeDiscrete₀ hU hf - · exact integrability_congr_changeDiscrete₀ hU (EventuallyEq.symm hf) - - -theorem integral_congr_changeDiscrete - {f₁ f₂ : ℂ → ℝ} - {U : Set ℂ} - {r : ℝ} - (hr : r ≠ 0) - (hU : Metric.sphere 0 |r| ⊆ U) - (hf : f₁ =ᶠ[Filter.codiscreteWithin U] f₂) : - ∫ (x : ℝ) in (0)..(2 * π), f₁ (circleMap 0 r x) = ∫ (x : ℝ) in (0)..(2 * π), f₂ (circleMap 0 r x) := by - - apply intervalIntegral.integral_congr_ae - rw [eventually_iff_exists_mem] - use (circleMap 0 r)⁻¹' {z | f₁ z = f₂ z} - constructor - · apply Set.Countable.measure_zero (d hr hU hf) - · tauto - - theorem MeromorphicOn.integrable_log_abs_f {f : ℂ → ℂ} {r : ℝ} (hr : 0 < r) - (h₁f : MeromorphicOn f (Metric.closedBall (0 : ℂ) r)) - (h₂f : ∃ u : (Metric.closedBall (0 : ℂ) r), (h₁f u u.2).order ≠ ⊤) : + -- 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 - have h₁U : IsCompact (Metric.closedBall (0 : ℂ) r) := isCompact_closedBall 0 r + by_cases h₂f : ∃ u : (Metric.closedBall (0 : ℂ) r), (h₁f u u.2).order ≠ ⊤ + · have h₁U : IsCompact (Metric.closedBall (0 : ℂ) r) := isCompact_closedBall 0 r - have h₂U : IsConnected (Metric.closedBall (0 : ℂ) r) := by - constructor - · exact Metric.nonempty_closedBall.mpr (le_of_lt hr) - · exact (convex_closedBall (0 : ℂ) r).isPreconnected + have h₂U : IsConnected (Metric.closedBall (0 : ℂ) r) := by + constructor + · exact Metric.nonempty_closedBall.mpr (le_of_lt hr) + · exact (convex_closedBall (0 : ℂ) r).isPreconnected - have h₃U : interior (Metric.closedBall (0 : ℂ) r) ≠ ∅ := by - rw [interior_closedBall, ← Set.nonempty_iff_ne_empty] - use 0; simp [hr]; - repeat exact Ne.symm (ne_of_lt hr) + -- This is where we use 'ball' instead of sphere. However, better + -- results should make this assumption unnecessary. + have h₃U : interior (Metric.closedBall (0 : ℂ) r) ≠ ∅ := by + rw [interior_closedBall, ← Set.nonempty_iff_ne_empty] + use 0; simp [hr]; + repeat exact Ne.symm (ne_of_lt hr) - have h₃f : Set.Finite (Function.support h₁f.divisor) := by - exact Divisor.finiteSupport h₁U h₁f.divisor + have h₃f : Set.Finite (Function.support h₁f.divisor) := by + exact Divisor.finiteSupport h₁U h₁f.divisor - obtain ⟨g, h₁g, h₂g, h₃g⟩ := MeromorphicOn.decompose_log h₁U h₂U h₃U h₁f h₂f - have : (fun z ↦ log ‖f (circleMap 0 r z)‖) = (fun z ↦ log ‖f z‖) ∘ (circleMap 0 r) := by - rfl - rw [this] - have : Metric.sphere (0 : ℂ) |r| ⊆ Metric.closedBall (0 : ℂ) r := by - rw [abs_of_pos hr] - apply Metric.sphere_subset_closedBall + obtain ⟨g, h₁g, h₂g, h₃g⟩ := MeromorphicOn.decompose_log h₁U h₂U h₃U h₁f h₂f + have : (fun z ↦ log ‖f (circleMap 0 r z)‖) = (fun z ↦ log ‖f z‖) ∘ (circleMap 0 r) := by + rfl + rw [this] + have : Metric.sphere (0 : ℂ) |r| ⊆ Metric.closedBall (0 : ℂ) r := by + rw [abs_of_pos hr] + apply Metric.sphere_subset_closedBall - rw [integrability_congr_changeDiscrete this h₃g] + rw [integrability_congr_changeDiscrete this h₃g] + + apply IntervalIntegrable.add + -- + apply Continuous.intervalIntegrable + apply continuous_iff_continuousAt.2 + intro x + have : (fun x => log ‖g (circleMap 0 r x)‖) = log ∘ Complex.abs ∘ g ∘ (fun x ↦ circleMap 0 r x) := + rfl + rw [this] + apply ContinuousAt.comp + apply Real.continuousAt_log + · simp + have : (circleMap 0 r x) ∈ (Metric.closedBall (0 : ℂ) r) := by + apply circleMap_mem_closedBall + exact le_of_lt hr + exact h₂g ⟨(circleMap 0 r x), this⟩ + apply ContinuousAt.comp + · apply Continuous.continuousAt Complex.continuous_abs + apply ContinuousAt.comp + · have : (circleMap 0 r x) ∈ (Metric.closedBall (0 : ℂ) r) := by + apply circleMap_mem_closedBall (0 : ℂ) (le_of_lt hr) x + apply (h₁g (circleMap 0 r x) this).continuousAt + apply Continuous.continuousAt (continuous_circleMap 0 r) + -- + have h {x : ℝ} : (Function.support fun s => (h₁f.divisor s) * log ‖circleMap 0 r x - s‖) ⊆ h₃f.toFinset := by + intro x; simp; tauto + simp_rw [finsum_eq_sum_of_support_subset _ h] + have : (fun x => ∑ s ∈ h₃f.toFinset, (h₁f.divisor s) * log ‖circleMap 0 r x - s‖) = (∑ s ∈ h₃f.toFinset, fun x => (h₁f.divisor s) * log ‖circleMap 0 r x - s‖) := by + ext x; simp + rw [this] + apply IntervalIntegrable.sum h₃f.toFinset + intro s hs + apply IntervalIntegrable.const_mul + + apply intervalIntegrable_logAbs_circleMap_sub_const + exact Ne.symm (ne_of_lt hr) + + · push_neg at h₂f + + let F := h₁f.makeStronglyMeromorphicOn + have : (fun z => log ‖f z‖) =ᶠ[Filter.codiscreteWithin (Metric.closedBall 0 r)] (fun z => log ‖F z‖) := by + -- WANT: apply Filter.eventuallyEq.congr + let A := (makeStronglyMeromorphicOn_changeDiscrete'' h₁f) + obtain ⟨s, h₁s, h₂s⟩ := eventuallyEq_iff_exists_mem.1 A + rw [eventuallyEq_iff_exists_mem] + use s + constructor + · exact h₁s + · intro x hx + simp_rw [h₂s hx] + have hU : Metric.sphere (0 : ℂ) |r| ⊆ Metric.closedBall 0 r := by + rw [abs_of_pos hr] + exact Metric.sphere_subset_closedBall + have t₀ : (fun z => log ‖f (circleMap 0 r z)‖) = (fun z => log ‖f z‖) ∘ circleMap 0 r := by + rfl + rw [t₀] + clear t₀ + rw [integrability_congr_changeDiscrete hU this] + + have : ∀ x ∈ Metric.closedBall 0 r, F x = 0 := by + sorry + + + sorry + +theorem MeromorphicOn.integrable_logpos_abs_f + {f : ℂ → ℂ} + {r : ℝ} + (hr : 0 < r) + -- WARNING: Not optimal. It suffices to be meromorphic on the Sphere + (h₁f : MeromorphicOn f (Metric.closedBall (0 : ℂ) r)) : + IntervalIntegrable (fun z ↦ logpos ‖f (circleMap 0 r z)‖) MeasureTheory.volume 0 (2 * π) := by + + simp_rw [logpos_norm] + simp_rw [mul_add] apply IntervalIntegrable.add - -- - apply Continuous.intervalIntegrable - apply continuous_iff_continuousAt.2 - intro x - have : (fun x => log ‖g (circleMap 0 r x)‖) = log ∘ Complex.abs ∘ g ∘ (fun x ↦ circleMap 0 r x) := - rfl - rw [this] - apply ContinuousAt.comp - apply Real.continuousAt_log - · simp - have : (circleMap 0 r x) ∈ (Metric.closedBall (0 : ℂ) r) := by - apply circleMap_mem_closedBall - exact le_of_lt hr - exact h₂g ⟨(circleMap 0 r x), this⟩ - apply ContinuousAt.comp - · apply Continuous.continuousAt Complex.continuous_abs - apply ContinuousAt.comp - · have : (circleMap 0 r x) ∈ (Metric.closedBall (0 : ℂ) r) := by - apply circleMap_mem_closedBall (0 : ℂ) (le_of_lt hr) x - apply (h₁g (circleMap 0 r x) this).continuousAt - apply Continuous.continuousAt (continuous_circleMap 0 r) - -- - have h {x : ℝ} : (Function.support fun s => (h₁f.divisor s) * log ‖circleMap 0 r x - s‖) ⊆ h₃f.toFinset := by - intro x; simp; tauto - simp_rw [finsum_eq_sum_of_support_subset _ h] - --let A := IntervalIntegrable.sum h₃f.toFinset - --have h : ∀ s ∈ h₃f.toFinset, IntervalIntegrable (f i) volume 0 (2 * π) := by - -- sorry - have : (fun x => ∑ s ∈ h₃f.toFinset, (h₁f.divisor s) * log ‖circleMap 0 r x - s‖) = (∑ s ∈ h₃f.toFinset, fun x => (h₁f.divisor s) * log ‖circleMap 0 r x - s‖) := by - ext x; simp - rw [this] - apply IntervalIntegrable.sum h₃f.toFinset - intro s hs apply IntervalIntegrable.const_mul + exact MeromorphicOn.integrable_log_abs_f hr h₁f - sorry + apply IntervalIntegrable.const_mul + apply IntervalIntegrable.norm + exact MeromorphicOn.integrable_log_abs_f hr h₁f diff --git a/Nevanlinna/specialFunctions_CircleIntegral_affine.lean b/Nevanlinna/specialFunctions_CircleIntegral_affine.lean index bfe992a..8724b9b 100644 --- a/Nevanlinna/specialFunctions_CircleIntegral_affine.lean +++ b/Nevanlinna/specialFunctions_CircleIntegral_affine.lean @@ -3,6 +3,7 @@ import Mathlib.MeasureTheory.Integral.CircleIntegral import Nevanlinna.specialFunctions_Integral_log_sin import Nevanlinna.harmonicAt_examples import Nevanlinna.harmonicAt_meanValue +import Nevanlinna.intervalIntegrability import Nevanlinna.periodic_integrability open scoped Interval Topology @@ -44,7 +45,7 @@ lemma l₂ {x : ℝ} : ‖(circleMap 0 1 x) - a‖ = ‖1 - (circleMap 0 1 (-x)) lemma int'₀ {a : ℂ} - (ha : a ∈ Metric.ball 0 1) : + (ha : ‖a‖ ≠ 1) : IntervalIntegrable (fun x ↦ log ‖circleMap 0 1 x - a‖) volume 0 (2 * π) := by apply Continuous.intervalIntegrable apply Continuous.log @@ -468,52 +469,65 @@ lemma int₄ -- apply intervalIntegral.intervalIntegrable_const -- - by_cases h₂a : Complex.abs (a / R) = 1 + by_cases h₂a : ‖a / R‖ = 1 · exact int'₂ h₂a - · apply int'₀ - simp - simp at h₁a - rw [lt_iff_le_and_ne] - constructor - · exact h₁a - · rw [← Complex.norm_eq_abs, ← norm_eq_abs] - refine div_ne_one_of_ne ?_ - rw [← Complex.norm_eq_abs, norm_div] at h₂a - by_contra hCon - rw [hCon] at h₂a - simp at h₂a - have : |R| ≠ 0 := by - simp - exact Ne.symm (ne_of_lt hR) - rw [div_self this] at h₂a - tauto + · exact int'₀ h₂a lemma intervalIntegrable_logAbs_circleMap_sub_const - {a c : ℂ} + {a : ℂ} {r : ℝ} (hr : r ≠ 0) : - IntervalIntegrable (fun x ↦ log ‖circleMap c r x - a‖) volume 0 (2 * π) := by + IntervalIntegrable (fun x ↦ log ‖circleMap 0 r x - a‖) volume 0 (2 * π) := by - have {x : ℝ} : log ‖circleMap c r x - a‖ = log ‖r * (circleMap 0 1 x - r⁻¹ * (a - c))‖ := by - unfold circleMap - congr 2 + have {z : ℂ} : z ≠ a → log ‖z - a‖ = log ‖r⁻¹ * z - r⁻¹ * a‖ + log ‖r‖ := by + intro hz + rw [← mul_sub, norm_mul] + rw [log_mul (by simp [hr]) (by simp [hz])] simp - rw [mul_sub] - rw [← mul_assoc] + + have : (fun z ↦ log ‖z - a‖) =ᶠ[Filter.codiscreteWithin ⊤] (fun z ↦ log ‖r⁻¹ * z - r⁻¹ * a‖ + log ‖r‖) := by + apply eventuallyEq_iff_exists_mem.mpr + use {a}ᶜ + constructor + · simp_rw [mem_codiscreteWithin, Filter.disjoint_principal_right] + simp + intro y + by_cases hy : y = a + · rw [← hy] + exact self_mem_nhdsWithin + · refine mem_nhdsWithin.mpr ?_ + simp + use {a}ᶜ + constructor + · exact isOpen_compl_singleton + · constructor + · tauto + · tauto + · intro x hx + simp at hx + simp only [Complex.norm_eq_abs] + repeat rw [← Complex.norm_eq_abs] + apply this hx + + have hU : Metric.sphere (0 : ℂ) |r| ⊆ ⊤ := by + exact fun ⦃a⦄ a => trivial + let A := integrability_congr_changeDiscrete hU this + + have : (fun z => log ‖z - a‖) ∘ circleMap 0 r = (fun z => log ‖circleMap 0 r z - a‖) := by + exact rfl + rw [this] at A + have : (fun z => log ‖r⁻¹ * z - r⁻¹ * a‖ + log ‖r‖) ∘ circleMap 0 r = (fun z => log ‖r⁻¹ * circleMap 0 r z - r⁻¹ * a‖ + log ‖r‖) := by + exact rfl + rw [this] at A + rw [A] + + apply IntervalIntegrable.add _ intervalIntegrable_const + have {x : ℝ} : r⁻¹ * circleMap 0 r x = circleMap 0 1 x := by + unfold circleMap simp [hr] - ring simp_rw [this] - have {x : ℝ} : log ‖r * (circleMap 0 1 x - r⁻¹ * (a - c))‖ = log r + log ‖(circleMap 0 1 x - r⁻¹ * (a - c))‖ := by - rw [norm_mul] - rw [log_mul] - simp - -- - simp [hr] - -- - - - - sorry - sorry + by_cases ha : ‖r⁻¹ * a‖ = 1 + · exact int'₂ ha + · apply int'₀ ha diff --git a/lake-manifest.json b/lake-manifest.json index 7578948..700c077 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "2144977fb121989a45d3f6e4d74fd8ab2350db3e", + "rev": "054d75b44095e8390c2afd9744e30c3b2b6cbd42", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null,