working

Nevanlinna/harmonicAt_meanValue.lean

@@ -5,8 +5,8 @@ theorem harmonic_meanValue
   {f : ℂ → ℝ}
   {z : ℂ}
   (ρ R : ℝ)
-  (hR : R > 0)
-  (hρ : ρ > 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

Nevanlinna/holomorphic_JensenFormula.lean

@@ -1,13 +1,48 @@
 import Nevanlinna.harmonicAt_examples
 import Nevanlinna.harmonicAt_meanValue
 
+lemma l₀
+  {x₁ x₂ : ℝ} :
+  (circleMap 0 1 x₁) * (circleMap 0 1 x₂) = circleMap 0 1 (x₁+x₂) := by
+  dsimp [circleMap]
+  simp
+  rw [add_mul, Complex.exp_add]
+
+
 lemma int₀
   {a : ℂ}
-  (ha : a ∈ Metric.ball 0 1)
-  :
+  (ha : a ∈ Metric.ball 0 1) :
   ∫ (x : ℝ) in (0)..2 * Real.pi, Real.log ‖circleMap 0 1 x - a‖ = 0 := by
+
+
+  have {x : ℝ} : ‖(circleMap 0 1 x) - a‖ = ‖(circleMap 0 1 x) - a‖ := by
+    calc ‖(circleMap 0 1 x) - a‖
+    _ = 1 * ‖(circleMap 0 1 x) - a‖ := by exact Eq.symm (one_mul ‖circleMap 0 1 x - a‖)
+    _ = ‖(circleMap 0 1 (-x))‖ * ‖(circleMap 0 1 x) - a‖ := by
+      have : ‖(circleMap 0 1 (-x))‖ = 1 := by
+        rw [Complex.norm_eq_abs, abs_circleMap_zero]
+        simp
+      rw [this]
+    _ = ‖(circleMap 0 1 (-x)) * ((circleMap 0 1 x) - a)‖ := by
+      exact Eq.symm (NormedField.norm_mul' (circleMap 0 1 (-x)) (circleMap 0 1 x - a))
+    _ = ‖(circleMap 0 1 (-x)) * (circleMap 0 1 x) - (circleMap 0 1 (-x)) * a‖ := by
+      rw [mul_sub]
+
+    _ =
     sorry
 
+  conv =>
+    left
+    arg 1
+    intro x
+    rw [← this]
+  simp
+
+  have hf : ∀ x ∈ Metric.ball 0 2, HarmonicAt F x := by sorry
+
+  sorry
+
+
 
 theorem jensen_case_R_eq_one
   (f : ℂ → ℂ)
@@ -25,15 +60,17 @@ theorem jensen_case_R_eq_one
 
   let logAbsF := fun w ↦ Real.log ‖F w‖
 
-  have t₀ : ∀ z, HarmonicAt logAbsF z := by
-    intro z
+  have t₀ : ∀ z ∈ Metric.ball 0 2, HarmonicAt logAbsF z := by
+    intro z _
     apply logabs_of_holomorphicAt_is_harmonic
     apply h₁F.holomorphicAt
     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
+    have hR : (0 : ℝ) < (1 : ℝ) := by apply Real.zero_lt_one
+    have hρ : (1 : ℝ) < (2 : ℝ) := by linarith
+    apply harmonic_meanValue 2 1 hR hρ t₀
+
 
   have t₂ : ∀ s, f (a s) = 0 := by
     intro s