From a55b084031057a1b4f0c2bd26616648b15949e8b Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Fri, 3 May 2024 15:54:51 +0200 Subject: [PATCH] Update complexHarmonic.lean --- Nevanlinna/complexHarmonic.lean | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/Nevanlinna/complexHarmonic.lean b/Nevanlinna/complexHarmonic.lean index 176a71f..5a907c8 100644 --- a/Nevanlinna/complexHarmonic.lean +++ b/Nevanlinna/complexHarmonic.lean @@ -1,3 +1,4 @@ +import Mathlib.Data.Fin.Tuple.Basic import Mathlib.Analysis.Complex.Basic import Mathlib.Analysis.Complex.TaylorSeries import Mathlib.Analysis.Calculus.LineDeriv.Basic @@ -21,17 +22,18 @@ def Harmonic (f : ℂ → ℂ) : Prop := #check second_derivative_symmetric -lemma zwoDiff (f : ℝ × ℝ → ℝ) (h : ContDiff ℝ 2 f) : ∀ z a b : ℂ, 0 = 1 := by +lemma zwoDiff (f : ℝ × ℝ → ℝ) (h : ContDiff ℝ 2 f) : ∀ z a b : ℝ × ℝ, 0 = 1 := by intro z a b - let fx := fun w ↦ (fderiv ℝ f w) 1 - let fxx := fun w ↦ (fderiv ℝ fx w) 1 - let f2 := (fderiv ℝ (fun w => fderiv ℝ f w) z) 1 1 - - have : iteratedFDeriv ℝ (1 + 1) f = 0 := by - rw [iteratedFDeriv_succ_eq_comp_left] + let fx := fun w ↦ (fderiv ℝ f w) a + let fxx := fun w ↦ (fderiv ℝ fx w) a + let f2 := (fderiv ℝ (fun w => fderiv ℝ f w) z) a a + have : iteratedFDeriv ℝ 1 f z ![a] = 0 := by + rw [iteratedFDeriv_succ_apply_left] simp + let g := iteratedFDeriv ℝ 0 f + simp at g sorry have : f2 = fxx z := by