Working…

Nevanlinna/complexHarmonic.examples.lean

@@ -249,6 +249,18 @@ theorem log_normSq_of_holomorphicOn_is_harmonicOn
   (h₂ : ∀ z ∈ s, f z ≠ 0) :
   HarmonicOn (Real.log ∘ Complex.normSq ∘ f) s := by
 
+  have slitPlaneLemma {z : ℂ} (hz : z ≠ 0) : z ∈ Complex.slitPlane ∨ -z ∈ Complex.slitPlane := by
+    rw [Complex.mem_slitPlane_iff]
+    rw [Complex.mem_slitPlane_iff]
+    simp at hz
+    rw [Complex.ext_iff] at hz
+    push_neg at hz
+    simp at hz
+    simp
+    by_contra contra
+    push_neg at contra
+    exact hz (le_antisymm contra.1.1 contra.2.1) contra.1.2
+
   let s₁ : Set ℂ := { z | f z ∈ Complex.slitPlane} ∩ s
 
   have hs₁ : IsOpen s₁ := by
@@ -318,10 +330,8 @@ theorem log_normSq_of_holomorphicOn_is_harmonicOn
     · exact hs₂
     · constructor
       · constructor
-        · simp
+        · apply Or.resolve_left (slitPlaneLemma (h₂ z hz)) hfz
-          rw [Complex.mem_slitPlane_iff]
+        · exact hz
-          rw [Complex.mem_slitPlane_iff] at hfz
-          simp at hfz
       · have : s₂ = s ∩ s₂ := by
           apply Set.right_eq_inter.mpr
           exact Set.inter_subset_right {z | -f z ∈ Complex.slitPlane} s

Nevanlinna/complexHarmonic.lean

@@ -23,11 +23,12 @@ variable {G₁ : Type*} [NormedAddCommGroup G₁] [NormedSpace ℂ G₁] [Comple
 
 
 def Harmonic (f : ℂ → F) : Prop :=
-  (ContDiff ℝ 2 f) ∧ (∀ z, Complex.laplace f z = 0)
+  (ContDiff ℝ 2 f) ∧ (∀ z, Δ f z = 0)
 
 
 def HarmonicOn (f : ℂ → F) (s : Set ℂ) : Prop :=
-  (ContDiffOn ℝ 2 f s) ∧ (∀ z ∈ s, Complex.laplace f z = 0)
+  (ContDiffOn ℝ 2 f s) ∧ (∀ z ∈ s, Δ f z = 0)
+
 
 
 theorem HarmonicOn_of_locally_HarmonicOn {f : ℂ → F} {s : Set ℂ} (h : ∀ x ∈ s, ∃ (u : Set ℂ), IsOpen u ∧ x ∈ u ∧ HarmonicOn f (s ∩ u)) :
@@ -135,7 +136,7 @@ theorem harmonic_comp_CLM_is_harmonic {f : ℂ → F₁} {l : F₁ →L[ℝ] G}
     apply ContDiff.comp
     exact ContinuousLinearMap.contDiff l
     exact h.1
-  · rw [laplace_compContLin]
+  · rw [laplace_compCLM]
     simp
     intro z
     rw [h.2 z]
@@ -152,7 +153,7 @@ theorem harmonicOn_comp_CLM_is_harmonicOn {f : ℂ → F₁} {s : Set ℂ} {l :
     exact h.1
   · -- Vanishing of Laplace
     intro z zHyp
-    rw [laplace_compContLinAt]
+    rw [laplace_compCLMAt]
     simp
     rw [h.2 z]
     simp

Nevanlinna/laplace.lean

@@ -20,18 +20,25 @@ variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
 variable {G : Type*} [NormedAddCommGroup G] [NormedSpace ℝ G]
 
 
-noncomputable def Complex.laplace : (ℂ → F) → (ℂ → F) :=
+noncomputable def Complex.laplace (f : ℂ → F) : ℂ → F :=
-  fun f ↦ partialDeriv ℝ 1 (partialDeriv ℝ 1 f) + partialDeriv ℝ Complex.I (partialDeriv ℝ Complex.I f)
+  partialDeriv ℝ 1 (partialDeriv ℝ 1 f) + partialDeriv ℝ Complex.I (partialDeriv ℝ Complex.I f)
+
+notation "Δ" => Complex.laplace
 
 
-theorem laplace_eventuallyEq {f₁ f₂ : ℂ → F} {x : ℂ} (h : f₁ =ᶠ[nhds x] f₂) : Complex.laplace f₁ x = Complex.laplace f₂ x := by
+theorem laplace_eventuallyEq {f₁ f₂ : ℂ → F} {x : ℂ} (h : f₁ =ᶠ[nhds x] f₂) : Δ f₁ x = Δ f₂ x := by
   unfold Complex.laplace
   simp
   rw [partialDeriv_eventuallyEq ℝ (partialDeriv_eventuallyEq' ℝ h 1) 1]
   rw [partialDeriv_eventuallyEq ℝ (partialDeriv_eventuallyEq' ℝ h Complex.I) Complex.I]
 
 
-theorem laplace_add {f₁ f₂ : ℂ → F} (h₁ : ContDiff ℝ 2 f₁) (h₂ : ContDiff ℝ 2 f₂): Complex.laplace (f₁ + f₂) = (Complex.laplace f₁) + (Complex.laplace f₂) := by
+theorem laplace_add 
+  {f₁ f₂ : ℂ → F}
+  (h₁ : ContDiff ℝ 2 f₁)
+  (h₂ : ContDiff ℝ 2 f₂) : 
+  Δ (f₁ + f₂) = (Δ f₁) + (Δ f₂) := by
+
   unfold Complex.laplace
   rw [partialDeriv_add₂]
   rw [partialDeriv_add₂]
@@ -59,7 +66,7 @@ theorem laplace_add_ContDiffOn
   (hs : IsOpen s)
   (h₁ : ContDiffOn ℝ 2 f₁ s)
   (h₂ : ContDiffOn ℝ 2 f₂ s) :
-  ∀ x ∈ s, Complex.laplace (f₁ + f₂) x = (Complex.laplace f₁) x + (Complex.laplace f₂) x := by
+  ∀ x ∈ s, Δ (f₁ + f₂) x = (Δ f₁) x + (Δ f₂) x := by
 
   unfold Complex.laplace
   simp
@@ -124,39 +131,21 @@ theorem laplace_add_ContDiffOn
   rw [add_comm]
 
 
-theorem laplace_smul {f : ℂ → F} : ∀ v : ℝ, Complex.laplace (v • f) = v • (Complex.laplace f) := by
+theorem laplace_smul {f : ℂ → F} : ∀ v : ℝ, Δ (v • f) = v • (Δ f) := by
   intro v
   unfold Complex.laplace
-  rw [partialDeriv_smul₂]
+  repeat
-  rw [partialDeriv_smul₂]
+    rw [partialDeriv_smul₂]
-  rw [partialDeriv_smul₂]
-  rw [partialDeriv_smul₂]
   simp
 
 
-theorem laplace_compContLin {f : ℂ → F} {l : F →L[ℝ] G} (h : ContDiff ℝ 2 f) :
+theorem laplace_compCLMAt {f : ℂ → F} {l : F →L[ℝ] G} {x : ℂ} (h : ContDiffAt ℝ 2 f x) :
-  Complex.laplace (l ∘ f) = l ∘ (Complex.laplace f) := by
+  Δ (l ∘ f) x = (l ∘ (Δ f)) x := by
-  unfold Complex.laplace
-  rw [partialDeriv_compContLin]
-  rw [partialDeriv_compContLin]
-  rw [partialDeriv_compContLin]
-  rw [partialDeriv_compContLin]
-  simp
 
-  exact (partialDeriv_contDiff ℝ h Complex.I).differentiable le_rfl
+  obtain ⟨v, hv₁, hv₂, hv₃, hv₄⟩ : ∃ v ∈ nhds x, (IsOpen v) ∧ (x ∈ v) ∧ (ContDiffOn ℝ 2 f v) := by
-  exact h.differentiable one_le_two
+    obtain ⟨u, hu₁, hu₂⟩ : ∃ u ∈ nhds x, ContDiffOn ℝ 2 f u := by
-  exact (partialDeriv_contDiff ℝ h 1).differentiable le_rfl
-  exact h.differentiable one_le_two
-
-
-theorem laplace_compContLinAt {f : ℂ → F} {l : F →L[ℝ] G} {x : ℂ} (h : ContDiffAt ℝ 2 f x) :
-  Complex.laplace (l ∘ f) x = (l ∘ (Complex.laplace f)) x := by
-
-  have A₂ : ∃ v ∈ nhds x, (IsOpen v) ∧ (x ∈ v) ∧ (ContDiffOn ℝ 2 f v) := by
-    have : ∃ u ∈ nhds x, ContDiffOn ℝ 2 f u := by
       apply ContDiffAt.contDiffOn h
       rfl
-    obtain ⟨u, hu₁, hu₂⟩ := this
     obtain ⟨v, hv₁, hv₂, hv₃⟩ := mem_nhds_iff.1 hu₁
     use v
     constructor
@@ -166,7 +155,6 @@ theorem laplace_compContLinAt {f : ℂ → F} {l : F →L[ℝ] G} {x : ℂ} (h :
       constructor
       · exact hv₃
       · exact ContDiffOn.congr_mono hu₂ (fun x => congrFun rfl) hv₁
-  obtain ⟨v, hv₁, hv₂, hv₃, hv₄⟩ := A₂
 
   have D : ∀ w : ℂ, partialDeriv ℝ w (l ∘ f) =ᶠ[nhds x] l ∘ partialDeriv ℝ w (f) := by
     intro w
@@ -192,17 +180,24 @@ theorem laplace_compContLinAt {f : ℂ → F} {l : F →L[ℝ] G} {x : ℂ} (h :
   simp
 
   -- DifferentiableAt ℝ (partialDeriv ℝ Complex.I f) x
-  apply ContDiffAt.differentiableAt (partialDeriv_contDiffAt ℝ (ContDiffOn.contDiffAt hv₄ hv₁) Complex.I)
+  apply ContDiffAt.differentiableAt (partialDeriv_contDiffAt ℝ (ContDiffOn.contDiffAt hv₄ hv₁) Complex.I) le_rfl
-  rfl
 
   -- DifferentiableAt ℝ (partialDeriv ℝ 1 f) x
-  apply ContDiffAt.differentiableAt (partialDeriv_contDiffAt ℝ (ContDiffOn.contDiffAt hv₄ hv₁) 1)
+  apply ContDiffAt.differentiableAt (partialDeriv_contDiffAt ℝ (ContDiffOn.contDiffAt hv₄ hv₁) 1) le_rfl
-  rfl
 
 
-theorem laplace_compCLE {f : ℂ → F} {l : F ≃L[ℝ] G} (h : ContDiff ℝ 2 f) :
+theorem laplace_compCLM 
-  Complex.laplace (l ∘ f) = l ∘ (Complex.laplace f) := by
+  {f : ℂ → F} 
-  let l' := (l : F →L[ℝ] G)
+  {l : F →L[ℝ] G} 
-  have : Complex.laplace (l' ∘ f) = l' ∘ (Complex.laplace f) := by
+  (h : ContDiff ℝ 2 f) :
-    exact laplace_compContLin h
+  Δ (l ∘ f) = l ∘ (Δ f) := by
-  exact this
+  funext z
+  exact laplace_compCLMAt h.contDiffAt 
+
+
+theorem laplace_compCLE {f : ℂ → F} {l : F ≃L[ℝ] G} :
+  Δ (l ∘ f) = l ∘ (Δ f) := by
+  unfold Complex.laplace
+  repeat
+    rw [partialDeriv_compCLE]
+  simp