From a6aba0fc683a71fbe5b39b93fd85087d021b2153 Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Thu, 6 Jun 2024 09:52:42 +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 | 28 ++++++++++++- Nevanlinna/complexHarmonic.lean | 51 ++++++++++++++++++++++++ Nevanlinna/holomorphic.lean | 25 +++++++++++- Nevanlinna/laplace.lean | 6 ++- Nevanlinna/partialDeriv.lean | 33 +++------------ 5 files changed, 111 insertions(+), 32 deletions(-) diff --git a/Nevanlinna/complexHarmonic.examples.lean b/Nevanlinna/complexHarmonic.examples.lean index 8818989..ec0fa00 100644 --- a/Nevanlinna/complexHarmonic.examples.lean +++ b/Nevanlinna/complexHarmonic.examples.lean @@ -23,7 +23,6 @@ variable {F₁ : Type*} [NormedAddCommGroup F₁] [NormedSpace ℂ F₁] [Comple 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₁} @@ -67,6 +66,33 @@ theorem holomorphicAt_is_harmonicAt simp +theorem re_of_holomorphicAt_is_harmonicAr + {f : ℂ → ℂ} + {z : ℂ} + (h : HolomorphicAt f z) : + HarmonicAt (Complex.reCLM ∘ f) z := by + apply harmonicAt_comp_CLM_is_harmonicAt + exact holomorphicAt_is_harmonicAt h + + +theorem im_of_holomorphicAt_is_harmonicAt + {f : ℂ → ℂ} + {z : ℂ} + (h : HolomorphicAt f z) : + HarmonicAt (Complex.imCLM ∘ f) z := by + apply harmonicAt_comp_CLM_is_harmonicAt + exact holomorphicAt_is_harmonicAt h + + +theorem antiholomorphicAt_is_harmonicAt + {f : ℂ → ℂ} + {z : ℂ} + (h : HolomorphicAt f z) : + HarmonicAt (Complex.conjCLE ∘ f) z := by + apply harmonicAt_iff_comp_CLE_is_harmonicAt.1 + exact holomorphicAt_is_harmonicAt h + + theorem holomorphic_is_harmonic {f : ℂ → F₁} (h : Differentiable ℂ f) : Harmonic f := by diff --git a/Nevanlinna/complexHarmonic.lean b/Nevanlinna/complexHarmonic.lean index fc5b753..7887293 100644 --- a/Nevanlinna/complexHarmonic.lean +++ b/Nevanlinna/complexHarmonic.lean @@ -195,6 +195,39 @@ theorem harmonicOn_comp_CLM_is_harmonicOn {f : ℂ → F₁} {s : Set ℂ} {l : exact IsOpen.mem_nhds hs zHyp +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) + + theorem harmonic_iff_comp_CLE_is_harmonic {f : ℂ → F₁} {l : F₁ ≃L[ℝ] G₁} : Harmonic f ↔ Harmonic (l ∘ f) := by @@ -210,6 +243,24 @@ theorem harmonic_iff_comp_CLE_is_harmonic {f : ℂ → F₁} {l : F₁ ≃L[ℝ] exact harmonic_comp_CLM_is_harmonic +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 + + 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 diff --git a/Nevanlinna/holomorphic.lean b/Nevanlinna/holomorphic.lean index 75b99ff..fb6730a 100644 --- a/Nevanlinna/holomorphic.lean +++ b/Nevanlinna/holomorphic.lean @@ -1,5 +1,4 @@ import Mathlib.Analysis.Complex.Basic -import Mathlib.Analysis.Calculus.ContDiff.Defs import Nevanlinna.partialDeriv variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] @@ -33,6 +32,28 @@ theorem HolomorphicAt_iff · assumption +theorem HolomorphicAt_isOpen' + {f : E → F} : + IsOpen { x : E | HolomorphicAt f x } := by + + rw [← subset_interior_iff_isOpen] + intro x hx + simp at hx + obtain ⟨s, h₁s, h₂s, h₃s⟩ := HolomorphicAt_iff.1 hx + use s + constructor + · simp + constructor + · exact h₁s + · intro x hx + simp + use s + constructor + · exact IsOpen.mem_nhds h₁s hx + · exact h₃s + · exact h₂s + +/- theorem HolomorphicAt_isOpen {f : E → F} {x : E} : @@ -62,7 +83,7 @@ theorem HolomorphicAt_isOpen · intro z hz obtain ⟨t, ht⟩ := (hf z hz) exact ht.2 z (mem_of_mem_nhds ht.1) - +-/ theorem CauchyRiemann'₅ {f : ℂ → F} diff --git a/Nevanlinna/laplace.lean b/Nevanlinna/laplace.lean index 405e220..147348d 100644 --- a/Nevanlinna/laplace.lean +++ b/Nevanlinna/laplace.lean @@ -170,7 +170,11 @@ theorem laplace_smul {f : ℂ → F} : ∀ v : ℝ, Δ (v • f) = v • (Δ f) simp -theorem laplace_compCLMAt {f : ℂ → F} {l : F →L[ℝ] G} {x : ℂ} (h : ContDiffAt ℝ 2 f x) : +theorem laplace_compCLMAt + {f : ℂ → F} + {l : F →L[ℝ] G} + {x : ℂ} + (h : ContDiffAt ℝ 2 f x) : Δ (l ∘ f) x = (l ∘ (Δ f)) x := by obtain ⟨v, hv₁, hv₂, hv₃, hv₄⟩ : ∃ v ∈ nhds x, (IsOpen v) ∧ (x ∈ v) ∧ (ContDiffOn ℝ 2 f v) := by diff --git a/Nevanlinna/partialDeriv.lean b/Nevanlinna/partialDeriv.lean index 33f3aec..18a1480 100644 --- a/Nevanlinna/partialDeriv.lean +++ b/Nevanlinna/partialDeriv.lean @@ -361,7 +361,7 @@ theorem partialDeriv_commOn (fderiv ℝ (fun w => fderiv ℝ f w) z) v₁ v₂ = (fderiv ℝ (fun w => fderiv ℝ f w) z) v₂ v₁ := by let f' := fderiv ℝ f - have h₀ : ∀ y ∈ s, HasFDerivAt f (f' y) y := by + have h₀1 : ∀ y ∈ s, HasFDerivAt f (f' y) y := by intro y hy apply DifferentiableAt.hasFDerivAt apply DifferentiableOn.differentiableAt _ (IsOpen.mem_nhds hs hy) @@ -393,31 +393,8 @@ theorem partialDeriv_commAt (h : ContDiffAt ℝ 2 f z) : ∀ v₁ v₂ : E, partialDeriv ℝ v₁ (partialDeriv ℝ v₂ f) z = partialDeriv ℝ v₂ (partialDeriv ℝ v₁ f) z := by + obtain ⟨u, hu₁, hu₂⟩ := h.contDiffOn le_rfl + obtain ⟨v, hv₁, hv₂, hv₃⟩ := mem_nhds_iff.1 hu₁ + intro v₁ v₂ - - have derivSymm : - (fderiv ℝ (fun w => fderiv ℝ f w) z) v₁ v₂ = (fderiv ℝ (fun w => fderiv ℝ f w) z) v₂ v₁ := by - - let f' := fderiv ℝ f - have h₀ : ∀ y ∈ s, HasFDerivAt f (f' y) y := by - intro y hy - apply DifferentiableAt.hasFDerivAt - apply DifferentiableOn.differentiableAt _ (IsOpen.mem_nhds hs hy) - apply h.differentiableOn one_le_two - - let f'' := (fderiv ℝ f' z) - have h₁ : HasFDerivAt f' f'' z := by - apply DifferentiableAt.hasFDerivAt - apply DifferentiableOn.differentiableAt _ (IsOpen.mem_nhds hs hz) - apply ContDiffOn.differentiableOn _ (Submonoid.oneLE.proof_2 ℕ∞) - exact ((contDiffOn_succ_iff_fderiv_of_isOpen hs).1 h).2 - - have h₀' : ∀ᶠ (y : E) in nhds z, HasFDerivAt f (f' y) y := by - apply eventually_nhds_iff.mpr - use s - - exact second_derivative_symmetric_of_eventually h₀' h₁ v₁ v₂ - - rw [← partialDeriv_fderivAt ℝ hs h v₂ v₁ z hz] - rw [derivSymm] - rw [← partialDeriv_fderivOn ℝ hs h v₁ v₂ z hz] + exact partialDeriv_commOn hv₂ (hu₂.mono hv₁) v₁ v₂ z hv₃