Nevanlinna/cauchyRiemann.lean

@@ -44,10 +44,8 @@ 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
 
@@ -64,21 +62,3 @@ theorem CauchyRiemann₄
     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,4 +1,20 @@
+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₁]
@@ -7,57 +23,11 @@ variable {G₁ : Type*} [NormedAddCommGroup G₁] [NormedSpace ℂ G₁] [Comple
 
 
 def Harmonic (f : ℂ → F) : Prop :=
-  (ContDiff ℝ 2 f) ∧ (∀ z, Δ f z = 0)
+  (ContDiff ℝ 2 f) ∧ (∀ z, Complex.laplace 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, Δ 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
+  (ContDiffOn ℝ 2 f s) ∧ (∀ z ∈ s, Complex.laplace f z = 0)
 
 
 theorem HarmonicOn_of_locally_HarmonicOn {f : ℂ → F} {s : Set ℂ} (h : ∀ x ∈ s, ∃ (u : Set ℂ), IsOpen u ∧ x ∈ u ∧ HarmonicOn f (s ∩ u)) :
@@ -73,50 +43,6 @@ 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
@@ -128,55 +54,17 @@ 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]
+  · rw [laplace_smul h.1]
     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
@@ -185,18 +73,6 @@ 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
 
@@ -205,7 +81,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_compCLM]
+  · rw [laplace_compContLin]
     simp
     intro z
     rw [h.2 z]
@@ -213,55 +89,19 @@ 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} (hs : IsOpen s) (h : HarmonicOn f s) :
+theorem harmonicOn_comp_CLM_is_harmonicOn {f : ℂ → F₁} {s : Set ℂ} {l : F₁ →L[ℝ] G} (h : HarmonicOn f s) :
   HarmonicOn (l ∘ f) s := by
 
   constructor
   · -- Continuous differentiability
     apply ContDiffOn.continuousLinearMap_comp
     exact h.1
-  · -- Vanishing of Laplace
-    intro z zHyp
-    rw [laplace_compCLMAt]
+  · rw [laplace_compContLin]
     simp
+    intro z zHyp
     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₁} :
@@ -279,34 +119,222 @@ theorem harmonic_iff_comp_CLE_is_harmonic {f : ℂ → F₁} {l : F₁ ≃L[ℝ]
     exact harmonic_comp_CLM_is_harmonic
 
 
-theorem harmonicAt_iff_comp_CLE_is_harmonicAt
-  {f : ℂ → F₁}
-  {z : ℂ}
-  {l : F₁ ≃L[ℝ] G₁} :
-  HarmonicAt f z ↔ HarmonicAt (l ∘ f) z := by
+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 ℕ∞)
 
   constructor
-  · have : l ∘ f = (l : F₁ →L[ℝ] G₁) ∘ f := by rfl
+  · -- 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
       rw [this]
-    exact harmonicAt_comp_CLM_is_harmonicAt
-  · have : f = (l.symm : G₁ →L[ℝ] F₁) ∘ l ∘ f := by
-      funext z
-      unfold Function.comp
+
+      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
-    nth_rewrite 2 [this]
-    exact harmonicAt_comp_CLM_is_harmonicAt
+
+    -- 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 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
+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
+      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
-  · have : l ∘ f = (l : F₁ →L[ℝ] G₁) ∘ f := by rfl
+    · exact Real.pi_pos
+    · exact Real.pi_nonneg
+    exact (AddEquivClass.map_ne_zero_iff starRingAut).mpr (h₂ z)
+    exact h₂ z
   rw [this]
-    exact harmonicOn_comp_CLM_is_harmonicOn hs
-  · have : f = (l.symm : G₁ →L[ℝ] F₁) ∘ l ∘ f := by
+
+  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 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
-    nth_rewrite 2 [this]
-    exact harmonicOn_comp_CLM_is_harmonicOn hs
+      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₃

Nevanlinna/harmonicAt.examples.lean

@@ -1,211 +0,0 @@
-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

@@ -1,161 +0,0 @@
-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

@@ -1,518 +0,0 @@
-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

@@ -1,147 +0,0 @@
-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,36 +1,28 @@
+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) : ℂ → F :=
-  partialDeriv ℝ 1 (partialDeriv ℝ 1 f) + partialDeriv ℝ Complex.I (partialDeriv ℝ Complex.I f)
-
-notation "Δ" => Complex.laplace
+noncomputable def Complex.laplace : (ℂ → F) → (ℂ → F) :=
+  fun f ↦ partialDeriv ℝ 1 (partialDeriv ℝ 1 f) + partialDeriv ℝ Complex.I (partialDeriv ℝ Complex.I f)
 
 
-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
-
+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
   unfold Complex.laplace
   rw [partialDeriv_add₂]
   rw [partialDeriv_add₂]
@@ -52,225 +44,39 @@ theorem laplace_add
   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, Δ (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
+theorem laplace_smul {f : ℂ → F} (h : ContDiff ℝ 2 f) : ∀ v : ℝ, Complex.laplace (v • f) = v • (Complex.laplace f) := by
   intro v
   unfold Complex.laplace
-  repeat
+  rw [partialDeriv_smul₂]
+  rw [partialDeriv_smul₂]
+  rw [partialDeriv_smul₂]
   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
 
-  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
+  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_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
+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

Nevanlinna/partialDeriv.lean

@@ -1,8 +1,6 @@
 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 𝕜]
@@ -16,28 +14,6 @@ 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 =>
@@ -54,35 +30,21 @@ theorem partialDeriv_add₁ {f : E → F} {v₁ v₂ : E} : partialDeriv 𝕜 (v
     rw [map_add]
 
 
-theorem partialDeriv_smul₂ {f : E → F} {a : 𝕜} {v : E} : partialDeriv 𝕜 v (a • f) = a • partialDeriv 𝕜 v f := by
+theorem partialDeriv_smul₂ {f : E → F} {a : 𝕜} {v : E} (h : Differentiable 𝕜 f) : 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]
-  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
+
+  conv =>
+    left
+    intro w
+    rw [fderiv_const_smul (h w)]
 
 
-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
+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
   unfold partialDeriv
-  intro v
+
   have : f₁ + f₂ = fun y ↦ f₁ y + f₂ y := by rfl
   rw [this]
   conv =>
@@ -92,49 +54,7 @@ theorem partialDeriv_add₂ {f₁ f₂ : E → F} (h₁ : Differentiable 𝕜 f
     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_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
+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 =>
@@ -146,29 +66,6 @@ theorem partialDeriv_compContLin
   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
@@ -187,33 +84,6 @@ 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
 
@@ -224,100 +94,17 @@ 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
 
-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
+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}
 
-  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} :
+theorem partialDeriv_restrictScalars {f : E → F} {v : E} :
   Differentiable 𝕜' f → partialDeriv 𝕜 v f = partialDeriv 𝕜' v f := by
   intro hf
   unfold partialDeriv
@@ -353,57 +140,3 @@ 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

@@ -1,40 +0,0 @@
-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