nevanlinna/Nevanlinna/holomorphic_JensenFormula2.lean

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