kebekus
/
nevanlinna
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Update laplace.lean

This commit is contained in:
Stefan Kebekus 2024-05-30 10:05:13 +02:00
parent f480ae2a0f
commit 47ab90446f
1 changed files with 4 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
Nevanlinna/laplace.lean
View File

@ -106,13 +106,12 @@ theorem laplace_compContLinAt {f : ℂ → F} {l : F →L[ℝ] G} {x : ℂ} (h :
simp simp
-- DifferentiableAt ℝ (partialDeriv ℝ Complex.I f) x -- DifferentiableAt ℝ (partialDeriv ℝ Complex.I f) x
unfold partialDeriv apply ContDiffAt.differentiableAt (partialDeriv_contDiffAt ℝ (ContDiffOn.contDiffAt hv₄ hv₁) Complex.I)
rfl
sorry
-- DifferentiableAt ℝ (partialDeriv ℝ 1 f) x -- DifferentiableAt ℝ (partialDeriv ℝ 1 f) x
apply ContDiffAt.differentiableAt (partialDeriv_contDiffAt ℝ (ContDiffOn.contDiffAt hv₄ hv₁) 1)
sorry rfl
theorem laplace_compCLE {f : ℂ → F} {l : F ≃L[ℝ] G} (h : ContDiff ℝ 2 f) : theorem laplace_compCLE {f : ℂ → F} {l : F ≃L[ℝ] G} (h : ContDiff ℝ 2 f) :