Nevanlinna/complexHarmonic.lean

@@ -126,22 +126,6 @@ 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
-
-  have t₂ : Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f = ⇑(starRingEnd ℂ) ∘ Complex.log ∘ f := by
-    funext z
-    unfold Function.comp
-    rw [Complex.log_conj]
-    exact Complex.slitPlane_arg_ne_pi (h₃ z)
-
-  have t₃ : ⇑(starRingEnd ℂ) ∘ Complex.log ∘ f = Complex.conjCLE ∘ Complex.log ∘ f := by
-    rfl
-
   -- The norm square is z * z.conj
   have normSq_conj : ∀ (z : ℂ), (starRingEnd ℂ) z * z = ↑‖z‖ ^ 2 := Complex.conj_mul'
 
@@ -161,16 +145,6 @@ theorem logabs_of_holomorphic_is_harmonic
     apply ContinuousLinearMap.contDiff Complex.imCLM
     apply ContinuousLinearMap.contDiff Complex.imCLM
 
-  have t₄ : ContDiff ℝ 2 (Real.log ∘ ⇑Complex.normSq ∘ f) := by
-    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
-
   constructor
   · -- logabs f is real C²
     have : (fun z ↦ Real.log ‖f z‖) = (2 : ℝ)⁻¹ • (Real.log ∘ Complex.normSq ∘ f) := by
@@ -217,8 +191,7 @@ theorem logabs_of_holomorphic_is_harmonic
       intro z
       rw [laplace_compContLin]
       simp
-      -- ContDiff ℝ 2 (Real.log ∘ ⇑Complex.normSq ∘ f)
+      sorry
-      exact t₄
     conv =>
       intro z
       rw [this z]
@@ -258,31 +231,32 @@ 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 t₀
+      let A := holomorphic_is_harmonic this
       funext z
       exact A.2 z
     rw [t₁]
     simp
 
-    rw [t₂]
+    have : Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f = ⇑(starRingEnd ℂ) ∘ Complex.log ∘ f := by
+      funext z
+      unfold Function.comp
+      rw [Complex.log_conj]
+      exact Complex.slitPlane_arg_ne_pi (h₃ z)
+    rw [this]
 
-    rw [t₃]
+    have : ⇑(starRingEnd ℂ) ∘ Complex.log ∘ f = Complex.conjCLE ∘ Complex.log ∘ f := by
+      rfl
+    rw [this]
     rw [laplace_compCLE]
     rw [t₁]
     simp
-
+    sorry
-    -- ContDiff ℝ 2 (Complex.log ∘ f)
+    sorry
-    exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff t₀)
+    sorry
-
-    -- ContDiff ℝ 2 (Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f)
-    rw [t₂, t₃]
-    apply ContDiff.comp
-    exact ContinuousLinearEquiv.contDiff Complex.conjCLE
-    exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff t₀)
-
-    -- ContDiff ℝ 2 (Complex.log ∘ f)
-    exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff t₀)
-
-    -- ContDiff ℝ 2 (Real.log ∘ ⇑Complex.normSq ∘ f)
-    exact t₄