Compare commits

...

2 Commits

Author SHA1 Message Date
Stefan Kebekus
c8e1aacb15 working 2024-05-30 17:02:15 +02:00
Stefan Kebekus
b0ab121868 working 2024-05-30 16:20:06 +02:00
3 changed files with 108 additions and 5 deletions

View File

@@ -35,14 +35,58 @@ theorem HarmonicOn_of_locally_HarmonicOn {f : → F} {s : Set } (h : ∀
constructor
· apply contDiffOn_of_locally_contDiffOn
intro x xHyp
obtain u, uHyp := h x xHyp
obtain u, uHyp := h x xHyp
use u
exact uHyp.1, uHyp.2.1, uHyp.2.2.1
· intro x xHyp
obtain u, uHyp := h x xHyp
obtain u, uHyp := h x xHyp
exact (uHyp.2.2.2) x xHyp, uHyp.2.1
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
have : f₁ =[nhds z] f₂ := by
unfold Filter.EventuallyEq
unfold Filter.Eventually
simp
refine mem_nhds_iff.mpr ?_
use s
constructor
· exact hf₁₂
· constructor
· exact hs
· exact hz
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
have : f₁ =[nhds z] f₂ := by
unfold Filter.EventuallyEq
unfold Filter.Eventually
simp
refine mem_nhds_iff.mpr ?_
use s
constructor
· exact hf₁₂
· constructor
· exact hs
· exact hz
rw [laplace_eventuallyEq this]
exact h₁.2 z hz
theorem harmonic_add_harmonic_is_harmonic {f₁ f₂ : F} (h₁ : Harmonic f₁) (h₂ : Harmonic f₂) :
Harmonic (f₁ + f₂) := by
constructor
@@ -54,6 +98,17 @@ theorem harmonic_add_harmonic_is_harmonic {f₁ f₂ : → F} (h₁ : Harmon
simp
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
· rw [laplace_add h₁.1 h₂.1]
simp
intro z
rw [h₁.2 z, h₂.2 z]
simp
theorem harmonic_smul_const_is_harmonic {f : F} {c : } (h : Harmonic f) :
Harmonic (c f) := by
constructor
@@ -240,7 +295,8 @@ theorem log_normSq_of_holomorphicOn_is_harmonicOn
exact (AddEquivClass.map_ne_zero_iff starRingAut).mpr (h₂ z hz)
exact h₂ z hz
rw [this]
rw [HarmonicOn_congr hs this]
simp
apply harmonic_add_harmonic_is_harmonic
have : Complex.log (starRingEnd ) f = Complex.conjCLE Complex.log f := by

View File

@@ -24,7 +24,14 @@ 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
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₂]
@@ -46,6 +53,37 @@ theorem laplace_add {f₁ f₂ : → F} (h₁ : ContDiff 2 f₁) (h₂
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 : partialDeriv 1 (f₁ + f₂) =[nhds x] (partialDeriv 1 f₁) + (partialDeriv 1 f₂) := by
sorry
rw [partialDeriv_eventuallyEq this]
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

View File

@@ -42,7 +42,7 @@ theorem partialDeriv_smul₂ {f : E → F} {a : 𝕜} {v : E} (h : Differentiabl
rw [fderiv_const_smul (h w)]
theorem partialDeriv_add₂ {f₁ f₂ : E F} {v : E} (h₁ : Differentiable 𝕜 f₁) (h₂ : Differentiable 𝕜 f₂) : partialDeriv 𝕜 v (f₁ + f₂) = (partialDeriv 𝕜 v f₁) + (partialDeriv 𝕜 v f₂) := by
theorem partialDeriv_add₂ {f₁ f₂ : E F} {v : E} (h₁ : Differentiable 𝕜 f₁) (h₂ : Differentiable 𝕜 f₂) : partialDeriv 𝕜 v (f₁ + f₂) = (partialDeriv 𝕜 v f₁) + (partialDeriv 𝕜 v f₂) := by
unfold partialDeriv
have : f₁ + f₂ = fun y f₁ y + f₂ y := by rfl
@@ -128,6 +128,15 @@ theorem partialDeriv_eventuallyEq {f₁ f₂ : E → F} {x : E} (h : f₁ =ᶠ[n
exact fun v => rfl
theorem partialDeriv_eventuallyEq' {f₁ f₂ : E F} {x : E} (h : f₁ =[nhds x] f₂) : v : E, partialDeriv 𝕜 v f₁ =[nhds x] partialDeriv 𝕜 v f₂ := by
unfold partialDeriv
intro v
let A : fderiv 𝕜 f₁ =[nhds x] fderiv 𝕜 f₂ := Filter.EventuallyEq.fderiv h
apply Filter.EventuallyEq.comp₂
exact A
simp
section restrictScalars
variable (𝕜 : Type*) [NontriviallyNormedField 𝕜]