Update complexHarmonic.lean

Nevanlinna/complexHarmonic.lean

@@ -126,6 +126,13 @@ theorem logabs_of_holomorphic_is_harmonic
   have f_is_real_C2 : ContDiff ℝ 2 f :=
     ContDiff.restrict_scalars ℝ (Differentiable.contDiff h₁)
 
+  -- Complex.log ∘ f is real C²
+  have t₀ : Differentiable ℂ (Complex.log ∘ f) := by
+    intro z
+    apply DifferentiableAt.comp
+    exact Complex.differentiableAt_log (h₃ z)
+    exact h₁ z
+
   -- The norm square is z * z.conj
   have normSq_conj : ∀ (z : ℂ), (starRingEnd ℂ) z * z = ↑‖z‖ ^ 2 := Complex.conj_mul'
 
@@ -231,14 +238,8 @@ theorem logabs_of_holomorphic_is_harmonic
     rw [this]
     rw [laplace_add]
 
-    have : Differentiable ℂ (Complex.log ∘ f) := by
-      intro z
-      apply DifferentiableAt.comp
-      exact Complex.differentiableAt_log (h₃ z)
-      exact h₁ z
-
     have t₁: Complex.laplace (Complex.log ∘ f) = 0 := by
-      let A := holomorphic_is_harmonic this
+      let A := holomorphic_is_harmonic t₀
       funext z
       exact A.2 z
     rw [t₁]
@@ -257,6 +258,23 @@ theorem logabs_of_holomorphic_is_harmonic
     rw [laplace_compCLE]
     rw [t₁]
     simp
+
+    -- ContDiff ℝ 2 (Complex.log ∘ f)
+    exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff t₀)
+
+    -- ContDiff ℝ 2 (Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f)
+
     sorry
-    sorry
-    sorry
+
+    -- ContDiff ℝ 2 (Complex.log ∘ f)
+    exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff t₀)
+
+    -- ContDiff ℝ 2 (Real.log ∘ ⇑Complex.normSq ∘ f)
+    rw [contDiff_iff_contDiffAt]
+    intro z
+    apply ContDiffAt.comp
+    apply Real.contDiffAt_log.mpr
+    simp
+    exact h₂ z
+    apply ContDiff.comp_contDiffAt z normSq_is_real_C2
+    exact ContDiff.contDiffAt f_is_real_C2