Update holomorphic_JensenFormula.lean

Nevanlinna/holomorphic_JensenFormula.lean

@@ -1,47 +1,103 @@
 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
 
+  by_cases h₁a : a = 0
+  · -- case: a = 0
+    rw [h₁a]
+    simp
 
-  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
-
+  -- case: a ≠ 0
+  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 ρ := ‖a‖⁻¹
+  have hρ : 1 < ρ := by
+    apply one_lt_inv_iff.mpr
+    constructor
+    · exact norm_pos_iff'.mpr h₁a
+    · exact mem_ball_zero_iff.mp ha
 
-  sorry
+  let F := fun z ↦ Real.log ‖1 - z * a‖
 
+  have hf : ∀ x ∈ Metric.ball 0 ρ, HarmonicAt F x := by
+    intro x hx
+    apply logabs_of_holomorphicAt_is_harmonic
+    apply Differentiable.holomorphicAt
+    fun_prop
+    apply sub_ne_zero_of_ne
+    by_contra h
+    have : ‖x * a‖ < 1 := by
+      calc ‖x * a‖
+      _ = ‖x‖ * ‖a‖ := by exact NormedField.norm_mul' x a
+      _ < ρ * ‖a‖ := by
+        apply (mul_lt_mul_right _).2
+        exact mem_ball_zero_iff.mp hx
+        exact norm_pos_iff'.mpr h₁a
+      _ = 1 := by
+        dsimp [ρ]
+        apply inv_mul_cancel
+        exact (AbsoluteValue.ne_zero_iff Complex.abs).mpr h₁a
+    rw [← h] at this
+    simp at this
+
+  let A := harmonic_meanValue ρ 1 Real.zero_lt_one hρ hf
+  dsimp [F] at A
+  simp at A
+  exact A
 
 
 theorem jensen_case_R_eq_one