From 52abf9b79b3b401a6e7f75291e44dc8ad51e4add Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Mon, 10 Jun 2024 12:39:40 +0200 Subject: [PATCH] Done with examples for holomorphicAt --- Nevanlinna/complexHarmonic.examples.lean | 146 +++++++++-------------- Nevanlinna/holomorphic.lean | 34 +++--- 2 files changed, 73 insertions(+), 107 deletions(-) diff --git a/Nevanlinna/complexHarmonic.examples.lean b/Nevanlinna/complexHarmonic.examples.lean index 30261aa..26b8fc4 100644 --- a/Nevanlinna/complexHarmonic.examples.lean +++ b/Nevanlinna/complexHarmonic.examples.lean @@ -1,27 +1,9 @@ -import Mathlib.Analysis.Complex.Basic -import Mathlib.Analysis.Complex.TaylorSeries -import Mathlib.Analysis.Calculus.LineDeriv.Basic -import Mathlib.Analysis.Calculus.ContDiff.Defs -import Mathlib.Analysis.Calculus.FDeriv.Basic -import Mathlib.Analysis.Calculus.FDeriv.Symmetric -import Mathlib.Analysis.RCLike.Basic -import Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv -import Mathlib.Data.Complex.Module -import Mathlib.Data.Complex.Order -import Mathlib.Data.Complex.Exponential -import Mathlib.Data.Fin.Tuple.Basic -import Mathlib.Topology.Algebra.InfiniteSum.Module -import Mathlib.Topology.Defs.Filter -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₁] theorem holomorphicAt_is_harmonicAt @@ -93,6 +75,18 @@ theorem log_normSq_of_holomorphicAt_is_harmonicAt (h₂f : f z ≠ 0) : HarmonicAt (Real.log ∘ Complex.normSq ∘ f) z := by + -- For later use + have slitPlaneLemma {z : ℂ} (hz : z ≠ 0) : z ∈ Complex.slitPlane ∨ -z ∈ Complex.slitPlane := by + rw [Complex.mem_slitPlane_iff, Complex.mem_slitPlane_iff] + simp at hz + rw [Complex.ext_iff] at hz + push_neg at hz + simp at hz + simp + by_contra contra + push_neg at contra + exact hz (le_antisymm contra.1.1 contra.2.1) contra.1.2 + -- 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 @@ -137,10 +131,44 @@ theorem log_normSq_of_holomorphicAt_is_harmonicAt simp apply hx.2 + -- Locally around z, rewrite Complex.log (g * gc) as Complex.log g + Complex.log.gc + -- This uses the assumption that g z is in Complex.slitPlane + have : (Complex.log ∘ (Complex.conjCLE ∘ g * g)) =ᶠ[nhds z] (Complex.conjCLE ∘ Complex.log ∘ g + Complex.log ∘ g) := by + apply Filter.eventuallyEq_iff_exists_mem.2 + use g⁻¹' (Complex.slitPlane ∩ {0}ᶜ) + constructor + · apply ContinuousAt.preimage_mem_nhds + · exact (HolomorphicAt_differentiableAt h₁g).continuousAt + · apply IsOpen.mem_nhds + apply IsOpen.inter Complex.isOpen_slitPlane isOpen_ne + constructor + · exact h₃g + · exact h₂g + · intro x hx + simp + rw [← Complex.log_conj] + rw [Complex.log_mul_eq_add_log_iff _ hx.2] + rw [Complex.arg_conj] + simp [Complex.slitPlane_arg_ne_pi hx.1] + constructor + · exact Real.pi_pos + · exact Real.pi_nonneg + simp + apply hx.2 + apply Complex.slitPlane_arg_ne_pi hx.1 + rw [HarmonicAt_eventuallyEq this] apply harmonicAt_add_harmonicAt_is_harmonicAt - · - sorry + · rw [← harmonicAt_iff_comp_CLE_is_harmonicAt] + apply holomorphicAt_is_harmonicAt + apply HolomorphicAt_comp + use Complex.slitPlane + constructor + · apply IsOpen.mem_nhds + exact Complex.isOpen_slitPlane + assumption + · exact fun z a => Complex.differentiableAt_log a + exact h₁g · apply holomorphicAt_is_harmonicAt apply HolomorphicAt_comp use Complex.slitPlane @@ -149,78 +177,16 @@ theorem log_normSq_of_holomorphicAt_is_harmonicAt exact Complex.isOpen_slitPlane assumption · exact fun z a => Complex.differentiableAt_log a + exact h₁g - - - - - sorry - assumption - - - - sorry - - - - -- Suffices to show Harmonic (Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f + Complex.log ∘ f) - -- THIS IS WHERE WE USE h₃ - have : (Complex.log ∘ (Complex.conjCLE ∘ f * f)) z = (Complex.log ∘ Complex.conjCLE ∘ f + Complex.log ∘ f) z := by - unfold Function.comp - simp - rw [Complex.log_mul_eq_add_log_iff] - - have : Complex.arg ((starRingEnd ℂ) (f z)) = - Complex.arg (f z) := by - rw [Complex.arg_conj] - have : ¬ Complex.arg (f z) = Real.pi := by - exact Complex.slitPlane_arg_ne_pi (h₃ z hz) - simp - tauto + by_cases h₃f : f z ∈ Complex.slitPlane + · exact lem₁ f h₁f h₂f h₃f + · have : Complex.normSq ∘ f = Complex.normSq ∘ (-f) := by funext; simp rw [this] - simp - constructor - · exact Real.pi_pos - · exact Real.pi_nonneg - exact (AddEquivClass.map_ne_zero_iff starRingAut).mpr (h₂ z hz) - exact h₂ z hz - - rw [HarmonicOn_congr hs this] - simp - - apply harmonicOn_add_harmonicOn_is_harmonicOn hs - - have : (fun x => Complex.log ((starRingEnd ℂ) (f x))) = (Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f) := by - rfl - rw [this] - - -- HarmonicOn (Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f) s - have : ∀ z ∈ s, (Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f) z = (Complex.conjCLE ∘ Complex.log ∘ f) z := by - intro z hz - unfold Function.comp - rw [Complex.log_conj] - rfl - exact Complex.slitPlane_arg_ne_pi (h₃ z hz) - rw [HarmonicOn_congr hs this] - - rw [← harmonicOn_iff_comp_CLE_is_harmonicOn] - - apply holomorphicOn_is_harmonicOn - exact hs - - intro z hz - apply DifferentiableAt.differentiableWithinAt - apply DifferentiableAt.comp - - - - exact Complex.differentiableAt_log (h₃ z hz) - apply DifferentiableOn.differentiableAt h₁ -- (h₁ z hz) - exact IsOpen.mem_nhds hs hz - exact hs - - -- HarmonicOn (Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f) s - apply holomorphicOn_is_harmonicOn hs - exact DifferentiableOn.clog h₁ h₃ + apply lem₁ (-f) + · exact HolomorphicAt_neg h₁f + · simpa + · exact (slitPlaneLemma h₂f).resolve_left h₃f theorem holomorphic_is_harmonic {f : ℂ → F₁} (h : Differentiable ℂ f) : diff --git a/Nevanlinna/holomorphic.lean b/Nevanlinna/holomorphic.lean index 782c0e2..e4eb207 100644 --- a/Nevanlinna/holomorphic.lean +++ b/Nevanlinna/holomorphic.lean @@ -1,21 +1,5 @@ -import Mathlib.Analysis.Complex.Basic import Mathlib.Analysis.Complex.TaylorSeries -import Mathlib.Analysis.Calculus.LineDeriv.Basic -import Mathlib.Analysis.Calculus.ContDiff.Defs -import Mathlib.Analysis.Calculus.FDeriv.Basic -import Mathlib.Analysis.Calculus.FDeriv.Symmetric -import Mathlib.Analysis.RCLike.Basic -import Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv -import Mathlib.Data.Complex.Module -import Mathlib.Data.Complex.Order -import Mathlib.Data.Complex.Exponential -import Mathlib.Data.Fin.Tuple.Basic -import Mathlib.Topology.Algebra.InfiniteSum.Module -import Mathlib.Topology.Defs.Filter -import Mathlib.Topology.Instances.RealVectorSpace import Nevanlinna.cauchyRiemann -import Nevanlinna.laplace -import Nevanlinna.complexHarmonic variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] @@ -28,7 +12,8 @@ def HolomorphicAt (f : E → F) (x : E) : Prop := theorem HolomorphicAt_iff {f : E → F} {x : E} : - HolomorphicAt f x ↔ ∃ s : Set E, IsOpen s ∧ x ∈ s ∧ (∀ z ∈ s, DifferentiableAt ℂ f z) := by + HolomorphicAt f x ↔ ∃ s : + Set E, IsOpen s ∧ x ∈ s ∧ (∀ z ∈ s, DifferentiableAt ℂ f z) := by constructor · intro hf obtain ⟨t, h₁t, h₂t⟩ := hf @@ -104,6 +89,21 @@ theorem HolomorphicAt_comp exact hx.1 +theorem HolomorphicAt_neg + {f : E → F} + {z : E} + (hf : HolomorphicAt f z) : + HolomorphicAt (-f) z := by + obtain ⟨UF, h₁UF, h₂UF⟩ := hf + use UF + constructor + · assumption + · intro z hz + apply differentiableAt_neg_iff.mp + simp + exact h₂UF z hz + + theorem HolomorphicAt_contDiffAt {f : ℂ → F} {z : ℂ}