working

Nevanlinna/holomorphic_primitive2.lean

@@ -515,15 +515,44 @@ theorem primitive_additivity'
   :
   primitive z₀ f =ᶠ[nhds z₁] fun z ↦ (primitive z₁ f z) + (primitive z₀ f z₁) := by
 
-  let ε := R - dist z₀ z₁
+  let d := fun ε ↦ √((z₁.re - z₀.re + ε) ^ 2 + (z₁.im - z₀.im + ε) ^ 2)
+  have h₀d : Continuous d := by continuity
+  have h₁d : ∀ ε, 0 ≤ d ε := fun ε ↦ Real.sqrt_nonneg ((z₁.re - z₀.re + ε) ^ 2 + (z₁.im - z₀.im + ε) ^ 2)
 
-  have hε : 0 < ε := by
+  obtain ⟨ε, h₀ε, h₁ε⟩ : ∃ ε > 0, d ε < R := by
-    dsimp [ε]
+    let Omega := d⁻¹' Metric.ball 0 R
-    simp
-    exact Metric.mem_ball'.mp hz₁
 
-  let rx := dist z₀.re z₁.re + ε/(2 : ℝ)
+    have lem₀Ω : IsOpen Omega := IsOpen.preimage h₀d Metric.isOpen_ball
-  let ry := dist z₀.im z₁.im + ε/(2 : ℝ)
+    have lem₁Ω : 0 ∈ Omega := by
+      dsimp [Omega, d]; simp
+      rw [← Complex.dist_eq_re_im]; simp
+      exact hz₁
+    obtain ⟨ε, h₁ε, h₂ε⟩ := Metric.isOpen_iff.1 lem₀Ω 0 lem₁Ω
+    have h'₁ε : 0 < ε := by exact h₁ε
+
+    let ε' := (2 : ℝ)⁻¹ * ε
+
+    have h₀ε' : ε' ∈ Omega := by
+      apply h₂ε
+      dsimp [ε']; simp
+      have : |ε| = ε := by apply abs_of_pos h₁ε
+      rw [this]
+      apply (inv_mul_lt_iff zero_lt_two).mpr
+      linarith
+    have h₁ε' : 0 < ε' := by
+      apply Real.mul_pos _ h₁ε
+      apply inv_pos.mpr
+      exact zero_lt_two
+
+    use ε'
+
+    constructor
+    · exact h₁ε'
+    · dsimp [Omega] at h₀ε'; simp at h₀ε'
+      rwa [abs_of_nonneg (h₁d ε')] at h₀ε'
+
+  let rx := dist z₁.re z₀.re + ε
+  let ry := dist z₁.im z₀.im + ε
 
   have h'ry : 0 < ry := by
     dsimp [ry]
@@ -535,13 +564,26 @@ theorem primitive_additivity'
     apply hf.mono
     intro x hx
     simp
+    rw [Complex.dist_eq_re_im]
+
+    have : dist x.re z₀.re < rx := Metric.mem_ball.mp hx.1
+    have : dist x.im z₀.im < ry := Metric.mem_ball.mp hx.2
+
+    have t₀ : √((x.re - z₀.re) ^ 2 + (x.im - z₀.im) ^ 2) < √( rx ^ 2 + ry ^ 2) := by
       sorry
+    have t₁ : √( rx ^ 2 + ry ^ 2) = d ε := by
+      sorry
+
+    calc √((x.re - z₀.re) ^ 2 + (x.im - z₀.im) ^ 2)
+    _ < √( rx ^ 2 + ry ^ 2) := by exact t₀
+    _ = d ε := by exact t₁
+    _ < R := by exact h₁ε
 
   have h'z₁ : z₁ ∈ (Metric.ball z₀.re rx ×ℂ Metric.ball z₀.im ry) := by
     dsimp [rx, ry]
     constructor
-    · rw [dist_comm]; simp; exact hε
+    · simp; exact h₀ε
-    · rw [dist_comm]; simp; exact hε
+    · simp; exact h₀ε
 
   obtain ⟨εx, hεx, εy, hεy, hε⟩ := primitive_additivity h'f h'ry h'z₁