Create logabs.lean

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 : 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