diff --git a/Nevanlinna/stronglyMeromorphic_JensenFormula.lean b/Nevanlinna/stronglyMeromorphic_JensenFormula.lean new file mode 100644 index 0000000..4b0fded --- /dev/null +++ b/Nevanlinna/stronglyMeromorphic_JensenFormula.lean @@ -0,0 +1,449 @@ +import Mathlib.Analysis.Complex.CauchyIntegral +import Mathlib.Analysis.Analytic.IsolatedZeros +import Nevanlinna.analyticOnNhd_zeroSet +import Nevanlinna.harmonicAt_examples +import Nevanlinna.harmonicAt_meanValue +import Nevanlinna.specialFunctions_CircleIntegral_affine +import Nevanlinna.stronglyMeromorphicOn +import Nevanlinna.stronglyMeromorphicOn_eliminate +import Nevanlinna.meromorphicOn_divisor + +open Real + + + +theorem jensen_case_R_eq_one + (f : ℂ → ℂ) + (h₁f : StronglyMeromorphicOn f (Metric.closedBall 0 1)) + (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 + + have h₁U : IsConnected (Metric.closedBall (0 : ℂ) 1) := by + constructor + · exact Set.Nonempty.of_subtype + · exact (convex_closedBall (0 : ℂ) 1).isPreconnected + + have h₂U : IsCompact (Metric.closedBall (0 : ℂ) 1) := + isCompact_closedBall 0 1 + + have h'₂f : ∃ u : (Metric.closedBall (0 : ℂ) 1), f u ≠ 0 := by + use ⟨0, Metric.mem_closedBall_self (by simp)⟩ + + obtain ⟨F, h₁F, h₂F, h₃F, h₄F⟩ := MeromorphicOn.decompose₃' h₂U h₁U h₁f h'₂f + + let G := fun z ↦ log ‖F z‖ + ∑ s ∈ (finiteZeros h₁U h₂U h₁f h'₂f).toFinset, (h₁f.order s).toNat * log ‖z - s‖ + + have decompose_f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, f z ≠ 0 → log ‖f z‖ = G z := by + intro z h₁z h₂z + + conv => + left + arg 1 + rw [h₃F] + rw [smul_eq_mul] + rw [norm_mul] + rw [norm_prod] + left + arg 2 + intro b + rw [norm_pow] + simp only [Complex.norm_eq_abs, Finset.univ_eq_attach] + rw [Real.log_mul] + rw [Real.log_prod] + conv => + left + left + arg 2 + intro s + rw [Real.log_pow] + dsimp [G] + abel + + -- ∀ x ∈ ⋯.toFinset, Complex.abs (z - ↑x) ^ (h'₁f.order x).toNat ≠ 0 + have : ∀ x ∈ (finiteZeros h₁U h₂U h₁f h'₂f).toFinset, Complex.abs (z - ↑x) ^ (h₁f.order x).toNat ≠ 0 := by + intro s hs + simp at hs + simp + intro h₂s + rw [h₂s] at h₂z + tauto + exact this + + -- ∏ x ∈ ⋯.toFinset, Complex.abs (z - ↑x) ^ (h'₁f.order x).toNat ≠ 0 + have : ∀ x ∈ (finiteZeros h₁U h₂U h₁f h'₂f).toFinset, Complex.abs (z - ↑x) ^ (h₁f.order x).toNat ≠ 0 := by + intro s hs + simp at hs + simp + intro h₂s + rw [h₂s] at h₂z + tauto + rw [Finset.prod_ne_zero_iff] + exact this + + -- Complex.abs (F z) ≠ 0 + simp + exact h₂F z h₁z + + + 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 + + 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)⁻¹' (Metric.closedBall 0 1 ∩ f⁻¹' {0}) := by + intro a ha + simp at ha + simp + by_contra C + have : (circleMap 0 1 a) ∈ Metric.closedBall 0 1 := + circleMap_mem_closedBall 0 (zero_le_one' ℝ) a + exact ha.2 (decompose_f (circleMap 0 1 a) this C) + + apply Set.Countable.mono t₀ + apply Set.Countable.preimage_circleMap + apply Set.Finite.countable + let A := finiteZeros h₁U h₂U h₁f h'₂f + + have : (Metric.closedBall 0 1 ∩ f ⁻¹' {0}) = (Metric.closedBall 0 1).restrict f ⁻¹' {0} := by + ext z + simp + tauto + rw [this] + exact Set.Finite.image Subtype.val A + exact Ne.symm (zero_ne_one' ℝ) + + + 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 ∈ (finiteZeros h₁U h₂U h₁f h'₂f).toFinset, (h₁f.order x).toNat * ∫ (x_1 : ℝ) in (0)..2 * π, log (Complex.abs (circleMap 0 1 x_1 - ↑x)) := by + dsimp [G] + rw [intervalIntegral.integral_add] + rw [intervalIntegral.integral_finset_sum] + simp_rw [intervalIntegral.integral_const_mul] + + -- ∀ i ∈ (finiteZeros h₁U h₂U h'₁f h'₂f).toFinset, + -- IntervalIntegrable (fun x => (h'₁f.order i).toNat * + -- 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.1‖ = 1 + -- case pos + 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) := + 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 1 x] + simp + tauto + 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 1 x)))) = log ∘ Complex.abs ∘ F ∘ (fun x ↦ circleMap 0 1 x) := + rfl + rw [this] + apply ContinuousAt.comp + apply Real.continuousAt_log + simp [h₂F] + -- 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 HolomorphicAt.differentiableAt + simp [h'₁F] + -- ContinuousAt (fun x => circleMap 0 1 x) x + apply Continuous.continuousAt + apply continuous_circleMap + + have : (fun x => ∑ s ∈ (finiteZeros h₁U h₂U h₁f h'₂f).toFinset, (h₁f.order s).toNat * log (Complex.abs (circleMap 0 1 x - ↑s))) + = ∑ s ∈ (finiteZeros h₁U h₂U h₁f h'₂f).toFinset, (fun x => (h₁f.order s).toNat * log (Complex.abs (circleMap 0 1 x - ↑s))) := by + funext x + simp + rw [this] + apply IntervalIntegrable.sum + intro i _ + apply IntervalIntegrable.const_mul + --have : i.1 ∈ Metric.closedBall (0 : ℂ) 1 := i.2 + --simp at this + by_cases h₂i : ‖i.1‖ = 1 + -- case pos + exact int'₂ h₂i + -- 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) := + 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 1 x] + simp + tauto + 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 + let logAbsF := fun w ↦ Real.log ‖F w‖ + have t₀ : ∀ z ∈ Metric.closedBall 0 1, HarmonicAt logAbsF z := by + intro z hz + apply logabs_of_holomorphicAt_is_harmonic + apply h'₁F z hz + exact h₂F z hz + + apply harmonic_meanValue₁ 1 Real.zero_lt_one t₀ + + simp_rw [← Complex.norm_eq_abs] at decompose_int_G + rw [t₁] at decompose_int_G + + conv at decompose_int_G => + right + right + arg 2 + intro x + right + rw [int₃ x.2] + simp at decompose_int_G + + rw [int_logAbs_f_eq_int_G] + rw [decompose_int_G] + rw [h₃F] + simp + have {l : ℝ} : π⁻¹ * 2⁻¹ * (2 * π * l) = l := by + calc π⁻¹ * 2⁻¹ * (2 * π * l) + _ = π⁻¹ * (2⁻¹ * 2) * π * l := by ring + _ = π⁻¹ * π * l := by ring + _ = (π⁻¹ * π) * l := by ring + _ = 1 * l := by + rw [inv_mul_cancel₀] + exact pi_ne_zero + _ = l := by simp + rw [this] + rw [log_mul] + rw [log_prod] + simp + + rw [finsum_eq_sum_of_support_subset _ (s := (finiteZeros h₁U h₂U h₁f h'₂f).toFinset)] + simp + simp + intro x ⟨h₁x, _⟩ + simp + + dsimp [AnalyticOnNhd.order] at h₁x + simp only [Function.mem_support, ne_eq, Nat.cast_eq_zero, not_or] at h₁x + exact AnalyticAt.supp_order_toNat (AnalyticOnNhd.order.proof_1 h₁f x) h₁x + + -- + intro x hx + simp at hx + simp + intro h₁x + nth_rw 1 [← h₁x] at h₂f + tauto + + -- + rw [Finset.prod_ne_zero_iff] + intro x hx + simp at hx + simp + intro h₁x + nth_rw 1 [← h₁x] at h₂f + tauto + + -- + simp + apply h₂F + simp + + +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 : AnalyticOnNhd ℂ f (Metric.closedBall 0 R)) + (h₂f : f 0 ≠ 0) : + log ‖f 0‖ = -∑ᶠ s, (h₁f.order s).toNat * log (R * ‖s.1‖⁻¹) + (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 : AnalyticOnNhd ℂ F (Metric.closedBall 0 1) := by + 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)