143 lines
5.3 KiB
Plaintext
143 lines
5.3 KiB
Plaintext
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.Order.Filter.Basic
|
||
import Mathlib.Topology.Algebra.InfiniteSum.Module
|
||
import Mathlib.Topology.Basic
|
||
import Mathlib.Topology.Instances.RealVectorSpace
|
||
import Nevanlinna.cauchyRiemann
|
||
import Nevanlinna.partialDeriv
|
||
|
||
variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
|
||
variable {G : Type*} [NormedAddCommGroup G] [NormedSpace ℝ G]
|
||
|
||
|
||
noncomputable def Complex.laplace : (ℂ → F) → (ℂ → F) :=
|
||
fun f ↦ partialDeriv ℝ 1 (partialDeriv ℝ 1 f) + partialDeriv ℝ Complex.I (partialDeriv ℝ Complex.I f)
|
||
|
||
|
||
theorem laplace_eventuallyEq {f₁ f₂ : ℂ → F} {x : ℂ} (h : f₁ =ᶠ[nhds x] f₂) : Complex.laplace f₁ x = Complex.laplace f₂ x := by
|
||
unfold Complex.laplace
|
||
simp
|
||
rw [partialDeriv_eventuallyEq ℝ (partialDeriv_eventuallyEq' ℝ h 1) 1]
|
||
rw [partialDeriv_eventuallyEq ℝ (partialDeriv_eventuallyEq' ℝ h Complex.I) Complex.I]
|
||
|
||
|
||
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
|
||
|
||
|
||
theorem laplace_compContLin {f : ℂ → F} {l : F →L[ℝ] G} (h : ContDiff ℝ 2 f) :
|
||
Complex.laplace (l ∘ f) = l ∘ (Complex.laplace f) := by
|
||
unfold Complex.laplace
|
||
rw [partialDeriv_compContLin]
|
||
rw [partialDeriv_compContLin]
|
||
rw [partialDeriv_compContLin]
|
||
rw [partialDeriv_compContLin]
|
||
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
|
||
|
||
|
||
theorem laplace_compContLinAt {f : ℂ → F} {l : F →L[ℝ] G} {x : ℂ} (h : ContDiffAt ℝ 2 f x) :
|
||
Complex.laplace (l ∘ f) x = (l ∘ (Complex.laplace f)) x := by
|
||
|
||
have A₂ : ∃ v ∈ nhds x, (IsOpen v) ∧ (x ∈ v) ∧ (ContDiffOn ℝ 2 f v) := by
|
||
have : ∃ u ∈ nhds x, ContDiffOn ℝ 2 f u := by
|
||
apply ContDiffAt.contDiffOn h
|
||
rfl
|
||
obtain ⟨u, hu₁, hu₂⟩ := this
|
||
obtain ⟨v, hv₁, hv₂, hv₃⟩ := mem_nhds_iff.1 hu₁
|
||
use v
|
||
constructor
|
||
· exact IsOpen.mem_nhds hv₂ hv₃
|
||
· constructor
|
||
exact hv₂
|
||
constructor
|
||
· exact hv₃
|
||
· exact ContDiffOn.congr_mono hu₂ (fun x => congrFun rfl) hv₁
|
||
obtain ⟨v, hv₁, hv₂, hv₃, hv₄⟩ := A₂
|
||
|
||
have D : ∀ w : ℂ, partialDeriv ℝ w (l ∘ f) =ᶠ[nhds x] l ∘ partialDeriv ℝ w (f) := by
|
||
intro w
|
||
apply Filter.eventuallyEq_iff_exists_mem.2
|
||
use v
|
||
constructor
|
||
· exact IsOpen.mem_nhds hv₂ hv₃
|
||
· intro y hy
|
||
apply partialDeriv_compContLinAt
|
||
let V := ContDiffOn.differentiableOn hv₄ one_le_two
|
||
apply DifferentiableOn.differentiableAt V
|
||
apply IsOpen.mem_nhds
|
||
assumption
|
||
assumption
|
||
|
||
unfold Complex.laplace
|
||
simp
|
||
|
||
rw [partialDeriv_eventuallyEq ℝ (D 1) 1]
|
||
rw [partialDeriv_compContLinAt]
|
||
rw [partialDeriv_eventuallyEq ℝ (D Complex.I) Complex.I]
|
||
rw [partialDeriv_compContLinAt]
|
||
simp
|
||
|
||
-- DifferentiableAt ℝ (partialDeriv ℝ Complex.I f) x
|
||
apply ContDiffAt.differentiableAt (partialDeriv_contDiffAt ℝ (ContDiffOn.contDiffAt hv₄ hv₁) Complex.I)
|
||
rfl
|
||
|
||
-- DifferentiableAt ℝ (partialDeriv ℝ 1 f) x
|
||
apply ContDiffAt.differentiableAt (partialDeriv_contDiffAt ℝ (ContDiffOn.contDiffAt hv₄ hv₁) 1)
|
||
rfl
|
||
|
||
|
||
theorem laplace_compCLE {f : ℂ → F} {l : F ≃L[ℝ] G} (h : ContDiff ℝ 2 f) :
|
||
Complex.laplace (l ∘ f) = l ∘ (Complex.laplace f) := by
|
||
let l' := (l : F →L[ℝ] G)
|
||
have : Complex.laplace (l' ∘ f) = l' ∘ (Complex.laplace f) := by
|
||
exact laplace_compContLin h
|
||
exact this
|