kebekus
/
nevanlinna
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

test

This commit is contained in:
janneklink 2024-07-14 10:55:58 +02:00
parent 789c1100bc
commit 34dfad798c
1 changed files with 6 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
Nevanlinna/test.lean
View File

@ -1,6 +1,6 @@
import Mathlib.Analysis.Complex.CauchyIntegral import Mathlib.Analysis.Complex.CauchyIntegral
--import Mathlib.Analysis.Complex.Module --import Mathlib.Analysis.Complex.Module
-- test
open ComplexConjugate open ComplexConjugate
@ -83,17 +83,17 @@ theorem JensenFormula₂ :
rw [← tmp] rw [← tmp]
rw [this] rw [this]
have : ∀ z : ℂ, 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 intro z
by_cases argHyp : Complex.arg z = π by_cases argHyp : Complex.arg z = π
· rw [Complex.log, argHyp, Complex.log] · rw [Complex.log, argHyp, Complex.log]
let ZZ := Complex.arg_conj z let ZZ := Complex.arg_conj z
rw [argHyp] at ZZ rw [argHyp] at ZZ
simp at ZZ simp at ZZ
have : conj z = z := by have : conj z = z := by
@ -103,7 +103,7 @@ theorem JensenFormula₂ :
let ZZ := Complex.log_conj z let ZZ := Complex.log_conj z
nth_rewrite 1 [Complex.log] nth_rewrite 1 [Complex.log]
simp simp
let φ := Complex.arg z let φ := Complex.arg z