nevanlinna/Nevanlinna/complexHarmonic.lean

277 lines
8.3 KiB
Plaintext
Raw Normal View History

2024-04-30 08:20:57 +02:00
import Mathlib.Analysis.Complex.Basic
2024-05-02 09:48:26 +02:00
import Mathlib.Analysis.Complex.TaylorSeries
2024-04-30 08:20:57 +02:00
import Mathlib.Analysis.Calculus.LineDeriv.Basic
import Mathlib.Analysis.Calculus.ContDiff.Defs
import Mathlib.Analysis.Calculus.FDeriv.Basic
2024-05-02 21:09:38 +02:00
import Mathlib.Analysis.Calculus.FDeriv.Symmetric
2024-06-03 12:56:30 +02:00
import Mathlib.Analysis.RCLike.Basic
2024-05-15 15:03:16 +02:00
import Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
2024-05-08 08:27:12 +02:00
import Mathlib.Data.Complex.Module
import Mathlib.Data.Complex.Order
import Mathlib.Data.Complex.Exponential
2024-05-15 15:03:16 +02:00
import Mathlib.Data.Fin.Tuple.Basic
2024-05-08 08:27:12 +02:00
import Mathlib.Topology.Algebra.InfiniteSum.Module
import Mathlib.Topology.Instances.RealVectorSpace
2024-04-30 08:20:57 +02:00
import Nevanlinna.cauchyRiemann
2024-05-13 09:23:08 +02:00
import Nevanlinna.laplace
2024-05-07 09:49:56 +02:00
import Nevanlinna.partialDeriv
2024-05-07 07:08:23 +02:00
2024-05-13 09:23:08 +02:00
variable {F : Type*} [NormedAddCommGroup F] [NormedSpace F]
2024-05-16 21:46:01 +02:00
variable {F₁ : Type*} [NormedAddCommGroup F₁] [NormedSpace F₁] [CompleteSpace F₁]
variable {G : Type*} [NormedAddCommGroup G] [NormedSpace G]
variable {G₁ : Type*} [NormedAddCommGroup G₁] [NormedSpace G₁] [CompleteSpace G₁]
2024-04-30 08:20:57 +02:00
2024-05-13 09:23:08 +02:00
def Harmonic (f : → F) : Prop :=
2024-06-04 10:27:46 +02:00
(ContDiff 2 f) ∧ (∀ z, Δ f z = 0)
2024-04-30 08:20:57 +02:00
2024-06-05 09:51:02 +02:00
def HarmonicAt (f : → F) (x : ) : Prop :=
(ContDiffAt 2 f x) ∧ (Δ f =ᶠ[nhds x] 0)
2024-05-03 12:23:09 +02:00
2024-05-18 12:13:30 +02:00
def HarmonicOn (f : → F) (s : Set ) : Prop :=
2024-06-04 10:27:46 +02:00
(ContDiffOn 2 f s) ∧ (∀ z ∈ s, Δ f z = 0)
2024-06-05 12:03:05 +02:00
2024-06-05 09:51:02 +02:00
theorem HarmonicAt_iff
{f : → F}
{x : } :
HarmonicAt f x ↔ ∃ s : Set , IsOpen s ∧ x ∈ s ∧ (ContDiffOn 2 f s) ∧ (∀ z ∈ s, Δ f z = 0) := by
constructor
· intro hf
obtain ⟨s₁, h₁s₁, h₂s₁, h₃s₁⟩ := hf.1.contDiffOn' le_rfl
simp at h₃s₁
obtain ⟨t₂, h₁t₂, h₂t₂⟩ := (Filter.eventuallyEq_iff_exists_mem.1 hf.2)
obtain ⟨s₂, h₁s₂, h₂s₂, h₃s₂⟩ := mem_nhds_iff.1 h₁t₂
let s := s₁ ∩ s₂
use s
constructor
· exact IsOpen.inter h₁s₁ h₂s₂
· constructor
· exact Set.mem_inter h₂s₁ h₃s₂
· constructor
· exact h₃s₁.mono (Set.inter_subset_left s₁ s₂)
· intro z hz
exact h₂t₂ (h₁s₂ hz.2)
· intro hyp
obtain ⟨s, h₁s, h₂s, h₁f, h₂f⟩ := hyp
constructor
· apply h₁f.contDiffAt
apply (IsOpen.mem_nhds_iff h₁s).2 h₂s
· apply Filter.eventuallyEq_iff_exists_mem.2
use s
constructor
· apply (IsOpen.mem_nhds_iff h₁s).2 h₂s
· exact h₂f
2024-05-18 12:13:30 +02:00
theorem HarmonicOn_of_locally_HarmonicOn {f : → F} {s : Set } (h : ∀ x ∈ s, ∃ (u : Set ), IsOpen u ∧ x ∈ u ∧ HarmonicOn f (s ∩ u)) :
HarmonicOn f s := by
constructor
· apply contDiffOn_of_locally_contDiffOn
intro x xHyp
2024-05-30 16:20:06 +02:00
obtain ⟨u, uHyp⟩ := h x xHyp
2024-05-18 12:13:30 +02:00
use u
2024-05-29 16:33:32 +02:00
exact ⟨ uHyp.1, ⟨uHyp.2.1, uHyp.2.2.1⟩⟩
2024-05-18 12:13:30 +02:00
· intro x xHyp
2024-05-30 16:20:06 +02:00
obtain ⟨u, uHyp⟩ := h x xHyp
2024-05-18 12:13:30 +02:00
exact (uHyp.2.2.2) x ⟨xHyp, uHyp.2.1⟩
2024-05-30 16:20:06 +02:00
theorem HarmonicOn_congr {f₁ f₂ : → F} {s : Set } (hs : IsOpen s) (hf₁₂ : ∀ x ∈ s, f₁ x = f₂ x) :
HarmonicOn f₁ s ↔ HarmonicOn f₂ s := by
constructor
· intro h₁
constructor
· apply ContDiffOn.congr h₁.1
intro x hx
rw [eq_comm]
exact hf₁₂ x hx
· intro z hz
2024-05-31 10:21:27 +02:00
have : f₁ =ᶠ[nhds z] f₂ := by
2024-05-30 16:20:06 +02:00
unfold Filter.EventuallyEq
unfold Filter.Eventually
simp
2024-05-30 17:02:15 +02:00
refine mem_nhds_iff.mpr ?_
use s
2024-05-31 10:21:27 +02:00
constructor
2024-05-30 17:02:15 +02:00
· exact hf₁₂
· constructor
· exact hs
· exact hz
2024-05-30 16:20:06 +02:00
rw [← laplace_eventuallyEq this]
exact h₁.2 z hz
· intro h₁
constructor
· apply ContDiffOn.congr h₁.1
intro x hx
exact hf₁₂ x hx
· intro z hz
2024-05-31 10:21:27 +02:00
have : f₁ =ᶠ[nhds z] f₂ := by
2024-05-30 17:02:15 +02:00
unfold Filter.EventuallyEq
unfold Filter.Eventually
simp
refine mem_nhds_iff.mpr ?_
use s
2024-05-31 10:21:27 +02:00
constructor
2024-05-30 17:02:15 +02:00
· exact hf₁₂
· constructor
· exact hs
· exact hz
2024-05-30 16:20:06 +02:00
rw [laplace_eventuallyEq this]
exact h₁.2 z hz
2024-05-17 12:31:36 +02:00
theorem harmonic_add_harmonic_is_harmonic {f₁ f₂ : → F} (h₁ : Harmonic f₁) (h₂ : Harmonic f₂) :
2024-05-17 10:09:14 +02:00
Harmonic (f₁ + f₂) := by
constructor
· exact ContDiff.add h₁.1 h₂.1
· rw [laplace_add h₁.1 h₂.1]
simp
intro z
rw [h₁.2 z, h₂.2 z]
simp
2024-05-30 17:02:15 +02:00
theorem harmonicOn_add_harmonicOn_is_harmonicOn {f₁ f₂ : → F} {s : Set } (hs : IsOpen s) (h₁ : HarmonicOn f₁ s) (h₂ : HarmonicOn f₂ s) :
HarmonicOn (f₁ + f₂) s := by
constructor
· exact ContDiffOn.add h₁.1 h₂.1
2024-05-31 10:21:27 +02:00
· intro z hz
rw [laplace_add_ContDiffOn hs h₁.1 h₂.1 z hz]
rw [h₁.2 z hz, h₂.2 z hz]
2024-05-30 17:02:15 +02:00
simp
2024-05-17 12:31:36 +02:00
theorem harmonic_smul_const_is_harmonic {f : → F} {c : } (h : Harmonic f) :
Harmonic (c • f) := by
constructor
· exact ContDiff.const_smul c h.1
2024-05-31 16:10:06 +02:00
· rw [laplace_smul]
2024-05-17 12:31:36 +02:00
dsimp
intro z
rw [h.2 z]
simp
theorem harmonic_iff_smul_const_is_harmonic {f : → F} {c : } (hc : c ≠ 0) :
Harmonic f ↔ Harmonic (c • f) := by
constructor
· exact harmonic_smul_const_is_harmonic
· nth_rewrite 2 [((eq_inv_smul_iff₀ hc).mpr rfl : f = c⁻¹ • c • f)]
exact fun a => harmonic_smul_const_is_harmonic a
2024-05-17 09:19:24 +02:00
theorem harmonic_comp_CLM_is_harmonic {f : → F₁} {l : F₁ →L[] G} (h : Harmonic f) :
2024-05-16 21:46:01 +02:00
Harmonic (l ∘ f) := by
constructor
· -- Continuous differentiability
apply ContDiff.comp
exact ContinuousLinearMap.contDiff l
2024-05-17 09:19:24 +02:00
exact h.1
2024-06-04 10:27:46 +02:00
· rw [laplace_compCLM]
2024-05-16 21:46:01 +02:00
simp
intro z
rw [h.2 z]
simp
2024-05-17 09:19:24 +02:00
exact ContDiff.restrict_scalars h.1
2024-05-16 21:46:01 +02:00
2024-05-30 10:41:10 +02:00
theorem harmonicOn_comp_CLM_is_harmonicOn {f : → F₁} {s : Set } {l : F₁ →L[] G} (hs : IsOpen s) (h : HarmonicOn f s) :
2024-05-18 12:13:30 +02:00
HarmonicOn (l ∘ f) s := by
constructor
· -- Continuous differentiability
apply ContDiffOn.continuousLinearMap_comp
exact h.1
2024-05-29 16:33:32 +02:00
· -- Vanishing of Laplace
2024-05-18 12:13:30 +02:00
intro z zHyp
2024-06-04 10:27:46 +02:00
rw [laplace_compCLMAt]
2024-05-30 10:41:10 +02:00
simp
2024-05-18 12:13:30 +02:00
rw [h.2 z]
simp
assumption
2024-05-30 10:41:10 +02:00
apply ContDiffOn.contDiffAt h.1
exact IsOpen.mem_nhds hs zHyp
2024-05-29 16:33:32 +02:00
2024-06-06 09:52:42 +02:00
theorem harmonicAt_comp_CLM_is_harmonicAt
{f : → F₁}
{z : }
{l : F₁ →L[] G}
(h : HarmonicAt f z) :
HarmonicAt (l ∘ f) z := by
constructor
· -- ContDiffAt 2 (⇑l ∘ f) z
apply ContDiffAt.continuousLinearMap_comp
exact h.1
· -- Δ (⇑l ∘ f) =ᶠ[nhds z] 0
obtain ⟨r, h₁r, h₂r⟩ := h.1.contDiffOn le_rfl
obtain ⟨s, h₁s, h₂s, h₃s⟩ := mem_nhds_iff.1 h₁r
obtain ⟨t, h₁t, h₂t⟩ := Filter.eventuallyEq_iff_exists_mem.1 h.2
obtain ⟨u, h₁u, h₂u, h₃u⟩ := mem_nhds_iff.1 h₁t
apply Filter.eventuallyEq_iff_exists_mem.2
use s ∩ u
constructor
· apply IsOpen.mem_nhds
exact IsOpen.inter h₂s h₂u
constructor
· exact h₃s
· exact h₃u
· intro x xHyp
rw [laplace_compCLMAt]
simp
rw [h₂t]
simp
exact h₁u xHyp.2
apply (h₂r.mono h₁s).contDiffAt (IsOpen.mem_nhds h₂s xHyp.1)
2024-05-16 21:46:01 +02:00
theorem harmonic_iff_comp_CLE_is_harmonic {f : → F₁} {l : F₁ ≃L[] G₁} :
Harmonic f ↔ Harmonic (l ∘ f) := by
constructor
· have : l ∘ f = (l : F₁ →L[] G₁) ∘ f := by rfl
rw [this]
exact harmonic_comp_CLM_is_harmonic
2024-05-17 09:05:15 +02:00
· have : f = (l.symm : G₁ →L[] F₁) ∘ l ∘ f := by
2024-05-16 21:46:01 +02:00
funext z
unfold Function.comp
simp
nth_rewrite 2 [this]
exact harmonic_comp_CLM_is_harmonic
2024-06-06 09:52:42 +02:00
theorem harmonicAt_iff_comp_CLE_is_harmonicAt
{f : → F₁}
{z : }
{l : F₁ ≃L[] G₁} :
HarmonicAt f z ↔ HarmonicAt (l ∘ f) z := by
constructor
· have : l ∘ f = (l : F₁ →L[] G₁) ∘ f := by rfl
rw [this]
exact harmonicAt_comp_CLM_is_harmonicAt
· have : f = (l.symm : G₁ →L[] F₁) ∘ l ∘ f := by
funext z
unfold Function.comp
simp
nth_rewrite 2 [this]
exact harmonicAt_comp_CLM_is_harmonicAt
2024-05-31 10:21:27 +02:00
theorem harmonicOn_iff_comp_CLE_is_harmonicOn {f : → F₁} {s : Set } {l : F₁ ≃L[] G₁} (hs : IsOpen s) :
HarmonicOn f s ↔ HarmonicOn (l ∘ f) s := by
constructor
· have : l ∘ f = (l : F₁ →L[] G₁) ∘ f := by rfl
rw [this]
exact harmonicOn_comp_CLM_is_harmonicOn hs
· have : f = (l.symm : G₁ →L[] F₁) ∘ l ∘ f := by
funext z
unfold Function.comp
simp
nth_rewrite 2 [this]
exact harmonicOn_comp_CLM_is_harmonicOn hs