kebekus/nevanlinna
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Working…

Browse Source
This commit is contained in:
Stefan Kebekus
2024-12-19 16:10:51 +01:00
parent e5b49993b7
commit 4cc853a5d9
6 changed files with 330 additions and 193 deletions
Download Patch File Download Diff File Expand all files Collapse all files

49
Nevanlinna/firstMain.lean
View File

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

98
Nevanlinna/intervalIntegrability.lean Normal file
View File

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

36
Nevanlinna/logpos.lean Normal file
View File

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

246
Nevanlinna/meromorphicOn_integrability.lean
View File

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

92
Nevanlinna/specialFunctions_CircleIntegral_affine.lean
View File

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