diff --git a/Nevanlinna/firstMain.lean b/Nevanlinna/firstMain.lean index 10d86df..5e30048 100644 --- a/Nevanlinna/firstMain.lean +++ b/Nevanlinna/firstMain.lean @@ -30,27 +30,28 @@ noncomputable def MeromorphicOn.N_zero {f : ℂ → ℂ} (hf : MeromorphicOn f ⊤) : ℝ → ℝ := - fun r ↦ ∑ᶠ z, (max 0 ((hf.restrict r).divisor z)) * log (r * ‖z‖⁻¹) + fun r ↦ ∑ᶠ z, (max 0 ((hf.restrict |r|).divisor z)) * log (r * ‖z‖⁻¹) noncomputable def MeromorphicOn.N_infty {f : ℂ → ℂ} (hf : MeromorphicOn f ⊤) : ℝ → ℝ := - fun r ↦ ∑ᶠ z, (max 0 (-((hf.restrict r).divisor z))) * log (r * ‖z‖⁻¹) + fun r ↦ ∑ᶠ z, (max 0 (-((hf.restrict |r|).divisor z))) * log (r * ‖z‖⁻¹) theorem Nevanlinna_counting₀ {f : ℂ → ℂ} (hf : MeromorphicOn f ⊤) : hf.inv.N_infty = hf.N_zero := by + funext r unfold MeromorphicOn.N_zero MeromorphicOn.N_infty - let A := (hf.restrict r).divisor.finiteSupport (isCompact_closedBall 0 r) + let A := (hf.restrict |r|).divisor.finiteSupport (isCompact_closedBall 0 |r|) repeat rw [finsum_eq_sum_of_support_subset (s := A.toFinset)] apply Finset.sum_congr rfl intro x hx congr - rw [hf.restrict_inv r] + let B := hf.restrict_inv |r| rw [MeromorphicOn.divisor_inv] simp -- @@ -67,9 +68,8 @@ theorem Nevanlinna_counting₀ contrapose simp intro hx h₁x - rw [hf.restrict_inv r] at h₁x - have hh : MeromorphicOn f (Metric.closedBall 0 r) := hf.restrict r - rw [hh.divisor_inv] at h₁x + + rw [MeromorphicOn.divisor_inv (hf.restrict |r|)] at h₁x simp at h₁x rw [hx] at h₁x tauto @@ -78,13 +78,13 @@ theorem Nevanlinna_counting₀ theorem Nevanlinna_counting {f : ℂ → ℂ} (hf : MeromorphicOn f ⊤) : - hf.N_zero - hf.N_infty = fun r ↦ ∑ᶠ z, ((hf.restrict r).divisor z) * log (r * ‖z‖⁻¹) := by + hf.N_zero - hf.N_infty = fun r ↦ ∑ᶠ z, ((hf.restrict |r|).divisor z) * log (r * ‖z‖⁻¹) := by funext r simp only [Pi.sub_apply] unfold MeromorphicOn.N_zero MeromorphicOn.N_infty - let A := (hf.restrict r).divisor.finiteSupport (isCompact_closedBall 0 r) + let A := (hf.restrict |r|).divisor.finiteSupport (isCompact_closedBall 0 |r|) repeat rw [finsum_eq_sum_of_support_subset (s := A.toFinset)] rw [← Finset.sum_sub_distrib] @@ -92,9 +92,9 @@ theorem Nevanlinna_counting congr funext x congr - by_cases h : 0 ≤ (hf.restrict r).divisor x + by_cases h : 0 ≤ (hf.restrict |r|).divisor x · simp [h] - · have h' : 0 ≤ -((hf.restrict r).divisor x) := by + · have h' : 0 ≤ -((hf.restrict |r|).divisor x) := by simp at h apply Int.le_neg_of_le_neg simp @@ -154,7 +154,7 @@ theorem Nevanlinna_firstMain₁ (h₁f : MeromorphicOn f ⊤) (h₂f : StronglyMeromorphicAt f 0) (h₃f : f 0 ≠ 0) : - (fun r ↦ log ‖f 0‖) + h₁f.inv.T_infty = h₁f.T_infty := by + (fun _ ↦ log ‖f 0‖) + h₁f.inv.T_infty = h₁f.T_infty := by rw [add_eq_of_eq_sub] unfold MeromorphicOn.T_infty @@ -170,10 +170,55 @@ theorem Nevanlinna_firstMain₁ simp rw [← Nevanlinna_proximity h₁f] - have hr : 0 < r := by sorry + by_cases h₁r : r = 0 + rw [h₁r] + simp + have : π⁻¹ * 2⁻¹ * (2 * π * log (Complex.abs (f 0))) = (π⁻¹ * (2⁻¹ * 2) * π) * log (Complex.abs (f 0)) := by + ring + rw [this] + clear this + simp [pi_ne_zero] + + by_cases hr : 0 < r + let A := jensen hr f (h₁f.restrict r) h₂f h₃f + simp at A + rw [A] + clear A + simp + have {A B : ℝ} : -A + B = B - A := by ring + rw [this] + have : |r| = r := by + rw [← abs_of_pos hr] + simp + rw [this] + + -- case 0 < -r + have h₂r : 0 < -r := by + simp [h₁r, hr] + by_contra hCon + -- Assume ¬(r < 0), which means r >= 0 + push_neg at hCon + -- Now h is r ≥ 0, so we split into cases + rcases lt_or_eq_of_le hCon with h|h + · tauto + · tauto + let A := jensen h₂r f (h₁f.restrict (-r)) h₂f h₃f + simp at A + rw [A] + clear A + simp + have {A B : ℝ} : -A + B = B - A := by ring + rw [this] + + congr 1 + congr 1 + let A := integrabl_congr_negRadius (f := (fun z ↦ log (Complex.abs (f z)))) (r := r) + rw [A] + have : |r| = -r := by + rw [← abs_of_pos h₂r] + simp + rw [this] - let A := jensen - sorry theorem Nevanlinna_firstMain₂ {f : ℂ → ℂ} @@ -181,4 +226,5 @@ theorem Nevanlinna_firstMain₂ {r : ℝ} (h₁f : MeromorphicOn f ⊤) : |(h₁f.T_infty r) - ((h₁f.sub (MeromorphicOn.const a)).T_infty r)| ≤ logpos ‖a‖ + log 2 := by + sorry diff --git a/Nevanlinna/stronglyMeromorphic_JensenFormula.lean b/Nevanlinna/stronglyMeromorphic_JensenFormula.lean index ee21ca5..ea597a0 100644 --- a/Nevanlinna/stronglyMeromorphic_JensenFormula.lean +++ b/Nevanlinna/stronglyMeromorphic_JensenFormula.lean @@ -96,7 +96,7 @@ theorem jensen₀ by_contra hCon rw [← hCon] at hx simp at hx - rw [← StronglyMeromorphicAt.order_eq_zero_iff] at h₂z + rw [← (h₁f z h₁z).order_eq_zero_iff] at h₂z unfold MeromorphicOn.divisor at hx simp [h₁z] at hx tauto @@ -112,7 +112,7 @@ theorem jensen₀ by_contra hCon rw [← hCon] at hx simp at hx - rw [← StronglyMeromorphicAt.order_eq_zero_iff] at h₂z + rw [← (h₁f z h₁z).order_eq_zero_iff] at h₂z unfold MeromorphicOn.divisor at hx simp [h₁z] at hx tauto @@ -198,62 +198,28 @@ theorem jensen₀ -- log (Complex.abs (circleMap 0 1 x - ↑i))) MeasureTheory.volume 0 (2 * π) intro i _ apply IntervalIntegrable.const_mul - --simp at this - by_cases h₂i : ‖i‖ = R - -- case pos - sorry - --exact int'₂ h₂i + apply intervalIntegrable_logAbs_circleMap_sub_const + linarith + -- -- case neg apply Continuous.intervalIntegrable apply continuous_iff_continuousAt.2 intro x - have : (fun x => log (Complex.abs (circleMap 0 R x - ↑i))) = log ∘ Complex.abs ∘ (fun x ↦ circleMap 0 R x - ↑i) := + have : (fun x => log (Complex.abs ( F (circleMap 0 R x)))) = log ∘ Complex.abs ∘ F ∘ circleMap 0 R := rfl rw [this] apply ContinuousAt.comp apply Real.continuousAt_log simp - - by_contra ha' - conv at h₂i => - arg 1 - rw [← ha'] - rw [Complex.norm_eq_abs] - rw [abs_circleMap_zero R x] - simp - linarith + let A := h₃F ⟨(circleMap 0 R x), circleMap_mem_closedBall 0 (le_of_lt hR) x⟩ + exact A -- apply ContinuousAt.comp apply Complex.continuous_abs.continuousAt - fun_prop - -- IntervalIntegrable (fun x => log (Complex.abs (F (circleMap 0 1 x)))) MeasureTheory.volume 0 (2 * π) - apply Continuous.intervalIntegrable - apply continuous_iff_continuousAt.2 - intro 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 - 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 - apply Complex.continuous_abs.continuousAt - apply ContinuousAt.comp - apply DifferentiableAt.continuousAt (𝕜 := ℂ) - apply AnalyticAt.differentiableAt - 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 + let A := h₂F (circleMap 0 R x) (circleMap_mem_closedBall 0 (le_of_lt hR) x) + apply A.continuousAt + exact (continuous_circleMap 0 R).continuousAt -- IntervalIntegrable (fun x => ∑ᶠ (s : ℂ), ↑(↑⋯.divisor s) * log (Complex.abs (circleMap 0 1 x - s))) MeasureTheory.volume 0 (2 * π) --simp? at h₁G have h₁G' {z : ℂ} : (Function.support fun s => (h₁f.meromorphicOn.divisor s) * log (Complex.abs (z - s))) ⊆ ↑h₃f.toFinset := by @@ -273,9 +239,8 @@ theorem jensen₀ by_cases h₂i : ‖i‖ = R -- case pos --exact int'₂ h₂i - sorry + apply intervalIntegrable_logAbs_circleMap_sub_const (Ne.symm (ne_of_lt hR)) -- case neg - --have : i.1 ∈ Metric.ball (0 : ℂ) 1 := by sorry apply Continuous.intervalIntegrable apply continuous_iff_continuousAt.2 intro x