nevanlinna/Nevanlinna/laplace.lean

209 lines
8.0 KiB
Plaintext
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

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_add_ContDiffOn
{f₁ f₂ : → F}
{s : Set }
(hs : IsOpen s)
(h₁ : ContDiffOn 2 f₁ s)
(h₂ : ContDiffOn 2 f₂ s) :
∀ x ∈ s, Complex.laplace (f₁ + f₂) x = (Complex.laplace f₁) x + (Complex.laplace f₂) x := by
unfold Complex.laplace
simp
intro x hx
have hf₁ : ∀ z ∈ s, DifferentiableAt f₁ z := by
intro z hz
convert DifferentiableOn.differentiableAt _ (IsOpen.mem_nhds hs hz)
apply ContDiffOn.differentiableOn h₁ one_le_two
have hf₂ : ∀ z ∈ s, DifferentiableAt f₂ z := by
intro z hz
convert DifferentiableOn.differentiableAt _ (IsOpen.mem_nhds hs hz)
apply ContDiffOn.differentiableOn h₂ one_le_two
have : partialDeriv 1 (f₁ + f₂) =ᶠ[nhds x] (partialDeriv 1 f₁) + (partialDeriv 1 f₂) := by
apply Filter.eventuallyEq_iff_exists_mem.2
use s
constructor
· exact IsOpen.mem_nhds hs hx
· intro z hz
apply partialDeriv_add₂_differentiableAt
exact hf₁ z hz
exact hf₂ z hz
rw [partialDeriv_eventuallyEq this]
have t₁ : DifferentiableAt (partialDeriv 1 f₁) x := by
let B₀ := (h₁ x hx).contDiffAt (IsOpen.mem_nhds hs hx)
let A₀ := partialDeriv_contDiffAt B₀ 1
exact A₀.differentiableAt (Submonoid.oneLE.proof_2 ℕ∞)
have t₂ : DifferentiableAt (partialDeriv 1 f₂) x := by
let B₀ := (h₂ x hx).contDiffAt (IsOpen.mem_nhds hs hx)
let A₀ := partialDeriv_contDiffAt B₀ 1
exact A₀.differentiableAt (Submonoid.oneLE.proof_2 ℕ∞)
rw [partialDeriv_add₂_differentiableAt t₁ t₂]
have : partialDeriv Complex.I (f₁ + f₂) =ᶠ[nhds x] (partialDeriv Complex.I f₁) + (partialDeriv Complex.I f₂) := by
apply Filter.eventuallyEq_iff_exists_mem.2
use s
constructor
· exact IsOpen.mem_nhds hs hx
· intro z hz
apply partialDeriv_add₂_differentiableAt
exact hf₁ z hz
exact hf₂ z hz
rw [partialDeriv_eventuallyEq this]
have t₃ : DifferentiableAt (partialDeriv Complex.I f₁) x := by
let B₀ := (h₁ x hx).contDiffAt (IsOpen.mem_nhds hs hx)
let A₀ := partialDeriv_contDiffAt B₀ Complex.I
exact A₀.differentiableAt (Submonoid.oneLE.proof_2 ℕ∞)
have t₄ : DifferentiableAt (partialDeriv Complex.I f₂) x := by
let B₀ := (h₂ x hx).contDiffAt (IsOpen.mem_nhds hs hx)
let A₀ := partialDeriv_contDiffAt B₀ Complex.I
exact A₀.differentiableAt (Submonoid.oneLE.proof_2 ℕ∞)
rw [partialDeriv_add₂_differentiableAt t₃ t₄]
-- I am super confused at this point because the tactic 'ring' does not work.
-- I do not understand why. So, I need to do things by hand.
rw [add_assoc]
rw [add_assoc]
rw [add_right_inj (partialDeriv 1 (partialDeriv 1 f₁) x)]
rw [add_comm]
rw [add_assoc]
rw [add_right_inj (partialDeriv Complex.I (partialDeriv Complex.I f₁) x)]
rw [add_comm]
theorem laplace_smul {f : → 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
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