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-03 17:21:22 +01:00
parent ad298459ee
commit ae3e64c83b
1 changed files with 62 additions and 216 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

278
Nevanlinna/stronglyMeromorphic_JensenFormula.lean
View File

@ -11,28 +11,30 @@ import Nevanlinna.meromorphicOn_divisor
open Real
theorem jensen_case_R_eq_one'
theorem jensen
{R : ℝ}
(hR : 0 < R)
(f : ℂ → ℂ)
(h₁f : StronglyMeromorphicOn f (Metric.closedBall 0 1))
(h₁f : StronglyMeromorphicOn f (Metric.closedBall 0 R))
(h₂f : f 0 ≠ 0) :
log ‖f 0‖ = -∑ᶠ s, (h₁f.meromorphicOn.divisor s) * log (‖s‖⁻¹) + (2 * π)⁻¹ * ∫ (x : ℝ) in (0)..(2 * π), log ‖f (circleMap 0 1 x)‖ := by
log ‖f 0‖ = -∑ᶠ s, (h₁f.meromorphicOn.divisor s) * log (R * ‖s‖⁻¹) + (2 * π)⁻¹ * ∫ (x : ℝ) in (0)..(2 * π), log ‖f (circleMap 0 R x)‖ := by
have h₁U : IsConnected (Metric.closedBall (0 : ℂ) 1) := by
have h₁U : IsConnected (Metric.closedBall (0 : ℂ) R) := by
constructor
· apply Metric.nonempty_closedBall.mpr (by simp)
· exact (convex_closedBall (0 : ℂ) 1).isPreconnected
· apply Metric.nonempty_closedBall.mpr
exact le_of_lt hR
· exact (convex_closedBall (0 : ℂ) R).isPreconnected
have h₂U : IsCompact (Metric.closedBall (0 : ℂ) 1) :=
isCompact_closedBall 0 1
have h₂U : IsCompact (Metric.closedBall (0 : ℂ) R) :=
isCompact_closedBall 0 R
have h'₂f : ∃ u : (Metric.closedBall (0 : ℂ) 1), f u ≠ 0 := by
use ⟨0, Metric.mem_closedBall_self (by simp)⟩
have h'₂f : ∃ u : (Metric.closedBall (0 : ℂ) R), f u ≠ 0 := by
use ⟨0, Metric.mem_closedBall_self (le_of_lt hR)⟩
have h₃f : Set.Finite (Function.support h₁f.meromorphicOn.divisor) := by
exact Divisor.finiteSupport h₂U (StronglyMeromorphicOn.meromorphicOn h₁f).divisor
have h₄f: Function.support (fun s ↦ (h₁f.meromorphicOn.divisor s) * log (‖s‖⁻¹)) ⊆ h₃f.toFinset := by
have h₄f: Function.support (fun s ↦ (h₁f.meromorphicOn.divisor s) * log (R * ‖s‖⁻¹)) ⊆ h₃f.toFinset := by
intro x
contrapose
simp
@ -63,7 +65,7 @@ theorem jensen_case_R_eq_one'
rw [hs]
simp
have decompose_f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, f z ≠ 0 → log ‖f z‖ = G z := by
have decompose_f : ∀ z ∈ Metric.closedBall (0 : ℂ) R, f z ≠ 0 → log ‖f z‖ = G z := by
intro z h₁z h₂z
rw [h₄F]
@ -104,40 +106,41 @@ theorem jensen_case_R_eq_one'
simpa
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
have int_logAbs_f_eq_int_G : ∫ (x : ℝ) in (0)..2 * π, log ‖f (circleMap 0 R x)‖ = ∫ (x : ℝ) in (0)..2 * π, G (circleMap 0 R 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)⁻¹' (h₃f.toFinset) := by
have t₀ : {a | a ∈ Ι 0 (2 * π) ∧ ¬log ‖f (circleMap 0 R a)‖ = G (circleMap 0 R a)}
⊆ (circleMap 0 R)⁻¹' (h₃f.toFinset) := by
intro a ha
simp at ha
simp
by_contra C
have t₀ : (circleMap 0 1 a) ∈ Metric.closedBall 0 1 :=
circleMap_mem_closedBall 0 (zero_le_one' ℝ) a
have t₁ : f (circleMap 0 1 a) ≠ 0 := by
let A := h₁f (circleMap 0 1 a) t₀
have t₀ : (circleMap 0 R a) ∈ Metric.closedBall 0 R := by
apply circleMap_mem_closedBall
exact le_of_lt hR
have t₁ : f (circleMap 0 R a) ≠ 0 := by
let A := h₁f (circleMap 0 R a) t₀
rw [← A.order_eq_zero_iff]
unfold MeromorphicOn.divisor at C
simp [t₀] at C
rcases C with C₁|C₂
· assumption
· let B := h₁f.meromorphicOn.order_ne_top' h₁U
let C := fun q ↦ B q ⟨(circleMap 0 1 a), t₀⟩
let C := fun q ↦ B q ⟨(circleMap 0 R a), t₀⟩
rw [C₂] at C
have : ∃ u : (Metric.closedBall (0 : ℂ) 1), (h₁f u u.2).meromorphicAt.order ≠ ⊤ := by
use ⟨(0 : ℂ), (by simp)⟩
let H := h₁f 0 (by simp)
have : ∃ u : (Metric.closedBall (0 : ℂ) R), (h₁f u u.2).meromorphicAt.order ≠ ⊤ := by
use ⟨(0 : ℂ), (by simp; exact le_of_lt hR)⟩
let H := h₁f 0 (by simp; exact le_of_lt hR)
let K := H.order_eq_zero_iff.2 h₂f
rw [K]
simp
let D := C this
tauto
exact ha.2 (decompose_f (circleMap 0 1 a) t₀ t₁)
exact ha.2 (decompose_f (circleMap 0 R a) t₀ t₁)
apply Set.Countable.mono t₀
apply Set.Countable.preimage_circleMap
@ -147,14 +150,14 @@ theorem jensen_case_R_eq_one'
simp
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, (h₁f.meromorphicOn.divisor x) * ∫ (x_1 : ℝ) in (0)..2 * π, log (Complex.abs (circleMap 0 1 x_1 - ↑x)) := by
have decompose_int_G : ∫ (x : ℝ) in (0)..2 * π, G (circleMap 0 R x)
= (∫ (x : ℝ) in (0)..2 * π, log (Complex.abs (F (circleMap 0 R x))))
+ ∑ᶠ x, (h₁f.meromorphicOn.divisor x) * ∫ (x_1 : ℝ) in (0)..2 * π, log (Complex.abs (circleMap 0 R x_1 - ↑x)) := by
dsimp [G]
rw [intervalIntegral.integral_add]
congr
have t₀ {x : ℝ} : Function.support (fun s ↦ (h₁f.meromorphicOn.divisor s) * log (Complex.abs (circleMap 0 1 x - s))) ⊆ h₃f.toFinset := by
have t₀ {x : ℝ} : Function.support (fun s ↦ (h₁f.meromorphicOn.divisor s) * log (Complex.abs (circleMap 0 R x - s))) ⊆ h₃f.toFinset := by
intro s hs
simp at hs
simp [hs.1]
@ -164,8 +167,8 @@ theorem jensen_case_R_eq_one'
intro x
rw [finsum_eq_sum_of_support_subset _ t₀]
rw [intervalIntegral.integral_finset_sum]
let G' := fun x ↦ ((h₁f.meromorphicOn.divisor x) : ℂ) * ∫ (x_1 : ℝ) in (0)..2 * π, log (Complex.abs (circleMap 0 1 x_1 - x))
have t₁ : (Function.support fun x ↦ (h₁f.meromorphicOn.divisor x) * ∫ (x_1 : ℝ) in (0)..2 * π, log (Complex.abs (circleMap 0 1 x_1 - x))) ⊆ h₃f.toFinset := by
let G' := fun x ↦ ((h₁f.meromorphicOn.divisor x) : ℂ) * ∫ (x_1 : ℝ) in (0)..2 * π, log (Complex.abs (circleMap 0 R x_1 - x))
have t₁ : (Function.support fun x ↦ (h₁f.meromorphicOn.divisor x) * ∫ (x_1 : ℝ) in (0)..2 * π, log (Complex.abs (circleMap 0 R x_1 - x))) ⊆ h₃f.toFinset := by
simp
intro s
contrapose!
@ -182,14 +185,15 @@ theorem jensen_case_R_eq_one'
intro i _
apply IntervalIntegrable.const_mul
--simp at this
by_cases h₂i : ‖i‖ = 1
by_cases h₂i : ‖i‖ = R
-- case pos
exact int'₂ h₂i
sorry
--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) :=
have : (fun x => log (Complex.abs (circleMap 0 R x - ↑i))) = log ∘ Complex.abs ∘ (fun x ↦ circleMap 0 R x - ↑i) :=
rfl
rw [this]
apply ContinuousAt.comp
@ -201,9 +205,10 @@ theorem jensen_case_R_eq_one'
arg 1
rw [← ha']
rw [Complex.norm_eq_abs]
rw [abs_circleMap_zero 1 x]
rw [abs_circleMap_zero R x]
simp
tauto
linarith
--
apply ContinuousAt.comp
apply Complex.continuous_abs.continuousAt
fun_prop
@ -211,13 +216,18 @@ theorem jensen_case_R_eq_one'
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) :=
have : (fun x => log (Complex.abs (F (circleMap 0 R x)))) = log ∘ Complex.abs ∘ F ∘ (fun x ↦ circleMap 0 R x) :=
rfl
rw [this]
apply ContinuousAt.comp
apply Real.continuousAt_log
simp
exact h₃F ⟨(circleMap 0 1 x), (by simp)⟩
have : (circleMap 0 R x) ∈ (Metric.closedBall 0 R) := by
simp
rw [abs_le]
simp [hR]
exact le_of_lt hR
exact h₃F ⟨(circleMap 0 R x), this⟩
-- ContinuousAt (⇑Complex.abs ∘ F ∘ fun x => circleMap 0 1 x) x
apply ContinuousAt.comp
@ -225,7 +235,8 @@ theorem jensen_case_R_eq_one'
apply ContinuousAt.comp
apply DifferentiableAt.continuousAt (𝕜 := ℂ)
apply AnalyticAt.differentiableAt
exact h₂F (circleMap 0 1 x) (by simp)
apply h₂F (circleMap 0 R x)
simp; rw [abs_le]; simp [hR]; exact le_of_lt hR
-- ContinuousAt (fun x => circleMap 0 1 x) x
apply Continuous.continuousAt
apply continuous_circleMap
@ -245,15 +256,16 @@ theorem jensen_case_R_eq_one'
apply IntervalIntegrable.const_mul
--have : i.1 ∈ Metric.closedBall (0 : ℂ) 1 := i.2
--simp at this
by_cases h₂i : ‖i‖ = 1
by_cases h₂i : ‖i‖ = R
-- case pos
exact int'₂ h₂i
--exact int'₂ h₂i
sorry
-- 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) :=
have : (fun x => log (Complex.abs (circleMap 0 R x - ↑i))) = log ∘ Complex.abs ∘ (fun x ↦ circleMap 0 R x - ↑i) :=
rfl
rw [this]
apply ContinuousAt.comp
@ -265,33 +277,34 @@ theorem jensen_case_R_eq_one'
arg 1
rw [← ha']
rw [Complex.norm_eq_abs]
rw [abs_circleMap_zero 1 x]
rw [abs_circleMap_zero R x]
simp
tauto
linarith
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
have t₁ : (∫ (x : ℝ) in (0)..2 * Real.pi, log ‖F (circleMap 0 R 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
have t₀ : ∀ z ∈ Metric.closedBall 0 R, HarmonicAt logAbsF z := by
intro z hz
apply logabs_of_holomorphicAt_is_harmonic
exact AnalyticAt.holomorphicAt (h₂F z hz)
exact h₃F ⟨z, hz⟩
apply harmonic_meanValue₁ 1 Real.zero_lt_one t₀
apply harmonic_meanValue₁ R hR t₀
simp_rw [← Complex.norm_eq_abs] at decompose_int_G
rw [t₁] at decompose_int_G
have h₁G' : (Function.support fun s => (h₁f.meromorphicOn.divisor s) * ∫ (x_1 : ℝ) in (0)..(2 * π), log ‖circleMap 0 1 x_1 - s‖) ⊆ ↑h₃f.toFinset := by
have h₁G' : (Function.support fun s => (h₁f.meromorphicOn.divisor s) * ∫ (x_1 : ℝ) in (0)..(2 * π), log ‖circleMap 0 R x_1 - s‖) ⊆ ↑h₃f.toFinset := by
intro s hs
simp at hs
simp [hs.1]
rw [finsum_eq_sum_of_support_subset _ h₁G'] at decompose_int_G
have : ∑ s ∈ h₃f.toFinset, (h₁f.meromorphicOn.divisor s) * ∫ (x_1 : ℝ) in (0)..(2 * π), log ‖circleMap 0 1 x_1 - s‖ = 0 := by
have : ∑ s ∈ h₃f.toFinset, (h₁f.meromorphicOn.divisor s) * ∫ (x_1 : ℝ) in (0)..(2 * π), log ‖circleMap 0 R x_1 - s‖ = 0 := by
apply Finset.sum_eq_zero
intro x hx
rw [int₃ _]
@ -359,170 +372,3 @@ theorem jensen_case_R_eq_one'
rw [h₂f] at hx
tauto
assumption
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 : StronglyMeromorphicOn f (Metric.closedBall 0 R))
(h₂f : f 0 ≠ 0) :
log ‖f 0‖ = -∑ᶠ s, (h₁f.meromorphicOn.divisor s) * log (R * ‖s‖⁻¹) + (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 : StronglyMeromorphicOn F (Metric.closedBall 0 1) := by
sorry
/-
apply AnalyticOnNhd.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
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
simp
by_cases hx : x = (0 : ℂ)
rw [hx]
simp
rw [log_mul, log_mul, log_inv, log_inv]
have : R = |R| := by exact Eq.symm (abs_of_pos hR)
rw [← this]
simp
left
congr 1
dsimp [AnalyticOnNhd.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)