import Mathlib.Analysis.Complex.CauchyIntegral import Mathlib.Analysis.Analytic.IsolatedZeros import Nevanlinna.analyticOn_zeroSet import Nevanlinna.harmonicAt_examples import Nevanlinna.harmonicAt_meanValue import Nevanlinna.specialFunctions_CircleIntegral_affine open Real theorem jensen_case_R_eq_one (f : ℂ → ℂ) (h₁f : AnalyticOnNhd ℂ f (Metric.closedBall 0 1)) (h₂f : f 0 ≠ 0) : log ‖f 0‖ = -∑ᶠ s, (h₁f.order s).toNat * log (‖s.1‖⁻¹) + (2 * π)⁻¹ * ∫ (x : ℝ) in (0)..(2 * π), log ‖f (circleMap 0 1 x)‖ := by have h₁U : IsPreconnected (Metric.closedBall (0 : ℂ) 1) := (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; simp; exact h₂f obtain ⟨F, h₁F, h₂F, h₃F⟩ := AnalyticOnNhdCompact.eliminateZeros₂ h₁U h₂U h₁f h'₂f have h'₁F : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt F z := by intro z h₁z apply AnalyticAt.holomorphicAt exact h₁F z h₁z 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)