From c44f7e2efd45c92656b949cc6390885a976efbb4 Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Mon, 5 Aug 2024 10:02:24 +0200 Subject: [PATCH] =?UTF-8?q?Working=E2=80=A6?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Nevanlinna/holomorphic_primitive2.lean | 115 +++++++++++++++++++------ lake-manifest.json | 6 +- 2 files changed, 91 insertions(+), 30 deletions(-) diff --git a/Nevanlinna/holomorphic_primitive2.lean b/Nevanlinna/holomorphic_primitive2.lean index b38262d..b6b4564 100644 --- a/Nevanlinna/holomorphic_primitive2.lean +++ b/Nevanlinna/holomorphic_primitive2.lean @@ -335,13 +335,19 @@ theorem primitive_additivity (f : ℂ → E) (z₀ : ℂ) (rx ry : ℝ) + (hrx : 0 < rx) + (hry : 0 < ry) (hf : DifferentiableOn ℂ f (Metric.ball z₀.re rx ×ℂ Metric.ball z₀.im ry)) (z₁ : ℂ) (hz₁ : z₁ ∈ (Metric.ball z₀.re rx ×ℂ Metric.ball z₀.im ry)) : - ∀ z ∈ Metric.ball z₁ (R - dist z₁ z₀), (primitive z₀ f z) - (primitive z₁ f z) - (primitive z₀ f z₁) = 0 := by + ∃ εx εy : ℝ, ∀ z ∈ (Metric.ball z₁.re εx ×ℂ Metric.ball z₁.im εy), (primitive z₀ f z) - (primitive z₁ f z) - (primitive z₀ f z₁) = 0 := by + + use rx - dist z₀.re z₁.re + use ry - dist z₀.im z₁.im intro z hz +/- have H : (Set.uIcc z₁.re z.re ×ℂ Set.uIcc z₀.im z₁.im) ⊆ Metric.ball z₀ R := by intro x hx @@ -383,7 +389,7 @@ theorem primitive_additivity _ < (R - dist z₁ z₀) + dist ⟨z₁.re, x.im⟩ z₀ := by apply add_lt_add_right A₃ _ ≤ (R - dist z₁ z₀) + dist z₁ z₀ := by exact (add_le_add_iff_left (R - dist z₁ z₀)).mpr B₁ _ = R := by exact sub_add_cancel R (dist z₁ z₀) - +-/ unfold primitive @@ -405,14 +411,16 @@ theorem primitive_additivity apply Continuous.continuousOn rw [this] continuity - -- -- Remains: Set.MapsTo (fun x => { re := x, im := z₀.im }) (Set.uIcc z₀.re z₁.re) (Metric.ball z₀ R) + -- Remains: Set.MapsTo (fun x => { re := x, im := z₀.im }) (Set.uIcc z₀.re z₁.re) (Metric.ball z₀.re rx ×ℂ Metric.ball z₀.im ry) intro w hw simp - simp_rw [Complex.dist_of_im_eq] - calc dist w z₀.re + apply Complex.mem_reProdIm.mpr + constructor + · simp + calc dist w z₀.re _ ≤ dist z₁.re z₀.re := by apply Real.dist_right_le_of_mem_uIcc; rwa [Set.uIcc_comm] at hw - _ ≤ dist z₁ z₀ := by sorry - _ < R := by simp at hz₁; assumption + _ < rx := by apply Metric.mem_ball.mp (Complex.mem_reProdIm.1 hz₁).1 + · simpa -- IntervalIntegrable (fun x => f { re := x, im := z₀.im }) MeasureTheory.volume z₁.re z.re apply ContinuousOn.intervalIntegrable @@ -428,27 +436,29 @@ theorem primitive_additivity apply Continuous.continuousOn rw [this] continuity - -- -- Remains: Set.MapsTo (fun x => { re := x, im := z₀.im }) (Set.uIcc z₁.re z.re) (Metric.ball z₀ R) + -- Remains: Set.MapsTo (fun x => { re := x, im := z₀.im }) (Set.uIcc z₁.re z.re) (Metric.ball z₀.re rx ×ℂ Metric.ball z₀.im ry) intro w hw simp - simp_rw [Complex.dist_of_im_eq] - calc dist w z₀.re + constructor + · simp + calc dist w z₀.re _ ≤ dist w z₁.re + dist z₁.re z₀.re := by exact dist_triangle w z₁.re z₀.re - _ ≤ dist z₁.re z.re + dist z₁.re z₀.re := by - apply add_le_add_right - apply Real.dist_le_of_mem_uIcc hw + _ ≤ dist z.re z₁.re + dist z₁.re z₀.re := by + apply (add_le_add_iff_right (dist z₁.re z₀.re)).mpr + rw [Set.uIcc_comm] at hw + exact Real.dist_right_le_of_mem_uIcc hw + _ < (rx - dist z₀.re z₁.re) + dist z₁.re z₀.re := by + apply (add_lt_add_iff_right (dist z₁.re z₀.re)).mpr + apply Metric.mem_ball.1 (Complex.mem_reProdIm.1 hz).1 + _ = rx := by + rw [dist_comm] simp - _ ≤ dist z₁ z + dist z₁ z₀ := by - sorry - _ < (R - dist z₁ z₀) + dist z₁ z₀ := by - apply add_lt_add_right - simp at hz - rwa [dist_comm] - _ = R := by simp + · simpa rw [this] have : (∫ (x : ℝ) in z₀.im..z.im, f { re := z.re, im := x }) = (∫ (x : ℝ) in z₀.im..z₁.im, f { re := z.re, im := x }) + (∫ (x : ℝ) in z₁.im..z.im, f { re := z.re, im := x }) := by rw [intervalIntegral.integral_add_adjacent_intervals] + -- IntervalIntegrable (fun x => f { re := z.re, im := x }) MeasureTheory.volume z₀.im z₁.im apply ContinuousOn.intervalIntegrable apply ContinuousOn.comp @@ -464,15 +474,67 @@ theorem primitive_additivity apply Continuous.add fun_prop fun_prop - -- Set.MapsTo (Complex.mk z.re) (Set.uIcc z₀.im z₁.im) (Metric.ball z₀ R) + -- Set.MapsTo (Complex.mk z.re) (Set.uIcc z₀.im z₁.im) (Metric.ball z₀.re rx ×ℂ Metric.ball z₀.im ry) intro w hw - simp + constructor + · simp + calc dist z.re z₀.re + _ ≤ dist z.re z₁.re + dist z₁.re z₀.re := by exact dist_triangle z.re z₁.re z₀.re + _ < (rx - dist z₀.re z₁.re) + dist z₁.re z₀.re := by + apply (add_lt_add_iff_right (dist z₁.re z₀.re)).mpr + apply Metric.mem_ball.1 (Complex.mem_reProdIm.1 hz).1 + _ = rx := by + rw [dist_comm] + simp + · simp + calc dist w z₀.im + _ ≤ dist z₁.im z₀.im := by rw [Set.uIcc_comm] at hw; exact Real.dist_right_le_of_mem_uIcc hw + _ < ry := by + rw [← Metric.mem_ball] + exact hz₁.2 - - sorry --apply integrability₂ f hf - - sorry --apply integrability₂ f hf + -- IntervalIntegrable (fun x => f { re := z.re, im := x }) MeasureTheory.volume z₁.im z.im + apply ContinuousOn.intervalIntegrable + apply ContinuousOn.comp + exact hf.continuousOn + apply Continuous.continuousOn + have {b : ℝ}: (Complex.mk b) = (fun x => Complex.I • Complex.ofRealCLM x + { re := b, im := 0 }) := by + funext x + apply Complex.ext + rw [Complex.add_re] + simp + simp + rw [this] + apply Continuous.add + fun_prop + fun_prop + -- Set.MapsTo (Complex.mk z.re) (Set.uIcc z₁.im z.im) (Metric.ball z₀.re rx ×ℂ Metric.ball z₀.im ry) + intro w hw + constructor + · simp + calc dist z.re z₀.re + _ ≤ dist z.re z₁.re + dist z₁.re z₀.re := by exact dist_triangle z.re z₁.re z₀.re + _ < (rx - dist z₀.re z₁.re) + dist z₁.re z₀.re := by + apply (add_lt_add_iff_right (dist z₁.re z₀.re)).mpr + apply Metric.mem_ball.1 (Complex.mem_reProdIm.1 hz).1 + _ = rx := by + rw [dist_comm] + simp + · simp + calc dist w z₀.im + _ ≤ dist w z₁.im + dist z₁.im z₀.im := by exact dist_triangle w z₁.im z₀.im + _ ≤ dist z.im z₁.im + dist z₁.im z₀.im := by + apply (add_le_add_iff_right (dist z₁.im z₀.im)).mpr + rw [Set.uIcc_comm] at hw + exact Real.dist_right_le_of_mem_uIcc hw + _ < (ry - dist z₀.im z₁.im) + dist z₁.im z₀.im := by + apply (add_lt_add_iff_right (dist z₁.im z₀.im)).mpr + apply Metric.mem_ball.1 (Complex.mem_reProdIm.1 hz).2 + _ = ry := by + rw [dist_comm] + simp rw [this] + simp have {a b c d e f g h : E} : (a + b) + (c + d) - (e + f) - (g + h) = b + (a - g) - e - f + d - h + (c) := by @@ -483,7 +545,6 @@ theorem primitive_additivity have H' : DifferentiableOn ℂ f (Set.uIcc z₁.re z.re ×ℂ Set.uIcc z₀.im z₁.im) := by apply DifferentiableOn.mono hf intro x hx - simp exact H hx diff --git a/lake-manifest.json b/lake-manifest.json index 85499dc..54aeae5 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "0f3e143dffdc3a591662f3401ce1d7a3405227c0", + "rev": "41bc768e2224d6c75128a877f1d6e198859b3178", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "209712c78b16c795453b6da7f7adbda4589a8f21", + "rev": "6058ab8d938c5104eace7d0fb5ac17b21cb067b1", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "c96401c7496392a2200dc78c0b334df0561466dc", + "rev": "d56e389960165aa122e7c97c098d67e4def09470", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null,