Merge branch 'main' of git.cplx.vm.uni-freiburg.de:kebekus/nevanlinna

nevanlinna/cauchyRiemann.lean

@@ -1,49 +1,40 @@
-import Mathlib.Analysis.Calculus.Conformal.NormedSpace
-import Mathlib.Analysis.Calculus.ContDiff.Basic
-import Mathlib.Analysis.Calculus.ContDiff.Defs
-import Mathlib.Analysis.Calculus.Deriv.Linear
-import Mathlib.Analysis.Calculus.FDeriv.Basic
-import Mathlib.Analysis.Calculus.FDeriv.RestrictScalars
 import Mathlib.Analysis.Calculus.LineDeriv.Basic
-import Mathlib.Analysis.Complex.Basic
-import Mathlib.Analysis.Complex.CauchyIntegral
-import Mathlib.Analysis.Complex.Conformal
 import Mathlib.Analysis.Complex.RealDeriv
 
 variable {z : ℂ} {f : ℂ → ℂ}
 
-example (h : DifferentiableAt ℂ f z) : f z = 0 := by
+theorem CauchyRiemann₁ : (DifferentiableAt ℂ f z)
+  → (fderiv ℝ f z) Complex.I = Complex.I * (fderiv ℝ f z) 1 := by
+  intro h
+  rw [DifferentiableAt.fderiv_restrictScalars ℝ h]
+  nth_rewrite 1 [← mul_one Complex.I]
+  exact ContinuousLinearMap.map_smul_of_tower (fderiv ℂ f z) Complex.I 1
 
-  let A := fderiv ℂ f z
-  let B := fderiv ℝ f
+theorem CauchyRiemann₂ : (DifferentiableAt ℂ f z)
+  → lineDeriv ℝ f z Complex.I = Complex.I * lineDeriv ℝ f z 1 := by
+  intro h
+  rw [DifferentiableAt.lineDeriv_eq_fderiv (h.restrictScalars ℝ)]
+  rw [DifferentiableAt.lineDeriv_eq_fderiv (h.restrictScalars ℝ)]
+  exact CauchyRiemann₁ h
 
-  let C : HasFDerivAt f (ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ f z)) z := h.hasFDerivAt.restrictScalars ℝ
-  let D := ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ f z)
-  let E := D 1
-  let F := D Complex.I
+theorem CauchyRiemann₃ : (DifferentiableAt ℂ f z)
+  → (lineDeriv ℝ (Complex.reCLM ∘ f) z 1 = lineDeriv ℝ (Complex.imCLM ∘ f) z Complex.I)
+    ∧ (lineDeriv ℝ (Complex.reCLM ∘ f) z Complex.I = -lineDeriv ℝ (Complex.imCLM ∘ f) z 1)
+   := by
 
-  have : A (Complex.I • 1) = Complex.I • (A 1) := by
-    exact ContinuousLinearMap.map_smul_of_tower A Complex.I 1
+  intro h
 
-  let AR := (ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ f z))
-  have : AR (Complex.I • 1) = Complex.I • (AR 1) := by
-    exact this
+  have ContinuousLinearMap.comp_lineDeriv : ∀ w : ℂ, ∀ l : ℂ →L[ℝ] ℝ, lineDeriv ℝ (l ∘ f) z w = l ((fderiv ℝ f z) w) := by
+    intro w l
+    rw [DifferentiableAt.lineDeriv_eq_fderiv]
+    rw [fderiv.comp]
+    simp
+    fun_prop
+    exact h.restrictScalars ℝ
+    apply (ContinuousLinearMap.differentiableAt l).comp
+    exact h.restrictScalars ℝ
 
-  let f₂ := fun x ↦ lineDeriv ℝ f x ⟨0,1⟩
-  have : lineDeriv ℝ f z Complex.I = (fderiv ℝ f z) Complex.I := by
-    apply DifferentiableAt.lineDeriv_eq_fderiv
-    apply h.restrictScalars ℝ
-
-  have : D Complex.I = Complex.I * (D 1) := by
-    -- x
-
-    sorry
-
-  have : HasFDerivAt f A z := by
-    exact DifferentiableAt.hasFDerivAt h
-
-  have : HasFDerivAt f (B z) z := by
-    sorry
-
-
-  sorry
+  repeat
+    rw [ContinuousLinearMap.comp_lineDeriv]
+  rw [CauchyRiemann₁ h, Complex.I_mul]
+  simp