From 951c25624e2a9f4b8206484989737f171638c4a2 Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Wed, 7 Aug 2024 13:29:58 +0200 Subject: [PATCH] Update holomorphic_primitive2.lean --- Nevanlinna/holomorphic_primitive2.lean | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) diff --git a/Nevanlinna/holomorphic_primitive2.lean b/Nevanlinna/holomorphic_primitive2.lean index 3447e8a..393f1d4 100644 --- a/Nevanlinna/holomorphic_primitive2.lean +++ b/Nevanlinna/holomorphic_primitive2.lean @@ -97,7 +97,16 @@ theorem primitive_fderivAtBasepointZero have B : Metric.ball (f 0) (c / 4) ∈ nhds (f 0) := by apply Metric.ball_mem_nhds (f 0) linarith - exact eventually_nhds_iff.mp (continuousAt_def.1 hf (Metric.ball (f 0) (c / (4 : ℝ))) B) + apply eventually_nhds_iff.mp + apply continuousAt_def.1 + apply Continuous.continuousAt + fun_prop + + apply continuousAt_def.1 + apply hf.continuousAt + exact Metric.ball_mem_nhds 0 hR + apply Metric.ball_mem_nhds (f 0) + simpa obtain ⟨ε, h₁ε, h₂ε⟩ : ∃ ε > 0, (Metric.ball 0 ε) ×ℂ (Metric.ball 0 ε) ⊆ s := by obtain ⟨ε', h₁ε', h₂ε'⟩ : ∃ ε' > 0, Metric.ball 0 ε' ⊆ s ∩ Metric.ball 0 R := by @@ -108,13 +117,12 @@ theorem primitive_fderivAtBasepointZero exact Metric.isOpen_ball constructor · exact h₂s.2 - · simp - - sorry + · simpa use (2 : ℝ)⁻¹ * ε' constructor · simpa · intro x hx + apply Set.inter_subset_left apply h₂ε' simp calc Complex.abs x