From 167db4310c76f37a2006fadf9e7d5999a52519bc Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Wed, 31 Jul 2024 12:25:30 +0200
Subject: [PATCH] Add mean value property of harmonic functions

---
 ...examples.lean => harmonicAt_examples.lean} |  0
 Nevanlinna/harmonicAt_meanValue.lean          | 65 +++++++++++++++++++
 Nevanlinna/holomorphic_examples.lean          |  7 +-
 3 files changed, 69 insertions(+), 3 deletions(-)
 rename Nevanlinna/{harmonicAt.examples.lean => harmonicAt_examples.lean} (100%)
 create mode 100644 Nevanlinna/harmonicAt_meanValue.lean

diff --git a/Nevanlinna/harmonicAt.examples.lean b/Nevanlinna/harmonicAt_examples.lean
similarity index 100%
rename from Nevanlinna/harmonicAt.examples.lean
rename to Nevanlinna/harmonicAt_examples.lean
diff --git a/Nevanlinna/harmonicAt_meanValue.lean b/Nevanlinna/harmonicAt_meanValue.lean
new file mode 100644
index 0000000..c36692c
--- /dev/null
+++ b/Nevanlinna/harmonicAt_meanValue.lean
@@ -0,0 +1,65 @@
+import Mathlib.Analysis.Complex.CauchyIntegral
+import Nevanlinna.holomorphic_examples
+
+theorem harmonic_meanValue
+  {f : ℂ → ℝ}
+  (hf : ∀ z, HarmonicAt f z)
+  (R : ℝ)
+  (hR : R > 0) :
+  (∫ (x : ℝ) in (0)..2 * Real.pi, f (circleMap 0 R x)) = 2 * Real.pi * f 0
+  := by
+
+  obtain ⟨F, h₁F, h₂F⟩ := harmonic_is_realOfHolomorphic hf
+
+  have regF : Differentiable ℂ F := fun z ↦ HolomorphicAt.differentiableAt (h₁F z)
+
+  have : (∮ (z : ℂ) in C(0, R), z⁻¹ • F z) = (2 * ↑Real.pi * Complex.I) • F 0 := by
+    let s : Set ℂ := ∅
+    let hs : s.Countable := Set.countable_empty
+    let _ : ℂ := 0
+    let hw : (0 : ℂ) ∈ Metric.ball 0 R := Metric.mem_ball_self hR
+    let hc : ContinuousOn F (Metric.closedBall 0 R) := by
+      apply Continuous.continuousOn
+      exact regF.continuous
+    let hd : ∀ x ∈ Metric.ball 0 R \ s, DifferentiableAt ℂ F x := by
+      intro x _
+      exact regF x
+
+    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 0 R θ) = Complex.I • F (circleMap 0 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)
+  simp_rw [t₁] at this
+  simp at this
+
+  have t₂ : Complex.reCLM (-Complex.I * (Complex.I * ∫ (x : ℝ) in (0)..2 * Real.pi, F (circleMap 0 R x))) = Complex.reCLM (-Complex.I * (2 * ↑Real.pi * Complex.I * F 0)) := by
+    rw [this]
+  simp at t₂
+  have xx {z : ℂ} : (F z).re = f z := by
+    rw [← h₂F]
+    simp
+  simp_rw [xx] at t₂
+  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₂
+  exact t₂
+  -- IntervalIntegrable (fun x => F (circleMap 0 1 x)) MeasureTheory.volume 0 (2 * Real.pi)
+  apply Continuous.intervalIntegrable
+  apply Continuous.comp
+  exact regF.continuous
+  exact continuous_circleMap 0 R
diff --git a/Nevanlinna/holomorphic_examples.lean b/Nevanlinna/holomorphic_examples.lean
index 63cc34f..58689cb 100644
--- a/Nevanlinna/holomorphic_examples.lean
+++ b/Nevanlinna/holomorphic_examples.lean
@@ -109,7 +109,7 @@ function.
 theorem harmonic_is_realOfHolomorphic
   {f : ℂ → ℝ}
   (hf : ∀ z, HarmonicAt f z) :
-  ∃ F : ℂ → ℂ, ∀ z, HolomorphicAt F z ∧ (Complex.reCLM ∘ F = f) := by
+  ∃ F : ℂ → ℂ, (∀ z, HolomorphicAt F z) ∧ (Complex.reCLM ∘ F = f) := by
 
   let f_1 : ℂ → ℂ := Complex.ofRealCLM ∘ (partialDeriv ℝ 1 f)
   let f_I : ℂ → ℂ := Complex.ofRealCLM ∘ (partialDeriv ℝ Complex.I f)
@@ -207,9 +207,10 @@ theorem harmonic_is_realOfHolomorphic
     exact reg₁
 
   use F
-  intro z
+
   constructor
-  · -- HolomorphicAt F z
+  · -- ∀ (z : ℂ), HolomorphicAt F z
+    intro z
     apply HolomorphicAt_iff.2
     use Set.univ
     constructor