Working…

Nevanlinna/complexHarmonic.examples.lean

@@ -16,12 +16,56 @@ import Mathlib.Topology.Instances.RealVectorSpace
 import Nevanlinna.cauchyRiemann
 import Nevanlinna.laplace
 import Nevanlinna.complexHarmonic
+import Nevanlinna.holomorphic
 
 variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
 variable {F₁ : Type*} [NormedAddCommGroup F₁] [NormedSpace ℂ F₁] [CompleteSpace F₁]
 variable {G : Type*} [NormedAddCommGroup G] [NormedSpace ℝ G]
 variable {G₁ : Type*} [NormedAddCommGroup G₁] [NormedSpace ℂ G₁] [CompleteSpace G₁]
 
+#check DifferentiableOn.contDiffOn
+
+theorem holomorphicAt_is_harmonicAt
+  {f : ℂ → F₁}
+  {z : ℂ}
+  (hf : HolomorphicAt f z) :
+  HarmonicAt f z := by
+
+  obtain ⟨s, hs, hz, h'f⟩ := HolomorphicAt_iff.1 hf
+
+  constructor
+  · -- ContDiffAt ℝ 2 f z
+    apply ContDiffOn.contDiffAt _ ((IsOpen.mem_nhds_iff hs).2 hz)
+    suffices h : ContDiffOn ℂ 2 f s from by
+      apply ContDiffOn.restrict_scalars ℝ h
+    apply DifferentiableOn.contDiffOn _ hs
+    intro w hw
+    apply DifferentiableAt.differentiableWithinAt
+    exact h'f w hw
+  · -- Δ f =ᶠ[nhds z] 0
+    obtain ⟨t, ht, hz, h'f⟩ := HolomorphicAt_isOpen.1 hf
+    apply Filter.eventuallyEq_iff_exists_mem.2
+    use t
+    constructor
+    · exact IsOpen.mem_nhds ht hz
+    · intro w hw
+      unfold Complex.laplace
+      simp
+
+      rw [partialDeriv_eventuallyEq ℝ (CauchyRiemann'₆ (h'f w hw)) Complex.I]
+      rw [partialDeriv_smul'₂]
+      simp
+
+      have f_is_real_C2 : ContDiffOn ℝ 2 f t :=
+        ContDiffOn.restrict_scalars ℝ (DifferentiableOn.contDiffOn h'f ht)
+      rw [partialDeriv_commOn ht f_is_real_C2 Complex.I 1 w hw]
+      rw [partialDeriv_eventuallyEq ℝ (CauchyRiemann'₆ (h'f w hw)) 1]
+      rw [partialDeriv_smul'₂]
+      simp
+
+      rw [← smul_assoc]
+      simp
+
 
 theorem holomorphic_is_harmonic {f : ℂ → F₁} (h : Differentiable ℂ f) :
   Harmonic f := by
@@ -115,9 +159,6 @@ theorem holomorphicOn_is_harmonicOn {f : ℂ → F₁} {s : Set ℂ} (hs : IsOpe
     simp
     rw [partialDeriv_commOn hs f_is_real_C2 Complex.I 1 z hz]
 
-    have : Complex.I • partialDeriv ℝ 1 (partialDeriv ℝ Complex.I f) z = Complex.I • (partialDeriv ℝ 1 (partialDeriv ℝ Complex.I f) z) := by
-      rfl
-    rw [this]
     have : partialDeriv ℝ Complex.I f =ᶠ[nhds z] Complex.I • partialDeriv ℝ 1 f := by
       unfold Filter.EventuallyEq
       unfold Filter.Eventually

Nevanlinna/complexHarmonic.lean

@@ -31,6 +31,7 @@ def HarmonicAt (f : ℂ → F) (x : ℂ) : Prop :=
 def HarmonicOn (f : ℂ → F) (s : Set ℂ) : Prop :=
   (ContDiffOn ℝ 2 f s) ∧ (∀ z ∈ s, Δ f z = 0)
 
+
 theorem HarmonicAt_iff
   {f : ℂ → F}
   {x : ℂ} :

Nevanlinna/holomorphic.lean

@@ -33,11 +33,42 @@ theorem HolomorphicAt_iff
     · assumption
 
 
-theorem CauchyRiemann₅
+theorem HolomorphicAt_isOpen
+  {f : E → F}
+  {x : E} :
+  HolomorphicAt f x ↔ ∃ s : Set E, IsOpen s ∧ x ∈ s ∧ (∀ z ∈ s, HolomorphicAt f z) := by
+  constructor
+  · intro hf
+    obtain ⟨t, h₁t, h₂t⟩ := hf
+    obtain ⟨s, h₁s, h₂s, h₃s⟩ := mem_nhds_iff.1 h₁t
+    use s
+    constructor
+    · assumption
+    · constructor
+      · assumption
+      · intro z hz
+        apply HolomorphicAt_iff.2
+        use s
+        constructor
+        · assumption
+        · constructor
+          · assumption
+          · exact fun w hw ↦ h₂t w (h₁s hw)
+  · intro hyp
+    obtain ⟨s, h₁s, h₂s, hf⟩ := hyp
+    use s
+    constructor
+    · apply (IsOpen.mem_nhds_iff h₁s).2 h₂s
+    · intro z hz
+      obtain ⟨t, ht⟩ := (hf z hz)
+      exact ht.2 z (mem_of_mem_nhds ht.1)
+
+
+theorem CauchyRiemann'₅
   {f : ℂ → F}
-  {z : ℂ} :
-  (DifferentiableAt ℂ f z) → partialDeriv ℝ Complex.I f z = Complex.I • partialDeriv ℝ 1 f z := by
-  intro h
+  {z : ℂ}
+  (h : DifferentiableAt ℂ f z) :
+  partialDeriv ℝ Complex.I f z = Complex.I • partialDeriv ℝ 1 f z := by
   unfold partialDeriv
 
   conv =>
@@ -53,11 +84,18 @@ theorem CauchyRiemann₅
     rw [DifferentiableAt.fderiv_restrictScalars ℝ h]
 
 
-theorem CauchyRiemann₆
-  {f : ℂ → ℂ}
-  {z : ℂ} :
-  (HolomorphicAt f z) → partialDeriv ℝ Complex.I f =ᶠ[nhds z] Complex.I • partialDeriv ℝ 1 f := by
+theorem CauchyRiemann'₆
+  {f : ℂ → F}
+  {z : ℂ}
+  (h : HolomorphicAt f z) :
+  partialDeriv ℝ Complex.I f =ᶠ[nhds z] Complex.I • partialDeriv ℝ 1 f := by
 
+  obtain ⟨s, h₁s, hz, h₂f⟩ := HolomorphicAt_iff.1 h
 
-
-  sorry
+  apply Filter.eventuallyEq_iff_exists_mem.2
+  use s
+  constructor
+  · exact IsOpen.mem_nhds h₁s hz
+  · intro w hw
+    apply CauchyRiemann'₅
+    exact h₂f w hw

Nevanlinna/partialDeriv.lean

@@ -16,7 +16,11 @@ noncomputable def partialDeriv : E → (E → F) → (E → F) :=
   fun v ↦ (fun f ↦ (fun w ↦ fderiv 𝕜 f w v))
 
 
-theorem partialDeriv_eventuallyEq' {f₁ f₂ : E → F} {x : E} (h : f₁ =ᶠ[nhds x] f₂) : ∀ v : E, partialDeriv 𝕜 v f₁ =ᶠ[nhds x] partialDeriv 𝕜 v f₂ := by
+theorem partialDeriv_eventuallyEq'
+  {f₁ f₂ : E → F}
+  {x : E}
+  (h : f₁ =ᶠ[nhds x] f₂) :
+  ∀ v : E, partialDeriv 𝕜 v f₁ =ᶠ[nhds x] partialDeriv 𝕜 v f₂ := by
   unfold partialDeriv
   intro v
   apply Filter.EventuallyEq.comp₂