Working...

Nevanlinna/cauchyRiemann.lean

@@ -0,0 +1,40 @@
+import Mathlib.Analysis.Calculus.LineDeriv.Basic
+import Mathlib.Analysis.Complex.RealDeriv
+
+variable {z : ℂ} {f : ℂ → ℂ}
+
+theorem CauchyRiemann₁ : (DifferentiableAt ℂ f z)
+  → (fderiv ℝ f z) Complex.I = Complex.I * (fderiv ℝ f z) 1 := by
+  intro h
+  rw [DifferentiableAt.fderiv_restrictScalars ℝ h]
+  nth_rewrite 1 [← mul_one Complex.I]
+  exact ContinuousLinearMap.map_smul_of_tower (fderiv ℂ f z) Complex.I 1
+
+theorem CauchyRiemann₂ : (DifferentiableAt ℂ f z)
+  → lineDeriv ℝ f z Complex.I = Complex.I * lineDeriv ℝ f z 1 := by
+  intro h
+  rw [DifferentiableAt.lineDeriv_eq_fderiv (h.restrictScalars ℝ)]
+  rw [DifferentiableAt.lineDeriv_eq_fderiv (h.restrictScalars ℝ)]
+  exact CauchyRiemann₁ h
+
+theorem CauchyRiemann₃ : (DifferentiableAt ℂ f z)
+  → (lineDeriv ℝ (Complex.reCLM ∘ f) z 1 = lineDeriv ℝ (Complex.imCLM ∘ f) z Complex.I)
+    ∧ (lineDeriv ℝ (Complex.reCLM ∘ f) z Complex.I = -lineDeriv ℝ (Complex.imCLM ∘ f) z 1)
+   := by
+
+  intro h
+
+  have ContinuousLinearMap.comp_lineDeriv : ∀ w : ℂ, ∀ l : ℂ →L[ℝ] ℝ, lineDeriv ℝ (l ∘ f) z w = l ((fderiv ℝ f z) w) := by
+    intro w l
+    rw [DifferentiableAt.lineDeriv_eq_fderiv]
+    rw [fderiv.comp]
+    simp
+    fun_prop
+    exact h.restrictScalars ℝ
+    apply (ContinuousLinearMap.differentiableAt l).comp
+    exact h.restrictScalars ℝ
+
+  repeat
+    rw [ContinuousLinearMap.comp_lineDeriv]
+  rw [CauchyRiemann₁ h, Complex.I_mul]
+  simp

Nevanlinna/complexHarmonic.lean

@@ -0,0 +1,37 @@
+import Mathlib.Analysis.Complex.Basic
+import Mathlib.Analysis.Calculus.LineDeriv.Basic
+import Mathlib.Analysis.Calculus.ContDiff.Defs
+import Mathlib.Analysis.Calculus.FDeriv.Basic
+import Nevanlinna.cauchyRiemann
+
+noncomputable def Complex.laplace : (ℂ → ℝ) → (ℂ → ℝ) := by
+  intro f
+  let f₁ := fun x ↦ lineDeriv ℝ f x 1
+  let f₁₁ := fun x ↦ lineDeriv ℝ f₁ x 1
+  let f₂ := fun x ↦ lineDeriv ℝ f x Complex.I
+  let f₂₂ := fun x ↦ lineDeriv ℝ f₂ x Complex.I
+  exact f₁₁ + f₂₂
+
+
+def Harmonic (f : ℂ → ℝ) : Prop :=
+  (ContDiff ℝ 2 f) ∧ (∀ z, Complex.laplace f z = 0)
+
+
+theorem re_comp_holomorphic_is_harmonic (f : ℂ → ℂ) : 
+  Differentiable ℂ f → Harmonic (Complex.reCLM ∘ f) := by
+
+  intro h
+
+  constructor
+  · -- f is two times real continuously differentiable
+    sorry
+
+  · -- Laplace of f is zero
+    intro z
+    unfold Complex.laplace
+    simp
+    let ZZ := (CauchyRiemann₃ (h z)).left
+    rw [ZZ]
+    
+    sorry
+

Nevanlinna/harmonic.lean

@@ -0,0 +1,445 @@
+import Mathlib.Analysis.Complex.Basic
+import Mathlib.Analysis.Calculus.LineDeriv.Basic
+import Mathlib.Analysis.SpecialFunctions.ExpDeriv
+import Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
+import Mathlib.Analysis.Calculus.ContDiff.Basic
+import Mathlib.Analysis.Calculus.Deriv.Linear
+import Mathlib.Analysis.Complex.Conformal
+import Mathlib.Analysis.Calculus.Conformal.NormedSpace
+import Mathlib.Analysis.Complex.RealDeriv
+
+/RealDeriv.lean
+-- Harmonic functions on the plane
+
+variable {f : ℂ → ℂ} {e' : ℂ} {z : ℝ} {h : HasDerivAt f e' z}
+
+ example : 1 = 0 := by
+
+  let XX := HasDerivAt.real_of_complex h
+  sorry
+
+
+noncomputable def lax (f : ℂ → ℝ) (z : ℂ) : ℝ :=
+  iteratedFDeriv ℝ 1 f z ![Complex.I]
+
+example : lax (fun z ↦ z.re) = fun z ↦ 1 := by
+  unfold lax
+  simp
+  funext x
+  
+  let XX := HasDerivAt.real_of_complex 
+
+  sorry
+
+
+noncomputable def laplace (f : ℂ → ℝ) (z : ℂ) : ℝ :=
+  iteratedFDeriv ℝ 2 f z ![1, 1] + iteratedFDeriv ℝ 2 f z ![Complex.I, Complex.I]
+
+
+example : laplace (fun z ↦ z.re) = fun z ↦ 0 := by
+  
+  unfold laplace
+  rw [iteratedFDeriv_succ_eq_comp_left]
+  rw [iteratedFDeriv_succ_eq_comp_left]
+  rw [iteratedFDeriv_zero_eq_comp]
+  simp
+
+  have : Fin.tail ![Complex.I, Complex.I] = ![Complex.I] := by
+    rfl
+  rw [this]
+
+  rw [deriv_comp]
+  
+  simp
+  simp
+
+
+  conv =>
+    lhs
+    intro x
+    arg 1
+    intro t
+    rw [deriv_add] <;> tactic => try fun_prop
+  simp
+  rfl
+
+example : laplace' (fun z ↦ (z*z).re) = fun z ↦ 0 := by
+  
+  unfold laplace' lineDeriv  
+  simp
+
+  conv =>
+    lhs
+    intro x
+    simp
+    arg 1
+    arg 1
+    intro t
+    rw [deriv_sub] <;> tactic => try fun_prop
+    simp
+    rw [deriv_mul] <;> tactic => try fun_prop
+    simp
+    rw [deriv_add] <;> tactic => try fun_prop
+    simp
+  
+  conv =>
+    lhs
+    intro x
+    arg 1
+    rw [deriv_add] <;> tactic => try fun_prop
+    rw [deriv_add] <;> tactic => try fun_prop
+    simp
+    rw [one_add_one_eq_two]
+
+
+  conv =>
+    lhs
+    intro x
+    arg 2
+    conv =>
+      arg 1
+      intro t
+      rw [deriv_sub] <;> tactic => try fun_prop
+      rw [deriv_mul] <;> tactic => try fun_prop
+      simp
+      rw [deriv_mul] <;> tactic => try fun_prop
+      simp
+      rw [deriv_add] <;> tactic => try fun_prop
+      rw [deriv_add] <;> tactic => try fun_prop
+      simp
+    
+  conv =>
+    lhs
+    intro x
+    rw [deriv_add] <;> tactic => try fun_prop
+    rw [deriv_add] <;> tactic => try fun_prop
+    simp
+
+  group
+
+open Complex ContinuousLinearMap
+
+open scoped ComplexConjugate
+
+variable {z : ℂ} {f : ℂ → ℂ}
+
+#check deriv_comp_const_add
+
+theorem DifferentiableAt_conformalAt (h : DifferentiableAt ℂ f z) :
+    ConformalAt f z := by
+
+  let XX := (h.hasFDerivAt.restrictScalars ℝ).fderiv
+
+  let f₁ := fun x ↦ lineDeriv ℝ f x 1
+  let f₂ := fun x ↦ lineDeriv ℝ f x Complex.I
+
+  have t₁ : deriv (fun (t : ℂ) => f (z + t)) 0 = deriv f z := by
+    rw [deriv_comp_const_add]
+    simp
+    simp
+    exact h
+  have t'₁ : deriv (fun (t : ℝ) => f (z + ↑t)) 0 = deriv f z := by
+    sorry
+
+  have : f₁ z = deriv f z := by
+    dsimp [f₁]
+    unfold lineDeriv
+    simp
+    exact t'₁
+
+  have : f₂ z = deriv f z := by
+    dsimp [f₂]
+    unfold lineDeriv
+    simp
+
+    exact t'₁
+
+
+  /-
+  simp at f₂
+
+  rw [conformalAt_iff_isConformalMap_fderiv, (h.hasFDerivAt.restrictScalars ℝ).fderiv]
+  apply isConformalMap_complex_linear
+  simpa only [Ne, ext_ring_iff]
+  -/
+
+example : laplace' (fun z ↦ (Complex.exp z).re) = fun z ↦ 0 := by
+
+  let f := fun z ↦ (Complex.exp z).re
+  let f₁ := fun x ↦ lineDeriv ℝ f x 1
+  let fz := fun x ↦ deriv f
+
+
+
+example : laplace' (fun z ↦ (Complex.exp z).re) = fun z ↦ 0 := by
+  
+  unfold laplace' lineDeriv  
+  simp
+  
+  conv =>
+    lhs
+    arg 1
+    intro x
+    arg 1
+    intro t
+    arg 1
+    intro t₁
+    rw [Complex.exp_add]
+    rw [Complex.exp_add]
+  
+  conv =>
+    lhs
+    arg 1
+    intro x
+    arg 1
+    intro t
+    simp
+    conv =>
+      rhs
+      arg 1
+      intro x₁
+      rw [Complex.exp_re]
+      simp
+    rw [Real.deriv_exp]
+    simp
+  
+  conv =>
+    lhs
+    arg 1
+    intro x
+    simp
+    rhs
+    arg 1
+    intro x
+    rw [Complex.exp_re]
+  
+  conv =>
+    lhs
+    lhs
+    intro x
+    rhs
+    lhs
+    intro x₁
+    simp
+  
+  simp
+
+  conv =>
+    lhs
+    rhs
+    intro x
+    lhs
+    intro t
+    arg 1
+    intro t₁
+    rw [Complex.exp_add]
+    rw [Complex.exp_add]
+    simp
+    rw [Complex.exp_re]
+    rw [Complex.exp_im]
+    simp
+
+  conv =>
+    lhs
+    rhs
+    intro x
+    lhs
+    intro t
+    simp
+    rw [deriv_sub] <;> tactic => try fun_prop
+    rw [deriv_mul] <;> tactic => try fun_prop
+    rw [deriv_mul] <;> tactic => try fun_prop
+    simp
+
+
+      
+
+    
+    
+  
+
+    
+
+    
+    -- oops
+
+
+
+
+        conv =>
+          lhs
+
+          rw [Complex.exp_add]
+                  
+        rw [deriv_mul] <;> tactic => try fun_prop
+
+
+
+  sorry
+
+  rw [deriv_add] <;> tactic => try fun_prop
+
+      
+
+
+
+
+
+
+  sorry
+
+noncomputable def laplace : (ℂ → ℝ) → (ℂ → ℝ) := by
+  intro f
+
+  let F : ℝ × ℝ → ℝ := fun x ↦ f (x.1 + x.2 * Complex.I)
+
+  let e₁ : ℝ × ℝ := ⟨1, 0⟩ 
+  let e₂ : ℝ × ℝ := ⟨0, 1⟩ 
+
+  let F₁ := fun x ↦ lineDeriv ℝ F x e₁
+  let F₁₁ := fun x ↦ lineDeriv ℝ F₁ x e₁
+  let F₂ := fun x ↦ lineDeriv ℝ F x e₂
+  let F₂₂ := fun x ↦ lineDeriv ℝ F₂ x e₂
+
+  exact fun x ↦ F₁₁ ⟨x.1, x.2⟩ + F₂₂ ⟨x.1, x.2⟩
+
+
+example : ∀ z₀ : ℂ, laplace (fun z ↦ (z*z).re) z₀ = 0 := by
+  intro z₀
+  unfold laplace
+  dsimp [lineDeriv]
+  simp
+  conv =>
+    lhs
+    lhs
+    arg 1
+    intro t
+    rw [deriv_sub] <;> tactic => try fun_prop
+    rw [deriv_mul] <;> tactic => try fun_prop
+    rw [deriv_const_add]
+    simp
+    ring_nf
+  conv =>
+    lhs
+    rhs
+    arg 1
+    intro t
+    rw [deriv_sub] <;> tactic => try fun_prop
+    rw [deriv_const]
+    rw [deriv_mul] <;> tactic => try fun_prop
+    rw [deriv_const_add]
+    simp
+    ring_nf
+  rw [deriv_const_add, deriv_sub] <;> try fun_prop
+  simp
+
+example : ∀ z₀ : ℂ, laplace (fun z ↦ (Complex.exp z).re) z₀ = 0 := by
+  intro z₀ 
+
+  unfold laplace
+  dsimp [lineDeriv]
+  simp
+
+  sorry
+
+example : deriv (fun (t : ℝ) ↦ 2 + t) = fun (t : ℝ) ↦ 1 := by
+  -- in my experience with the library, more results are stated about
+  -- `HasDerivAt` than about equality of `deriv`
+  rw [deriv_eq] 
+  
+  intro x
+  
+  -- I guessed the name `HasDerivAt.add`, which didn't work, but the
+  -- autocomplete dropdown showed `add_const` and `const_add` too
+  apply HasDerivAt.const_add 
+
+  -- I assumed this was in the library, and `apply?` found it
+  exact hasDerivAt_id' x 
+
+
+example : laplace (fun z ↦ (Complex.exp z).re) = 0 := by
+  have : (fun z => (Complex.exp z).re) = (fun z => Real.exp z.re * Real.cos z.im) := by
+    funext z
+    rw [Complex.exp_re]
+  rw [this]
+
+  unfold laplace
+  simp
+
+  have F₁ : (fun (x : ℝ × ℝ) => lineDeriv ℝ (fun (t : ℝ × ℝ) => Real.exp t.1 * Real.cos t.2) x ⟨1, 0⟩) = ((fun (x : ℝ × ℝ) => (Real.exp x.1 * Real.cos x.2))) := by
+    funext x    
+    dsimp [lineDeriv]        
+    simp
+    left
+    have t₁ : (fun x_1 => Real.exp (x.1 + x_1)) = (fun x_1 => Real.exp x.1 * Real.exp x_1) := by
+      funext t
+      exact Real.exp_add x.1 t
+    rw [t₁]
+    simp
+
+  have F₂ : (fun (x : ℝ × ℝ) => lineDeriv ℝ (fun (t : ℝ × ℝ) => Real.exp t.1 * Real.sin t.2) x ⟨0, 1⟩) = ((fun (x : ℝ × ℝ) => (Real.exp x.1 * Real.cos x.2))) := by
+    funext x    
+    
+    dsimp [lineDeriv]
+    simp 
+
+    have t₁ : (fun t => Real.sin (x.2 + t)) = (Real.sin ∘ (fun t => x.2 + t)) := by
+      rfl
+    rw [t₁]
+    rw [deriv.comp]
+    simp
+
+    have : deriv (fun (t : ℝ) ↦ 2 + t) = fun (t : ℝ) ↦ 1 := by
+      simp [deriv.add]            
+      sorry
+      
+      
+
+    rw [this]
+    simp
+    · exact Real.differentiableAt_sin
+    · -- DifferentiableAt ℝ (fun t => x.2 + t) 0
+      sorry
+
+
+  rw [this]
+
+  sorry
+
+    have : deriv (fun x_1 => Real.exp (x_1 + x_1)) 0 = 2 := by
+      simp
+      group
+    
+    
+    rw [this]
+    simp
+    
+    have : deriv (fun t => Real.cos (x.2 + t * y.2)) = (fun t => -y.2 * Real.sin (x.2 + t * y.2)) := by
+      funext t₀
+      have t₁ : (fun t => Real.cos (x.2 + t * y.2)) = (Real.cos ∘ (fun t => x.2 + t * y.2)) := by
+        rfl
+      rw [t₁]
+      rw [deriv.comp]
+      simp
+      · group
+      · exact Real.differentiableAt_cos
+      · simp
+    
+    simp
+    simp
+
+    sorry
+  
+  let XX := fderiv ℝ (fun (x : ℝ × ℝ) => Real.exp x.1 * Real.cos x.2)
+  simp at XX
+
+  have : fderiv ℝ fun x => Real.exp x.1 * Real.cos x.2 = 0 := by
+
+    sorry
+
+  funext z
+  simp
+  funext 
+
+  let ZZ := Complex.exp_re z
+  sorry

Nevanlinna/logabs.lean

@@ -0,0 +1,56 @@
+import Mathlib.Analysis.Complex.CauchyIntegral
+open ComplexConjugate
+
+/- logAbs of a product is sum of logAbs of factors -/
+
+lemma logAbs_mul : ∀ z₁ z₂ : ℂ, z₁ ≠ 0 → z₂ ≠ 0 → Real.log (Complex.abs (z₁ * z₂)) = Real.log (Complex.abs z₁) + Real.log (Complex.abs z₂) := by
+  intro z₁ z₂ z₁Hyp z₂Hyp
+  rw [Complex.instNormedFieldComplex.proof_2 z₁ z₂]
+  exact Real.log_mul ((AbsoluteValue.ne_zero_iff Complex.abs).mpr z₁Hyp) ((AbsoluteValue.ne_zero_iff Complex.abs).mpr z₂Hyp)
+
+lemma absAndProd : ∀ z : ℂ, Complex.abs z = Real.sqrt ( (z * conj z).re ) := by
+  intro z
+  simp
+  rfl
+
+#check Complex.log_mul_eq_add_log_iff
+#check Complex.arg_eq_pi_iff
+
+lemma logAbsXX : ∀ z : ℂ, z ≠ 0 → Real.log (Complex.abs z) = (1 / 2) * Complex.log z + (1 / 2) * Complex.log (conj z) := by
+  intro z z₁Hyp
+
+  by_cases argHyp : Complex.arg z = Real.pi
+
+  -- Show pos: Complex.arg z = Real.pi
+  have : conj z = z := by
+    apply Complex.conj_eq_iff_im.2
+    rw [Complex.arg_eq_pi_iff] at argHyp
+    exact argHyp.right
+  rw [this]
+  sorry
+
+  -- Show pos: Complex.arg z ≠ Real.pi
+  have t₁ : Complex.abs z = Real.sqrt (Complex.normSq z) := by
+    exact rfl
+  rw [t₁]
+  
+  have t₂ : 0 ≤ Complex.normSq z := by
+    exact Complex.normSq_nonneg z
+  rw [ Real.log_sqrt t₂ ]
+
+
+  have t₃ : Real.log (Complex.normSq z) = Complex.log (Complex.normSq z) := by
+    apply Complex.ofReal_log
+    exact t₂
+  simp
+  rw [t₃]
+  rw [Complex.normSq_eq_conj_mul_self]
+  
+  have t₄ : conj z ≠ 0 := by
+    exact (AddEquivClass.map_ne_zero_iff starRingAut).mpr z₁Hyp
+
+  let XX := Complex.log_mul_eq_add_log_iff this z₁Hyp
+
+
+
+  sorry

Nevanlinna/realHarmonic.lean

@@ -0,0 +1,16 @@
+import Mathlib.Analysis.Calculus.LineDeriv.Basic
+import Mathlib.Analysis.Calculus.ContDiff.Defs
+
+noncomputable def Real.laplace : (ℝ × ℝ → ℝ) → (ℝ × ℝ → ℝ) := by
+  intro f
+
+  let f₁ := fun x ↦ lineDeriv ℝ f x ⟨1,0⟩
+  let f₁₁ := fun x ↦ lineDeriv ℝ f₁ x ⟨1,0⟩
+  let f₂ := fun x ↦ lineDeriv ℝ f x ⟨0,1⟩
+  let f₂₂ := fun x ↦ lineDeriv ℝ f₂ x ⟨0,1⟩
+
+  exact f₁₁ + f₂₂
+
+
+def Harmonic (f : ℝ × ℝ → ℝ) : Prop :=
+  (ContDiff ℝ 2 f) ∧ (∀ x, Real.laplace f x = 0)

Nevanlinna/test.lean

@@ -0,0 +1,130 @@
+import Mathlib.Analysis.Complex.CauchyIntegral
+--import Mathlib.Analysis.Complex.Module
+
+
+open ComplexConjugate
+
+#check DiffContOnCl.circleIntegral_sub_inv_smul
+
+open Real
+
+theorem CauchyIntegralFormula :
+  ∀
+  {R : ℝ} -- Radius of the ball
+  {w : ℂ} -- Point in the interior of the ball
+  {f : ℂ → ℂ}, -- Holomorphic function
+  DiffContOnCl ℂ f (Metric.ball 0 R)
+  → w ∈ Metric.ball 0 R
+  → (∮ (z : ℂ) in C(0, R), (z - w)⁻¹ • f z) = (2 * π * Complex.I) • f w := by
+
+  exact DiffContOnCl.circleIntegral_sub_inv_smul
+
+#check CauchyIntegralFormula
+#check HasDerivAt.continuousAt
+#check Real.log
+#check ComplexConjugate.conj
+#check Complex.exp
+
+theorem SimpleCauchyFormula :
+  ∀
+  {R : ℝ} -- Radius of the ball
+  {w : ℂ} -- Point in the interior of the ball
+  {f : ℂ → ℂ}, -- Holomorphic function
+  Differentiable ℂ f
+  → w ∈ Metric.ball 0 R
+  → (∮ (z : ℂ) in C(0, R), (z - w)⁻¹ • f z) = (2 * Real.pi * Complex.I) • f w := by
+
+  intro R w f fHyp
+
+  apply DiffContOnCl.circleIntegral_sub_inv_smul
+
+  constructor
+  · exact Differentiable.differentiableOn fHyp
+  · suffices Continuous f from by
+      exact Continuous.continuousOn this
+    rw [continuous_iff_continuousAt]
+    intro x
+    exact DifferentiableAt.continuousAt (fHyp x)
+
+
+theorem JensenFormula₂ :
+  ∀
+  {R : ℝ} -- Radius of the ball
+  {f : ℂ → ℂ}, -- Holomorphic function
+  Differentiable ℂ f
+  → (∀ z ∈ Metric.ball 0 R, f z ≠ 0)
+  → (∫ (θ : ℝ) in Set.Icc 0 (2 * π), Complex.log ‖f (circleMap 0 R θ)‖ ) = 2 * π * Complex.log ‖f 0‖ := by
+
+  intro r f fHyp₁ fHyp₂
+
+  /- We treat the trivial case r = 0 separately. -/
+  by_cases rHyp : r = 0
+  rw [rHyp]
+  simp
+  left
+  unfold ENNReal.ofReal
+  simp
+  rw [max_eq_left (mul_nonneg zero_le_two pi_nonneg)]
+  simp
+  /- From hereon, we assume that r ≠ 0. -/
+
+  /- Replace the integral over 0 … 2π by a circle integral -/
+  suffices (∮ (z : ℂ) in C(0, r), -(Complex.I * z⁻¹ * Complex.log ↑(Complex.abs (f z)))) = 2 * ↑π * Complex.log ↑‖f 0‖ from by
+    have : ∫ (θ : ℝ) in Set.Icc 0 (2 * π), Complex.log ↑‖f (circleMap 0 r θ)‖ = (∮ (z : ℂ) in C(0, r), -(Complex.I * z⁻¹ * Complex.log ↑(Complex.abs (f z)))) := by
+      have : (fun θ ↦ Complex.log ‖f (circleMap 0 r θ)‖) = (fun θ ↦ ((deriv (circleMap 0 r) θ)) • ((deriv (circleMap 0 r) θ)⁻¹ • Complex.log ↑‖f (circleMap 0 r θ)‖)) := by
+        funext θ
+        rw [← smul_assoc, smul_eq_mul, smul_eq_mul, mul_inv_cancel, one_mul]
+        simp
+        exact rHyp
+      rw [this]
+      simp
+      let tmp := circleIntegral_def_Icc (fun z ↦ -(Complex.I * z⁻¹ * (Complex.log ↑‖f z‖))) 0 r
+      simp at tmp
+      rw [← tmp]
+    rw [this]
+
+  
+
+  have : ∀ z : ℂ, log (Complex.abs z) = 1/2 * Complex.log z + 1/2 * Complex.log (conj z) := by
+    intro z
+
+    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
+
+
+
+
+
+
+
+
+
+  sorry