Minor cleanup

Nevanlinna/holomorphic_examples.lean

@@ -1,17 +1,18 @@
 import Nevanlinna.complexHarmonic
 import Nevanlinna.holomorphicAt
 import Nevanlinna.holomorphic_primitive
+import Nevanlinna.mathlibAddOn
 
 
 theorem CauchyRiemann₆
-  {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] 
+  {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]
-  {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] 
+  {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F]
   {f : E → F}
-  {z : E} : 
+  {z : E} :
   (DifferentiableAt ℂ f z) ↔ (DifferentiableAt ℝ f z) ∧ ∀ e, partialDeriv ℝ (Complex.I • e) f z = Complex.I • partialDeriv ℝ e f z := by
   constructor
 
-  · -- Direction "→" 
+  · -- Direction "→"
     intro h
     constructor
     · exact DifferentiableAt.restrictScalars ℝ h
@@ -30,7 +31,7 @@ theorem CauchyRiemann₆
         rw [DifferentiableAt.fderiv_restrictScalars ℝ h]
       simp
 
-  · -- Direction "←" 
+  · -- Direction "←"
     intro ⟨h₁, h₂⟩
     apply (differentiableAt_iff_restrictScalars ℝ h₁).2
 
@@ -52,9 +53,9 @@ theorem CauchyRiemann₆
 
 
 theorem CauchyRiemann₇
-  {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] 
+  {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F]
   {f : ℂ → F}
-  {z : ℂ} : 
+  {z : ℂ} :
   (DifferentiableAt ℂ f z) ↔ (DifferentiableAt ℝ f z) ∧ partialDeriv ℝ Complex.I f z = Complex.I • partialDeriv ℝ 1 f z := by
   constructor
   · intro hf
@@ -68,7 +69,7 @@ theorem CauchyRiemann₇
     constructor
     · exact h₁
     · intro e
-      have : Complex.I • e = e • Complex.I := by 
+      have : Complex.I • e = e • Complex.I := by
         rw [smul_eq_mul, smul_eq_mul]
         exact CommMonoid.mul_comm Complex.I e
       rw [this]
@@ -94,12 +95,14 @@ theorem CauchyRiemann₇
       have : - (e.im : ℂ) = (-e.im : ℝ) • (1 : ℂ) := by simp
       rw [this, partialDeriv_smul₁ ℝ]
       simp
-  
+
+
 
 
 /-
 
-A harmonic, real-valued function on ℂ is the real part of a suitable holomorphic function.
+A harmonic, real-valued function on ℂ is the real part of a suitable holomorphic
+function.
 
 -/
 
@@ -114,34 +117,32 @@ theorem harmonic_is_realOfHolomorphic
   let g : ℂ → ℂ := f_1 - Complex.I • f_I
 
   have reg₂f : ContDiff ℝ 2 f := by
-    apply contDiff_iff_contDiffAt.mpr 
+    apply contDiff_iff_contDiffAt.mpr
     intro z
     exact (hf z).1
 
   have reg₁f_1 : ContDiff ℝ 1 f_1 := by
-    apply contDiff_iff_contDiffAt.mpr 
+    apply contDiff_iff_contDiffAt.mpr
     intro z
     dsimp [f_1]
     apply ContDiffAt.continuousLinearMap_comp
     exact partialDeriv_contDiffAt ℝ (hf z).1 1
 
   have reg₁f_I : ContDiff ℝ 1 f_I := by
-    apply contDiff_iff_contDiffAt.mpr 
+    apply contDiff_iff_contDiffAt.mpr
     intro z
     dsimp [f_I]
     apply ContDiffAt.continuousLinearMap_comp
     exact partialDeriv_contDiffAt ℝ (hf z).1 Complex.I
 
-  have reg₁g : ContDiff ℝ 1 g := by 
+  have reg₁g : ContDiff ℝ 1 g := by
     dsimp [g]
     apply ContDiff.sub
     exact reg₁f_1
-    have : Complex.I • f_I = fun x ↦ Complex.I • f_I x := rfl
+    apply ContDiff.const_smul'
-    rw [this]
-    apply ContDiff.const_smul
     exact reg₁f_I
-  
+
-  have reg₁ : Differentiable ℂ g := by 
+  have reg₁ : Differentiable ℂ g := by
     intro z
     apply CauchyRiemann₇.2
     constructor
@@ -174,33 +175,29 @@ theorem harmonic_is_realOfHolomorphic
 
       --Differentiable ℝ (partialDeriv ℝ _ f)
       repeat
-        apply ContDiff.differentiable 
+        apply ContDiff.differentiable
-        apply contDiff_iff_contDiffAt.mpr 
+        apply contDiff_iff_contDiffAt.mpr
         exact fun w ↦ partialDeriv_contDiffAt ℝ (hf w).1 _
         apply le_rfl
       -- Differentiable ℝ f_1
       exact reg₁f_1.differentiable le_rfl
       -- Differentiable ℝ (Complex.I • f_I)
-      have : Complex.I • f_I = fun x ↦ Complex.I • f_I x := rfl
+      apply Differentiable.const_smul'
-      rw [this]
-      apply Differentiable.const_smul
       exact reg₁f_I.differentiable le_rfl
       -- Differentiable ℝ f_1
       exact reg₁f_1.differentiable le_rfl
       -- Differentiable ℝ (Complex.I • f_I)
-      have : Complex.I • f_I = fun x ↦ Complex.I • f_I x := rfl
+      apply Differentiable.const_smul'
-      rw [this]
-      apply Differentiable.const_smul
       exact reg₁f_I.differentiable le_rfl
-  
+
   let F := fun z ↦ (primitive 0 g) z + f 0
 
-  have regF : Differentiable ℂ F := by 
+  have regF : Differentiable ℂ F := by
     apply Differentiable.add
     apply primitive_differentiable reg₁
     simp
 
-  have pF'' : ∀ x, (fderiv ℝ F x) = ContinuousLinearMap.lsmul ℝ ℂ (g x) := by 
+  have pF'' : ∀ x, (fderiv ℝ F x) = ContinuousLinearMap.lsmul ℝ ℂ (g x) := by
     intro x
     rw [DifferentiableAt.fderiv_restrictScalars ℝ (regF x)]
     dsimp [F]
@@ -223,11 +220,11 @@ theorem harmonic_is_realOfHolomorphic
         exact regF w
   · -- (F z).re = f z
     have A := reg₂f.differentiable one_le_two
-    have B : Differentiable ℝ (Complex.reCLM ∘ F) := by 
+    have B : Differentiable ℝ (Complex.reCLM ∘ F) := by
       apply Differentiable.comp
       exact ContinuousLinearMap.differentiable Complex.reCLM
       exact Differentiable.restrictScalars ℝ regF
-    have C : (F 0).re = f 0 := by 
+    have C : (F 0).re = f 0 := by
       dsimp [F]
       rw [primitive_zeroAtBasepoint]
       simp
@@ -251,6 +248,5 @@ theorem harmonic_is_realOfHolomorphic
     ring
     -- DifferentiableAt ℝ (⇑Complex.reCLM) (F x)
     fun_prop
-    -- DifferentiableAt ℝ F x    
+    -- DifferentiableAt ℝ F x
     exact regF.restrictScalars ℝ x
-

Nevanlinna/mathlibAddOn.lean

@@ -0,0 +1,35 @@
+import Mathlib.Analysis.Calculus.ContDiff.Basic
+import Mathlib.Analysis.Calculus.FDeriv.Add
+
+variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
+variable {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
+variable {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
+variable {G : Type*} [NormedAddCommGroup G] [NormedSpace 𝕜 G]
+variable {G' : Type*} [NormedAddCommGroup G'] [NormedSpace 𝕜 G']
+variable {f f₀ f₁ g : E → F}
+variable {f' f₀' f₁' g' : E →L[𝕜] F}
+variable (e : E →L[𝕜] F)
+variable {x : E}
+variable {s t : Set E}
+variable {L L₁ L₂ : Filter E}
+
+variable {R : Type*} [Semiring R] [Module R F] [SMulCommClass 𝕜 R F] [ContinuousConstSMul R F]
+
+
+-- import Mathlib.Analysis.Calculus.FDeriv.Add
+
+@[fun_prop]
+theorem Differentiable.const_smul' (h : Differentiable 𝕜 f) (c : R) :
+    Differentiable 𝕜 (c • f) := by
+  have : c • f = fun x ↦ c • f x := rfl
+  rw [this]
+  exact Differentiable.const_smul h c
+
+
+-- Mathlib.Analysis.Calculus.ContDiff.Basic
+
+theorem ContDiff.const_smul' {f : E → F} (c : R) (hf : ContDiff 𝕜 n f) :
+    ContDiff 𝕜 n (c • f) := by
+  have : c • f = fun x ↦ c • f x := rfl
+  rw [this]
+  exact ContDiff.const_smul c hf