Working…

Nevanlinna/cauchyRiemann.lean

@@ -44,8 +44,10 @@ theorem CauchyRiemann₃ : (DifferentiableAt ℂ f z)
   simp
 
 
-theorem CauchyRiemann₄ {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] {f : ℂ → F} : (Differentiable ℂ f)
-  → partialDeriv ℝ Complex.I f = Complex.I • partialDeriv ℝ 1 f := by
+theorem CauchyRiemann₄
+  {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] 
+  {f : ℂ → F} : 
+  (Differentiable ℂ f) → partialDeriv ℝ Complex.I f = Complex.I • partialDeriv ℝ 1 f := by
   intro h
   unfold partialDeriv
 
@@ -62,3 +64,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

@@ -1,20 +1,4 @@
-import Mathlib.Analysis.Complex.Basic
-import Mathlib.Analysis.Complex.TaylorSeries
-import Mathlib.Analysis.Calculus.LineDeriv.Basic
-import Mathlib.Analysis.Calculus.ContDiff.Defs
-import Mathlib.Analysis.Calculus.FDeriv.Basic
-import Mathlib.Analysis.Calculus.FDeriv.Symmetric
-import Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
-import Mathlib.Data.Complex.Module
-import Mathlib.Data.Complex.Order
-import Mathlib.Data.Complex.Exponential
-import Mathlib.Data.Fin.Tuple.Basic
-import Mathlib.Analysis.RCLike.Basic
-import Mathlib.Topology.Algebra.InfiniteSum.Module
-import Mathlib.Topology.Instances.RealVectorSpace
-import Nevanlinna.cauchyRiemann
 import Nevanlinna.laplace
-import Nevanlinna.partialDeriv
 
 variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
 variable {F₁ : Type*} [NormedAddCommGroup F₁] [NormedSpace ℂ F₁] [CompleteSpace F₁]
@@ -23,11 +7,57 @@ 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 HarmonicAt (f : ℂ → F) (x : ℂ) : Prop :=
+  (ContDiffAt ℝ 2 f x) ∧ (Δ f =ᶠ[nhds x] 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 HarmonicAt_iff
+  {f : ℂ → F}
+  {x : ℂ} :
+  HarmonicAt f x ↔ ∃ s : Set ℂ, IsOpen s ∧ x ∈ s ∧ (ContDiffOn ℝ 2 f s) ∧ (∀ z ∈ s, Δ f z = 0) := by
+  constructor
+  · intro hf
+    obtain ⟨s₁, h₁s₁, h₂s₁, h₃s₁⟩ := hf.1.contDiffOn' le_rfl
+    simp at h₃s₁
+    obtain ⟨t₂, h₁t₂, h₂t₂⟩ := (Filter.eventuallyEq_iff_exists_mem.1 hf.2)
+    obtain ⟨s₂, h₁s₂, h₂s₂, h₃s₂⟩ := mem_nhds_iff.1 h₁t₂
+    let s := s₁ ∩ s₂
+    use s
+    constructor
+    · exact IsOpen.inter h₁s₁ h₂s₂
+    · constructor
+      · exact Set.mem_inter h₂s₁ h₃s₂
+      · constructor
+        · exact h₃s₁.mono (Set.inter_subset_left s₁ s₂)
+        · intro z hz
+          exact h₂t₂ (h₁s₂ hz.2)
+  · intro hyp
+    obtain ⟨s, h₁s, h₂s, h₁f, h₂f⟩ := hyp
+    constructor
+    · apply h₁f.contDiffAt
+      apply (IsOpen.mem_nhds_iff h₁s).2 h₂s
+    · apply Filter.eventuallyEq_iff_exists_mem.2
+      use s
+      constructor
+      · apply (IsOpen.mem_nhds_iff h₁s).2 h₂s
+      · exact h₂f
+
+
+theorem HarmonicAt_eventuallyEq {f₁ f₂ : ℂ → F} {x : ℂ} (h : f₁ =ᶠ[nhds x] f₂) : HarmonicAt f₁ x ↔ HarmonicAt f₂ x := by
+  constructor
+  · intro h₁
+    constructor
+    · exact ContDiffAt.congr_of_eventuallyEq h₁.1 (Filter.EventuallyEq.symm h)
+    · exact Filter.EventuallyEq.trans (laplace_eventuallyEq' (Filter.EventuallyEq.symm h)) h₁.2
+  · intro h₁
+    constructor
+    · exact ContDiffAt.congr_of_eventuallyEq h₁.1 h
+    · exact Filter.EventuallyEq.trans (laplace_eventuallyEq' h) h₁.2
 
 
 theorem HarmonicOn_of_locally_HarmonicOn {f : ℂ → F} {s : Set ℂ} (h : ∀ x ∈ s, ∃ (u : Set ℂ), IsOpen u ∧ x ∈ u ∧ HarmonicOn f (s ∩ u)) :
@@ -43,6 +73,50 @@ theorem HarmonicOn_of_locally_HarmonicOn {f : ℂ → F} {s : Set ℂ} (h : ∀
     exact (uHyp.2.2.2) x ⟨xHyp, uHyp.2.1⟩
 
 
+theorem HarmonicOn_congr {f₁ f₂ : ℂ → F} {s : Set ℂ} (hs : IsOpen s) (hf₁₂ : ∀ x ∈ s, f₁ x = f₂ x) :
+  HarmonicOn f₁ s ↔ HarmonicOn f₂ s := by
+  constructor
+  · intro h₁
+    constructor
+    · apply ContDiffOn.congr h₁.1
+      intro x hx
+      rw [eq_comm]
+      exact hf₁₂ x hx
+    · intro z hz
+      have : f₁ =ᶠ[nhds z] f₂ := by
+        unfold Filter.EventuallyEq
+        unfold Filter.Eventually
+        simp
+        refine mem_nhds_iff.mpr ?_
+        use s
+        constructor
+        · exact hf₁₂
+        · constructor
+          · exact hs
+          · exact hz
+      rw [← laplace_eventuallyEq this]
+      exact h₁.2 z hz
+  · intro h₁
+    constructor
+    · apply ContDiffOn.congr h₁.1
+      intro x hx
+      exact hf₁₂ x hx
+    · intro z hz
+      have : f₁ =ᶠ[nhds z] f₂ := by
+        unfold Filter.EventuallyEq
+        unfold Filter.Eventually
+        simp
+        refine mem_nhds_iff.mpr ?_
+        use s
+        constructor
+        · exact hf₁₂
+        · constructor
+          · exact hs
+          · exact hz
+      rw [laplace_eventuallyEq this]
+      exact h₁.2 z hz
+
+
 theorem harmonic_add_harmonic_is_harmonic {f₁ f₂ : ℂ → F} (h₁ : Harmonic f₁) (h₂ : Harmonic f₂) :
   Harmonic (f₁ + f₂) := by
   constructor
@@ -54,17 +128,55 @@ theorem harmonic_add_harmonic_is_harmonic {f₁ f₂ : ℂ → F} (h₁ : Harmon
     simp
 
 
+theorem harmonicOn_add_harmonicOn_is_harmonicOn {f₁ f₂ : ℂ → F} {s : Set ℂ} (hs : IsOpen s) (h₁ : HarmonicOn f₁ s) (h₂ : HarmonicOn f₂ s) :
+  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]
+    simp
+
+
+theorem harmonicAt_add_harmonicAt_is_harmonicAt
+  {f₁ f₂ : ℂ → F}
+  {x : ℂ}
+  (h₁ : HarmonicAt f₁ x)
+  (h₂ : HarmonicAt f₂ x) :
+  HarmonicAt (f₁ + f₂) x := by
+  constructor
+  · exact ContDiffAt.add h₁.1 h₂.1
+  · apply Filter.EventuallyEq.trans (laplace_add_ContDiffAt' h₁.1 h₂.1)
+    apply Filter.EventuallyEq.trans (Filter.EventuallyEq.add h₁.2 h₂.2)
+    simp
+    rfl
+
+
 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]
+  · rw [laplace_smul]
     dsimp
     intro z
     rw [h.2 z]
     simp
 
 
+theorem harmonicAt_smul_const_is_harmonicAt
+  {f : ℂ → F}
+  {x : ℂ}
+  {c : ℝ}
+  (h : HarmonicAt f x) :
+  HarmonicAt (c • f) x := by
+  constructor
+  · exact ContDiffAt.const_smul c h.1
+  · rw [laplace_smul]
+    have A := Filter.EventuallyEq.const_smul h.2 c
+    simp at A
+    assumption
+
+
 theorem harmonic_iff_smul_const_is_harmonic {f : ℂ → F} {c : ℝ} (hc : c ≠ 0) :
   Harmonic f ↔ Harmonic (c • f) := by
   constructor
@@ -73,6 +185,18 @@ theorem harmonic_iff_smul_const_is_harmonic {f : ℂ → F} {c : ℝ} (hc : c
     exact fun a => harmonic_smul_const_is_harmonic a
 
 
+theorem harmonicAt_iff_smul_const_is_harmonicAt
+  {f : ℂ → F}
+  {x : ℂ}
+  {c : ℝ}
+  (hc : c ≠ 0) :
+  HarmonicAt f x ↔ HarmonicAt (c • f) x := by
+  constructor
+  · exact harmonicAt_smul_const_is_harmonicAt
+  · nth_rewrite 2 [((eq_inv_smul_iff₀ hc).mpr rfl : f = c⁻¹ • c • f)]
+    exact fun a => harmonicAt_smul_const_is_harmonicAt a
+
+
 theorem harmonic_comp_CLM_is_harmonic {f : ℂ → F₁} {l : F₁ →L[ℝ] G} (h : Harmonic f) :
   Harmonic (l ∘ f) := by
 
@@ -81,7 +205,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]
@@ -89,19 +213,55 @@ theorem harmonic_comp_CLM_is_harmonic {f : ℂ → F₁} {l : F₁ →L[ℝ] G}
     exact ContDiff.restrict_scalars ℝ h.1
 
 
-theorem harmonicOn_comp_CLM_is_harmonicOn {f : ℂ → F₁} {s : Set ℂ} {l : F₁ →L[ℝ] G} (h : HarmonicOn f s) :
+theorem harmonicOn_comp_CLM_is_harmonicOn {f : ℂ → F₁} {s : Set ℂ} {l : F₁ →L[ℝ] G} (hs : IsOpen s) (h : HarmonicOn f s) :
   HarmonicOn (l ∘ f) s := by
 
   constructor
   · -- Continuous differentiability
     apply ContDiffOn.continuousLinearMap_comp
     exact h.1
-  · rw [laplace_compContLin]
-    simp
+  · -- Vanishing of Laplace
     intro z zHyp
+    rw [laplace_compCLMAt]
+    simp
     rw [h.2 z]
     simp
     assumption
+    apply ContDiffOn.contDiffAt h.1
+    exact IsOpen.mem_nhds hs zHyp
+
+
+theorem harmonicAt_comp_CLM_is_harmonicAt
+  {f : ℂ → F₁}
+  {z : ℂ}
+  {l : F₁ →L[ℝ] G}
+  (h : HarmonicAt f z) :
+  HarmonicAt (l ∘ f) z := by
+
+  constructor
+  · -- ContDiffAt ℝ 2 (⇑l ∘ f) z
+    apply ContDiffAt.continuousLinearMap_comp
+    exact h.1
+  · -- Δ (⇑l ∘ f) =ᶠ[nhds z] 0
+    obtain ⟨r, h₁r, h₂r⟩ := h.1.contDiffOn le_rfl
+    obtain ⟨s, h₁s, h₂s, h₃s⟩ := mem_nhds_iff.1 h₁r
+    obtain ⟨t, h₁t, h₂t⟩ := Filter.eventuallyEq_iff_exists_mem.1 h.2
+    obtain ⟨u, h₁u, h₂u, h₃u⟩ := mem_nhds_iff.1 h₁t
+    apply Filter.eventuallyEq_iff_exists_mem.2
+    use s ∩ u
+    constructor
+    · apply IsOpen.mem_nhds
+      exact IsOpen.inter h₂s h₂u
+      constructor
+      · exact h₃s
+      · exact h₃u
+    · intro x xHyp
+      rw [laplace_compCLMAt]
+      simp
+      rw [h₂t]
+      simp
+      exact h₁u xHyp.2
+      apply (h₂r.mono h₁s).contDiffAt (IsOpen.mem_nhds h₂s xHyp.1)
 
 
 theorem harmonic_iff_comp_CLE_is_harmonic {f : ℂ → F₁} {l : F₁ ≃L[ℝ] G₁} :
@@ -119,222 +279,34 @@ theorem harmonic_iff_comp_CLE_is_harmonic {f : ℂ → F₁} {l : F₁ ≃L[ℝ]
     exact harmonic_comp_CLM_is_harmonic
 
 
-theorem holomorphic_is_harmonic {f : ℂ → F₁} (h : Differentiable ℂ f) :
-  Harmonic f := by
-
-  -- f is real C²
-  have f_is_real_C2 : ContDiff ℝ 2 f :=
-    ContDiff.restrict_scalars ℝ (Differentiable.contDiff h)
-
-  have fI_is_real_differentiable : Differentiable ℝ (partialDeriv ℝ 1 f) := by
-    exact (partialDeriv_contDiff ℝ f_is_real_C2 1).differentiable (Submonoid.oneLE.proof_2 ℕ∞)
+theorem harmonicAt_iff_comp_CLE_is_harmonicAt
+  {f : ℂ → F₁}
+  {z : ℂ}
+  {l : F₁ ≃L[ℝ] G₁} :
+  HarmonicAt f z ↔ HarmonicAt (l ∘ f) z := by
 
   constructor
-  · -- f is two times real continuously differentiable
-    exact f_is_real_C2
-
-  · -- Laplace of f is zero
-    unfold Complex.laplace
-    rw [CauchyRiemann₄ h]
-
-    -- 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
+  · have : l ∘ f = (l : F₁ →L[ℝ] G₁) ∘ f := 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
-  exact holomorphic_is_harmonic h
-
-
-theorem im_of_holomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f) :
-  Harmonic (Complex.imCLM ∘ f) := by
-  apply harmonic_comp_CLM_is_harmonic
-  exact holomorphic_is_harmonic h
-
-
-theorem antiholomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f) :
-  Harmonic (Complex.conjCLE ∘ f) := by
-  apply harmonic_iff_comp_CLE_is_harmonic.1
-  exact holomorphic_is_harmonic h
-
-
-theorem log_normSq_of_holomorphicOn_is_harmonicOn
-  {f : ℂ → ℂ}
-  {s : Set ℂ}
-  (h₁ : DifferentiableOn ℂ f s)
-  (h₂ : ∀ z ∈ s, f z ≠ 0)
-  (h₃ : ∀ z ∈ s, f z ∈ Complex.slitPlane) :
-  HarmonicOn (Real.log ∘ Complex.normSq ∘ f) s := by
-
-  suffices hyp : Harmonic (⇑Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ f) from
-    (harmonic_comp_CLM_is_harmonic hyp : Harmonic (Complex.reCLM ∘ Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ f))
-
-  suffices hyp : Harmonic (Complex.log ∘ (((starRingEnd ℂ) ∘ f) * f)) from by
-    have : Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ f = Complex.log ∘ (((starRingEnd ℂ) ∘ f) * f) := by
+    exact harmonicAt_comp_CLM_is_harmonicAt
+  · have : f = (l.symm : G₁ →L[ℝ] F₁) ∘ l ∘ f := by
       funext z
-      simp
-      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)
-  -- THIS IS WHERE WE USE h₃
-  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]
+    nth_rewrite 2 [this]
+    exact harmonicAt_comp_CLM_is_harmonicAt
+
+
+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
 
-    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
+  · have : l ∘ f = (l : F₁ →L[ℝ] G₁) ∘ f := by rfl
     rw [this]
-
-  apply harmonic_add_harmonic_is_harmonic
-  have : Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f = Complex.conjCLE ∘ Complex.log ∘ f := by
+    exact harmonicOn_comp_CLM_is_harmonicOn hs
+  · have : f = (l.symm : G₁ →L[ℝ] F₁) ∘ l ∘ f := by
       funext z
       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]
-
-  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
-  {f : ℂ → ℂ}
-  (h₁ : Differentiable ℂ f)
-  (h₂ : ∀ z, f z ≠ 0)
-  (h₃ : ∀ z, f z ∈ Complex.slitPlane) :
-  Harmonic (Real.log ∘ Complex.normSq ∘ f) := by
-
-  suffices hyp : Harmonic (⇑Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ f) from
-    (harmonic_comp_CLM_is_harmonic hyp : Harmonic (Complex.reCLM ∘ Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ f))
-
-  suffices hyp : Harmonic (Complex.log ∘ (((starRingEnd ℂ) ∘ f) * f)) from by
-    have : Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ f = Complex.log ∘ (((starRingEnd ℂ) ∘ f) * f) := by
-      funext z
       simp
-      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)
-  -- THIS IS WHERE WE USE h₃
-  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]
-
-  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)
-  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 logabs_of_holomorphic_is_harmonic
-  {f : ℂ → ℂ}
-  (h₁ : Differentiable ℂ f)
-  (h₂ : ∀ z, f z ≠ 0)
-  (h₃ : ∀ z, f z ∈ Complex.slitPlane) :
-  Harmonic (fun z ↦ Real.log ‖f z‖) := by
-
-  -- Suffices: Harmonic (2⁻¹ • Real.log ∘ ⇑Complex.normSq ∘ f)
-  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]
-
-  -- Suffices: Harmonic (Real.log ∘ ⇑Complex.normSq ∘ f)
-  apply (harmonic_iff_smul_const_is_harmonic (inv_ne_zero two_ne_zero)).1
-
-  exact log_normSq_of_holomorphic_is_harmonic h₁ h₂ h₃
+    nth_rewrite 2 [this]
+    exact harmonicOn_comp_CLM_is_harmonicOn hs

Nevanlinna/harmonicAt.examples.lean

@@ -0,0 +1,211 @@
+import Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
+import Nevanlinna.complexHarmonic
+import Nevanlinna.holomorphicAt
+
+variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F]
+
+
+theorem holomorphicAt_is_harmonicAt
+  {f : ℂ → F}
+  {z : ℂ}
+  (hf : HolomorphicAt f z) :
+  HarmonicAt f z := by
+
+  let t := {x | HolomorphicAt f x}
+  have ht : IsOpen t := HolomorphicAt_isOpen f
+  have hz : z ∈ t := by exact hf
+
+  constructor
+  · -- ContDiffAt ℝ 2 f z
+    exact hf.contDiffAt
+
+  · -- Δ f =ᶠ[nhds z] 0
+    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 ℝ hw.CauchyRiemannAt Complex.I]
+      rw [partialDeriv_smul'₂]
+      simp
+
+      rw [partialDeriv_commAt hw.contDiffAt Complex.I 1]
+      rw [partialDeriv_eventuallyEq ℝ hw.CauchyRiemannAt 1]
+      rw [partialDeriv_smul'₂]
+      simp
+
+      rw [← smul_assoc]
+      simp
+
+
+theorem re_of_holomorphicAt_is_harmonicAr
+  {f : ℂ → ℂ}
+  {z : ℂ}
+  (h : HolomorphicAt f z) :
+  HarmonicAt (Complex.reCLM ∘ f) z := by
+  apply harmonicAt_comp_CLM_is_harmonicAt
+  exact holomorphicAt_is_harmonicAt h
+
+
+theorem im_of_holomorphicAt_is_harmonicAt
+  {f : ℂ → ℂ}
+  {z : ℂ}
+  (h : HolomorphicAt f z) :
+  HarmonicAt (Complex.imCLM ∘ f) z := by
+  apply harmonicAt_comp_CLM_is_harmonicAt
+  exact holomorphicAt_is_harmonicAt h
+
+
+theorem antiholomorphicAt_is_harmonicAt
+  {f : ℂ → ℂ}
+  {z : ℂ}
+  (h : HolomorphicAt f z) :
+  HarmonicAt (Complex.conjCLE ∘ f) z := by
+  apply harmonicAt_iff_comp_CLE_is_harmonicAt.1
+  exact holomorphicAt_is_harmonicAt h
+
+
+theorem log_normSq_of_holomorphicAt_is_harmonicAt
+  {f : ℂ → ℂ}
+  {z : ℂ}
+  (h₁f : HolomorphicAt f z)
+  (h₂f : f z ≠ 0) :
+  HarmonicAt (Real.log ∘ Complex.normSq ∘ f) z := by
+
+  -- For later use
+  have slitPlaneLemma {z : ℂ} (hz : z ≠ 0) : z ∈ Complex.slitPlane ∨ -z ∈ Complex.slitPlane := by
+    rw [Complex.mem_slitPlane_iff, 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
+
+  -- First prove the theorem for functions with image in the slitPlane
+  have lem₁ : ∀ g : ℂ → ℂ, (HolomorphicAt g z) → (g z ≠ 0) → (g z ∈ Complex.slitPlane) → HarmonicAt (Real.log ∘ Complex.normSq ∘ g) z := by
+    intro g h₁g h₂g h₃g
+
+    -- Rewrite the log |g|² as Complex.log (g * gc)
+    suffices hyp : HarmonicAt (Complex.log ∘ ((Complex.conjCLE ∘ g) * g)) z from by
+      have : Real.log ∘ Complex.normSq ∘ g = Complex.reCLM ∘ Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ g := by
+        funext x
+        simp
+      rw [this]
+
+      have : Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ g = Complex.log ∘ ((Complex.conjCLE ∘ g) * g) := by
+        funext x
+        simp
+        rw [Complex.ofReal_log]
+        rw [Complex.normSq_eq_conj_mul_self]
+        exact Complex.normSq_nonneg (g x)
+      rw [← this] at hyp
+      apply harmonicAt_comp_CLM_is_harmonicAt hyp
+
+    -- Locally around z, rewrite Complex.log (g * gc) as Complex.log g + Complex.log.gc
+    -- This uses the assumption that g z is in Complex.slitPlane
+    have : (Complex.log ∘ (Complex.conjCLE ∘ g * g)) =ᶠ[nhds z] (Complex.log ∘ Complex.conjCLE ∘ g + Complex.log ∘ g) := by
+      apply Filter.eventuallyEq_iff_exists_mem.2
+      use g⁻¹' (Complex.slitPlane ∩ {0}ᶜ)
+      constructor
+      · apply ContinuousAt.preimage_mem_nhds
+        · exact h₁g.differentiableAt.continuousAt
+        · apply IsOpen.mem_nhds
+          apply IsOpen.inter Complex.isOpen_slitPlane isOpen_ne
+          constructor
+          · exact h₃g
+          · exact h₂g
+      · intro x hx
+        simp
+        rw [Complex.log_mul_eq_add_log_iff _ hx.2]
+        rw [Complex.arg_conj]
+        simp [Complex.slitPlane_arg_ne_pi hx.1]
+        constructor
+        · exact Real.pi_pos
+        · exact Real.pi_nonneg
+        simp
+        apply hx.2
+
+    -- Locally around z, rewrite Complex.log (g * gc) as Complex.log g + Complex.log.gc
+    -- This uses the assumption that g z is in Complex.slitPlane
+    have : (Complex.log ∘ (Complex.conjCLE ∘ g * g)) =ᶠ[nhds z] (Complex.conjCLE ∘ Complex.log ∘ g + Complex.log ∘ g) := by
+      apply Filter.eventuallyEq_iff_exists_mem.2
+      use g⁻¹' (Complex.slitPlane ∩ {0}ᶜ)
+      constructor
+      · apply ContinuousAt.preimage_mem_nhds
+        · exact h₁g.differentiableAt.continuousAt
+        · apply IsOpen.mem_nhds
+          apply IsOpen.inter Complex.isOpen_slitPlane isOpen_ne
+          constructor
+          · exact h₃g
+          · exact h₂g
+      · intro x hx
+        simp
+        rw [← Complex.log_conj]
+        rw [Complex.log_mul_eq_add_log_iff _ hx.2]
+        rw [Complex.arg_conj]
+        simp [Complex.slitPlane_arg_ne_pi hx.1]
+        constructor
+        · exact Real.pi_pos
+        · exact Real.pi_nonneg
+        simp
+        apply hx.2
+        apply Complex.slitPlane_arg_ne_pi hx.1
+
+    rw [HarmonicAt_eventuallyEq this]
+    apply harmonicAt_add_harmonicAt_is_harmonicAt
+    · rw [← harmonicAt_iff_comp_CLE_is_harmonicAt]
+      apply holomorphicAt_is_harmonicAt
+      apply HolomorphicAt_comp
+      use Complex.slitPlane
+      constructor
+      · apply IsOpen.mem_nhds
+        exact Complex.isOpen_slitPlane
+        assumption
+      · exact fun z a => Complex.differentiableAt_log a
+      exact h₁g
+    · apply holomorphicAt_is_harmonicAt
+      apply HolomorphicAt_comp
+      use Complex.slitPlane
+      constructor
+      · apply IsOpen.mem_nhds
+        exact Complex.isOpen_slitPlane
+        assumption
+      · exact fun z a => Complex.differentiableAt_log a
+      exact h₁g
+
+  by_cases h₃f : f z ∈ Complex.slitPlane
+  · exact lem₁ f h₁f h₂f h₃f
+  · have : Complex.normSq ∘ f = Complex.normSq ∘ (-f) := by funext; simp
+    rw [this]
+    apply lem₁ (-f)
+    · exact HolomorphicAt_neg h₁f
+    · simpa
+    · exact (slitPlaneLemma h₂f).resolve_left h₃f
+
+
+theorem logabs_of_holomorphicAt_is_harmonic
+  {f : ℂ → ℂ}
+  {z : ℂ}
+  (h₁f : HolomorphicAt f z)
+  (h₂f : f z ≠ 0) :
+  HarmonicAt (fun w ↦ Real.log ‖f w‖) z := by
+
+  -- Suffices: Harmonic (2⁻¹ • Real.log ∘ ⇑Complex.normSq ∘ f)
+  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]
+
+  -- Suffices: Harmonic (Real.log ∘ ⇑Complex.normSq ∘ f)
+  apply (harmonicAt_iff_smul_const_is_harmonicAt (inv_ne_zero two_ne_zero)).1
+  exact log_normSq_of_holomorphicAt_is_harmonicAt h₁f h₂f

Nevanlinna/holomorphic.lean

@@ -0,0 +1,161 @@
+import Mathlib.Analysis.Complex.TaylorSeries
+import Nevanlinna.cauchyRiemann
+
+variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]
+variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F]
+variable {G : Type*} [NormedAddCommGroup G] [NormedSpace ℂ G] [CompleteSpace G]
+
+def HolomorphicAt (f : E → F) (x : E) : Prop :=
+  ∃ s ∈ nhds x, ∀ z ∈ s, DifferentiableAt ℂ f z
+
+
+theorem HolomorphicAt_iff
+  {f : E → F}
+  {x : E} :
+  HolomorphicAt f x ↔ ∃ s :
+  Set E, IsOpen s ∧ x ∈ s ∧ (∀ z ∈ s, DifferentiableAt ℂ 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
+        exact h₂t z (h₁s hz)
+  · intro hyp
+    obtain ⟨s, h₁s, h₂s, hf⟩ := hyp
+    use s
+    constructor
+    · apply (IsOpen.mem_nhds_iff h₁s).2 h₂s
+    · assumption
+
+
+theorem HolomorphicAt_differentiableAt
+  {f : E → F}
+  {x : E} :
+  HolomorphicAt f x →  DifferentiableAt ℂ f x := by
+  intro hf
+  obtain ⟨s, _, h₂s, h₃s⟩ := HolomorphicAt_iff.1 hf
+  exact h₃s x h₂s
+
+
+theorem HolomorphicAt_isOpen
+  (f : E → F) :
+  IsOpen { x : E | HolomorphicAt f x } := by
+
+  rw [← subset_interior_iff_isOpen]
+  intro x hx
+  simp at hx
+  obtain ⟨s, h₁s, h₂s, h₃s⟩ := HolomorphicAt_iff.1 hx
+  use s
+  constructor
+  · simp
+    constructor
+    · exact h₁s
+    · intro x hx
+      simp
+      use s
+      constructor
+      · exact IsOpen.mem_nhds h₁s hx
+      · exact h₃s
+  · exact h₂s
+
+
+theorem HolomorphicAt_comp
+  {g : E → F}
+  {f : F → G}
+  {z : E}
+  (hf : HolomorphicAt f (g z))
+  (hg : HolomorphicAt g z) :
+  HolomorphicAt (f ∘ g) z := by
+  obtain ⟨UE, h₁UE, h₂UE⟩ := hg
+  obtain ⟨UF, h₁UF, h₂UF⟩ := hf
+  use UE ∩ g⁻¹' UF
+  constructor
+  · simp
+    constructor
+    · assumption
+    · apply ContinuousAt.preimage_mem_nhds
+      apply (h₂UE z (mem_of_mem_nhds h₁UE)).continuousAt
+      assumption
+  · intro x hx
+    apply DifferentiableAt.comp
+    apply h₂UF
+    exact hx.2
+    apply h₂UE
+    exact hx.1
+
+
+theorem HolomorphicAt_neg
+  {f : E → F}
+  {z : E}
+  (hf : HolomorphicAt f z) :
+  HolomorphicAt (-f) z := by
+  obtain ⟨UF, h₁UF, h₂UF⟩ := hf
+  use UF
+  constructor
+  · assumption
+  · intro z hz
+    apply differentiableAt_neg_iff.mp
+    simp
+    exact h₂UF z hz
+
+
+theorem HolomorphicAt_contDiffAt
+  {f : ℂ → F}
+  {z : ℂ}
+  (hf : HolomorphicAt f z) :
+  ContDiffAt ℝ 2 f z := by
+
+  let t := {x | HolomorphicAt f x}
+  have ht : IsOpen t := HolomorphicAt_isOpen f
+  have hz : z ∈ t := by exact hf
+
+  -- ContDiffAt ℝ 2 f z
+  apply ContDiffOn.contDiffAt _ ((IsOpen.mem_nhds_iff ht).2 hz)
+  suffices h : ContDiffOn ℂ 2 f t from by
+    apply ContDiffOn.restrict_scalars ℝ h
+  apply DifferentiableOn.contDiffOn _ ht
+  intro w hw
+  apply DifferentiableAt.differentiableWithinAt
+  exact HolomorphicAt_differentiableAt hw
+
+
+theorem CauchyRiemann'₅
+  {f : ℂ → F}
+  {z : ℂ}
+  (h : DifferentiableAt ℂ f z) :
+  partialDeriv ℝ Complex.I f z = Complex.I • partialDeriv ℝ 1 f z := by
+  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]
+
+
+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
+
+  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/holomorphic.primitive.lean

@@ -0,0 +1,518 @@
+import Mathlib.Analysis.Complex.TaylorSeries
+import Mathlib.Analysis.SpecialFunctions.Integrals
+import Mathlib.MeasureTheory.Integral.DivergenceTheorem
+import Mathlib.MeasureTheory.Integral.IntervalIntegral
+import Mathlib.MeasureTheory.Function.LocallyIntegrable
+
+import Nevanlinna.cauchyRiemann
+
+
+theorem MeasureTheory.integral2_divergence₃
+  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
+  (f g : ℝ × ℝ → E)
+  (h₁f : ContDiff ℝ 1 f)
+  (h₁g : ContDiff ℝ 1 g)
+  (a₁ : ℝ)
+  (a₂ : ℝ)
+  (b₁ : ℝ)
+  (b₂ : ℝ) :
+  ∫ (x : ℝ) in a₁..b₁, ∫ (y : ℝ) in a₂..b₂, ((fderiv ℝ f) (x, y)) (1, 0) + ((fderiv ℝ g) (x, y)) (0, 1) = (((∫ (x : ℝ) in a₁..b₁, g (x, b₂)) - ∫ (x : ℝ) in a₁..b₁, g (x, a₂)) + ∫ (y : ℝ) in a₂..b₂, f (b₁, y)) - ∫ (y : ℝ) in a₂..b₂, f (a₁, y) := by
+
+  apply integral2_divergence_prod_of_hasFDerivWithinAt_off_countable f g (fderiv ℝ f) (fderiv ℝ g) a₁ a₂ b₁ b₂ ∅
+  exact Set.countable_empty
+  -- ContinuousOn f (Set.uIcc a₁ b₁ ×ˢ Set.uIcc a₂ b₂)
+  exact h₁f.continuous.continuousOn
+  --
+  exact h₁g.continuous.continuousOn
+  --
+  rw [Set.diff_empty]
+  intro x _
+  exact DifferentiableAt.hasFDerivAt ((h₁f.differentiable le_rfl) x)
+  --
+  rw [Set.diff_empty]
+  intro y _
+  exact DifferentiableAt.hasFDerivAt ((h₁g.differentiable le_rfl) y)
+  --
+  apply ContinuousOn.integrableOn_compact
+  apply IsCompact.prod
+  exact isCompact_uIcc
+  exact isCompact_uIcc
+  apply ContinuousOn.add
+  apply Continuous.continuousOn
+  exact Continuous.clm_apply (ContDiff.continuous_fderiv h₁f le_rfl) continuous_const
+  apply Continuous.continuousOn
+  exact Continuous.clm_apply (ContDiff.continuous_fderiv h₁g le_rfl) continuous_const
+
+
+theorem integral_divergence₄
+  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
+  (f g : ℂ  → E)
+  (h₁f : ContDiff ℝ 1 f)
+  (h₁g : ContDiff ℝ 1 g)
+  (a₁ : ℝ)
+  (a₂ : ℝ)
+  (b₁ : ℝ)
+  (b₂ : ℝ) :
+  ∫ (x : ℝ) in a₁..b₁, ∫ (y : ℝ) in a₂..b₂, ((fderiv ℝ f) ⟨x, y⟩ ) 1 + ((fderiv ℝ g) ⟨x, y⟩) Complex.I = (((∫ (x : ℝ) in a₁..b₁, g ⟨x, b₂⟩) - ∫ (x : ℝ) in a₁..b₁, g ⟨x, a₂⟩) + ∫ (y : ℝ) in a₂..b₂, f ⟨b₁, y⟩) - ∫ (y : ℝ) in a₂..b₂, f ⟨a₁, y⟩ := by
+
+  let fr : ℝ × ℝ → E := f ∘ Complex.equivRealProdCLM.symm
+  let gr : ℝ × ℝ → E := g ∘ Complex.equivRealProdCLM.symm
+
+  have sfr {x y : ℝ} : f { re := x, im := y } = fr (x, y) := by exact rfl
+  have sgr {x y : ℝ} : g { re := x, im := y } = gr (x, y) := by exact rfl
+  repeat (conv in f { re := _, im := _ } => rw [sfr])
+  repeat (conv in g { re := _, im := _ } => rw [sgr])
+
+  have sfr' {x y : ℝ} {z : ℂ} : (fderiv ℝ f { re := x, im := y }) z = fderiv ℝ fr (x, y) (Complex.equivRealProdCLM z) := by
+    rw [fderiv.comp]
+    rw [Complex.equivRealProdCLM.symm.fderiv]
+    tauto
+    apply Differentiable.differentiableAt
+    exact h₁f.differentiable le_rfl
+    exact Complex.equivRealProdCLM.symm.differentiableAt
+  conv in ⇑(fderiv ℝ f { re := _, im := _ }) _ => rw [sfr']
+
+  have sgr' {x y : ℝ} {z : ℂ} : (fderiv ℝ g { re := x, im := y }) z = fderiv ℝ gr (x, y) (Complex.equivRealProdCLM z) := by
+    rw [fderiv.comp]
+    rw [Complex.equivRealProdCLM.symm.fderiv]
+    tauto
+    apply Differentiable.differentiableAt
+    exact h₁g.differentiable le_rfl
+    exact Complex.equivRealProdCLM.symm.differentiableAt
+  conv in ⇑(fderiv ℝ g { re := _, im := _ }) _ => rw [sgr']
+
+  apply MeasureTheory.integral2_divergence₃ fr gr _ _ a₁ a₂ b₁ b₂
+  -- ContDiff ℝ 1 fr
+  exact (ContinuousLinearEquiv.contDiff_comp_iff (ContinuousLinearEquiv.symm Complex.equivRealProdCLM)).mpr h₁f
+  -- ContDiff ℝ 1 gr
+  exact (ContinuousLinearEquiv.contDiff_comp_iff (ContinuousLinearEquiv.symm Complex.equivRealProdCLM)).mpr h₁g
+
+
+theorem integral_divergence₅
+  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
+  (F : ℂ  → E)
+  (hF : Differentiable ℂ F)
+  (lowerLeft upperRight : ℂ) :
+  (∫ (x : ℝ) in lowerLeft.re..upperRight.re, F ⟨x, lowerLeft.im⟩)  + Complex.I • ∫ (x : ℝ) in lowerLeft.im..upperRight.im, F ⟨upperRight.re, x⟩ =
+  (∫ (x : ℝ) in lowerLeft.re..upperRight.re, F ⟨x, upperRight.im⟩) + Complex.I • ∫ (x : ℝ) in lowerLeft.im..upperRight.im, F ⟨lowerLeft.re,  x⟩ := by
+
+  let h₁f : ContDiff ℝ 1 F := (hF.contDiff : ContDiff ℂ 1 F).restrict_scalars ℝ
+
+  let h₁g : ContDiff ℝ 1 (-Complex.I • F) := by
+    have : -Complex.I • F = fun x ↦ -Complex.I • F x := by rfl
+    rw [this]
+    apply ContDiff.comp
+    exact contDiff_const_smul _
+    exact h₁f
+
+  let A := integral_divergence₄ (-Complex.I • F) F h₁g h₁f lowerLeft.re upperRight.im upperRight.re lowerLeft.im
+  have {z : ℂ} : fderiv ℝ F z Complex.I = partialDeriv ℝ _ F z := by rfl
+  conv at A in (fderiv ℝ F _) _ => rw [this]
+  have {z : ℂ} : fderiv ℝ (-Complex.I • F) z 1 = partialDeriv ℝ _ (-Complex.I • F) z := by rfl
+  conv at A in (fderiv ℝ (-Complex.I • F) _) _ => rw [this]
+  conv at A =>
+    left
+    arg 1
+    intro x
+    arg 1
+    intro y
+    rw [CauchyRiemann₄ hF]
+    rw [partialDeriv_smul'₂]
+    simp
+  simp at A
+
+  have {t₁ t₂ t₃ t₄ : E} : 0 = (t₁ - t₂) + t₃ + t₄ → t₁ + t₃ = t₂ - t₄ := by
+    intro hyp
+    calc
+      t₁ + t₃ = t₁ + t₃ - 0 := by rw [sub_zero (t₁ + t₃)]
+      _ = t₁ + t₃ - (t₁ - t₂ + t₃ + t₄) := by rw [hyp]
+      _ = t₂ - t₄ := by abel
+  let B := this A
+  repeat
+    rw [intervalIntegral.integral_symm lowerLeft.im upperRight.im] at B
+  simp at B
+  exact B
+
+
+noncomputable def primitive
+  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] :
+  ℂ  → (ℂ → E) → (ℂ → E) := by
+  intro z₀
+  intro f
+  exact fun z ↦ (∫ (x : ℝ) in z₀.re..z.re, f ⟨x, z₀.im⟩) + Complex.I • ∫ (x : ℝ) in z₀.im..z.im, f ⟨z.re, x⟩
+
+
+theorem primitive_zeroAtBasepoint
+  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
+  (f : ℂ  → E)
+  (z₀ : ℂ) :
+  (primitive z₀ f) z₀ = 0 := by
+  unfold primitive
+  simp
+
+
+theorem primitive_fderivAtBasepointZero
+  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
+  (f : ℂ  → E)
+  (hf : Continuous f) :
+  HasDerivAt (primitive 0 f) (f 0) 0 := by
+  unfold primitive
+  simp
+  apply hasDerivAt_iff_isLittleO.2
+  simp
+  rw [Asymptotics.isLittleO_iff]
+  intro c hc
+
+  have {z : ℂ} {e : E} : z • e = (∫ (_ : ℝ) in (0)..(z.re), e) + Complex.I • ∫ (_ : ℝ) in (0)..(z.im), e:= by
+    simp
+    rw [smul_comm]
+    rw [← smul_assoc]
+    simp
+    have : z.re • e = (z.re : ℂ) • e := by exact rfl
+    rw [this, ← add_smul]
+    simp
+  conv =>
+    left
+    intro x
+    left
+    arg 1
+    arg 2
+    rw [this]
+  have {A B C D :E} : (A + B) - (C + D) = (A - C) + (B - D) := by
+    abel
+  have t₀ {r : ℝ} : IntervalIntegrable (fun x => f { re := x, im := 0 }) MeasureTheory.volume 0 r := by
+    apply Continuous.intervalIntegrable
+    apply Continuous.comp
+    exact hf
+    have : (fun x => ({ re := x, im := 0 } : ℂ)) = Complex.ofRealLI := by rfl
+    rw [this]
+    continuity
+  have t₁ {r : ℝ} : IntervalIntegrable (fun _ => f 0) MeasureTheory.volume 0 r := by
+    apply Continuous.intervalIntegrable
+    apply Continuous.comp
+    exact hf
+    fun_prop
+  have t₂ {a b : ℝ} : IntervalIntegrable (fun x_1 => f { re := a, im := x_1 }) MeasureTheory.volume 0 b := by
+    apply Continuous.intervalIntegrable
+    apply Continuous.comp
+    exact hf
+    have : ((fun x => { re := a, im := x }) : ℝ → ℂ) = (fun x => { re := a, im := 0 } + { re := 0, im := x }) := by
+      funext x
+      apply Complex.ext
+      rw [Complex.add_re]
+      simp
+      rw [Complex.add_im]
+      simp
+    rw [this]
+    apply Continuous.add
+    fun_prop
+    have : (fun x => { re := 0, im := x } : ℝ → ℂ) = Complex.I • Complex.ofRealCLM := by
+      funext x
+      simp
+      have : (x : ℂ) = {re := x, im := 0} := by rfl
+      rw [this]
+      rw [Complex.I_mul]
+      simp
+    continuity
+
+  have t₃ {a : ℝ} : IntervalIntegrable (fun _ => f 0) MeasureTheory.volume 0 a := by
+    apply Continuous.intervalIntegrable
+    apply Continuous.comp
+    exact hf
+    fun_prop
+  conv =>
+    left
+    intro x
+    left
+    arg 1
+    rw [this]
+    rw [← smul_sub]
+    rw [← intervalIntegral.integral_sub t₀ t₁]
+    rw [← intervalIntegral.integral_sub t₂ t₃]
+  rw [Filter.eventually_iff_exists_mem]
+
+  let s := f⁻¹' Metric.ball (f 0) (c / (4 : ℝ))
+  have h₁s : IsOpen s := IsOpen.preimage hf Metric.isOpen_ball
+  have h₂s : 0 ∈ s := by
+    apply Set.mem_preimage.mpr
+    apply Metric.mem_ball_self
+    linarith
+
+  obtain ⟨ε, h₁ε, h₂ε⟩ := Metric.isOpen_iff.1 h₁s 0 h₂s
+
+  have h₃ε : ∀ y ∈ Metric.ball 0 ε, ‖(f y) - (f 0)‖ < (c / (4 : ℝ)) := by
+    intro y hy
+    apply mem_ball_iff_norm.mp (h₂ε hy)
+
+  use Metric.ball 0 (ε / (4 : ℝ))
+  constructor
+  · apply Metric.ball_mem_nhds 0
+    linarith
+  · intro y hy
+    have h₁y : |y.re| < ε / 4 := by
+      calc |y.re|
+      _ ≤ Complex.abs y := by apply Complex.abs_re_le_abs
+      _ < ε / 4 := by
+        let A := mem_ball_iff_norm.1 hy
+        simp at A
+        linarith
+    have h₂y : |y.im| < ε / 4 := by
+      calc |y.im|
+      _ ≤ Complex.abs y := by apply Complex.abs_im_le_abs
+      _ < ε / 4 := by
+        let A := mem_ball_iff_norm.1 hy
+        simp at A
+        linarith
+
+    have intervalComputation {x' y' : ℝ} (h : x' ∈ Ι 0 y') : |x'| ≤ |y'| := by
+      let A := h.1
+      let B := h.2
+      rcases le_total 0 y' with hy | hy
+      · simp [hy] at A
+        simp [hy] at B
+        rw [abs_of_nonneg hy]
+        rw [abs_of_nonneg (le_of_lt A)]
+        exact B
+      · simp [hy] at A
+        simp [hy] at B
+        rw [abs_of_nonpos hy]
+        rw [abs_of_nonpos]
+        linarith [h.1]
+        exact B
+
+    have t₁ : ‖(∫ (x : ℝ) in (0)..(y.re), f { re := x, im := 0 } - f 0)‖ ≤ (c / (4 : ℝ)) * |y.re - 0| := by
+      apply intervalIntegral.norm_integral_le_of_norm_le_const
+      intro x hx
+
+      have h₁x : |x| < ε / 4 := by
+        calc |x|
+          _ ≤ |y.re| := intervalComputation hx
+          _ < ε / 4 := h₁y
+      apply le_of_lt
+      apply h₃ε { re := x, im := 0 }
+      rw [mem_ball_iff_norm]
+      simp
+      have : { re := x, im := 0 } = (x : ℂ) := by rfl
+      rw [this]
+      rw [Complex.abs_ofReal]
+      linarith
+
+    have t₂ : ‖∫ (x : ℝ) in (0)..(y.im), f { re := y.re, im := x } - f 0‖ ≤ (c / (4 : ℝ)) * |y.im - 0| := by
+      apply intervalIntegral.norm_integral_le_of_norm_le_const
+      intro x hx
+
+      have h₁x : |x| < ε / 4 := by
+        calc |x|
+          _ ≤ |y.im| := intervalComputation hx
+          _ < ε / 4 := h₂y
+
+      apply le_of_lt
+      apply h₃ε { re := y.re, im := x }
+      simp
+
+      calc Complex.abs { re := y.re, im := x }
+        _ ≤ |y.re| + |x| := by
+          apply Complex.abs_le_abs_re_add_abs_im { re := y.re, im := x }
+        _ < ε := by
+          linarith
+
+    calc ‖(∫ (x : ℝ) in (0)..(y.re), f { re := x, im := 0 } - f 0) + Complex.I • ∫ (x : ℝ) in (0)..(y.im), f { re := y.re, im := x } - f 0‖
+      _ ≤ ‖(∫ (x : ℝ) in (0)..(y.re), f { re := x, im := 0 } - f 0)‖ + ‖Complex.I • ∫ (x : ℝ) in (0)..(y.im), f { re := y.re, im := x } - f 0‖ := by
+        apply norm_add_le
+      _ ≤ ‖(∫ (x : ℝ) in (0)..(y.re), f { re := x, im := 0 } - f 0)‖ + ‖∫ (x : ℝ) in (0)..(y.im), f { re := y.re, im := x } - f 0‖ := by
+        simp
+        rw [norm_smul]
+        simp
+      _ ≤ (c / (4 : ℝ)) * |y.re - 0| + (c / (4 : ℝ)) * |y.im - 0| := by
+        apply add_le_add
+        exact t₁
+        exact t₂
+      _ ≤ (c / (4 : ℝ)) * (|y.re| + |y.im|) := by
+        simp
+        rw [mul_add]
+      _ ≤ (c / (4 : ℝ)) * (4 * ‖y‖) := by
+        have : |y.re| + |y.im| ≤ 4 * ‖y‖ := by
+          calc |y.re| + |y.im|
+            _ ≤ ‖y‖ + ‖y‖ := by
+              apply add_le_add
+              apply Complex.abs_re_le_abs
+              apply Complex.abs_im_le_abs
+            _ ≤ 4 * ‖y‖ := by
+              rw [← two_mul]
+              apply mul_le_mul
+              linarith
+              rfl
+              exact norm_nonneg y
+              linarith
+
+        apply mul_le_mul
+        rfl
+        exact this
+        apply add_nonneg
+        apply abs_nonneg
+        apply abs_nonneg
+        linarith
+      _ ≤ c * ‖y‖ := by
+        linarith
+
+
+theorem primitive_translation
+  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
+  (f : ℂ  → E)
+  (z₀ t : ℂ) :
+  primitive z₀ (f ∘ fun z ↦ (z - t)) = ((primitive (z₀ - t) f) ∘ fun z ↦ (z - t)) := by
+  funext z
+  unfold primitive
+  simp
+
+  let g : ℝ → E := fun x ↦ f ( {re := x, im := z₀.im - t.im} )
+  have {x : ℝ} : f ({ re := x, im := z₀.im } - t) = g (1*x - t.re) := by
+    congr 1
+    apply Complex.ext <;> simp
+  conv =>
+    left
+    left
+    arg 1
+    intro x
+    rw [this]
+  rw [intervalIntegral.integral_comp_mul_sub g one_ne_zero (t.re)]
+  simp
+
+  congr 1
+  let g : ℝ → E := fun x ↦ f ( {re := z.re - t.re, im := x} )
+  have {x : ℝ} : f ({ re := z.re, im := x} - t) = g (1*x - t.im) := by
+    congr 1
+    apply Complex.ext <;> simp
+  conv =>
+    left
+    arg 1
+    intro x
+    rw [this]
+  rw [intervalIntegral.integral_comp_mul_sub g one_ne_zero (t.im)]
+  simp
+
+
+theorem primitive_fderivAtBasepoint
+  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
+  {z₀ : ℂ}
+  (f : ℂ  → E)
+  (hf : Continuous f) :
+  HasDerivAt (primitive z₀ f) (f z₀) z₀ := by
+
+  let g := f ∘ fun z ↦ z + z₀
+  have : Continuous g := by continuity
+  let A := primitive_fderivAtBasepointZero g this
+  simp at A
+
+  let B := primitive_translation g z₀ z₀
+  simp at B
+  have : (g ∘ fun z ↦ (z - z₀)) = f := by
+    funext z
+    dsimp [g]
+    simp
+  rw [this] at B
+  rw [B]
+  have : f z₀ = (1 : ℂ) • (f z₀) := by
+    exact (MulAction.one_smul (f z₀)).symm
+  conv =>
+    arg 2
+    rw [this]
+
+  apply HasDerivAt.scomp
+  simp
+  have : g 0 = f z₀ := by simp [g]
+  rw [← this]
+  exact A
+  apply HasDerivAt.sub_const
+  have : (fun (x : ℂ) ↦ x) = id := by
+    funext x
+    simp
+  rw [this]
+  exact hasDerivAt_id z₀
+
+
+lemma integrability₁
+  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
+  (f : ℂ  → E)
+  (hf : Differentiable ℂ f)
+  (a₁ a₂ b : ℝ) :
+  IntervalIntegrable (fun x => f { re := x, im := b }) MeasureTheory.volume a₁ a₂ := by
+  apply Continuous.intervalIntegrable
+  apply Continuous.comp
+  exact Differentiable.continuous hf
+  have : ((fun x => { re := x, im := b }) : ℝ → ℂ) = (fun x => Complex.ofRealCLM x + { re := 0, im := b }) := by
+    funext x
+    apply Complex.ext
+    rw [Complex.add_re]
+    simp
+    rw [Complex.add_im]
+    simp
+  rw [this]
+  continuity
+
+
+lemma integrability₂
+  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
+  (f : ℂ  → E)
+  (hf : Differentiable ℂ f)
+  (a₁ a₂ b : ℝ) :
+  IntervalIntegrable (fun x => f { re := b, im := x }) MeasureTheory.volume a₁ a₂ := by
+  apply Continuous.intervalIntegrable
+  apply Continuous.comp
+  exact Differentiable.continuous hf
+  have : ((fun x => { re := b, im := x }) : ℝ → ℂ) = (fun x => Complex.I • Complex.ofRealCLM x + { re := b, im := 0 }) := by
+    funext x
+    apply Complex.ext
+    rw [Complex.add_re]
+    simp
+    simp
+  rw [this]
+  apply Continuous.add
+  continuity
+  fun_prop
+
+
+theorem primitive_additivity
+  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
+  (f : ℂ  → E)
+  (hf : Differentiable ℂ f)
+  (z₀ z₁ : ℂ) :
+  primitive z₀ f = fun z ↦ (primitive z₁ f) z + (primitive z₀ f z₁) := by
+  funext z
+  unfold primitive
+
+  have : (∫ (x : ℝ) in z₀.re..z.re, f { re := x, im := z₀.im }) = (∫ (x : ℝ) in z₀.re..z₁.re, f { re := x, im := z₀.im }) + (∫ (x : ℝ) in z₁.re..z.re, f { re := x, im := z₀.im }) := by
+    rw [intervalIntegral.integral_add_adjacent_intervals]   
+    apply integrability₁ f hf 
+    apply integrability₁ f hf 
+  rw [this]
+
+  have : (∫ (x : ℝ) in z₀.im..z.im, f { re := z.re, im := x }) = (∫ (x : ℝ) in z₀.im..z₁.im, f { re := z.re, im := x }) + (∫ (x : ℝ) in z₁.im..z.im, f { re := z.re, im := x }) := by
+    rw [intervalIntegral.integral_add_adjacent_intervals]
+    apply integrability₂ f hf 
+    apply integrability₂ f hf 
+  rw [this]
+  simp
+
+  let A := integral_divergence₅ f hf ⟨z₁.re, z₀.im⟩ ⟨z.re, z₁.im⟩
+  simp at A
+
+  have {a b c d : E} : (b + a) + (c + d) = (a + c) + (b + d) := by
+    abel
+  rw [this]
+  rw [A]
+  abel
+
+
+theorem primitive_fderiv
+  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
+  {z₀ z : ℂ}
+  (f : ℂ  → E)
+  (hf : Differentiable ℂ f) :
+  HasDerivAt (primitive z₀ f) (f z) z := by
+  rw [primitive_additivity f hf z₀ z]
+  rw [← add_zero (f z)]
+  apply HasDerivAt.add
+  apply primitive_fderivAtBasepoint
+  exact hf.continuous
+  apply hasDerivAt_const

Nevanlinna/holomorphicAt.lean

@@ -0,0 +1,147 @@
+import Mathlib.Analysis.Complex.TaylorSeries
+import Nevanlinna.cauchyRiemann
+
+variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]
+variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F]
+variable {G : Type*} [NormedAddCommGroup G] [NormedSpace ℂ G]
+
+def HolomorphicAt (f : E → F) (x : E) : Prop :=
+  ∃ s ∈ nhds x, ∀ z ∈ s, DifferentiableAt ℂ f z
+
+
+theorem HolomorphicAt_iff
+  {f : E → F}
+  {x : E} :
+  HolomorphicAt f x ↔ ∃ s :
+  Set E, IsOpen s ∧ x ∈ s ∧ (∀ z ∈ s, DifferentiableAt ℂ 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
+        exact h₂t z (h₁s hz)
+  · intro hyp
+    obtain ⟨s, h₁s, h₂s, hf⟩ := hyp
+    use s
+    constructor
+    · apply (IsOpen.mem_nhds_iff h₁s).2 h₂s
+    · assumption
+
+
+theorem HolomorphicAt_isOpen
+  (f : E → F) :
+  IsOpen { x : E | HolomorphicAt f x } := by
+
+  rw [← subset_interior_iff_isOpen]
+  intro x hx
+  simp at hx
+  obtain ⟨s, h₁s, h₂s, h₃s⟩ := HolomorphicAt_iff.1 hx
+  use s
+  constructor
+  · simp
+    constructor
+    · exact h₁s
+    · intro x hx
+      simp
+      use s
+      constructor
+      · exact IsOpen.mem_nhds h₁s hx
+      · exact h₃s
+  · exact h₂s
+
+
+theorem HolomorphicAt_comp
+  {g : E → F}
+  {f : F → G}
+  {z : E}
+  (hf : HolomorphicAt f (g z))
+  (hg : HolomorphicAt g z) :
+  HolomorphicAt (f ∘ g) z := by
+  obtain ⟨UE, h₁UE, h₂UE⟩ := hg
+  obtain ⟨UF, h₁UF, h₂UF⟩ := hf
+  use UE ∩ g⁻¹' UF
+  constructor
+  · simp
+    constructor
+    · assumption
+    · apply ContinuousAt.preimage_mem_nhds
+      apply (h₂UE z (mem_of_mem_nhds h₁UE)).continuousAt
+      assumption
+  · intro x hx
+    apply DifferentiableAt.comp
+    apply h₂UF
+    exact hx.2
+    apply h₂UE
+    exact hx.1
+
+
+theorem HolomorphicAt_neg
+  {f : E → F}
+  {z : E}
+  (hf : HolomorphicAt f z) :
+  HolomorphicAt (-f) z := by
+  obtain ⟨UF, h₁UF, h₂UF⟩ := hf
+  use UF
+  constructor
+  · assumption
+  · intro z hz
+    apply differentiableAt_neg_iff.mp
+    simp
+    exact h₂UF z hz
+
+
+theorem HolomorphicAt.contDiffAt
+  [CompleteSpace F]
+  {f : ℂ → F}
+  {z : ℂ}
+  {n : ℕ}
+  (hf : HolomorphicAt f z) :
+  ContDiffAt ℝ n f z := by
+
+  let t := {x | HolomorphicAt f x}
+  have ht : IsOpen t := HolomorphicAt_isOpen f
+  have hz : z ∈ t := by exact hf
+
+  -- ContDiffAt ℝ _ f z
+  apply ContDiffOn.contDiffAt _ ((IsOpen.mem_nhds_iff ht).2 hz)
+  suffices h : ContDiffOn ℂ n f t from by
+    apply ContDiffOn.restrict_scalars ℝ h
+  apply DifferentiableOn.contDiffOn _ ht
+  intro w hw
+  apply DifferentiableAt.differentiableWithinAt
+  -- DifferentiableAt ℂ f w
+  let hfw : HolomorphicAt f w := hw
+  obtain ⟨s, _, h₂s, h₃s⟩ := HolomorphicAt_iff.1 hfw
+  exact h₃s w h₂s
+
+
+theorem HolomorphicAt.differentiableAt
+  {f : ℂ → F}
+  {z : ℂ}
+  (hf : HolomorphicAt f z) :
+  DifferentiableAt ℂ f z := by
+  obtain ⟨s, _, h₂s, h₃s⟩ := HolomorphicAt_iff.1 hf
+  exact h₃s z h₂s
+
+
+theorem HolomorphicAt.CauchyRiemannAt
+  {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
+
+  apply Filter.eventuallyEq_iff_exists_mem.2
+  use s
+  constructor
+  · exact IsOpen.mem_nhds h₁s hz
+  · intro w hw
+    let h := h₂f w hw
+    unfold partialDeriv
+    apply CauchyRiemann₅ h

Nevanlinna/laplace.lean

@@ -1,28 +1,36 @@
-import Mathlib.Data.Fin.Tuple.Basic
 import Mathlib.Analysis.Complex.Basic
-import Mathlib.Analysis.Complex.TaylorSeries
-import Mathlib.Analysis.Calculus.LineDeriv.Basic
-import Mathlib.Analysis.Calculus.ContDiff.Defs
-import Mathlib.Analysis.Calculus.FDeriv.Basic
-import Mathlib.Analysis.Calculus.FDeriv.Symmetric
-import Mathlib.Data.Complex.Module
-import Mathlib.Data.Complex.Order
-import Mathlib.Data.Complex.Exponential
-import Mathlib.Analysis.RCLike.Basic
-import Mathlib.Topology.Algebra.InfiniteSum.Module
-import Mathlib.Topology.Instances.RealVectorSpace
-import Nevanlinna.cauchyRiemann
 import Nevanlinna.partialDeriv
 
 variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
 variable {G : Type*} [NormedAddCommGroup G] [NormedSpace ℝ G]
 
 
-noncomputable def Complex.laplace : (ℂ → F) → (ℂ → F) :=
-  fun f ↦ partialDeriv ℝ 1 (partialDeriv ℝ 1 f) + partialDeriv ℝ Complex.I (partialDeriv ℝ Complex.I f)
+noncomputable def Complex.laplace (f : ℂ → F) : ℂ → F :=
+  partialDeriv ℝ 1 (partialDeriv ℝ 1 f) + partialDeriv ℝ Complex.I (partialDeriv ℝ Complex.I f)
+
+notation "Δ" => Complex.laplace
 
 
-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_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_eventuallyEq' {f₁ f₂ : ℂ → F} {x : ℂ} (h : f₁ =ᶠ[nhds x] f₂) : Δ f₁ =ᶠ[nhds x] Δ f₂ := by
+  unfold Complex.laplace
+  apply Filter.EventuallyEq.add
+  exact partialDeriv_eventuallyEq' ℝ (partialDeriv_eventuallyEq' ℝ h 1) 1
+  exact partialDeriv_eventuallyEq' ℝ (partialDeriv_eventuallyEq' ℝ h Complex.I) Complex.I
+
+
+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₂]
@@ -44,39 +52,225 @@ theorem laplace_add {f₁ f₂ : ℂ → F} (h₁ : ContDiff ℝ 2 f₁)  (h₂
   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
+theorem laplace_add_ContDiffOn
+  {f₁ f₂ : ℂ → F}
+  {s : Set ℂ}
+  (hs : IsOpen s)
+  (h₁ : ContDiffOn ℝ 2 f₁ s)
+  (h₂ : ContDiffOn ℝ 2 f₂ s) :
+  ∀ x ∈ s, Δ (f₁ + f₂) x = (Δ f₁) x + (Δ f₂) x := by
+
+  unfold Complex.laplace
+  simp
+  intro x hx
+
+  have hf₁ : ∀ z ∈ s, DifferentiableAt ℝ f₁ z := by
+    intro z hz
+    convert DifferentiableOn.differentiableAt _ (IsOpen.mem_nhds hs hz)
+    apply ContDiffOn.differentiableOn h₁ one_le_two
+  have hf₂ : ∀ z ∈ s, DifferentiableAt ℝ f₂ z := by
+    intro z hz
+    convert DifferentiableOn.differentiableAt _ (IsOpen.mem_nhds hs hz)
+    apply ContDiffOn.differentiableOn h₂ one_le_two
+  have : partialDeriv ℝ 1 (f₁ + f₂) =ᶠ[nhds x] (partialDeriv ℝ 1 f₁) + (partialDeriv ℝ 1 f₂) := by
+    apply Filter.eventuallyEq_iff_exists_mem.2
+    use s
+    constructor
+    · exact IsOpen.mem_nhds hs hx
+    · intro z hz
+      apply partialDeriv_add₂_differentiableAt
+      exact hf₁ z hz
+      exact hf₂ z hz
+  rw [partialDeriv_eventuallyEq ℝ this]
+  have t₁ : DifferentiableAt ℝ (partialDeriv ℝ 1 f₁) x := by
+    let B₀ := (h₁ x hx).contDiffAt (IsOpen.mem_nhds hs hx)
+    let A₀ := partialDeriv_contDiffAt ℝ B₀ 1
+    exact A₀.differentiableAt (Submonoid.oneLE.proof_2 ℕ∞)
+  have t₂ : DifferentiableAt ℝ (partialDeriv ℝ 1 f₂) x := by
+    let B₀ := (h₂ x hx).contDiffAt (IsOpen.mem_nhds hs hx)
+    let A₀ := partialDeriv_contDiffAt ℝ B₀ 1
+    exact A₀.differentiableAt (Submonoid.oneLE.proof_2 ℕ∞)
+  rw [partialDeriv_add₂_differentiableAt ℝ t₁ t₂]
+
+  have : partialDeriv ℝ Complex.I (f₁ + f₂) =ᶠ[nhds x] (partialDeriv ℝ Complex.I f₁) + (partialDeriv ℝ Complex.I f₂) := by
+    apply Filter.eventuallyEq_iff_exists_mem.2
+    use s
+    constructor
+    · exact IsOpen.mem_nhds hs hx
+    · intro z hz
+      apply partialDeriv_add₂_differentiableAt
+      exact hf₁ z hz
+      exact hf₂ z hz
+  rw [partialDeriv_eventuallyEq ℝ this]
+  have t₃ : DifferentiableAt ℝ (partialDeriv ℝ Complex.I f₁) x := by
+    let B₀ := (h₁ x hx).contDiffAt (IsOpen.mem_nhds hs hx)
+    let A₀ := partialDeriv_contDiffAt ℝ B₀ Complex.I
+    exact A₀.differentiableAt (Submonoid.oneLE.proof_2 ℕ∞)
+  have t₄ : DifferentiableAt ℝ (partialDeriv ℝ Complex.I f₂) x := by
+    let B₀ := (h₂ x hx).contDiffAt (IsOpen.mem_nhds hs hx)
+    let A₀ := partialDeriv_contDiffAt ℝ B₀ Complex.I
+    exact A₀.differentiableAt (Submonoid.oneLE.proof_2 ℕ∞)
+  rw [partialDeriv_add₂_differentiableAt ℝ t₃ t₄]
+
+  -- 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_add_ContDiffAt
+  {f₁ f₂ : ℂ → F}
+  {x : ℂ}
+  (h₁ : ContDiffAt ℝ 2 f₁ x)
+  (h₂ : ContDiffAt ℝ 2 f₂ x) :
+  Δ (f₁ + f₂) x = (Δ f₁) x + (Δ f₂) x := by
+
+  unfold Complex.laplace
+  simp
+
+  have h₁₁ : ContDiffAt ℝ 1 f₁ x := h₁.of_le one_le_two
+  have h₂₁ : ContDiffAt ℝ 1 f₂ x := h₂.of_le one_le_two
+  repeat
+    rw [partialDeriv_eventuallyEq ℝ (partialDeriv_add₂_contDiffAt ℝ h₁₁ h₂₁)]
+    rw [partialDeriv_add₂_differentiableAt]
+
+  -- 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]
+
+  repeat
+    apply fun v ↦ (partialDeriv_contDiffAt ℝ h₁ v).differentiableAt le_rfl
+    apply fun v ↦ (partialDeriv_contDiffAt ℝ h₂ v).differentiableAt le_rfl
+
+
+theorem laplace_add_ContDiffAt'
+  {f₁ f₂ : ℂ → F}
+  {x : ℂ}
+  (h₁ : ContDiffAt ℝ 2 f₁ x)
+  (h₂ : ContDiffAt ℝ 2 f₂ x) :
+  Δ (f₁ + f₂) =ᶠ[nhds x] (Δ f₁) + (Δ f₂):= by
+
+  unfold Complex.laplace
+
+  rw [add_assoc]
+  nth_rw  5 [add_comm]
+  rw [add_assoc]
+  rw [← add_assoc]
+
+  have dualPDeriv : ∀ v : ℂ, partialDeriv ℝ v (partialDeriv ℝ v (f₁ + f₂)) =ᶠ[nhds x]
+    partialDeriv ℝ v (partialDeriv ℝ v f₁) + partialDeriv ℝ v (partialDeriv ℝ v f₂) := by
+
+    intro v
+    have h₁₁ : ContDiffAt ℝ 1 f₁ x := h₁.of_le one_le_two
+    have h₂₁ : ContDiffAt ℝ 1 f₂ x := h₂.of_le one_le_two
+
+    have t₁ : partialDeriv ℝ v (partialDeriv ℝ v (f₁ + f₂)) =ᶠ[nhds x] partialDeriv ℝ v (partialDeriv ℝ v f₁ + partialDeriv ℝ v f₂) := by
+      exact partialDeriv_eventuallyEq' ℝ (partialDeriv_add₂_contDiffAt ℝ h₁₁ h₂₁) v
+
+    have t₂ : partialDeriv ℝ v (partialDeriv ℝ v f₁ + partialDeriv ℝ v f₂) =ᶠ[nhds x] (partialDeriv ℝ v (partialDeriv ℝ v f₁)) + (partialDeriv ℝ v (partialDeriv ℝ v f₂)) := by
+      apply partialDeriv_add₂_contDiffAt ℝ
+      apply partialDeriv_contDiffAt
+      exact h₁
+      apply partialDeriv_contDiffAt
+      exact h₂
+
+    apply Filter.EventuallyEq.trans t₁ t₂
+
+  have eventuallyEq_add
+    {a₁ a₂ b₁ b₂ : ℂ → F}
+    (h : a₁ =ᶠ[nhds x] b₁)
+    (h' : a₂ =ᶠ[nhds x] b₂) : (a₁ + a₂) =ᶠ[nhds x] (b₁ + b₂) := by
+    have {c₁ c₂ : ℂ → F} : (fun x => c₁ x + c₂ x) = c₁ + c₂ := by rfl
+    rw [← this, ← this]
+    exact Filter.EventuallyEq.add h h'
+  apply eventuallyEq_add
+  · exact dualPDeriv 1
+  · nth_rw 2 [add_comm]
+    exact dualPDeriv Complex.I
+
+
+theorem laplace_smul {f : ℂ → F} : ∀ v : ℝ, Δ (v • f) = v • (Δ f) := by
   intro v
   unfold Complex.laplace
-  rw [partialDeriv_smul₂]
-  rw [partialDeriv_smul₂]
-  rw [partialDeriv_smul₂]
+  repeat
     rw [partialDeriv_smul₂]
   simp
 
-  exact (partialDeriv_contDiff ℝ h Complex.I).differentiable le_rfl
-  exact h.differentiable one_le_two
-  exact (partialDeriv_contDiff ℝ h 1).differentiable le_rfl
-  exact h.differentiable one_le_two
 
+theorem laplace_compCLMAt
+  {f : ℂ → F}
+  {l : F →L[ℝ] G}
+  {x : ℂ}
+  (h : ContDiffAt ℝ 2 f x) :
+  Δ (l ∘ f) x = (l ∘ (Δ f)) x := by
+
+  obtain ⟨v, hv₁, hv₂, hv₃, hv₄⟩ : ∃ v ∈ nhds x, (IsOpen v) ∧ (x ∈ v) ∧ (ContDiffOn ℝ 2 f v) := by
+    obtain ⟨u, hu₁, hu₂⟩ : ∃ u ∈ nhds x, ContDiffOn ℝ 2 f u := by
+      apply ContDiffAt.contDiffOn h
+      rfl
+    obtain ⟨v, hv₁, hv₂, hv₃⟩ := mem_nhds_iff.1 hu₁
+    use v
+    constructor
+    · exact IsOpen.mem_nhds hv₂ hv₃
+    · constructor
+      exact hv₂
+      constructor
+      · exact hv₃
+      · exact ContDiffOn.congr_mono hu₂ (fun x => congrFun rfl) hv₁
+
+  have D : ∀ w : ℂ, partialDeriv ℝ w (l ∘ f) =ᶠ[nhds x] l ∘ partialDeriv ℝ w (f) := by
+    intro w
+    apply Filter.eventuallyEq_iff_exists_mem.2
+    use v
+    constructor
+    · exact IsOpen.mem_nhds hv₂ hv₃
+    · intro y hy
+      apply partialDeriv_compContLinAt
+      let V := ContDiffOn.differentiableOn hv₄ one_le_two
+      apply DifferentiableOn.differentiableAt V
+      apply IsOpen.mem_nhds
+      assumption
+      assumption
 
-theorem laplace_compContLin {f : ℂ → F} {l : F →L[ℝ] G} (h : ContDiff ℝ 2 f) :
-  Complex.laplace (l ∘ f) = l ∘ (Complex.laplace f) := 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
-  exact h.differentiable one_le_two
-  exact (partialDeriv_contDiff ℝ h 1).differentiable le_rfl
-  exact h.differentiable one_le_two
+  rw [partialDeriv_eventuallyEq ℝ (D 1) 1]
+  rw [partialDeriv_compContLinAt]
+  rw [partialDeriv_eventuallyEq ℝ (D Complex.I) Complex.I]
+  rw [partialDeriv_compContLinAt]
+  simp
+
+  -- DifferentiableAt ℝ (partialDeriv ℝ Complex.I f) x
+  apply ContDiffAt.differentiableAt (partialDeriv_contDiffAt ℝ (ContDiffOn.contDiffAt hv₄ hv₁) Complex.I) le_rfl
+
+  -- DifferentiableAt ℝ (partialDeriv ℝ 1 f) x
+  apply ContDiffAt.differentiableAt (partialDeriv_contDiffAt ℝ (ContDiffOn.contDiffAt hv₄ hv₁) 1) le_rfl
 
 
-theorem laplace_compCLE {f : ℂ → F} {l : F ≃L[ℝ] G} (h : ContDiff ℝ 2 f) :
-  Complex.laplace (l ∘ f) = l ∘ (Complex.laplace f) := by
-  let l' := (l : F →L[ℝ] G)
-  have : Complex.laplace (l' ∘ f) = l' ∘ (Complex.laplace f) := by
-    exact laplace_compContLin h
-  exact this
+theorem laplace_compCLM
+  {f : ℂ → F}
+  {l : F →L[ℝ] G}
+  (h : ContDiff ℝ 2 f) :
+  Δ (l ∘ f) = l ∘ (Δ f) := by
+  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

Nevanlinna/partialDeriv.lean

@@ -1,6 +1,8 @@
 import Mathlib.Analysis.Calculus.FDeriv.Basic
 import Mathlib.Analysis.Calculus.FDeriv.Symmetric
 import Mathlib.Analysis.Calculus.ContDiff.Basic
+import Mathlib.Topology.Basic
+import Mathlib.Topology.Defs.Filter
 
 
 variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
@@ -14,6 +16,28 @@ 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
+  unfold partialDeriv
+  intro v
+  apply Filter.EventuallyEq.comp₂
+  exact Filter.EventuallyEq.fderiv h
+  simp
+
+
+theorem partialDeriv_eventuallyEq
+  {f₁ f₂ : E → F}
+  {x : E}
+  (h : f₁ =ᶠ[nhds x] f₂) :
+  ∀ v : E, partialDeriv 𝕜 v f₁ x = partialDeriv 𝕜 v f₂ x := by
+  unfold partialDeriv
+  rw [Filter.EventuallyEq.fderiv_eq h]
+  exact fun v => rfl
+
+
 theorem partialDeriv_smul₁ {f : E → F} {a : 𝕜} {v : E} : partialDeriv 𝕜 (a • v) f = a • partialDeriv 𝕜 v f := by
   unfold partialDeriv
   conv =>
@@ -30,21 +54,35 @@ theorem partialDeriv_add₁ {f : E → F} {v₁ v₂ : E} : partialDeriv 𝕜 (v
     rw [map_add]
 
 
-theorem partialDeriv_smul₂ {f : E → F} {a : 𝕜} {v : E} (h : Differentiable 𝕜 f) : partialDeriv 𝕜 v (a • f) = a • partialDeriv 𝕜 v f := by
+theorem partialDeriv_smul₂ {f : E → F} {a : 𝕜} {v : E} : partialDeriv 𝕜 v (a • f) = a • partialDeriv 𝕜 v f := by
   unfold partialDeriv
-
+  funext w
   have : a • f = fun y ↦ a • f y := by rfl
   rw [this]
-
-  conv =>
-    left
-    intro w
-    rw [fderiv_const_smul (h w)]
+  by_cases ha : a = 0
+  · rw [ha]
+    simp
+  · by_cases hf : DifferentiableAt 𝕜 f w
+    · rw [fderiv_const_smul hf]
+      simp
+    · have : ¬DifferentiableAt 𝕜 (fun y => a • f y) w := by
+        by_contra contra
+        let ZZ := DifferentiableAt.const_smul contra a⁻¹
+        have : (fun y => a⁻¹ • a • f y) = f := by
+          funext i
+          rw [← smul_assoc, smul_eq_mul, mul_comm, mul_inv_cancel ha]
+          simp
+        rw [this] at ZZ
+        exact hf ZZ
+      simp
+      rw [fderiv_zero_of_not_differentiableAt hf]
+      rw [fderiv_zero_of_not_differentiableAt this]
+      simp
 
 
-theorem partialDeriv_add₂ {f₁ f₂ : E → F} {v : E} (h₁ : Differentiable 𝕜 f₁)  (h₂ : Differentiable 𝕜 f₂) : partialDeriv 𝕜 v (f₁ + f₂) = (partialDeriv 𝕜 v f₁) + (partialDeriv 𝕜 v f₂) := by
+theorem partialDeriv_add₂ {f₁ f₂ : E → F} (h₁ : Differentiable 𝕜 f₁) (h₂ : Differentiable 𝕜 f₂) : ∀ v : E, partialDeriv 𝕜 v (f₁ + f₂) = (partialDeriv 𝕜 v f₁) + (partialDeriv 𝕜 v f₂) := by
   unfold partialDeriv
-
+  intro v
   have : f₁ + f₂ = fun y ↦ f₁ y + f₂ y := by rfl
   rw [this]
   conv =>
@@ -54,7 +92,49 @@ theorem partialDeriv_add₂ {f₁ f₂ : E → F} {v : E} (h₁ : Differentiable
     rw [fderiv_add (h₁ w) (h₂ w)]
 
 
-theorem partialDeriv_compContLin {f : E → F} {l : F →L[𝕜] G} {v : E} (h : Differentiable 𝕜 f) : partialDeriv 𝕜 v (l ∘ f) = l ∘ partialDeriv 𝕜 v f := by
+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_add₂_contDiffAt
+  {f₁ f₂ : E → F}
+  {v : E}
+  {x : E}
+  (h₁ : ContDiffAt 𝕜 1 f₁ x)
+  (h₂ : ContDiffAt 𝕜 1 f₂ x) :
+  partialDeriv 𝕜 v (f₁ + f₂) =ᶠ[nhds x] (partialDeriv 𝕜 v f₁) + (partialDeriv 𝕜 v f₂) := by
+
+  obtain ⟨f₁', u₁, hu₁, _, hf₁'⟩ := contDiffAt_one_iff.1 h₁
+  obtain ⟨f₂', u₂, hu₂, _, hf₂'⟩ := contDiffAt_one_iff.1 h₂
+
+  apply Filter.eventuallyEq_iff_exists_mem.2
+  use u₁ ∩ u₂
+  constructor
+  · exact Filter.inter_mem hu₁ hu₂
+  · intro x hx
+    simp
+    apply partialDeriv_add₂_differentiableAt 𝕜
+    exact (hf₁' x (Set.mem_of_mem_inter_left hx)).differentiableAt
+    exact (hf₂' x (Set.mem_of_mem_inter_right hx)).differentiableAt
+
+
+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
 
   conv =>
@@ -66,6 +146,29 @@ theorem partialDeriv_compContLin {f : E → F} {l : F →L[𝕜] G} {v : E} (h :
   rfl
 
 
+theorem partialDeriv_compContLinAt {f : E → F} {l : F →L[𝕜] G} {v : E} {x : E} (h : DifferentiableAt 𝕜 f x) : (partialDeriv 𝕜 v (l ∘ f)) x = (l ∘ partialDeriv 𝕜 v f) x:= by
+  unfold partialDeriv
+  rw [fderiv.comp x (ContinuousLinearMap.differentiableAt l) h]
+  simp
+
+
+theorem partialDeriv_compCLE {f : E → F} {l : F ≃L[𝕜] G} {v : E} : partialDeriv 𝕜 v (l ∘ f) = l ∘ partialDeriv 𝕜 v f := by
+  funext x
+  by_cases hyp : DifferentiableAt 𝕜 f x
+  · let lCLM : F →L[𝕜] G := l
+    suffices shyp : partialDeriv 𝕜 v (lCLM ∘ f) x = (lCLM ∘ partialDeriv 𝕜 v f) x from by tauto
+    apply partialDeriv_compContLinAt
+    exact hyp
+  · unfold partialDeriv
+    rw [fderiv_zero_of_not_differentiableAt]
+    simp
+    rw [fderiv_zero_of_not_differentiableAt]
+    simp
+    exact hyp
+    rw [ContinuousLinearEquiv.comp_differentiableAt_iff]
+    exact hyp
+
+
 theorem partialDeriv_contDiff {n : ℕ} {f : E → F} (h : ContDiff 𝕜 (n + 1) f) : ∀ v : E, ContDiff 𝕜 n (partialDeriv 𝕜 v f) := by
   unfold partialDeriv
   intro v
@@ -84,6 +187,33 @@ theorem partialDeriv_contDiff {n : ℕ} {f : E → F} (h : ContDiff 𝕜 (n + 1)
   exact contDiff_const
 
 
+theorem partialDeriv_contDiffAt
+  {n : ℕ}
+  {f : E → F}
+  {x : E}
+  (h : ContDiffAt 𝕜 (n + 1) f x) :
+  ∀ v : E, ContDiffAt 𝕜 n (partialDeriv 𝕜 v f) x := by
+
+  unfold partialDeriv
+  intro v
+
+  let eval_at_v : (E →L[𝕜] F) →L[𝕜] F :=
+  {
+    toFun := fun l ↦ l v
+    map_add' := by simp
+    map_smul' := by simp
+  }
+
+  have : (fun w => (fderiv 𝕜 f w) v) = eval_at_v ∘ (fun w => (fderiv 𝕜 f w)) := by
+    rfl
+  rw [this]
+
+  apply ContDiffAt.continuousLinearMap_comp
+  -- ContDiffAt 𝕜 (↑n) (fun w => fderiv 𝕜 f w) x
+  apply ContDiffAt.fderiv_right h
+  rfl
+
+
 lemma partialDeriv_fderiv {f : E → F} (hf : ContDiff 𝕜 2 f) (z a b : E) :
     fderiv 𝕜 (fderiv 𝕜 f) z b a = partialDeriv 𝕜 b (partialDeriv 𝕜 a f) z := by
 
@@ -94,17 +224,100 @@ lemma partialDeriv_fderiv {f : E → F} (hf : ContDiff 𝕜 2 f) (z a b : E) :
   · simp
 
 
+lemma partialDeriv_fderivOn
+  {s : Set E}
+  {f : E → F}
+  (hs : IsOpen s)
+  (hf : ContDiffOn 𝕜 2 f s) (a b : E) :
+  ∀ z ∈ s, fderiv 𝕜 (fderiv 𝕜 f) z b a = partialDeriv 𝕜 b (partialDeriv 𝕜 a f) z := by
+
+  intro z hz
+  unfold partialDeriv
+  rw [fderiv_clm_apply]
+  · simp
+  · convert DifferentiableOn.differentiableAt _ (IsOpen.mem_nhds hs hz)
+    apply ContDiffOn.differentiableOn _ (Submonoid.oneLE.proof_2 ℕ∞)
+    exact ((contDiffOn_succ_iff_fderiv_of_isOpen hs).1 hf).2
+  · simp
+
+
+lemma partialDeriv_fderivAt
+  {z : E}
+  {f : E → F}
+  (hf : ContDiffAt 𝕜 2 f z)
+  (a b : E) :
+  fderiv 𝕜 (fderiv 𝕜 f) z b a = partialDeriv 𝕜 b (partialDeriv 𝕜 a f) z := by
+
+  unfold partialDeriv
+  rw [fderiv_clm_apply]
+  simp
+
+  -- DifferentiableAt 𝕜 (fun w => fderiv 𝕜 f w) z
+  obtain ⟨f', ⟨u, h₁u, h₂u⟩, hf' ⟩ := contDiffAt_succ_iff_hasFDerivAt.1 hf
+  have t₁ : (fun w ↦ fderiv 𝕜 f w) =ᶠ[nhds z] f' := by
+    apply Filter.eventuallyEq_iff_exists_mem.2
+    use u
+    constructor
+    · exact h₁u
+    · intro x hx
+      exact HasFDerivAt.fderiv (h₂u x hx)
+  rw [Filter.EventuallyEq.differentiableAt_iff t₁]
+  exact hf'.differentiableAt le_rfl
+
+  -- DifferentiableAt 𝕜 (fun w => a) z
+  exact differentiableAt_const a
+
+
 section restrictScalars
 
-variable (𝕜 : Type*) [NontriviallyNormedField 𝕜]
-variable {𝕜' : Type*} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜']
-variable {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E]
-variable [IsScalarTower 𝕜 𝕜' E]
-variable {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace 𝕜' F]
-variable [IsScalarTower 𝕜 𝕜' F]
---variable {f : E → F}
+theorem partialDeriv_smul'₂
+  (𝕜 : Type*) [NontriviallyNormedField 𝕜]
+  {𝕜' : Type*} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜']
+  {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
+  {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace 𝕜' F]
+  [IsScalarTower 𝕜 𝕜' F]
+  {f : E → F} {a : 𝕜'} {v : E} :
+  partialDeriv 𝕜 v (a • f) = a • partialDeriv 𝕜 v f := by
 
-theorem partialDeriv_restrictScalars {f : E → F} {v : E} :
+  funext w
+  by_cases ha : a = 0
+  · unfold partialDeriv
+    have : a • f = fun y ↦ a • f y := by rfl
+    rw [this, ha]
+    simp
+  · -- Now a is not zero. We present scalar multiplication with a as a continuous linear equivalence.
+    let smulCLM : F ≃L[𝕜] F :=
+    {
+      toFun := fun x ↦ a • x
+      map_add' := fun x y => DistribSMul.smul_add a x y
+      map_smul' := fun m x => (smul_comm ((RingHom.id 𝕜) m) a x).symm
+      invFun := fun x ↦ a⁻¹ • x
+      left_inv := by
+        intro x
+        simp
+        rw [← smul_assoc, smul_eq_mul, mul_comm, mul_inv_cancel ha, one_smul]
+      right_inv := by
+        intro x
+        simp
+        rw [← smul_assoc, smul_eq_mul, mul_inv_cancel ha, one_smul]
+      continuous_toFun := continuous_const_smul a
+      continuous_invFun := continuous_const_smul a⁻¹
+    }
+
+    have : a • f = smulCLM ∘ f := by tauto
+    rw [this]
+    rw [partialDeriv_compCLE]
+    tauto
+
+
+theorem partialDeriv_restrictScalars
+  (𝕜 : Type*) [NontriviallyNormedField 𝕜]
+  {𝕜' : Type*} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜']
+  {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E]
+  [IsScalarTower 𝕜 𝕜' E]
+  {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace 𝕜' F]
+  [IsScalarTower 𝕜 𝕜' F]
+  {f : E → F} {v : E} :
   Differentiable 𝕜' f → partialDeriv 𝕜 v f = partialDeriv 𝕜' v f := by
   intro hf
   unfold partialDeriv
@@ -140,3 +353,57 @@ theorem partialDeriv_comm
   rw [← partialDeriv_fderiv ℝ h z v₂ v₁]
   rw [derivSymm]
   rw [partialDeriv_fderiv ℝ h z v₁ v₂]
+
+
+theorem partialDeriv_commOn
+  {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
+  {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
+  {s : Set E}
+  {f : E → F}
+  (hs : IsOpen s)
+  (h : ContDiffOn ℝ 2 f s) :
+  ∀ v₁ v₂ : E, ∀ z ∈ s, partialDeriv ℝ v₁ (partialDeriv ℝ v₂ f) z = partialDeriv ℝ v₂ (partialDeriv ℝ v₁ f) z := by
+
+  intro v₁ v₂ z hz
+
+  have derivSymm :
+    (fderiv ℝ (fun w => fderiv ℝ f w) z) v₁ v₂ = (fderiv ℝ (fun w => fderiv ℝ f w) z) v₂ v₁ := by
+
+    let f' := fderiv ℝ f
+    have h₀1 : ∀ y ∈ s, HasFDerivAt f (f' y) y := by
+      intro y hy
+      apply DifferentiableAt.hasFDerivAt
+      apply DifferentiableOn.differentiableAt _ (IsOpen.mem_nhds hs hy)
+      apply h.differentiableOn one_le_two
+
+    let f'' := (fderiv ℝ f' z)
+    have h₁ : HasFDerivAt f' f'' z := by
+      apply DifferentiableAt.hasFDerivAt
+      apply DifferentiableOn.differentiableAt _ (IsOpen.mem_nhds hs hz)
+      apply ContDiffOn.differentiableOn _ (Submonoid.oneLE.proof_2 ℕ∞)
+      exact ((contDiffOn_succ_iff_fderiv_of_isOpen hs).1 h).2
+
+    have h₀' : ∀ᶠ (y : E) in nhds z, HasFDerivAt f (f' y) y := by
+      apply eventually_nhds_iff.mpr
+      use s
+
+    exact second_derivative_symmetric_of_eventually h₀' h₁ v₁ v₂
+
+  rw [← partialDeriv_fderivOn ℝ hs h v₂ v₁ z hz]
+  rw [derivSymm]
+  rw [← partialDeriv_fderivOn ℝ hs h v₁ v₂ z hz]
+
+
+theorem partialDeriv_commAt
+  {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
+  {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
+  {z : E}
+  {f : E → F}
+  (h : ContDiffAt ℝ 2 f z) :
+  ∀ v₁ v₂ : E, partialDeriv ℝ v₁ (partialDeriv ℝ v₂ f) z = partialDeriv ℝ v₂ (partialDeriv ℝ v₁ f) z := by
+
+  obtain ⟨u, hu₁, hu₂⟩ := h.contDiffOn le_rfl
+  obtain ⟨v, hv₁, hv₂, hv₃⟩ := mem_nhds_iff.1 hu₁
+
+  intro v₁ v₂
+  exact partialDeriv_commOn hv₂ (hu₂.mono hv₁) v₁ v₂ z hv₃

Nevanlinna/smulImprovement.lean

@@ -0,0 +1,40 @@
+import Mathlib.Analysis.Complex.CauchyIntegral
+--import Mathlib.Analysis.Complex.Module
+
+
+
+example simplificationTest₁
+  {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] [IsScalarTower ℝ ℂ E]
+  {v : E}
+  {z : ℂ} :
+  z • v =  z.re • v + Complex.I • z.im • v := by
+
+  /-
+  An attempt to write  "rw [add_smul]" will fail with "did not find instance of
+  the pattern in the target -- expression (?r + ?s) • ?x".
+  -/
+  sorry
+
+
+theorem add_smul'
+  (𝕜₁ : Type*) [NontriviallyNormedField ℝ]
+  {𝕜₂ : Type*} [NontriviallyNormedField ℂ] [NormedAlgebra ℝ ℂ]
+  {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] [IsScalarTower ℝ ℂ E]
+  {v : E}
+  {r s : ℂ} :
+  (r + s) • v = r • v + s • v :=
+  Module.add_smul r s v
+
+
+theorem smul_add' (a : M) (b₁ b₂ : A) : a • (b₁ + b₂) = a • b₁ + a • b₂ :=
+  DistribSMul.smul_add _ _ _
+#align smul_add smul_add
+
+
+
+
+example simplificationTest₂
+  {v : E}
+  {z : ℂ} :
+  z • v =  z.re • v + Complex.I • z.im • v := by
+  sorry