import Nevanlinna.harmonicAt_examples
import Nevanlinna.harmonicAt_meanValue


theorem jensen_case_R_eq_one
  (f : ℂ → ℂ)
  (h₁f : Differentiable ℂ f)
  (h₂f : f 0 ≠ 0)
  (S : Finset ℕ)
  (a : S → ℂ)
  (ha : ∀ s, a s ∈ Metric.ball 0 1)
  (F : ℂ → ℂ)
  (h₁F : Differentiable ℂ F)
  (h₂F : ∀ z, F z ≠ 0)
  (h₃F : f = fun z ↦ (F z) * ∑ s : S, (z - a s))
  :
  Real.log ‖f 0‖ = -∑ s, Real.log (‖a s‖⁻¹) + (2 * Real.pi)⁻¹ * ∫ (x : ℝ) in (0)..2 * Real.pi, Real.log ‖f (circleMap 0 1 x)‖ := by

  let logAbsF := fun w ↦ Real.log ‖F w‖

  have t₀ : ∀ z, HarmonicAt logAbsF z := by
    intro z
    apply logabs_of_holomorphicAt_is_harmonic
    sorry
    exact h₂F z

  have t₁ : (∫ (x : ℝ) in (0)..2 * Real.pi, logAbsF (circleMap 0 1 x)) = 2 * Real.pi * logAbsF 0 := by
    apply harmonic_meanValue t₀ 1
    exact Real.zero_lt_one

  let logAbsf := fun w ↦ Real.log ‖f w‖
  have s₀ : ∀ z, f z ≠ 0 → logAbsf z = logAbsF z + ∑ s, Real.log ‖z - a s‖ := by
    sorry
  have s₁ : ∀ z, f z ≠ 0 → logAbsF z = logAbsf z - ∑ s, Real.log ‖z - a s‖ := by
    sorry

  rw [s₁ 0 h₂f] at t₁

  have {x : ℝ} : f (circleMap 0 1 x) ≠ 0 := by sorry
  simp_rw [s₁ (circleMap 0 1 _) this] at t₁
  rw [intervalIntegral.integral_sub] at t₁
  rw [intervalIntegral.integral_finset_sum] at t₁

  have {i : S} : ∫ (x : ℝ) in (0)..2 * Real.pi, Real.log ‖circleMap 0 1 x - a i‖ = 0 := by

    sorry
  simp_rw [this] at t₁
  simp at t₁
  rw [t₁]
  simp
  have {w : ℝ} : Real.pi⁻¹ * 2⁻¹ * (2 * Real.pi * w) = w := by
    ring_nf
    simp [mul_inv_cancel Real.pi_ne_zero]
  rw [this]
  simp
  rfl
  -- ∀ i ∈ Finset.univ, IntervalIntegrable (fun x => Real.log ‖circleMap 0 1 x - a i‖) MeasureTheory.volume 0 (2 * Real.pi)
  intro i hi
  apply Continuous.intervalIntegrable
  apply continuous_iff_continuousAt.2
  intro x
  have : (fun x => Real.log ‖circleMap 0 1 x - a i‖) = Real.log ∘ Complex.abs ∘ (fun x ↦ circleMap 0 1 x - a i) :=
    rfl
  rw [this]
  apply ContinuousAt.comp
  apply Real.continuousAt_log
  simp
  by_contra ha'
  let A := ha i
  rw [← ha'] at A
  simp at A
  apply ContinuousAt.comp
  apply Complex.continuous_abs.continuousAt
  fun_prop
  -- IntervalIntegrable (fun x => logAbsf (circleMap 0 1 x)) MeasureTheory.volume 0 (2 * Real.pi)
  apply Continuous.intervalIntegrable
  apply continuous_iff_continuousAt.2
  intro x
  have : (fun x => logAbsf (circleMap 0 1 x)) = Real.log ∘ Complex.abs ∘ f ∘ (fun x ↦ circleMap 0 1 x) :=
    rfl
  rw [this]
  apply ContinuousAt.comp
  simp
  sorry
  apply ContinuousAt.comp
  apply Complex.continuous_abs.continuousAt
  apply ContinuousAt.comp
  apply h₁f.continuous.continuousAt
  let A := continuous_circleMap 0 1
  apply A.continuousAt
  -- IntervalIntegrable (fun x => ∑ s : { x // x ∈ S }, Real.log ‖circleMap 0 1 x - a s‖) MeasureTheory.volume 0 (2 * Real.pi)
  apply Continuous.intervalIntegrable
  apply continuous_finset_sum
  intro i hi
  apply continuous_iff_continuousAt.2
  intro x
  have : (fun x => Real.log ‖circleMap 0 1 x - a i‖) = Real.log ∘ Complex.abs ∘ (fun x ↦ circleMap 0 1 x - a i) :=
    rfl
  rw [this]
  apply ContinuousAt.comp
  apply Real.continuousAt_log
  simp
  by_contra ha'
  let A := ha i
  rw [← ha'] at A
  simp at A
  apply ContinuousAt.comp
  apply Complex.continuous_abs.continuousAt
  fun_prop