done for today

Nevanlinna/cauchyRiemann.lean

@@ -62,3 +62,21 @@ theorem CauchyRiemann₄ {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F]
     right
     intro w
     rw [DifferentiableAt.fderiv_restrictScalars ℝ (h w)]
+
+
+theorem CauchyRiemann₅ {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] {f : ℂ → F} {z : ℂ} : (DifferentiableAt ℂ f z)
+  → partialDeriv ℝ Complex.I f z = Complex.I • partialDeriv ℝ 1 f z := by
+  intro h
+  unfold partialDeriv
+
+  conv =>
+    left
+    rw [DifferentiableAt.fderiv_restrictScalars ℝ h]
+    simp
+    rw [← mul_one Complex.I]
+    rw [← smul_eq_mul]
+    rw [ContinuousLinearMap.map_smul_of_tower (fderiv ℂ f z) Complex.I 1]
+  conv =>
+    right
+    right
+    rw [DifferentiableAt.fderiv_restrictScalars ℝ h]

Nevanlinna/complexHarmonic.lean

@@ -102,10 +102,9 @@ theorem harmonicOn_add_harmonicOn_is_harmonicOn {f₁ f₂ : ℂ → F} {s : Set
   HarmonicOn (f₁ + f₂) s := by
   constructor
   · exact ContDiffOn.add h₁.1 h₂.1
-  · rw [laplace_add h₁.1 h₂.1]
-    simp
-    intro z
-    rw [h₁.2 z, h₂.2 z]
+  · intro z hz
+    rw [laplace_add_ContDiffOn hs h₁.1 h₂.1 z hz]
+    rw [h₁.2 z hz, h₂.2 z hz]
     simp
 
 
@@ -177,6 +176,21 @@ theorem harmonic_iff_comp_CLE_is_harmonic {f : ℂ → F₁} {l : F₁ ≃L[ℝ]
     exact harmonic_comp_CLM_is_harmonic
 
 
+theorem harmonicOn_iff_comp_CLE_is_harmonicOn {f : ℂ → F₁} {s : Set ℂ} {l : F₁ ≃L[ℝ] G₁} (hs : IsOpen s) :
+  HarmonicOn f s ↔ HarmonicOn (l ∘ f) s := by
+
+  constructor
+  · have : l ∘ f = (l : F₁ →L[ℝ] G₁) ∘ f := by rfl
+    rw [this]
+    exact harmonicOn_comp_CLM_is_harmonicOn hs
+  · have : f = (l.symm : G₁ →L[ℝ] F₁) ∘ l ∘ f := by
+      funext z
+      unfold Function.comp
+      simp
+    nth_rewrite 2 [this]
+    exact harmonicOn_comp_CLM_is_harmonicOn hs
+
+
 theorem holomorphic_is_harmonic {f : ℂ → F₁} (h : Differentiable ℂ f) :
   Harmonic f := by
 
@@ -233,6 +247,71 @@ theorem holomorphic_is_harmonic {f : ℂ → F₁} (h : Differentiable ℂ f) :
     exact fI_is_real_differentiable
 
 
+theorem holomorphicOn_is_harmonicOn {f : ℂ → F₁} {s : Set ℂ} (hs : IsOpen s) (h : DifferentiableOn ℂ f s) :
+  HarmonicOn f s := by
+
+  -- f is real C²
+  have f_is_real_C2 : ContDiffOn ℝ 2 f s :=
+    ContDiffOn.restrict_scalars ℝ (DifferentiableOn.contDiffOn h hs)
+
+  have fI_is_real_differentiable : DifferentiableOn ℝ (partialDeriv ℝ 1 f) s := by
+    intro z hz
+    apply DifferentiableAt.differentiableWithinAt
+    let ZZ := (f_is_real_C2 z hz).contDiffAt (IsOpen.mem_nhds hs hz)
+    let AA := partialDeriv_contDiffAt ℝ ZZ 1
+    exact AA.differentiableAt (by rfl)
+
+  constructor
+  · -- f is two times real continuously differentiable
+    exact f_is_real_C2
+
+  · -- Laplace of f is zero
+    unfold Complex.laplace
+    intro z hz
+    simp
+    have : DifferentiableAt ℂ f z := by
+      sorry
+    let ZZ := h z hz
+    rw [CauchyRiemann₅ this]
+
+    -- This lemma says that partial derivatives commute with complex scalar
+    -- multiplication. This is a consequence of partialDeriv_compContLin once we
+    -- note that complex scalar multiplication is continuous ℝ-linear.
+    have : ∀ v, ∀ s : ℂ, ∀ g : ℂ → F₁, Differentiable ℝ g → partialDeriv ℝ v (s • g) = s • (partialDeriv ℝ v g) := by
+      intro v s g hg
+
+      -- Present scalar multiplication as a continuous ℝ-linear map. This is
+      -- horrible, there must be better ways to do that.
+      let sMuls : F₁ →L[ℝ] F₁ :=
+      {
+        toFun := fun x ↦ s • x
+        map_add' := by exact fun x y => DistribSMul.smul_add s x y
+        map_smul' := by exact fun m x => (smul_comm ((RingHom.id ℝ) m) s x).symm
+        cont := continuous_const_smul s
+      }
+
+      -- Bring the goal into a form that is recognized by
+      -- partialDeriv_compContLin.
+      have : s • g = sMuls ∘ g := by rfl
+      rw [this]
+
+      rw [partialDeriv_compContLin ℝ hg]
+      rfl
+
+    rw [this]
+    rw [partialDeriv_comm f_is_real_C2 Complex.I 1]
+    rw [CauchyRiemann₄ h]
+    rw [this]
+    rw [← smul_assoc]
+    simp
+
+    -- Subgoals coming from the application of 'this'
+    -- Differentiable ℝ (Real.partialDeriv 1 f)
+    exact fI_is_real_differentiable
+    -- Differentiable ℝ (Real.partialDeriv 1 f)
+    exact fI_is_real_differentiable
+
+
 theorem re_of_holomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f) :
   Harmonic (Complex.reCLM ∘ f) := by
   apply harmonic_comp_CLM_is_harmonic
@@ -298,24 +377,29 @@ theorem log_normSq_of_holomorphicOn_is_harmonicOn
   rw [HarmonicOn_congr hs this]
   simp
 
-  apply harmonic_add_harmonic_is_harmonic
-  have : Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f = Complex.conjCLE ∘ Complex.log ∘ f := by
-    funext z
+  apply harmonicOn_add_harmonicOn_is_harmonicOn
+  exact hs
+  have : (fun x => Complex.log ((starRingEnd ℂ) (f x))) = (Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f) := by
+    rfl
+  rw [this]
+  have : ∀ z ∈ s, (Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f) z = (Complex.conjCLE ∘ Complex.log ∘ f) z := by
+    intro z hz
     unfold Function.comp
     rw [Complex.log_conj]
     rfl
-    exact Complex.slitPlane_arg_ne_pi (h₃ z)
-  rw [this]
-  rw [← harmonic_iff_comp_CLE_is_harmonic]
+    exact Complex.slitPlane_arg_ne_pi (h₃ z hz)
+  rw [HarmonicOn_congr hs this]
 
-  repeat
-    apply holomorphic_is_harmonic
+  rw [← harmonicOn_iff_comp_CLE_is_harmonicOn]
+
+  apply holomorphicOn_is_harmonicOn
   intro z
   apply DifferentiableAt.comp
   exact Complex.differentiableAt_log (h₃ z)
   exact h₁ z
 
 
+
 theorem log_normSq_of_holomorphic_is_harmonic
   {f : ℂ → ℂ}
   (h₁ : Differentiable ℂ f)

Nevanlinna/laplace.lean

@@ -53,35 +53,45 @@ theorem laplace_add {f₁ f₂ : ℂ → F} (h₁ : ContDiff ℝ 2 f₁) (h₂ :
   exact h₂.differentiable one_le_two
 
 
-theorem laplace_add_ContDiffOn {f₁ f₂ : ℂ → F} {s : Set ℂ} (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
+theorem laplace_add_ContDiffOn
+  {f₁ f₂ : ℂ → F}
+  {s : Set ℂ}
+  (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
 
   unfold Complex.laplace
   simp
   intro x hx
+
   have : partialDeriv ℝ 1 (f₁ + f₂) =ᶠ[nhds x] (partialDeriv ℝ 1 f₁) + (partialDeriv ℝ 1 f₂) := by
     sorry
   rw [partialDeriv_eventuallyEq ℝ this]
+  have t₁ : DifferentiableAt ℝ (partialDeriv ℝ 1 f₁) x := by
+    sorry
+  have t₂ : DifferentiableAt ℝ (partialDeriv ℝ 1 f₂) x := by
+    sorry
+  rw [partialDeriv_add₂_differentiableAt ℝ t₁ t₂]
 
+  have : partialDeriv ℝ Complex.I (f₁ + f₂) =ᶠ[nhds x] (partialDeriv ℝ Complex.I f₁) + (partialDeriv ℝ Complex.I f₂) := by
+    sorry
+  rw [partialDeriv_eventuallyEq ℝ this]
+  have t₃ : DifferentiableAt ℝ (partialDeriv ℝ Complex.I f₁) x := by
+    sorry
+  have t₄ : DifferentiableAt ℝ (partialDeriv ℝ Complex.I f₂) x := by
+    sorry
+  rw [partialDeriv_add₂_differentiableAt ℝ t₃ t₄]
 
-  rw [partialDeriv_add₂]
-
-  rw [partialDeriv_add₂]
-  rw [partialDeriv_add₂]
-  rw [partialDeriv_add₂]
-  exact
-    add_add_add_comm (partialDeriv ℝ 1 (partialDeriv ℝ 1 f₁))
-      (partialDeriv ℝ 1 (partialDeriv ℝ 1 f₂))
-      (partialDeriv ℝ Complex.I (partialDeriv ℝ Complex.I f₁))
-      (partialDeriv ℝ Complex.I (partialDeriv ℝ Complex.I f₂))
-
-  exact (partialDeriv_contDiff ℝ h₁ Complex.I).differentiable le_rfl
-  exact (partialDeriv_contDiff ℝ h₂ Complex.I).differentiable le_rfl
-  exact h₁.differentiable one_le_two
-  exact h₂.differentiable one_le_two
-  exact (partialDeriv_contDiff ℝ h₁ 1).differentiable le_rfl
-  exact (partialDeriv_contDiff ℝ h₂ 1).differentiable le_rfl
-  exact h₁.differentiable one_le_two
-  exact h₂.differentiable one_le_two
+  -- I am super confused at this point because the tactic 'ring' does not work.
+  -- I do not understand why. So, I need to do things by hand.
+  rw [add_assoc]
+  rw [add_assoc]
+  rw [add_right_inj (partialDeriv ℝ 1 (partialDeriv ℝ 1 f₁) x)]
+  rw [add_comm]
+  rw [add_assoc]
+  rw [add_right_inj (partialDeriv ℝ Complex.I (partialDeriv ℝ Complex.I f₁) x)]
+  rw [add_comm]
 
 
 theorem laplace_smul {f : ℂ → F} (h : ContDiff ℝ 2 f) : ∀ v : ℝ, Complex.laplace (v • f) = v • (Complex.laplace f) := by

Nevanlinna/partialDeriv.lean

@@ -54,6 +54,22 @@ theorem partialDeriv_add₂ {f₁ f₂ : E → F} {v : E} (h₁ : Differentiable
     rw [fderiv_add (h₁ w) (h₂ w)]
 
 
+theorem partialDeriv_add₂_differentiableAt
+  {f₁ f₂ : E → F}
+  {v : E}
+  {x : E}
+  (h₁ : DifferentiableAt 𝕜 f₁ x)
+  (h₂ : DifferentiableAt 𝕜 f₂ x)
+  :
+  partialDeriv 𝕜 v (f₁ + f₂) x = (partialDeriv 𝕜 v f₁) x + (partialDeriv 𝕜 v f₂) x := by
+
+  unfold partialDeriv
+  have : f₁ + f₂ = fun y ↦ f₁ y + f₂ y := by rfl
+  rw [this]
+  rw [fderiv_add h₁ h₂]
+  rfl
+
+
 theorem partialDeriv_compContLin {f : E → F} {l : F →L[𝕜] G} {v : E} (h : Differentiable 𝕜 f) : partialDeriv 𝕜 v (l ∘ f) = l ∘ partialDeriv 𝕜 v f := by
   unfold partialDeriv