nevanlinna/nevanlinna/test.lean

import Mathlib.Analysis.Complex.CauchyIntegral

#check DiffContOnCl.circleIntegral_sub_inv_smul

open Real

theorem CauchyIntegralFormula :
  ∀
  {R : ℝ} -- Radius of the ball
  {w : ℂ} -- Point in the interior of the ball
  {f : ℂ → ℂ}, -- Holomorphic function
  DiffContOnCl ℂ f (Metric.ball 0 R)
  → w ∈ Metric.ball 0 R
  → (∮ (z : ℂ) in C(0, R), (z - w)⁻¹ • f z) = (2 * π * Complex.I) • f w := by

  exact DiffContOnCl.circleIntegral_sub_inv_smul

#check CauchyIntegralFormula
#check HasDerivAt.continuousAt
#check Real.log
#check Complex.log
#check Complex.exp

theorem SimpleCauchyFormula :
  ∀
  {R : ℝ} -- Radius of the ball
  {w : ℂ} -- Point in the interior of the ball
  {f : ℂ → ℂ}, -- Holomorphic function
  Differentiable ℂ f
  → w ∈ Metric.ball 0 R
  → (∮ (z : ℂ) in C(0, R), (z - w)⁻¹ • f z) = (2 * Real.pi * Complex.I) • f w := by

  intro R w f fHyp

  apply DiffContOnCl.circleIntegral_sub_inv_smul

  constructor
  · exact Differentiable.differentiableOn fHyp
  · suffices Continuous f from by
      exact Continuous.continuousOn this
    rw [continuous_iff_continuousAt]
    intro x
    exact DifferentiableAt.continuousAt (fHyp x)


theorem JensenFormula₂ :
  ∀
  {R : ℝ} -- Radius of the ball
  {w : ℂ} -- Point in the interior of the ball
  {f : ℂ → ℂ}, -- Holomorphic function
  Differentiable ℂ f
  → ∀ z ∈ Metric.ball 0 R, f z ≠ 0
  → (∮ (z : ℂ) in C(0, R), Complex.log ‖f z‖ ) = 2 * π * R * log ‖f 0‖ := by

  sorry