Update complexHarmonic.lean

Nevanlinna/complexHarmonic.lean

@@ -26,7 +26,7 @@ def Harmonic (f : ℂ → F) : Prop :=
   (ContDiff ℝ 2 f) ∧ (∀ z, Complex.laplace f z = 0)
 
 
-theorem harmonic_add_harmonic_is_harmonic {f₁ f₂ : ℂ → F₁} (h₁ : Harmonic f₁) (h₂ : Harmonic f₂) :
+theorem harmonic_add_harmonic_is_harmonic {f₁ f₂ : ℂ → F} (h₁ : Harmonic f₁) (h₂ : Harmonic f₂) :
   Harmonic (f₁ + f₂) := by
   constructor
   · exact ContDiff.add h₁.1 h₂.1
@@ -37,6 +37,25 @@ theorem harmonic_add_harmonic_is_harmonic {f₁ f₂ : ℂ → F₁} (h₁ : Har
     simp
 
 
+theorem harmonic_smul_const_is_harmonic {f : ℂ → F} {c : ℝ} (h : Harmonic f) :
+  Harmonic (c • f) := by
+  constructor
+  · exact ContDiff.const_smul c h.1
+  · rw [laplace_smul h.1]
+    dsimp
+    intro z
+    rw [h.2 z]
+    simp
+
+
+theorem harmonic_iff_smul_const_is_harmonic {f : ℂ → F} {c : ℝ} (hc : c ≠ 0) :
+  Harmonic f ↔ Harmonic (c • f) := by
+  constructor
+  · exact harmonic_smul_const_is_harmonic
+  · nth_rewrite 2 [((eq_inv_smul_iff₀ hc).mpr rfl : f = c⁻¹ • c • f)]
+    exact fun a => harmonic_smul_const_is_harmonic a
+
+
 theorem harmonic_comp_CLM_is_harmonic {f : ℂ → F₁} {l : F₁ →L[ℝ] G} (h : Harmonic f) :
   Harmonic (l ∘ f) := by
 
@@ -149,31 +168,17 @@ theorem log_normSq_of_holomorphic_is_harmonic
   (h₃ : ∀ z, f z ∈ Complex.slitPlane) :
   Harmonic (Real.log ∘ Complex.normSq ∘ f) := by
 
-  -- Suffices to show Harmonic (⇑Complex.ofRealCLM ∘ Real.log ∘ ⇑Complex.normSq ∘ f)
+  suffices hyp : Harmonic (⇑Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ f) from
-  let F := Real.log ∘ Complex.normSq ∘ f
+    (harmonic_comp_CLM_is_harmonic hyp : Harmonic (Complex.reCLM ∘ Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ f))
-  have : Harmonic (Complex.ofRealCLM ∘ F) → Harmonic F := by
-    intro hyp
-    have t₁ : Harmonic (Complex.reCLM ∘ Complex.ofRealCLM ∘ F) := harmonic_comp_CLM_is_harmonic hyp
-    have t₂ : Complex.reCLM ∘ Complex.ofRealCLM ∘ F = F := rfl
-    rw [t₂] at t₁
-    exact t₁
-  apply this
-  dsimp [F]
 
-  -- Suffices to show Harmonic (Complex.log ∘ Complex.ofRealCLM ∘ Complex.normSq ∘ f)
+  suffices hyp : Harmonic (Complex.log ∘ (((starRingEnd ℂ) ∘ f) * f)) from by
-  have : Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ f = Complex.log ∘ Complex.ofRealCLM ∘ Complex.normSq ∘ f := by
+    have : Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ f = Complex.log ∘ (((starRingEnd ℂ) ∘ f) * f) := by
-    unfold Function.comp
-    funext z
-    apply Complex.ofReal_log
-    exact Complex.normSq_nonneg (f z)
-  rw [this]
-
-  -- Suffices to show Harmonic (Complex.log ∘ (⇑(starRingEnd ℂ) ∘ f * f))
-  have : Complex.ofRealCLM ∘ ⇑Complex.normSq ∘ f = ((starRingEnd ℂ) ∘ f) * f := by
       funext z
       simp
-    exact Complex.normSq_eq_conj_mul_self
+      rw [Complex.ofReal_log (Complex.normSq_nonneg (f z))]
+      rw [Complex.normSq_eq_conj_mul_self]
     rw [this]
+    exact hyp
 
 
   -- Suffices to show Harmonic (Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f + Complex.log ∘ f)
@@ -224,55 +229,7 @@ theorem logabs_of_holomorphic_is_harmonic
   (h₃ : ∀ z, f z ∈ Complex.slitPlane) :
   Harmonic (fun z ↦ Real.log ‖f z‖) := by
 
-  /- We start with a number of lemmas on regularity of all the functions involved -/
+  -- Suffices: Harmonic (2⁻¹ • Real.log ∘ ⇑Complex.normSq ∘ f)
-
-  -- The norm square is real C²
-  have normSq_is_real_C2 : ContDiff ℝ 2 Complex.normSq := by
-    unfold Complex.normSq
-    simp
-    conv =>
-      arg 3
-      intro x
-      rw [← Complex.reCLM_apply, ← Complex.imCLM_apply]
-    apply ContDiff.add
-    apply ContDiff.mul
-    apply ContinuousLinearMap.contDiff Complex.reCLM
-    apply ContinuousLinearMap.contDiff Complex.reCLM
-    apply ContDiff.mul
-    apply ContinuousLinearMap.contDiff Complex.imCLM
-    apply ContinuousLinearMap.contDiff Complex.imCLM
-
-  -- f is real C²
-  have f_is_real_C2 : ContDiff ℝ 2 f :=
-    ContDiff.restrict_scalars ℝ (Differentiable.contDiff h₁)
-
-  -- Complex.log ∘ f is real C²
-  have log_f_is_holomorphic : Differentiable ℂ (Complex.log ∘ f) := by
-    intro z
-    apply DifferentiableAt.comp
-    exact Complex.differentiableAt_log (h₃ z)
-    exact h₁ z
-
-  -- Real.log |f|² is real C²
-  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
-
-  have t₂ : Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f = Complex.conjCLE ∘ Complex.log ∘ f := by
-    funext z
-    unfold Function.comp
-    rw [Complex.log_conj]
-    rfl
-    exact Complex.slitPlane_arg_ne_pi (h₃ z)
-
-  constructor
-  · -- logabs f is real C²
   have : (fun z ↦ Real.log ‖f z‖) = (2 : ℝ)⁻¹ • (Real.log ∘ Complex.normSq ∘ f) := by
     funext z
     simp
@@ -283,87 +240,7 @@ theorem logabs_of_holomorphic_is_harmonic
     exact Complex.normSq_nonneg (f z)
   rw [this]
 
-    have : (2 : ℝ)⁻¹ • (Real.log ∘ Complex.normSq ∘ f) = (fun z ↦ (2 : ℝ)⁻¹ • ((Real.log ∘ ⇑Complex.normSq ∘ f) z)) := by
+  -- Suffices: Harmonic (Real.log ∘ ⇑Complex.normSq ∘ f)
-      exact rfl
+  apply (harmonic_iff_smul_const_is_harmonic (inv_ne_zero two_ne_zero)).1
-    rw [this]
-    apply ContDiff.const_smul
-    exact t₄
 
-  · -- Laplace vanishes
+  exact log_normSq_of_holomorphic_is_harmonic h₁ h₂ h₃
-    have : (fun z ↦ Real.log ‖f z‖) = (2 : ℝ)⁻¹ • (Real.log ∘ Complex.normSq ∘ f) := by
-      funext z
-      simp
-      unfold Complex.abs
-      simp
-      rw [Real.log_sqrt]
-      rw [div_eq_inv_mul (Real.log (Complex.normSq (f z))) 2]
-      exact Complex.normSq_nonneg (f z)
-    rw [this]
-    rw [laplace_smul]
-    simp
-
-    have : ∀ (z : ℂ), Complex.laplace (Real.log ∘ ⇑Complex.normSq ∘ f) z = 0 ↔ Complex.laplace (Complex.ofRealCLM ∘ Real.log ∘ ⇑Complex.normSq ∘ f) z = 0 := by
-      intro z
-      rw [laplace_compContLin]
-      simp
-      -- ContDiff ℝ 2 (Real.log ∘ ⇑Complex.normSq ∘ f)
-      exact t₄
-    conv =>
-      intro z
-      rw [this z]
-
-    have : Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ f = Complex.log ∘ Complex.ofRealCLM ∘ Complex.normSq ∘ f := by
-      unfold Function.comp
-      funext z
-      apply Complex.ofReal_log
-      exact Complex.normSq_nonneg (f z)
-    rw [this]
-
-    have : Complex.ofRealCLM ∘ ⇑Complex.normSq ∘ f = ((starRingEnd ℂ) ∘ f) * f := by
-      funext z
-      simp
-      exact Complex.normSq_eq_conj_mul_self
-    rw [this]
-
-    have : Complex.log ∘ (⇑(starRingEnd ℂ) ∘ f * f) = Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f + Complex.log ∘ f := by
-      unfold Function.comp
-      funext z
-      simp
-      rw [Complex.log_mul_eq_add_log_iff]
-
-      have : Complex.arg ((starRingEnd ℂ) (f z)) = - Complex.arg (f z) := by
-        rw [Complex.arg_conj]
-        have : ¬ Complex.arg (f z) = Real.pi := by
-          exact Complex.slitPlane_arg_ne_pi (h₃ z)
-        simp
-        tauto
-      rw [this]
-      simp
-      constructor
-      · exact Real.pi_pos
-      · exact Real.pi_nonneg
-      exact (AddEquivClass.map_ne_zero_iff starRingAut).mpr (h₂ z)
-      exact h₂ z
-    rw [this]
-    rw [laplace_add]
-
-    rw [t₂, laplace_compCLE]
-    intro z
-    simp
-    rw [(holomorphic_is_harmonic log_f_is_holomorphic).2 z]
-    simp
-
-    -- ContDiff ℝ 2 (Complex.log ∘ f)
-    exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff log_f_is_holomorphic)
-
-    -- ContDiff ℝ 2 (Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f)
-    rw [t₂]
-    apply ContDiff.comp
-    exact ContinuousLinearEquiv.contDiff Complex.conjCLE
-    exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff log_f_is_holomorphic)
-
-    -- ContDiff ℝ 2 (Complex.log ∘ f)
-    exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff log_f_is_holomorphic)
-
-    -- ContDiff ℝ 2 (Real.log ∘ ⇑Complex.normSq ∘ f)
-    exact t₄