Working…

Nevanlinna/specialFunctions_CircleIntegral_affine.lean

@@ -382,3 +382,100 @@ lemma int₃
     simp at h₁a
     simp
     linarith
+
+
+lemma int₄
+  {a : ℂ}
+  {R : ℝ}
+  (hR : 0 < R)
+  (ha : a ∈ Metric.closedBall 0 R) :
+  ∫ x in (0)..(2 * π), log ‖circleMap 0 R x - a‖ = (2 * π) * log R := by
+
+  have h₁a : a / R ∈ Metric.closedBall 0 1 := by
+    simp
+    simp at ha
+    sorry
+
+  have t₀ {x : ℝ} : circleMap 0 R x = R * circleMap 0 1 x := by
+    unfold circleMap
+    simp
+
+  have {x : ℝ} : circleMap 0 R x - a = R * (circleMap 0 1 x - (a / R)) := by
+    rw [t₀, mul_sub, mul_div_cancel₀]
+    rw [ne_eq, Complex.ofReal_eq_zero]
+    exact Ne.symm (ne_of_lt hR)
+
+  have {x : ℝ} : circleMap 0 R x ≠ a → log ‖circleMap 0 R x - a‖ = log R + log ‖circleMap 0 1 x - (a / R)‖ := by
+    intro hx
+    rw [this]
+    rw [norm_mul]
+    rw [log_mul]
+    congr
+    --
+    simp
+    exact le_of_lt hR
+    --
+    simp
+    exact Ne.symm (ne_of_lt hR)
+    --
+    simp
+    rw [t₀] at hx
+    by_contra hCon
+    rw [hCon] at hx
+    simp at hx
+    rw [mul_div_cancel₀] at hx
+    tauto
+    simp
+    exact Ne.symm (ne_of_lt hR)
+
+  have : ∫ x in (0)..(2 * π), log ‖circleMap 0 R x - a‖ = ∫ x in (0)..(2 * π), log R + log ‖circleMap 0 1 x - (a / R)‖ := by
+    rw [intervalIntegral.integral_congr_ae]
+    rw [MeasureTheory.ae_iff]
+    apply Set.Countable.measure_zero
+    let A := (circleMap 0 R)⁻¹' { a }
+    have s₀ : {a_1 | ¬(a_1 ∈ Ι 0 (2 * π) → log ‖circleMap 0 R a_1 - a‖ = log R + log ‖circleMap 0 1 a_1 - a / ↑R‖)} ⊆ A := by
+      intro x
+      contrapose
+      intro hx
+      unfold A at hx
+      simp at hx
+      simp
+      intro h₂x
+      let B := this hx
+      simp at B
+      rw [B]
+    have s₁ : A.Countable := by
+      apply Set.Countable.preimage_circleMap
+      exact Set.countable_singleton a
+      exact Ne.symm (ne_of_lt hR)
+    exact Set.Countable.mono s₀ s₁
+
+  rw [this]
+  rw [intervalIntegral.integral_add]
+  rw [int₃]
+  rw [intervalIntegral.integral_const]
+  simp
+  --
+  exact h₁a
+  --
+  apply intervalIntegral.intervalIntegrable_const
+  --
+  by_cases h₂a : Complex.abs (a / R) = 1
+  · exact int'₂ h₂a
+  · apply int'₀
+    simp
+    simp at h₁a
+    rw [lt_iff_le_and_ne]
+    constructor
+    · exact h₁a
+    · rw [← Complex.norm_eq_abs, ← norm_eq_abs]
+      refine div_ne_one_of_ne ?_
+      rw [← Complex.norm_eq_abs, norm_div] at h₂a
+      by_contra hCon
+      rw [hCon] at h₂a
+      simp at h₂a
+      have : |R| ≠ 0 := by
+        simp
+        exact Ne.symm (ne_of_lt hR)
+      rw [div_self this] at h₂a
+      tauto