working…

Nevanlinna/harmonicAt_meanValue.lean

@@ -3,28 +3,51 @@ 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
+  {z : ℂ}
+  (ρ R : ℝ)
+  (hR : R > 0)
+  (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 hf
+  obtain ⟨F, h₁F, h₂F⟩ := harmonic_is_realOfHolomorphic (gt_trans hρ hR) hf
 
-  have regF : Differentiable ℂ F := fun z ↦ HolomorphicAt.differentiableAt (h₁F z)
+  have hrρ : Metric.ball z R ⊆ Metric.ball z ρ := by
+    intro x hx
+    exact gt_trans hρ hx
 
-  have : (∮ (z : ℂ) in C(0, R), z⁻¹ • F z) = (2 * ↑Real.pi * Complex.I) • F 0 := by
+  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
-    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
-
+    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
@@ -32,7 +55,7 @@ theorem harmonic_meanValue
   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
+  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

Nevanlinna/holomorphic_examples.lean

@@ -1,6 +1,6 @@
 import Nevanlinna.complexHarmonic
 import Nevanlinna.holomorphicAt
-import Nevanlinna.holomorphic_primitive2
+import Nevanlinna.holomorphic_primitive
 import Nevanlinna.mathlibAddOn