From 9c53bb793afb6ddb5361381c675c9a4ae38d3dae Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Wed, 5 Jun 2024 12:03:05 +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 | 47 +++++++++++++++++-- Nevanlinna/complexHarmonic.lean | 1 + Nevanlinna/holomorphic.lean | 58 ++++++++++++++++++++---- Nevanlinna/partialDeriv.lean | 6 ++- 4 files changed, 98 insertions(+), 14 deletions(-) diff --git a/Nevanlinna/complexHarmonic.examples.lean b/Nevanlinna/complexHarmonic.examples.lean index b4764c8..8818989 100644 --- a/Nevanlinna/complexHarmonic.examples.lean +++ b/Nevanlinna/complexHarmonic.examples.lean @@ -16,12 +16,56 @@ import Mathlib.Topology.Instances.RealVectorSpace import Nevanlinna.cauchyRiemann import Nevanlinna.laplace import Nevanlinna.complexHarmonic +import Nevanlinna.holomorphic variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] 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₁] +#check DifferentiableOn.contDiffOn + +theorem holomorphicAt_is_harmonicAt + {f : ℂ → F₁} + {z : ℂ} + (hf : HolomorphicAt f z) : + HarmonicAt f z := by + + obtain ⟨s, hs, hz, h'f⟩ := HolomorphicAt_iff.1 hf + + constructor + · -- ContDiffAt ℝ 2 f z + apply ContDiffOn.contDiffAt _ ((IsOpen.mem_nhds_iff hs).2 hz) + suffices h : ContDiffOn ℂ 2 f s from by + apply ContDiffOn.restrict_scalars ℝ h + apply DifferentiableOn.contDiffOn _ hs + intro w hw + apply DifferentiableAt.differentiableWithinAt + exact h'f w hw + · -- Δ f =ᶠ[nhds z] 0 + obtain ⟨t, ht, hz, h'f⟩ := HolomorphicAt_isOpen.1 hf + apply Filter.eventuallyEq_iff_exists_mem.2 + use t + constructor + · exact IsOpen.mem_nhds ht hz + · intro w hw + unfold Complex.laplace + simp + + rw [partialDeriv_eventuallyEq ℝ (CauchyRiemann'₆ (h'f w hw)) Complex.I] + rw [partialDeriv_smul'₂] + simp + + have f_is_real_C2 : ContDiffOn ℝ 2 f t := + ContDiffOn.restrict_scalars ℝ (DifferentiableOn.contDiffOn h'f ht) + rw [partialDeriv_commOn ht f_is_real_C2 Complex.I 1 w hw] + rw [partialDeriv_eventuallyEq ℝ (CauchyRiemann'₆ (h'f w hw)) 1] + rw [partialDeriv_smul'₂] + simp + + rw [← smul_assoc] + simp + theorem holomorphic_is_harmonic {f : ℂ → F₁} (h : Differentiable ℂ f) : Harmonic f := by @@ -115,9 +159,6 @@ theorem holomorphicOn_is_harmonicOn {f : ℂ → F₁} {s : Set ℂ} (hs : IsOpe simp rw [partialDeriv_commOn hs f_is_real_C2 Complex.I 1 z hz] - have : Complex.I • partialDeriv ℝ 1 (partialDeriv ℝ Complex.I f) z = Complex.I • (partialDeriv ℝ 1 (partialDeriv ℝ Complex.I f) z) := by - rfl - rw [this] have : partialDeriv ℝ Complex.I f =ᶠ[nhds z] Complex.I • partialDeriv ℝ 1 f := by unfold Filter.EventuallyEq unfold Filter.Eventually diff --git a/Nevanlinna/complexHarmonic.lean b/Nevanlinna/complexHarmonic.lean index c5c2224..fc5b753 100644 --- a/Nevanlinna/complexHarmonic.lean +++ b/Nevanlinna/complexHarmonic.lean @@ -31,6 +31,7 @@ def HarmonicAt (f : ℂ → F) (x : ℂ) : Prop := def HarmonicOn (f : ℂ → F) (s : Set ℂ) : Prop := (ContDiffOn ℝ 2 f s) ∧ (∀ z ∈ s, Δ f z = 0) + theorem HarmonicAt_iff {f : ℂ → F} {x : ℂ} : diff --git a/Nevanlinna/holomorphic.lean b/Nevanlinna/holomorphic.lean index 3f0330d..75b99ff 100644 --- a/Nevanlinna/holomorphic.lean +++ b/Nevanlinna/holomorphic.lean @@ -33,11 +33,42 @@ theorem HolomorphicAt_iff · assumption -theorem CauchyRiemann₅ +theorem HolomorphicAt_isOpen + {f : E → F} + {x : E} : + HolomorphicAt f x ↔ ∃ s : Set E, IsOpen s ∧ x ∈ s ∧ (∀ z ∈ s, HolomorphicAt f z) := by + constructor + · intro hf + obtain ⟨t, h₁t, h₂t⟩ := hf + obtain ⟨s, h₁s, h₂s, h₃s⟩ := mem_nhds_iff.1 h₁t + use s + constructor + · assumption + · constructor + · assumption + · intro z hz + apply HolomorphicAt_iff.2 + use s + constructor + · assumption + · constructor + · assumption + · exact fun w hw ↦ h₂t w (h₁s hw) + · intro hyp + obtain ⟨s, h₁s, h₂s, hf⟩ := hyp + use s + constructor + · apply (IsOpen.mem_nhds_iff h₁s).2 h₂s + · intro z hz + obtain ⟨t, ht⟩ := (hf z hz) + exact ht.2 z (mem_of_mem_nhds ht.1) + + +theorem CauchyRiemann'₅ {f : ℂ → F} - {z : ℂ} : - (DifferentiableAt ℂ f z) → partialDeriv ℝ Complex.I f z = Complex.I • partialDeriv ℝ 1 f z := by - intro h + {z : ℂ} + (h : DifferentiableAt ℂ f z) : + partialDeriv ℝ Complex.I f z = Complex.I • partialDeriv ℝ 1 f z := by unfold partialDeriv conv => @@ -53,11 +84,18 @@ theorem CauchyRiemann₅ rw [DifferentiableAt.fderiv_restrictScalars ℝ h] -theorem CauchyRiemann₆ - {f : ℂ → ℂ} - {z : ℂ} : - (HolomorphicAt f z) → partialDeriv ℝ Complex.I f =ᶠ[nhds z] Complex.I • partialDeriv ℝ 1 f := by +theorem CauchyRiemann'₆ + {f : ℂ → F} + {z : ℂ} + (h : HolomorphicAt f z) : + partialDeriv ℝ Complex.I f =ᶠ[nhds z] Complex.I • partialDeriv ℝ 1 f := by + obtain ⟨s, h₁s, hz, h₂f⟩ := HolomorphicAt_iff.1 h - - sorry + apply Filter.eventuallyEq_iff_exists_mem.2 + use s + constructor + · exact IsOpen.mem_nhds h₁s hz + · intro w hw + apply CauchyRiemann'₅ + exact h₂f w hw diff --git a/Nevanlinna/partialDeriv.lean b/Nevanlinna/partialDeriv.lean index d9813ce..19d4bed 100644 --- a/Nevanlinna/partialDeriv.lean +++ b/Nevanlinna/partialDeriv.lean @@ -16,7 +16,11 @@ noncomputable def partialDeriv : E → (E → F) → (E → F) := fun v ↦ (fun f ↦ (fun w ↦ fderiv 𝕜 f w v)) -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 +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 apply Filter.EventuallyEq.comp₂