working…

Nevanlinna/complexHarmonic.lean

@@ -269,36 +269,26 @@ theorem holomorphicOn_is_harmonicOn {f : ℂ → F₁} {s : Set ℂ} (hs : IsOpe
     unfold Complex.laplace
     intro z hz
     simp
-    have : DifferentiableAt ℂ f z := by
+    have : ∀ z ∈ s, partialDeriv ℝ Complex.I f z = Complex.I • partialDeriv ℝ 1 f z := by
       sorry
-    let ZZ := h z hz
-    rw [CauchyRiemann₅ this]
+    have : partialDeriv ℝ Complex.I f =ᶠ[nhds z] Complex.I • partialDeriv ℝ 1 f := by
+      unfold Filter.EventuallyEq
+      unfold Filter.Eventually
+      simp
+      refine mem_nhds_iff.mpr ?_
+      use s
+      constructor
+      · intro x hx
+        simp
+        apply CauchyRiemann₅
+        apply DifferentiableOn.differentiableAt h
+        exact IsOpen.mem_nhds hs hx
+      · constructor
+        · exact hs
+        · exact hz
+    rw [partialDeriv_eventuallyEq ℝ this Complex.I]
+    rw [partialDeriv_smul'₂]
 
-    -- This lemma says that partial derivatives commute with complex scalar
-    -- multiplication. This is a consequence of partialDeriv_compContLin once we
-    -- note that complex scalar multiplication is continuous ℝ-linear.
-    have : ∀ v, ∀ s : ℂ, ∀ g : ℂ → F₁, Differentiable ℝ g → partialDeriv ℝ v (s • g) = s • (partialDeriv ℝ v g) := by
-      intro v s g hg
-
-      -- Present scalar multiplication as a continuous ℝ-linear map. This is
-      -- horrible, there must be better ways to do that.
-      let sMuls : F₁ →L[ℝ] F₁ :=
-      {
-        toFun := fun x ↦ s • x
-        map_add' := by exact fun x y => DistribSMul.smul_add s x y
-        map_smul' := by exact fun m x => (smul_comm ((RingHom.id ℝ) m) s x).symm
-        cont := continuous_const_smul s
-      }
-
-      -- Bring the goal into a form that is recognized by
-      -- partialDeriv_compContLin.
-      have : s • g = sMuls ∘ g := by rfl
-      rw [this]
-
-      rw [partialDeriv_compContLin ℝ hg]
-      rfl
-
-    rw [this]
     rw [partialDeriv_comm f_is_real_C2 Complex.I 1]
     rw [CauchyRiemann₄ h]
     rw [this]
@@ -399,7 +389,6 @@ theorem log_normSq_of_holomorphicOn_is_harmonicOn
   exact h₁ z
 
 
-
 theorem log_normSq_of_holomorphic_is_harmonic
   {f : ℂ → ℂ}
   (h₁ : Differentiable ℂ f)

Nevanlinna/laplace.lean

@@ -94,7 +94,7 @@ theorem laplace_add_ContDiffOn
   rw [add_comm]
 
 
-theorem laplace_smul {f : ℂ → F} (h : ContDiff ℝ 2 f) : ∀ v : ℝ, Complex.laplace (v • f) = v • (Complex.laplace f) := by
+theorem laplace_smul {f : ℂ → F} : ∀ v : ℝ, Complex.laplace (v • f) = v • (Complex.laplace f) := by
   intro v
   unfold Complex.laplace
   rw [partialDeriv_smul₂]
@@ -103,11 +103,6 @@ theorem laplace_smul {f : ℂ → F} (h : ContDiff ℝ 2 f) : ∀ v : ℝ, Compl
   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_compContLin {f : ℂ → F} {l : F →L[ℝ] G} (h : ContDiff ℝ 2 f) :
   Complex.laplace (l ∘ f) = l ∘ (Complex.laplace f) := by

Nevanlinna/partialDeriv.lean

@@ -30,16 +30,30 @@ 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
@@ -59,8 +73,7 @@ theorem partialDeriv_add₂_differentiableAt
   {v : E}
   {x : E}
   (h₁ : DifferentiableAt 𝕜 f₁ x)
-  (h₂ : DifferentiableAt 𝕜 f₂ x)
-  :
+  (h₂ : DifferentiableAt 𝕜 f₂ x) :
   partialDeriv 𝕜 v (f₁ + f₂) x = (partialDeriv 𝕜 v f₁) x + (partialDeriv 𝕜 v f₂) x := by
 
   unfold partialDeriv
@@ -88,6 +101,23 @@ theorem partialDeriv_compContLinAt {f : E → F} {l : F →L[𝕜] G} {v : E} {x
   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
@@ -155,15 +185,54 @@ theorem partialDeriv_eventuallyEq' {f₁ f₂ : E → F} {x : E} (h : f₁ =ᶠ[
 
 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