Nevanlinna/holomorphic_JensenFormula.lean

@@ -1,103 +1,47 @@
 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
 
-  -- 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
+  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]
-  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)]
+    rw [← this]
   simp
-  dsimp [f₁]
 
-  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
+  have hf : ∀ x ∈ Metric.ball 0 2, HarmonicAt F x := by sorry
 
-  let F := fun z ↦ Real.log ‖1 - z * a‖
+  sorry
 
-  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