Nevanlinna/cauchyRiemann.lean

@@ -62,21 +62,3 @@ 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

@@ -53,13 +53,13 @@ theorem HarmonicOn_congr {f₁ f₂ : ℂ → F} {s : Set ℂ} (hs : IsOpen s) (
       rw [eq_comm]
       exact hf₁₂ x hx
     · intro z hz
-      have : f₁ =ᶠ[nhds z] f₂ := by
+      have : f₁ =ᶠ[nhds z] f₂ := by 
         unfold Filter.EventuallyEq
         unfold Filter.Eventually
         simp
         refine mem_nhds_iff.mpr ?_
         use s
-        constructor
+        constructor 
         · exact hf₁₂
         · constructor
           · exact hs
@@ -72,13 +72,13 @@ theorem HarmonicOn_congr {f₁ f₂ : ℂ → F} {s : Set ℂ} (hs : IsOpen s) (
       intro x hx
       exact hf₁₂ x hx
     · intro z hz
-      have : f₁ =ᶠ[nhds z] f₂ := by
+      have : f₁ =ᶠ[nhds z] f₂ := by 
         unfold Filter.EventuallyEq
         unfold Filter.Eventually
         simp
         refine mem_nhds_iff.mpr ?_
         use s
-        constructor
+        constructor 
         · exact hf₁₂
         · constructor
           · exact hs
@@ -102,9 +102,10 @@ theorem harmonicOn_add_harmonicOn_is_harmonicOn {f₁ f₂ : ℂ → F} {s : Set
   HarmonicOn (f₁ + f₂) s := by
   constructor
   · exact ContDiffOn.add h₁.1 h₂.1
-  · intro z hz
-    rw [laplace_add_ContDiffOn hs h₁.1 h₂.1 z hz]
-    rw [h₁.2 z hz, h₂.2 z hz]
+  · rw [laplace_add h₁.1 h₂.1]
+    simp
+    intro z
+    rw [h₁.2 z, h₂.2 z]
     simp
 
 
@@ -176,21 +177,6 @@ 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
 
@@ -247,71 +233,6 @@ 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
@@ -373,31 +294,26 @@ theorem log_normSq_of_holomorphicOn_is_harmonicOn
     · exact Real.pi_nonneg
     exact (AddEquivClass.map_ne_zero_iff starRingAut).mpr (h₂ z hz)
     exact h₂ z hz
-
+  
   rw [HarmonicOn_congr hs this]
   simp
 
-  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
+  apply harmonic_add_harmonic_is_harmonic
+  have : 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 hz)
-  rw [HarmonicOn_congr hs this]
-
-  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
+    exact Complex.slitPlane_arg_ne_pi (h₃ z)
+  rw [this]
+  rw [← harmonic_iff_comp_CLE_is_harmonic]
 
+  repeat
+    apply holomorphic_is_harmonic
+    intro z
+    apply DifferentiableAt.comp
+    exact Complex.differentiableAt_log (h₃ z)
+    exact h₁ z
 
 
 theorem log_normSq_of_holomorphic_is_harmonic

Nevanlinna/laplace.lean

@@ -53,45 +53,35 @@ 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₂]
 
-  -- 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]
+  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
 
 
 theorem laplace_smul {f : ℂ → F} (h : ContDiff ℝ 2 f) : ∀ v : ℝ, Complex.laplace (v • f) = v • (Complex.laplace f) := by
@@ -129,7 +119,7 @@ theorem laplace_compContLinAt {f : ℂ → F} {l : F →L[ℝ] G} {x : ℂ} (h :
 
   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
+      apply ContDiffAt.contDiffOn h 
       rfl
     obtain ⟨u, hu₁, hu₂⟩ := this
     obtain ⟨v, hv₁, hv₂, hv₃⟩ := mem_nhds_iff.1 hu₁
@@ -140,7 +130,7 @@ theorem laplace_compContLinAt {f : ℂ → F} {l : F →L[ℝ] G} {x : ℂ} (h :
       exact hv₂
       constructor
       · exact hv₃
-      · exact ContDiffOn.congr_mono hu₂ (fun x => congrFun rfl) 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

Nevanlinna/partialDeriv.lean

@@ -54,22 +54,6 @@ 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
 
@@ -111,7 +95,7 @@ theorem partialDeriv_contDiffAt {n : ℕ} {f : E → F} {x : E} (h : ContDiffAt
   unfold partialDeriv
   intro v
 
-  let eval_at_v : (E →L[𝕜] F) →L[𝕜] F :=
+  let eval_at_v : (E →L[𝕜] F) →L[𝕜] F := 
   {
     toFun := fun l ↦ l v
     map_add' := by simp
@@ -148,7 +132,7 @@ theorem partialDeriv_eventuallyEq' {f₁ f₂ : E → F} {x : E} (h : f₁ =ᶠ[
   unfold partialDeriv
   intro v
   let A : fderiv 𝕜 f₁ =ᶠ[nhds x] fderiv 𝕜 f₂ := Filter.EventuallyEq.fderiv h
-  apply Filter.EventuallyEq.comp₂
+  apply Filter.EventuallyEq.comp₂ 
   exact A
   simp