nevanlinna/Nevanlinna/laplace.lean

277 lines
9.8 KiB
Plaintext
Raw Permalink Normal View History

2024-05-13 09:23:08 +02:00
import Mathlib.Analysis.Complex.Basic
import Nevanlinna.partialDeriv
variable {F : Type*} [NormedAddCommGroup F] [NormedSpace F]
2024-05-13 09:52:15 +02:00
variable {G : Type*} [NormedAddCommGroup G] [NormedSpace G]
2024-05-13 09:23:08 +02:00
2024-05-13 09:46:21 +02:00
2024-06-04 10:27:46 +02:00
noncomputable def Complex.laplace (f : → F) : → F :=
partialDeriv 1 (partialDeriv 1 f) + partialDeriv Complex.I (partialDeriv Complex.I f)
2024-05-13 09:46:21 +02:00
2024-06-04 10:27:46 +02:00
notation "Δ" => Complex.laplace
2024-05-13 09:46:21 +02:00
2024-06-04 10:27:46 +02:00
theorem laplace_eventuallyEq {f₁ f₂ : → F} {x : } (h : f₁ =ᶠ[nhds x] f₂) : Δ f₁ x = Δ f₂ x := by
2024-05-30 16:20:06 +02:00
unfold Complex.laplace
simp
rw [partialDeriv_eventuallyEq (partialDeriv_eventuallyEq' h 1) 1]
rw [partialDeriv_eventuallyEq (partialDeriv_eventuallyEq' h Complex.I) Complex.I]
2024-06-07 13:16:41 +02:00
theorem laplace_eventuallyEq' {f₁ f₂ : → F} {x : } (h : f₁ =ᶠ[nhds x] f₂) : Δ f₁ =ᶠ[nhds x] Δ f₂ := by
unfold Complex.laplace
apply Filter.EventuallyEq.add
exact partialDeriv_eventuallyEq' (partialDeriv_eventuallyEq' h 1) 1
exact partialDeriv_eventuallyEq' (partialDeriv_eventuallyEq' h Complex.I) Complex.I
2024-06-05 09:06:25 +02:00
theorem laplace_add
2024-06-04 10:27:46 +02:00
{f₁ f₂ : → F}
(h₁ : ContDiff 2 f₁)
2024-06-05 09:06:25 +02:00
(h₂ : ContDiff 2 f₂) :
2024-06-04 10:27:46 +02:00
Δ (f₁ + f₂) = (Δ f₁) + (Δ f₂) := by
2024-05-13 09:46:21 +02:00
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
2024-05-13 09:48:16 +02:00
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
2024-05-30 17:02:15 +02:00
2024-05-31 09:21:35 +02:00
theorem laplace_add_ContDiffOn
{f₁ f₂ : → F}
{s : Set }
(hs : IsOpen s)
(h₁ : ContDiffOn 2 f₁ s)
(h₂ : ContDiffOn 2 f₂ s) :
2024-06-04 10:27:46 +02:00
∀ x ∈ s, Δ (f₁ + f₂) x = (Δ f₁) x + (Δ f₂) x := by
2024-05-30 17:02:15 +02:00
unfold Complex.laplace
simp
intro x hx
2024-05-31 09:21:35 +02:00
2024-06-03 13:35:53 +02:00
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
2024-05-30 17:02:15 +02:00
have : partialDeriv 1 (f₁ + f₂) =ᶠ[nhds x] (partialDeriv 1 f₁) + (partialDeriv 1 f₂) := by
2024-06-03 13:35:53 +02:00
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
2024-05-30 17:02:15 +02:00
rw [partialDeriv_eventuallyEq this]
2024-05-31 09:21:35 +02:00
have t₁ : DifferentiableAt (partialDeriv 1 f₁) x := by
2024-06-04 12:30:25 +02:00
let B₀ := (h₁ x hx).contDiffAt (IsOpen.mem_nhds hs hx)
let A₀ := partialDeriv_contDiffAt B₀ 1
2024-09-09 12:45:07 +02:00
apply A₀.differentiableAt (Preorder.le_refl 1)
2024-06-04 12:30:25 +02:00
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
2024-09-09 12:45:07 +02:00
exact A₀.differentiableAt (Preorder.le_refl 1)
2024-06-04 12:30:25 +02:00
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
2024-09-09 12:45:07 +02:00
exact A₀.differentiableAt (Preorder.le_refl 1)
2024-06-04 12:30:25 +02:00
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
2024-09-09 12:45:07 +02:00
exact A₀.differentiableAt (Preorder.le_refl 1)
2024-06-04 12:30:25 +02:00
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_add_ContDiffAt
{f₁ f₂ : → F}
{x : }
(h₁ : ContDiffAt 2 f₁ x)
(h₂ : ContDiffAt 2 f₂ x) :
Δ (f₁ + f₂) x = (Δ f₁) x + (Δ f₂) x := by
unfold Complex.laplace
simp
2024-06-05 09:06:25 +02:00
have h₁₁ : ContDiffAt 1 f₁ x := h₁.of_le one_le_two
have h₂₁ : ContDiffAt 1 f₂ x := h₂.of_le one_le_two
repeat
rw [partialDeriv_eventuallyEq (partialDeriv_add₂_contDiffAt h₁₁ h₂₁)]
rw [partialDeriv_add₂_differentiableAt]
2024-05-30 17:02:15 +02:00
2024-05-31 09:21:35 +02:00
-- I am super confused at this point because the tactic 'ring' does not work.
2024-05-31 10:21:27 +02:00
-- I do not understand why. So, I need to do things by hand.
2024-05-31 09:21:35 +02:00
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]
2024-05-13 09:48:16 +02:00
2024-06-05 09:06:25 +02:00
repeat
apply fun v ↦ (partialDeriv_contDiffAt h₁ v).differentiableAt le_rfl
apply fun v ↦ (partialDeriv_contDiffAt h₂ v).differentiableAt le_rfl
2024-06-10 10:58:57 +02:00
2024-06-07 13:16:41 +02:00
theorem laplace_add_ContDiffAt'
{f₁ f₂ : → F}
{x : }
(h₁ : ContDiffAt 2 f₁ x)
(h₂ : ContDiffAt 2 f₂ x) :
Δ (f₁ + f₂) =ᶠ[nhds x] (Δ f₁) + (Δ f₂):= by
unfold Complex.laplace
rw [add_assoc]
2024-06-10 10:58:57 +02:00
nth_rw 5 [add_comm]
2024-06-07 13:16:41 +02:00
rw [add_assoc]
2024-06-10 10:58:57 +02:00
rw [← add_assoc]
have dualPDeriv : ∀ v : , partialDeriv v (partialDeriv v (f₁ + f₂)) =ᶠ[nhds x]
partialDeriv v (partialDeriv v f₁) + partialDeriv v (partialDeriv v f₂) := by
intro v
have h₁₁ : ContDiffAt 1 f₁ x := h₁.of_le one_le_two
have h₂₁ : ContDiffAt 1 f₂ x := h₂.of_le one_le_two
have t₁ : partialDeriv v (partialDeriv v (f₁ + f₂)) =ᶠ[nhds x] partialDeriv v (partialDeriv v f₁ + partialDeriv v f₂) := by
exact partialDeriv_eventuallyEq' (partialDeriv_add₂_contDiffAt h₁₁ h₂₁) v
have t₂ : partialDeriv v (partialDeriv v f₁ + partialDeriv v f₂) =ᶠ[nhds x] (partialDeriv v (partialDeriv v f₁)) + (partialDeriv v (partialDeriv v f₂)) := by
apply partialDeriv_add₂_contDiffAt
apply partialDeriv_contDiffAt
exact h₁
apply partialDeriv_contDiffAt
exact h₂
apply Filter.EventuallyEq.trans t₁ t₂
have eventuallyEq_add
{a₁ a₂ b₁ b₂ : → F}
(h : a₁ =ᶠ[nhds x] b₁)
(h' : a₂ =ᶠ[nhds x] b₂) : (a₁ + a₂) =ᶠ[nhds x] (b₁ + b₂) := by
have {c₁ c₂ : → F} : (fun x => c₁ x + c₂ x) = c₁ + c₂ := by rfl
rw [← this, ← this]
exact Filter.EventuallyEq.add h h'
apply eventuallyEq_add
· exact dualPDeriv 1
· nth_rw 2 [add_comm]
exact dualPDeriv Complex.I
2024-06-07 13:16:41 +02:00
2024-05-13 09:46:21 +02:00
2024-06-04 10:27:46 +02:00
theorem laplace_smul {f : → F} : ∀ v : , Δ (v • f) = v • (Δ f) := by
2024-05-13 09:46:21 +02:00
intro v
unfold Complex.laplace
2024-06-04 10:27:46 +02:00
repeat
rw [partialDeriv_smul₂]
2024-05-13 09:52:15 +02:00
simp
2024-05-15 15:31:57 +02:00
2024-06-06 09:52:42 +02:00
theorem laplace_compCLMAt
{f : → F}
{l : F →L[] G}
{x : }
(h : ContDiffAt 2 f x) :
2024-06-04 10:27:46 +02:00
Δ (l ∘ f) x = (l ∘ (Δ f)) x := by
2024-05-29 16:33:32 +02:00
2024-06-04 10:27:46 +02:00
obtain ⟨v, hv₁, hv₂, hv₃, hv₄⟩ : ∃ v ∈ nhds x, (IsOpen v) ∧ (x ∈ v) ∧ (ContDiffOn 2 f v) := by
obtain ⟨u, hu₁, hu₂⟩ : ∃ u ∈ nhds x, ContDiffOn 2 f u := by
2024-05-31 09:21:35 +02:00
apply ContDiffAt.contDiffOn h
2024-05-30 10:26:39 +02:00
rfl
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₃
2024-05-31 09:21:35 +02:00
· exact ContDiffOn.congr_mono hu₂ (fun x => congrFun rfl) hv₁
2024-05-29 16:33:32 +02:00
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
2024-06-04 10:27:46 +02:00
apply ContDiffAt.differentiableAt (partialDeriv_contDiffAt (ContDiffOn.contDiffAt hv₄ hv₁) Complex.I) le_rfl
2024-05-29 16:33:32 +02:00
-- DifferentiableAt (partialDeriv 1 f) x
2024-06-04 10:27:46 +02:00
apply ContDiffAt.differentiableAt (partialDeriv_contDiffAt (ContDiffOn.contDiffAt hv₄ hv₁) 1) le_rfl
2024-05-29 16:33:32 +02:00
2024-06-05 09:06:25 +02:00
theorem laplace_compCLM
{f : → F}
{l : F →L[] G}
2024-06-04 10:27:46 +02:00
(h : ContDiff 2 f) :
Δ (l ∘ f) = l ∘ (Δ f) := by
funext z
2024-06-05 09:06:25 +02:00
exact laplace_compCLMAt h.contDiffAt
2024-05-29 16:33:32 +02:00
2024-06-04 10:27:46 +02:00
theorem laplace_compCLE {f : → F} {l : F ≃L[] G} :
Δ (l ∘ f) = l ∘ (Δ f) := by
unfold Complex.laplace
repeat
rw [partialDeriv_compCLE]
simp