experimenting…

nevanlinna/harmonic.lean

@@ -2,23 +2,57 @@ import Mathlib.Analysis.Complex.Basic
 import Mathlib.Analysis.Calculus.LineDeriv.Basic
 import Mathlib.Analysis.SpecialFunctions.ExpDeriv
 import Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
+import Mathlib.Analysis.Calculus.ContDiff.Basic
+import Mathlib.Analysis.Calculus.Deriv.Linear
+import Mathlib.Analysis.Complex.Conformal
+import Mathlib.Analysis.Calculus.Conformal.NormedSpace
+import Mathlib.Analysis.Complex.RealDeriv
 
+/RealDeriv.lean
 -- Harmonic functions on the plane
 
+variable {f : ℂ → ℂ} {e' : ℂ} {z : ℝ} {h : HasDerivAt f e' z}
 
-noncomputable def laplace' : (ℂ → ℝ) → (ℂ → ℝ) := by
+ example : 1 = 0 := by
-  intro f
 
-  let f₁ := fun x ↦ lineDeriv ℝ f x 1
+  let XX := HasDerivAt.real_of_complex h
-  let f₁₁ := fun x ↦ lineDeriv ℝ f₁ x 1
+  sorry
-  let f₂ := fun x ↦ lineDeriv ℝ f x Complex.I
-  let f₂₂ := fun x ↦ lineDeriv ℝ f₂ x Complex.I
-  exact f₁₁ + f₂₂
 
-example : laplace' (fun z ↦ z.re) = fun z ↦ 0 := by
 
-  unfold laplace' lineDeriv  
+noncomputable def lax (f : ℂ → ℝ) (z : ℂ) : ℝ :=
+  iteratedFDeriv ℝ 1 f z ![Complex.I]
+
+example : lax (fun z ↦ z.re) = fun z ↦ 1 := by
+  unfold lax
   simp
+  funext x
+  
+  let XX := HasDerivAt.real_of_complex 
+
+  sorry
+
+
+noncomputable def laplace (f : ℂ → ℝ) (z : ℂ) : ℝ :=
+  iteratedFDeriv ℝ 2 f z ![1, 1] + iteratedFDeriv ℝ 2 f z ![Complex.I, Complex.I]
+
+
+example : laplace (fun z ↦ z.re) = fun z ↦ 0 := by
+  
+  unfold laplace
+  rw [iteratedFDeriv_succ_eq_comp_left]
+  rw [iteratedFDeriv_succ_eq_comp_left]
+  rw [iteratedFDeriv_zero_eq_comp]
+  simp
+
+  have : Fin.tail ![Complex.I, Complex.I] = ![Complex.I] := by
+    rfl
+  rw [this]
+
+  rw [deriv_comp]
+  
+  simp
+  simp
+
 
   conv =>
     lhs
@@ -83,6 +117,60 @@ example : laplace' (fun z ↦ (z*z).re) = fun z ↦ 0 := by
 
   group
 
+open Complex ContinuousLinearMap
+
+open scoped ComplexConjugate
+
+variable {z : ℂ} {f : ℂ → ℂ}
+
+#check deriv_comp_const_add
+
+theorem DifferentiableAt_conformalAt (h : DifferentiableAt ℂ f z) :
+    ConformalAt f z := by
+
+  let XX := (h.hasFDerivAt.restrictScalars ℝ).fderiv
+
+  let f₁ := fun x ↦ lineDeriv ℝ f x 1
+  let f₂ := fun x ↦ lineDeriv ℝ f x Complex.I
+
+  have t₁ : deriv (fun (t : ℂ) => f (z + t)) 0 = deriv f z := by
+    rw [deriv_comp_const_add]
+    simp
+    simp
+    exact h
+  have t'₁ : deriv (fun (t : ℝ) => f (z + ↑t)) 0 = deriv f z := by
+    sorry
+
+  have : f₁ z = deriv f z := by
+    dsimp [f₁]
+    unfold lineDeriv
+    simp
+    exact t'₁
+
+  have : f₂ z = deriv f z := by
+    dsimp [f₂]
+    unfold lineDeriv
+    simp
+
+    exact t'₁
+
+
+  /-
+  simp at f₂
+
+  rw [conformalAt_iff_isConformalMap_fderiv, (h.hasFDerivAt.restrictScalars ℝ).fderiv]
+  apply isConformalMap_complex_linear
+  simpa only [Ne, ext_ring_iff]
+  -/
+
+example : laplace' (fun z ↦ (Complex.exp z).re) = fun z ↦ 0 := by
+
+  let f := fun z ↦ (Complex.exp z).re
+  let f₁ := fun x ↦ lineDeriv ℝ f x 1
+  let fz := fun x ↦ deriv f
+
+
+
 example : laplace' (fun z ↦ (Complex.exp z).re) = fun z ↦ 0 := by
   
   unfold laplace' lineDeriv  
@@ -157,8 +245,16 @@ example : laplace' (fun z ↦ (Complex.exp z).re) = fun z ↦ 0 := by
     intro x
     lhs
     intro t
-    
     simp
+    rw [deriv_sub] <;> tactic => try fun_prop
+    rw [deriv_mul] <;> tactic => try fun_prop
+    rw [deriv_mul] <;> tactic => try fun_prop
+    simp
+
+
+      
+
+    
     
   
 

nevanlinna/realHarmonic.lean

@@ -0,0 +1,10 @@
+import Mathlib.Analysis.Calculus.LineDeriv.Basic
+
+noncomputable def Real.laplace : (R [× n] → ℝ) → (ℂ → ℝ) := by
+  intro f
+
+  let f₁ := fun x ↦ lineDeriv ℝ f x 1
+  let f₁₁ := fun x ↦ lineDeriv ℝ f₁ x 1
+  let f₂ := fun x ↦ lineDeriv ℝ f x Complex.I
+  let f₂₂ := fun x ↦ lineDeriv ℝ f₂ x Complex.I
+  exact f₁₁ + f₂₂