60 lines
2.3 KiB
Lean4
60 lines
2.3 KiB
Lean4
import Mathlib.Data.Fin.Tuple.Basic
|
||
import Mathlib.Analysis.Complex.Basic
|
||
import Mathlib.Analysis.Complex.TaylorSeries
|
||
import Mathlib.Analysis.Calculus.LineDeriv.Basic
|
||
import Mathlib.Analysis.Calculus.ContDiff.Defs
|
||
import Mathlib.Analysis.Calculus.FDeriv.Basic
|
||
import Mathlib.Analysis.Calculus.FDeriv.Symmetric
|
||
import Mathlib.Data.Complex.Module
|
||
import Mathlib.Data.Complex.Order
|
||
import Mathlib.Data.Complex.Exponential
|
||
import Mathlib.Analysis.RCLike.Basic
|
||
import Mathlib.Topology.Algebra.InfiniteSum.Module
|
||
import Mathlib.Topology.Instances.RealVectorSpace
|
||
import Nevanlinna.cauchyRiemann
|
||
import Nevanlinna.partialDeriv
|
||
|
||
variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
|
||
|
||
|
||
noncomputable def Complex.laplace : (ℂ → F) → (ℂ → F) :=
|
||
fun f ↦ partialDeriv ℝ 1 (partialDeriv ℝ 1 f) + partialDeriv ℝ Complex.I (partialDeriv ℝ Complex.I f)
|
||
|
||
|
||
theorem laplace_add {f₁ f₂ : ℂ → F} (h₁ : ContDiff ℝ 2 f₁) (h₂ : ContDiff ℝ 2 f₂): Complex.laplace (f₁ + f₂) = (Complex.laplace f₁) + (Complex.laplace f₂) := by
|
||
unfold Complex.laplace
|
||
rw [partialDeriv_add₂]
|
||
rw [partialDeriv_add₂]
|
||
rw [partialDeriv_add₂]
|
||
rw [partialDeriv_add₂]
|
||
exact
|
||
add_add_add_comm (partialDeriv ℝ 1 (partialDeriv ℝ 1 f₁))
|
||
(partialDeriv ℝ 1 (partialDeriv ℝ 1 f₂))
|
||
(partialDeriv ℝ Complex.I (partialDeriv ℝ Complex.I f₁))
|
||
(partialDeriv ℝ Complex.I (partialDeriv ℝ Complex.I f₂))
|
||
|
||
exact (partialDeriv_contDiff ℝ h₁ Complex.I).differentiable le_rfl
|
||
exact (partialDeriv_contDiff ℝ h₂ Complex.I).differentiable le_rfl
|
||
exact h₁.differentiable one_le_two
|
||
exact h₂.differentiable one_le_two
|
||
exact (partialDeriv_contDiff ℝ h₁ 1).differentiable le_rfl
|
||
exact (partialDeriv_contDiff ℝ h₂ 1).differentiable le_rfl
|
||
exact h₁.differentiable one_le_two
|
||
exact h₂.differentiable one_le_two
|
||
|
||
|
||
|
||
theorem laplace_smul {f : ℂ → F} (h : ContDiff ℝ 2 f) : ∀ v : ℝ, Complex.laplace (v • f) = v • (Complex.laplace f) := by
|
||
intro v
|
||
unfold Complex.laplace
|
||
rw [partialDeriv_smul₂]
|
||
rw [partialDeriv_smul₂]
|
||
rw [partialDeriv_smul₂]
|
||
rw [partialDeriv_smul₂]
|
||
simp
|
||
|
||
exact (partialDeriv_contDiff ℝ h Complex.I).differentiable le_rfl
|
||
exact h.differentiable one_le_two
|
||
exact (partialDeriv_contDiff ℝ h 1).differentiable le_rfl
|
||
exact h.differentiable one_le_two
|