Update holomorphic_JensenFormula.lean

Nevanlinna/holomorphic_JensenFormula.lean

@@ -1,47 +1,72 @@
 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
+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 l₁ {x : ℝ} : ‖circleMap 0 1 x‖ = 1 := by
+  rw [Complex.norm_eq_abs, abs_circleMap_zero]
+  simp
+
+lemma l₂ {x : ℝ} : ‖(circleMap 0 1 x) - a‖ = ‖1 - (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
+    rw [l₁]
+  _ = ‖(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]
+  _ = ‖(circleMap 0 1 0) - (circleMap 0 1 (-x)) * a‖ := by
+    rw [l₀]
+    simp
+  _ = ‖1 - (circleMap 0 1 (-x)) * a‖ := by
+    congr
+    dsimp [circleMap]
+    simp
 
 lemma int₀
   {a : ℂ}
   (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
-
+  simp_rw [l₂]
+  have {x : ℝ} : Real.log ‖1 - circleMap 0 1 (-x) * a‖ = (fun w ↦ Real.log ‖1 - circleMap 0 1 (w) * a‖) (-x) := by rfl
   conv =>
     left
     arg 1
     intro x
-    rw [← this]
+    rw [this]
+  rw [intervalIntegral.integral_comp_neg ((fun w ↦ Real.log ‖1 - circleMap 0 1 (w) * a‖))]
+
+  let f₁ := fun w ↦ Real.log ‖1 - circleMap 0 1 w * a‖
+  have {x : ℝ} : Real.log ‖1 - circleMap 0 1 x * a‖ = f₁ (x + 2 * Real.pi) := by
+    dsimp [f₁]
+    congr 4
+    let A := periodic_circleMap 0 1 x
+    simp at A
+    exact id (Eq.symm A)
+  conv =>
+    left
+    arg 1
+    intro x
+    rw [this]
+  rw [intervalIntegral.integral_comp_add_right f₁ (2 * Real.pi)]
   simp
+  dsimp [f₁]
 
-  have hf : ∀ x ∈ Metric.ball 0 2, HarmonicAt F x := by sorry
+  let F := fun z ↦ Real.log ‖1 - z * a‖
 
+  have hf : ∀ x ∈ Metric.ball 0 2 , HarmonicAt F x := by
     sorry
 
+  let A := harmonic_meanValue 2 1 Real.zero_lt_one one_lt_two hf
+  dsimp [F] at A
+  simp at A
+  exact A
 
 
 theorem jensen_case_R_eq_one