From fb5bf47170a165baf551284adecc7aa670e4580f Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Wed, 24 Apr 2024 16:23:39 +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/test.lean | 34 +++++++++++++++++++++++++++++----- 1 file changed, 29 insertions(+), 5 deletions(-) diff --git a/nevanlinna/test.lean b/nevanlinna/test.lean index 7ae3ebc..4e27dc2 100644 --- a/nevanlinna/test.lean +++ b/nevanlinna/test.lean @@ -84,13 +84,37 @@ theorem JensenFormula₂ : rw [this] - have : ∀ z : ℂ, Complex.log (Complex.abs z) = 1/2 * Complex.log z + 1/2 * Complex.log (conj z) := by + have : ∀ z : ℂ, log (Complex.abs z) = 1/2 * Complex.log z + 1/2 * Complex.log (conj z) := by intro z - have : ∃ r φ : ℝ, z = r * Complex.exp (φ * Complex.I) := by - sorry - obtain ⟨r, φ, h⟩ := this - rw [h] + by_cases argHyp : Complex.arg z = π + + · rw [Complex.log, argHyp, Complex.log] + let ZZ := Complex.arg_conj z + rw [argHyp] at ZZ + + simp at ZZ + + have : conj z = z := by + apply? + sorry + + let ZZ := Complex.log_conj z + + nth_rewrite 1 [Complex.log] + + simp + + let φ := Complex.arg z + let r := Complex.abs z + have : z = r * Complex.exp (φ * Complex.I) := by + exact (Complex.abs_mul_exp_arg_mul_I z).symm + + have : Complex.log z = Complex.log r + r*Complex.I := by + apply? + sorry + simp at XX + sorry