nevanlinna/Nevanlinna/harmonicAt_meanValue.lean

import Mathlib.Analysis.NormedSpace.Pointwise
import Mathlib.Topology.MetricSpace.Thickening
import Mathlib.Analysis.Complex.CauchyIntegral
import Nevanlinna.holomorphic_examples

theorem harmonic_meanValue
  {f : ℂ → ℝ}
  {z : ℂ}
  (ρ R : ℝ)
  (hR : 0 < R)
  (hρ : R < ρ)
  (hf : ∀ x ∈ Metric.ball z ρ , HarmonicAt f x) :
  (∫ (x : ℝ) in (0)..2 * Real.pi, f (circleMap z R x)) = 2 * Real.pi * f z
  := by

  obtain ⟨F, h₁F, h₂F⟩ := harmonic_is_realOfHolomorphic (gt_trans hρ hR) hf

  have hrρ : Metric.ball z R ⊆ Metric.ball z ρ := by
    intro x hx
    exact gt_trans hρ hx

  have reg₀F : DifferentiableOn ℂ F (Metric.ball z ρ) := by
    intro x hx
    apply DifferentiableAt.differentiableWithinAt
    apply HolomorphicAt.differentiableAt (h₁F x _)
    exact hx

  have reg₁F : DifferentiableOn ℂ F (Metric.ball z R) := by
    intro x hx
    apply DifferentiableAt.differentiableWithinAt
    apply HolomorphicAt.differentiableAt (h₁F x _)
    exact hrρ hx

  have : (∮ (x : ℂ) in C(z, R), (x - z)⁻¹ • F x) = (2 * ↑Real.pi * Complex.I) • F z := by
    let s : Set ℂ := ∅
    let hs : s.Countable := Set.countable_empty
    let _ : ℂ := 0
    have hw : (z : ℂ) ∈ Metric.ball z R := Metric.mem_ball_self hR
    have hc : ContinuousOn F (Metric.closedBall z R) := by
      apply reg₀F.continuousOn.mono
      intro x hx
      simp at hx
      simp
      linarith
    have hd : ∀ x ∈ Metric.ball z R \ s, DifferentiableAt ℂ F x := by
      intro x hx
      let A := reg₁F x hx.1
      apply A.differentiableAt
      apply (IsOpen.mem_nhds_iff ?hs).mpr
      exact hx.1
      exact Metric.isOpen_ball
    let CIF := Complex.circleIntegral_sub_inv_smul_of_differentiable_on_off_countable hs hw hc hd
    simp at CIF
    assumption

  unfold circleIntegral at this
  simp_rw [deriv_circleMap] at this

  have t₁ {θ : ℝ} : (circleMap 0 R θ * Complex.I) • (circleMap 0 R θ)⁻¹ • F (circleMap z R θ) = Complex.I • F (circleMap z R θ) := by
    rw [← smul_assoc]
    congr 1
    simp
    nth_rw 1 [mul_comm]
    rw [← mul_assoc]
    simp
    apply inv_mul_cancel
    apply circleMap_ne_center
    exact Ne.symm (ne_of_lt hR)
  have t'₁  {θ : ℝ} : circleMap 0 R θ = circleMap z R θ - z := by
    exact Eq.symm (circleMap_sub_center z R θ)
  simp_rw [← t'₁, t₁] at this
  simp at this

  have t₂ : Complex.reCLM (-Complex.I * (Complex.I * ∫ (x : ℝ) in (0)..2 * Real.pi, F (circleMap z R x))) = Complex.reCLM (-Complex.I * (2 * ↑Real.pi * Complex.I * F z)) := by
    rw [this]
  simp at t₂
  have xx {x : ℝ} : (F (circleMap z R x)).re = f (circleMap z R x) := by
    rw [← h₂F]
    simp
    simp
    rw [Complex.dist_eq]
    rw [circleMap_sub_center]
    simp
    rwa [abs_of_nonneg (le_of_lt hR)]
  have x₁ {z : ℂ} : z.re = Complex.reCLM z := by rfl
  rw [x₁] at t₂
  rw [← ContinuousLinearMap.intervalIntegral_comp_comm] at t₂
  simp at t₂
  simp_rw [xx] at t₂
  have x₁ {z : ℂ} : z.re = Complex.reCLM z := by rfl
  rw [x₁] at t₂
  have : Complex.reCLM (F z) = f z := by
    apply h₂F
    simp
    exact gt_trans hρ hR
  rw [this] at t₂
  exact t₂

  -- IntervalIntegrable (fun x => F (circleMap 0 1 x)) MeasureTheory.volume 0 (2 * Real.pi)
  apply ContinuousOn.intervalIntegrable
  apply ContinuousOn.comp reg₀F.continuousOn _
  intro θ _
  simp
  rw [Complex.dist_eq, circleMap_sub_center]
  simp
  rwa [abs_of_nonneg (le_of_lt hR)]
  apply Continuous.continuousOn
  exact continuous_circleMap z R

/- Probably not optimal yet. We want a statements that requires harmonicity in
the interior and continuity on the closed ball.
-/


theorem harmonic_meanValue₁
  {f : ℂ → ℝ}
  {z : ℂ}
  (R : ℝ)
  (hR : 0 < R)
  (hf : ∀ x ∈ Metric.closedBall z R , HarmonicAt f x) :
  (∫ (x : ℝ) in (0)..2 * Real.pi, f (circleMap z R x)) = 2 * Real.pi * f z := by

  obtain ⟨e, h₁e, h₂e⟩ := IsCompact.exists_thickening_subset_open (isCompact_closedBall z R) (HarmonicAt_isOpen f) hf
  rw [thickening_closedBall] at h₂e
  apply harmonic_meanValue (e + R) R
  assumption
  norm_num
  assumption
  exact fun x a => h₂e a
  assumption
  linarith