From 83f9aa5d725edbd84fb73222f021bb131b55a014 Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Wed, 7 Aug 2024 15:15:03 +0200 Subject: [PATCH] Update holomorphic_primitive2.lean --- Nevanlinna/holomorphic_primitive2.lean | 164 +++++++++++++++---------- 1 file changed, 102 insertions(+), 62 deletions(-) diff --git a/Nevanlinna/holomorphic_primitive2.lean b/Nevanlinna/holomorphic_primitive2.lean index 393f1d4..8a8ff39 100644 --- a/Nevanlinna/holomorphic_primitive2.lean +++ b/Nevanlinna/holomorphic_primitive2.lean @@ -47,22 +47,110 @@ theorem primitive_fderivAtBasepointZero arg 1 arg 2 rw [this] - have {A B C D :E} : (A + B) - (C + D) = (A - C) + (B - D) := by - abel - have t₀ {r : ℝ} : IntervalIntegrable (fun x => f { re := x, im := 0 }) MeasureTheory.volume 0 r := by - apply Continuous.intervalIntegrable - apply Continuous.comp + obtain ⟨s, h₁s, h₂s⟩ : ∃ s ⊆ f⁻¹' Metric.ball (f 0) (c / (4 : ℝ)), IsOpen s ∧ 0 ∈ s := by + have B : Metric.ball (f 0) (c / 4) ∈ nhds (f 0) := by + apply Metric.ball_mem_nhds (f 0) + linarith + 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 ∧ (Metric.ball 0 ε) ×ℂ (Metric.ball 0 ε) ⊆ Metric.ball 0 R := by + obtain ⟨ε', h₁ε', h₂ε'⟩ : ∃ ε' > 0, Metric.ball 0 ε' ⊆ s ∩ Metric.ball 0 R := by + apply Metric.mem_nhds_iff.mp + apply IsOpen.mem_nhds + apply IsOpen.inter + exact h₂s.1 + exact Metric.isOpen_ball + constructor + · exact h₂s.2 + · simpa + + use (2 : ℝ)⁻¹ * ε' + + constructor + · simpa + · constructor + · intro x hx + apply (h₂ε' _).1 + simp + calc Complex.abs x + _ ≤ |x.re| + |x.im| := Complex.abs_le_abs_re_add_abs_im x + _ < (2 : ℝ)⁻¹ * ε' + |x.im| := by + apply (add_lt_add_iff_right |x.im|).mpr + have : x.re ∈ Metric.ball 0 (2⁻¹ * ε') := (Complex.mem_reProdIm.1 hx).1 + simp at this + exact this + _ < (2 : ℝ)⁻¹ * ε' + (2 : ℝ)⁻¹ * ε' := by + apply (add_lt_add_iff_left ((2 : ℝ)⁻¹ * ε')).mpr + have : x.im ∈ Metric.ball 0 (2⁻¹ * ε') := (Complex.mem_reProdIm.1 hx).2 + simp at this + exact this + _ = ε' := by + rw [← add_mul] + abel_nf + simp + · intro x hx + apply (h₂ε' _).2 + simp + calc Complex.abs x + _ ≤ |x.re| + |x.im| := Complex.abs_le_abs_re_add_abs_im x + _ < (2 : ℝ)⁻¹ * ε' + |x.im| := by + apply (add_lt_add_iff_right |x.im|).mpr + have : x.re ∈ Metric.ball 0 (2⁻¹ * ε') := (Complex.mem_reProdIm.1 hx).1 + simp at this + exact this + _ < (2 : ℝ)⁻¹ * ε' + (2 : ℝ)⁻¹ * ε' := by + apply (add_lt_add_iff_left ((2 : ℝ)⁻¹ * ε')).mpr + have : x.im ∈ Metric.ball 0 (2⁻¹ * ε') := (Complex.mem_reProdIm.1 hx).2 + simp at this + exact this + _ = ε' := by + rw [← add_mul] + abel_nf + simp + + have h₃ε : ∀ y ∈ (Metric.ball 0 ε) ×ℂ (Metric.ball 0 ε), ‖(f y) - (f 0)‖ < (c / (4 : ℝ)) := by + intro y hy + apply mem_ball_iff_norm.mp + apply h₁s + exact h₂ε.1 hy + + have t₀ {r : ℝ} (hr : r ∈ Metric.ball 0 ε) : IntervalIntegrable (fun x => f { re := x, im := 0 }) MeasureTheory.volume 0 r := by + apply ContinuousOn.intervalIntegrable + apply ContinuousOn.comp exact hf have : (fun x => ({ re := x, im := 0 } : ℂ)) = Complex.ofRealLI := by rfl rw [this] + apply Continuous.continuousOn continuity + intro x hx + apply h₂ε.2 + simp + constructor + · simp + calc |x| + _ < ε := by + sorry + · simpa - have t₁ {r : ℝ} : IntervalIntegrable (fun _ => f 0) MeasureTheory.volume 0 r := by - apply Continuous.intervalIntegrable - apply Continuous.comp - exact hf + have t₁ {r : ℝ} (hr : r ∈ Metric.ball 0 ε) : IntervalIntegrable (fun _ => f 0) MeasureTheory.volume 0 r := by + apply ContinuousOn.intervalIntegrable + apply ContinuousOn.comp + apply hf fun_prop + intro x hx + simpa + + have t₂ {a b : ℝ} : IntervalIntegrable (fun x_1 => f { re := a, im := x_1 }) MeasureTheory.volume 0 b := by apply Continuous.intervalIntegrable apply Continuous.comp hf @@ -82,6 +170,9 @@ theorem primitive_fderivAtBasepointZero apply Continuous.comp exact hf fun_prop + + have {A B C D :E} : (A + B) - (C + D) = (A - C) + (B - D) := by + abel conv => left intro x @@ -89,63 +180,12 @@ theorem primitive_fderivAtBasepointZero arg 1 rw [this] rw [← smul_sub] + rw [← intervalIntegral.integral_sub t₀ t₁] rw [← intervalIntegral.integral_sub t₂ t₃] + rw [Filter.eventually_iff_exists_mem] - obtain ⟨s, h₁s, h₂s⟩ : ∃ s ⊆ f⁻¹' Metric.ball (f 0) (c / (4 : ℝ)), IsOpen s ∧ 0 ∈ s := by - have B : Metric.ball (f 0) (c / 4) ∈ nhds (f 0) := by - apply Metric.ball_mem_nhds (f 0) - linarith - 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 - apply Metric.mem_nhds_iff.mp - apply IsOpen.mem_nhds - apply IsOpen.inter - exact h₂s.1 - exact Metric.isOpen_ball - constructor - · exact h₂s.2 - · simpa - use (2 : ℝ)⁻¹ * ε' - constructor - · simpa - · intro x hx - apply Set.inter_subset_left - apply h₂ε' - simp - calc Complex.abs x - _ ≤ |x.re| + |x.im| := Complex.abs_le_abs_re_add_abs_im x - _ < (2 : ℝ)⁻¹ * ε' + |x.im| := by - apply (add_lt_add_iff_right |x.im|).mpr - have : x.re ∈ Metric.ball 0 (2⁻¹ * ε') := (Complex.mem_reProdIm.1 hx).1 - simp at this - exact this - _ < (2 : ℝ)⁻¹ * ε' + (2 : ℝ)⁻¹ * ε' := by - apply (add_lt_add_iff_left ((2 : ℝ)⁻¹ * ε')).mpr - have : x.im ∈ Metric.ball 0 (2⁻¹ * ε') := (Complex.mem_reProdIm.1 hx).2 - simp at this - exact this - _ = ε' := by - rw [← add_mul] - abel_nf - simp - - have h₃ε : ∀ y ∈ (Metric.ball 0 ε) ×ℂ (Metric.ball 0 ε), ‖(f y) - (f 0)‖ < (c / (4 : ℝ)) := by - intro y hy - apply mem_ball_iff_norm.mp - exact h₁s (h₂ε hy) use Metric.ball 0 (ε / (4 : ℝ)) constructor