From 21693bd12df4057452c01d88d63599c7971c947d Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Fri, 7 Jun 2024 13:16:41 +0200 Subject: [PATCH] =?UTF-8?q?working=E2=80=A6?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Nevanlinna/complexHarmonic.examples.lean | 9 ++-- Nevanlinna/complexHarmonic.lean | 27 +++++++++++ Nevanlinna/laplace.lean | 59 ++++++++++++++++++++++++ 3 files changed, 92 insertions(+), 3 deletions(-) diff --git a/Nevanlinna/complexHarmonic.examples.lean b/Nevanlinna/complexHarmonic.examples.lean index d5165d8..36ce469 100644 --- a/Nevanlinna/complexHarmonic.examples.lean +++ b/Nevanlinna/complexHarmonic.examples.lean @@ -93,9 +93,7 @@ theorem log_normSq_of_holomorphicAt_is_harmonicAt (h₂f : f z ≠ 0) : HarmonicAt (Real.log ∘ Complex.normSq ∘ f) z := by - /- First prove the theorem under the additional assumption that - - -/ + -- First prove the theorem for functions with image in the slitPlane have lem₁ : ∀ g : ℂ → ℂ, (HolomorphicAt g z) → (g z ≠ 0) → (g z ∈ Complex.slitPlane) → HarmonicAt (Real.log ∘ Complex.normSq ∘ g) z := by intro g h₁g h₂g h₃g @@ -139,6 +137,11 @@ theorem log_normSq_of_holomorphicAt_is_harmonicAt simp apply hx.2 + rw [HarmonicAt_eventuallyEq this] + + + + sorry diff --git a/Nevanlinna/complexHarmonic.lean b/Nevanlinna/complexHarmonic.lean index 4ea6643..8acc506 100644 --- a/Nevanlinna/complexHarmonic.lean +++ b/Nevanlinna/complexHarmonic.lean @@ -64,6 +64,18 @@ theorem HarmonicAt_iff · exact h₂f +theorem HarmonicAt_eventuallyEq {f₁ f₂ : ℂ → F} {x : ℂ} (h : f₁ =ᶠ[nhds x] f₂) : HarmonicAt f₁ x ↔ HarmonicAt f₂ x := by + constructor + · intro h₁ + constructor + · exact ContDiffAt.congr_of_eventuallyEq h₁.1 (Filter.EventuallyEq.symm h) + · exact Filter.EventuallyEq.trans (laplace_eventuallyEq' (Filter.EventuallyEq.symm h)) h₁.2 + · intro h₁ + constructor + · exact ContDiffAt.congr_of_eventuallyEq h₁.1 h + · exact Filter.EventuallyEq.trans (laplace_eventuallyEq' h) h₁.2 + + 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 @@ -142,6 +154,21 @@ theorem harmonicOn_add_harmonicOn_is_harmonicOn {f₁ f₂ : ℂ → F} {s : Set simp +theorem harmonicAt_add_harmonicAt_is_harmonicAt + {f₁ f₂ : ℂ → F} + {x : ℂ} + (h₁ : HarmonicAt f₁ x) + (h₂ : HarmonicAt f₂ x) : + HarmonicAt (f₁ + f₂) x := by + constructor + · exact ContDiffAt.add h₁.1 h₂.1 + · rw [laplace_add_ContDiffAt] + intro z hz + rw [laplace_add_ContDiffOn hs h₁.1 h₂.1 z hz] + rw [h₁.2 z hz, h₂.2 z hz] + simp + + theorem harmonic_smul_const_is_harmonic {f : ℂ → F} {c : ℝ} (h : Harmonic f) : Harmonic (c • f) := by constructor diff --git a/Nevanlinna/laplace.lean b/Nevanlinna/laplace.lean index 147348d..64711c5 100644 --- a/Nevanlinna/laplace.lean +++ b/Nevanlinna/laplace.lean @@ -33,6 +33,14 @@ theorem laplace_eventuallyEq {f₁ f₂ : ℂ → F} {x : ℂ} (h : f₁ =ᶠ[nh rw [partialDeriv_eventuallyEq ℝ (partialDeriv_eventuallyEq' ℝ h Complex.I) Complex.I] + +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 + + theorem laplace_add {f₁ f₂ : ℂ → F} (h₁ : ContDiff ℝ 2 f₁) @@ -161,6 +169,57 @@ theorem laplace_add_ContDiffAt apply fun v ↦ (partialDeriv_contDiffAt ℝ h₁ v).differentiableAt le_rfl apply fun v ↦ (partialDeriv_contDiffAt ℝ h₂ v).differentiableAt le_rfl +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 + have : partialDeriv ℝ 1 (partialDeriv ℝ 1 f₁) + partialDeriv ℝ Complex.I (partialDeriv ℝ Complex.I f₁) + + (partialDeriv ℝ 1 (partialDeriv ℝ 1 f₂) + partialDeriv ℝ Complex.I (partialDeriv ℝ Complex.I f₂)) = + (partialDeriv ℝ 1 (partialDeriv ℝ 1 f₁) + (partialDeriv ℝ 1 (partialDeriv ℝ 1 f₂)) + + (partialDeriv ℝ Complex.I (partialDeriv ℝ Complex.I f₁) + partialDeriv ℝ Complex.I (partialDeriv ℝ Complex.I f₂))) := by + group + rw [this] + apply Filter.EventuallyEq.add + + suffices hyp : partialDeriv ℝ 1 (partialDeriv ℝ 1 (f₁ + f₂)) =ᶠ[nhds x] partialDeriv ℝ 1 (partialDeriv ℝ 1 f₁) + partialDeriv ℝ 1 (partialDeriv ℝ 1 f₂) from by + have : (fun x => partialDeriv ℝ 1 (partialDeriv ℝ 1 (f₁ + f₂)) x) = partialDeriv ℝ 1 (partialDeriv ℝ 1 (f₁ + f₂)) := by + rfl + rw [this] + have : (fun x => (partialDeriv ℝ 1 (partialDeriv ℝ 1 f₁) + partialDeriv ℝ 1 (partialDeriv ℝ 1 f₂)) x) = (partialDeriv ℝ 1 (partialDeriv ℝ 1 f₁)) + (partialDeriv ℝ 1 (partialDeriv ℝ 1 f₂)) := by + rfl + rwa [this] + + simp + + have h₁₁ : ContDiffAt ℝ 1 f₁ x := h₁.of_le one_le_two + have h₂₁ : ContDiffAt ℝ 1 f₂ x := h₂.of_le one_le_two + let A : partialDeriv ℝ 1 (f₁ + f₂) =ᶠ[nhds x] (partialDeriv ℝ 1 f₁) + (partialDeriv ℝ 1 f₂) := by + exact partialDeriv_add₂_contDiffAt ℝ h₁₁ h₂₁ + let B : partialDeriv ℝ 1 (partialDeriv ℝ 1 (f₁ + f₂)) =ᶠ[nhds x] (partialDeriv ℝ 1 (partialDeriv ℝ 1 f₁)) + (partialDeriv ℝ 1 (partialDeriv ℝ 1 f₂)) := by + sorry + + sorry + repeat + rw [partialDeriv_eventuallyEq ℝ (partialDeriv_add₂_contDiffAt ℝ h₁₁ h₂₁)] + rw [partialDeriv_add₂_differentiableAt] + + -- 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] + + repeat + apply fun v ↦ (partialDeriv_contDiffAt ℝ h₁ v).differentiableAt le_rfl + apply fun v ↦ (partialDeriv_contDiffAt ℝ h₂ v).differentiableAt le_rfl theorem laplace_smul {f : ℂ → F} : ∀ v : ℝ, Δ (v • f) = v • (Δ f) := by intro v