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 noncomputable def Zeroset {f : ℂ → ℂ} {s : Set ℂ} (hf : ∀ z ∈ s, HolomorphicAt f z) : Set ℂ := by exact f⁻¹' {0} ∩ s noncomputable def ZeroFinset {f : ℂ → ℂ} (h₁f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt f z) (h₂f : f 0 ≠ 0) : Finset ℂ := by let Z := f⁻¹' {0} ∩ Metric.closedBall (0 : ℂ) 1 have hZ : Set.Finite Z := by dsimp [Z] rw [Set.inter_comm] apply finiteZeros -- Ball is preconnected apply IsConnected.isPreconnected apply Convex.isConnected exact convex_closedBall 0 1 exact Set.nonempty_of_nonempty_subtype -- exact isCompact_closedBall 0 1 -- intro x hx have A := (h₁f x hx) let B := HolomorphicAt_iff.1 A obtain ⟨s, h₁s, h₂s, h₃s⟩ := B apply DifferentiableOn.analyticAt (s := s) intro z hz apply DifferentiableAt.differentiableWithinAt apply h₃s exact hz exact IsOpen.mem_nhds h₁s h₂s -- use 0 constructor · simp · exact h₂f exact hZ.toFinset lemma ZeroFinset_mem_iff {f : ℂ → ℂ} (h₁f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt f z) {h₂f : f 0 ≠ 0} (z : ℂ) : z ∈ ↑(ZeroFinset h₁f h₂f) ↔ z ∈ Metric.closedBall 0 1 ∧ f z = 0 := by dsimp [ZeroFinset]; simp tauto noncomputable def order {f : ℂ → ℂ} {h₁f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt f z} {h₂f : f 0 ≠ 0} : ZeroFinset h₁f h₂f → ℕ := by intro i let A := ((ZeroFinset_mem_iff h₁f i).1 i.2).1 let B := (h₁f i.1 A).analyticAt exact B.order.toNat theorem jensen_case_R_eq_one (f : ℂ → ℂ) (h₁f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt f z) (h'₁f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, AnalyticAt ℂ f z) (h₂f : f 0 ≠ 0) : log ‖f 0‖ = -∑ s : (ZeroFinset h₁f h₂f), order s * log (‖s.1‖⁻¹) + (2 * π )⁻¹ * ∫ (x : ℝ) in (0)..2 * π, log ‖f (circleMap 0 1 x)‖ := by have F : ℂ → ℂ := by sorry have h₁F : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt F z := by sorry have h₂F : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, F z ≠ 0 := by sorry have h₃F : f = fun z ↦ (F z) * ∏ s : ZeroFinset h₁f h₂f, (z - s) ^ (order s) := by sorry let G := fun z ↦ log ‖F z‖ + ∑ s : ZeroFinset h₁f h₂f, (order s) * 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 [norm_mul] rw [norm_prod] right 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 right arg 2 intro s rw [Real.log_pow] dsimp [G] -- ∀ x ∈ (ZeroFinset h₁f).attach, Complex.abs (z - ↑x) ^ order x ≠ 0 simp intro s hs rw [ZeroFinset_mem_iff h₁f s] at hs rw [← hs.2] at h₂z tauto -- Complex.abs (F z) ≠ 0 simp exact h₂F z h₁z -- ∏ I : { x // x ∈ S }, Complex.abs (z - a I) ≠ 0 by_contra C obtain ⟨s, h₁s, h₂s⟩ := Finset.prod_eq_zero_iff.1 C simp at h₂s rw [← ((ZeroFinset_mem_iff h₁f s).1 (Finset.coe_mem s)).2, h₂s.1] at h₂z tauto have : ∫ (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 := by sorry 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 apply finiteZeros -- IsPreconnected (Metric.closedBall (0 : ℂ) 1) apply IsConnected.isPreconnected apply Convex.isConnected exact convex_closedBall 0 1 exact Set.nonempty_of_nonempty_subtype -- exact isCompact_closedBall 0 1 -- exact h'₁f use 0 exact ⟨Metric.mem_closedBall_self (zero_le_one' ℝ), h₂f⟩ exact Ne.symm (zero_ne_one' ℝ) have h₁Gi : ∀ i ∈ (ZeroFinset h₁f h₂f).attach, IntervalIntegrable (fun x => log (Complex.abs (circleMap 0 1 x - ↑i))) MeasureTheory.volume 0 (2 * π) := by -- This is hard. Need to invoke specialFunctions_CircleIntegral_affine. sorry have : ∫ (x : ℝ) in (0)..2 * π, G (circleMap 0 1 x) = (∫ (x : ℝ) in (0)..2 * π, log (Complex.abs (F (circleMap 0 1 x)))) + ∑ x ∈ (ZeroFinset h₁f h₂f).attach, ↑(order x) * ∫ (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 ∈ (ZeroFinset h₁f).attach, IntervalIntegrable (fun x => ↑(order i) * -- log (Complex.abs (circleMap 0 1 x - ↑i))) MeasureTheory.volume 0 (2 * π) intro i hi apply IntervalIntegrable.const_mul have : i.1 ∈ Metric.closedBall (0 : ℂ) 1 := by exact ((ZeroFinset_mem_iff h₁f i).1 i.2).1 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 -- 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] -- apply ContinuousAt.comp apply Complex.continuous_abs.continuousAt apply ContinuousAt.comp apply DifferentiableAt.continuousAt (𝕜 := ℂ ) apply HolomorphicAt.differentiableAt simp [h₁F] -- apply Continuous.continuousAt apply continuous_circleMap -- have : (fun x => ∑ s ∈ (ZeroFinset h₁f h₂f).attach, ↑(order s) * log (Complex.abs (circleMap 0 1 x - ↑s))) = ∑ s ∈ (ZeroFinset h₁f h₂f).attach, (fun x => ↑(order s) * log (Complex.abs (circleMap 0 1 x - ↑s))) := by funext x simp rw [this] apply IntervalIntegrable.sum intro i h₂i apply IntervalIntegrable.const_mul have : i.1 ∈ Metric.closedBall (0 : ℂ) 1 := by exact ((ZeroFinset_mem_iff h₁f i).1 i.2).1 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 this rw [t₁] at this --let Z₁ := (ZeroFinset h₁f h₂f) ∩ (Metric.ball 0 1) let Z₂ := { x : ZeroFinset h₁f h₂f | ‖x.1‖ = 1 } sorry