From c3ec40490e744df258f2a9ca4f4acf979167f091 Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Tue, 11 Jun 2024 13:28:02 +0200 Subject: [PATCH] working --- Nevanlinna/complexHarmonic.examples.lean | 592 ----------------------- Nevanlinna/complexHarmonic.lean | 26 + Nevanlinna/harmonicAt.examples.lean | 211 ++++++++ Nevanlinna/holomorphicAt.lean | 159 ++++++ 4 files changed, 396 insertions(+), 592 deletions(-) delete mode 100644 Nevanlinna/complexHarmonic.examples.lean create mode 100644 Nevanlinna/harmonicAt.examples.lean create mode 100644 Nevanlinna/holomorphicAt.lean diff --git a/Nevanlinna/complexHarmonic.examples.lean b/Nevanlinna/complexHarmonic.examples.lean deleted file mode 100644 index 9db98eb..0000000 --- a/Nevanlinna/complexHarmonic.examples.lean +++ /dev/null @@ -1,592 +0,0 @@ -import Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv -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] - - -theorem holomorphicAt_is_harmonicAt - {f : ℂ → F₁} - {z : ℂ} - (hf : HolomorphicAt f z) : - HarmonicAt f z := by - - let t := {x | HolomorphicAt f x} - have ht : IsOpen t := HolomorphicAt_isOpen f - have hz : z ∈ t := by exact hf - - constructor - · -- ContDiffAt ℝ 2 f z - exact HolomorphicAt_contDiffAt hf - - · -- Δ f =ᶠ[nhds z] 0 - 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'₆ hw) Complex.I] - rw [partialDeriv_smul'₂] - simp - - rw [partialDeriv_commAt (HolomorphicAt_contDiffAt hw) Complex.I 1] - rw [partialDeriv_eventuallyEq ℝ (CauchyRiemann'₆ hw) 1] - rw [partialDeriv_smul'₂] - simp - - rw [← smul_assoc] - 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 log_normSq_of_holomorphicAt_is_harmonicAt - {f : ℂ → ℂ} - {z : ℂ} - (h₁f : HolomorphicAt f z) - (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 - - -- Rewrite the log |g|² as Complex.log (g * gc) - suffices hyp : HarmonicAt (Complex.log ∘ ((Complex.conjCLE ∘ g) * g)) z from by - have : Real.log ∘ Complex.normSq ∘ g = Complex.reCLM ∘ Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ g := by - funext x - simp - rw [this] - - have : Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ g = Complex.log ∘ ((Complex.conjCLE ∘ g) * g) := by - funext x - simp - rw [Complex.ofReal_log] - rw [Complex.normSq_eq_conj_mul_self] - exact Complex.normSq_nonneg (g x) - rw [← this] at hyp - apply harmonicAt_comp_CLM_is_harmonicAt hyp - - -- 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.log ∘ Complex.conjCLE ∘ 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_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 - - -- 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 - · 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 - constructor - · apply IsOpen.mem_nhds - exact Complex.isOpen_slitPlane - assumption - · exact fun z a => Complex.differentiableAt_log a - exact h₁g - - 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] - 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) : - Harmonic f := by - - -- f is real C² - have f_is_real_C2 : ContDiff ℝ 2 f := - ContDiff.restrict_scalars ℝ (Differentiable.contDiff h) - - have fI_is_real_differentiable : Differentiable ℝ (partialDeriv ℝ 1 f) := by - exact (partialDeriv_contDiff ℝ f_is_real_C2 1).differentiable (Submonoid.oneLE.proof_2 ℕ∞) - - constructor - · -- f is two times real continuously differentiable - exact f_is_real_C2 - - · -- Laplace of f is zero - unfold Complex.laplace - rw [CauchyRiemann₄ h] - - -- This lemma says that partial derivatives commute with complex scalar - -- multiplication. This is a consequence of partialDeriv_compContLin once we - -- note that complex scalar multiplication is continuous ℝ-linear. - have : ∀ v, ∀ s : ℂ, ∀ g : ℂ → F₁, Differentiable ℝ g → partialDeriv ℝ v (s • g) = s • (partialDeriv ℝ v g) := by - intro v s g hg - - -- Present scalar multiplication as a continuous ℝ-linear map. This is - -- horrible, there must be better ways to do that. - let sMuls : F₁ →L[ℝ] F₁ := - { - toFun := fun x ↦ s • x - map_add' := by exact fun x y => DistribSMul.smul_add s x y - map_smul' := by exact fun m x => (smul_comm ((RingHom.id ℝ) m) s x).symm - cont := continuous_const_smul s - } - - -- Bring the goal into a form that is recognized by - -- partialDeriv_compContLin. - have : s • g = sMuls ∘ g := by rfl - rw [this] - - rw [partialDeriv_compContLin ℝ hg] - rfl - - rw [this] - rw [partialDeriv_comm f_is_real_C2 Complex.I 1] - rw [CauchyRiemann₄ h] - rw [this] - rw [← smul_assoc] - simp - - -- Subgoals coming from the application of 'this' - -- Differentiable ℝ (Real.partialDeriv 1 f) - exact fI_is_real_differentiable - -- Differentiable ℝ (Real.partialDeriv 1 f) - exact fI_is_real_differentiable - - -theorem holomorphicOn_is_harmonicOn {f : ℂ → F₁} {s : Set ℂ} (hs : IsOpen s) (h : DifferentiableOn ℂ f s) : - HarmonicOn f s := by - - -- f is real C² - have f_is_real_C2 : ContDiffOn ℝ 2 f s := - ContDiffOn.restrict_scalars ℝ (DifferentiableOn.contDiffOn h hs) - - constructor - · -- f is two times real continuously differentiable - exact f_is_real_C2 - - · -- Laplace of f is zero - unfold Complex.laplace - intro z hz - simp - have : partialDeriv ℝ Complex.I f =ᶠ[nhds z] Complex.I • partialDeriv ℝ 1 f := by - unfold Filter.EventuallyEq - unfold Filter.Eventually - simp - refine mem_nhds_iff.mpr ?_ - use s - constructor - · intro x hx - simp - apply CauchyRiemann₅ - apply DifferentiableOn.differentiableAt h - exact IsOpen.mem_nhds hs hx - · constructor - · exact hs - · exact hz - rw [partialDeriv_eventuallyEq ℝ this Complex.I] - rw [partialDeriv_smul'₂] - - simp - rw [partialDeriv_commOn hs f_is_real_C2 Complex.I 1 z hz] - - have : partialDeriv ℝ Complex.I f =ᶠ[nhds z] Complex.I • partialDeriv ℝ 1 f := by - unfold Filter.EventuallyEq - unfold Filter.Eventually - simp - refine mem_nhds_iff.mpr ?_ - use s - constructor - · intro x hx - simp - apply CauchyRiemann₅ - apply DifferentiableOn.differentiableAt h - exact IsOpen.mem_nhds hs hx - · constructor - · exact hs - · exact hz - rw [partialDeriv_eventuallyEq ℝ this 1] - rw [partialDeriv_smul'₂] - simp - rw [← smul_assoc] - simp - - -theorem re_of_holomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f) : - Harmonic (Complex.reCLM ∘ f) := by - apply harmonic_comp_CLM_is_harmonic - exact holomorphic_is_harmonic h - - -theorem im_of_holomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f) : - Harmonic (Complex.imCLM ∘ f) := by - apply harmonic_comp_CLM_is_harmonic - exact holomorphic_is_harmonic h - - -theorem antiholomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f) : - Harmonic (Complex.conjCLE ∘ f) := by - apply harmonic_iff_comp_CLE_is_harmonic.1 - exact holomorphic_is_harmonic h - - -theorem log_normSq_of_holomorphicOn_is_harmonicOn' - {f : ℂ → ℂ} - {s : Set ℂ} - (hs : IsOpen s) - (h₁ : DifferentiableOn ℂ f s) - (h₂ : ∀ z ∈ s, f z ≠ 0) - (h₃ : ∀ z ∈ s, f z ∈ Complex.slitPlane) : - HarmonicOn (Real.log ∘ Complex.normSq ∘ f) s := by - - suffices hyp : HarmonicOn (⇑Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ f) s from - (harmonicOn_comp_CLM_is_harmonicOn hs hyp : HarmonicOn (Complex.reCLM ∘ Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ f) s) - - suffices hyp : HarmonicOn (Complex.log ∘ (((starRingEnd ℂ) ∘ f) * f)) s from by - have : Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ f = Complex.log ∘ (((starRingEnd ℂ) ∘ f) * f) := by - funext z - simp - rw [Complex.ofReal_log (Complex.normSq_nonneg (f z))] - rw [Complex.normSq_eq_conj_mul_self] - rw [this] - exact hyp - - - -- Suffices to show Harmonic (Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f + Complex.log ∘ f) - -- THIS IS WHERE WE USE h₃ - have : ∀ z ∈ s, (Complex.log ∘ (⇑(starRingEnd ℂ) ∘ f * f)) z = (Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f + Complex.log ∘ f) z := by - intro z hz - 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 - 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₃ - - -theorem log_normSq_of_holomorphicOn_is_harmonicOn - {f : ℂ → ℂ} - {s : Set ℂ} - (hs : IsOpen s) - (h₁ : DifferentiableOn ℂ f s) - (h₂ : ∀ z ∈ s, f z ≠ 0) : - HarmonicOn (Real.log ∘ Complex.normSq ∘ f) s := by - - have slitPlaneLemma {z : ℂ} (hz : z ≠ 0) : z ∈ Complex.slitPlane ∨ -z ∈ Complex.slitPlane := by - rw [Complex.mem_slitPlane_iff] - rw [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 - - let s₁ : Set ℂ := { z | f z ∈ Complex.slitPlane} ∩ s - - have hs₁ : IsOpen s₁ := by - let A := DifferentiableOn.continuousOn h₁ - let B := continuousOn_iff'.1 A - obtain ⟨u, hu₁, hu₂⟩ := B Complex.slitPlane Complex.isOpen_slitPlane - have : u ∩ s = s₁ := by - rw [← hu₂] - tauto - rw [← this] - apply IsOpen.inter hu₁ hs - - have harm₁ : HarmonicOn (Real.log ∘ Complex.normSq ∘ f) s₁ := by - apply log_normSq_of_holomorphicOn_is_harmonicOn' - exact hs₁ - apply DifferentiableOn.mono h₁ (Set.inter_subset_right {z | f z ∈ Complex.slitPlane} s) - -- ∀ z ∈ s₁, f z ≠ 0 - exact fun z hz ↦ h₂ z (Set.mem_of_mem_inter_right hz) - -- ∀ z ∈ s₁, f z ∈ Complex.slitPlane - intro z hz - apply hz.1 - - let s₂ : Set ℂ := { z | -f z ∈ Complex.slitPlane} ∩ s - - have h₁' : DifferentiableOn ℂ (-f) s := by - rw [← differentiableOn_neg_iff] - simp - exact h₁ - - have hs₂ : IsOpen s₂ := by - let A := DifferentiableOn.continuousOn h₁' - let B := continuousOn_iff'.1 A - obtain ⟨u, hu₁, hu₂⟩ := B Complex.slitPlane Complex.isOpen_slitPlane - have : u ∩ s = s₂ := by - rw [← hu₂] - tauto - rw [← this] - apply IsOpen.inter hu₁ hs - - have harm₂ : HarmonicOn (Real.log ∘ Complex.normSq ∘ (-f)) s₂ := by - apply log_normSq_of_holomorphicOn_is_harmonicOn' - exact hs₂ - apply DifferentiableOn.mono h₁' (Set.inter_subset_right {z | -f z ∈ Complex.slitPlane} s) - -- ∀ z ∈ s₁, f z ≠ 0 - intro z hz - simp - exact h₂ z (Set.mem_of_mem_inter_right hz) - -- ∀ z ∈ s₁, f z ∈ Complex.slitPlane - intro z hz - apply hz.1 - - apply HarmonicOn_of_locally_HarmonicOn - intro z hz - by_cases hfz : f z ∈ Complex.slitPlane - · use s₁ - constructor - · exact hs₁ - · constructor - · tauto - · have : s₁ = s ∩ s₁ := by - apply Set.right_eq_inter.mpr - exact Set.inter_subset_right {z | f z ∈ Complex.slitPlane} s - rw [← this] - exact harm₁ - · use s₂ - constructor - · exact hs₂ - · constructor - · constructor - · apply Or.resolve_left (slitPlaneLemma (h₂ z hz)) hfz - · exact hz - · have : s₂ = s ∩ s₂ := by - apply Set.right_eq_inter.mpr - exact Set.inter_subset_right {z | -f z ∈ Complex.slitPlane} s - rw [← this] - have : Real.log ∘ ⇑Complex.normSq ∘ f = Real.log ∘ ⇑Complex.normSq ∘ (-f) := by - funext x - simp - rw [this] - exact harm₂ - - -theorem log_normSq_of_holomorphic_is_harmonic - {f : ℂ → ℂ} - (h₁ : Differentiable ℂ f) - (h₂ : ∀ z, f z ≠ 0) - (h₃ : ∀ z, f z ∈ Complex.slitPlane) : - Harmonic (Real.log ∘ Complex.normSq ∘ f) := by - - suffices hyp : Harmonic (⇑Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ f) from - (harmonic_comp_CLM_is_harmonic hyp : Harmonic (Complex.reCLM ∘ Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ f)) - - suffices hyp : Harmonic (Complex.log ∘ (((starRingEnd ℂ) ∘ f) * f)) from by - have : Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ f = Complex.log ∘ (((starRingEnd ℂ) ∘ f) * f) := by - funext z - simp - rw [Complex.ofReal_log (Complex.normSq_nonneg (f z))] - rw [Complex.normSq_eq_conj_mul_self] - rw [this] - exact hyp - - - -- Suffices to show Harmonic (Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f + Complex.log ∘ f) - -- THIS IS WHERE WE USE h₃ - have : Complex.log ∘ (⇑(starRingEnd ℂ) ∘ f * f) = Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f + Complex.log ∘ f := by - unfold Function.comp - funext z - 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) - simp - tauto - rw [this] - simp - constructor - · exact Real.pi_pos - · exact Real.pi_nonneg - exact (AddEquivClass.map_ne_zero_iff starRingAut).mpr (h₂ z) - exact h₂ z - rw [this] - - apply harmonic_add_harmonic_is_harmonic - have : Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f = Complex.conjCLE ∘ Complex.log ∘ f := by - funext z - unfold Function.comp - rw [Complex.log_conj] - rfl - exact Complex.slitPlane_arg_ne_pi (h₃ z) - rw [this] - rw [← harmonic_iff_comp_CLE_is_harmonic] - - repeat - apply holomorphic_is_harmonic - intro z - apply DifferentiableAt.comp - exact Complex.differentiableAt_log (h₃ z) - exact h₁ z - - -theorem logabs_of_holomorphic_is_harmonic - {f : ℂ → ℂ} - (h₁ : Differentiable ℂ f) - (h₂ : ∀ z, f z ≠ 0) - (h₃ : ∀ z, f z ∈ Complex.slitPlane) : - Harmonic (fun z ↦ Real.log ‖f z‖) := by - - -- Suffices: Harmonic (2⁻¹ • Real.log ∘ ⇑Complex.normSq ∘ f) - have : (fun z ↦ Real.log ‖f z‖) = (2 : ℝ)⁻¹ • (Real.log ∘ Complex.normSq ∘ f) := by - funext z - simp - unfold Complex.abs - simp - rw [Real.log_sqrt] - rw [div_eq_inv_mul (Real.log (Complex.normSq (f z))) 2] - exact Complex.normSq_nonneg (f z) - rw [this] - - -- Suffices: Harmonic (Real.log ∘ ⇑Complex.normSq ∘ f) - apply (harmonic_iff_smul_const_is_harmonic (inv_ne_zero two_ne_zero)).1 - - exact log_normSq_of_holomorphic_is_harmonic h₁ h₂ h₃ diff --git a/Nevanlinna/complexHarmonic.lean b/Nevanlinna/complexHarmonic.lean index cdd9e9c..d604f03 100644 --- a/Nevanlinna/complexHarmonic.lean +++ b/Nevanlinna/complexHarmonic.lean @@ -163,6 +163,20 @@ theorem harmonic_smul_const_is_harmonic {f : ℂ → F} {c : ℝ} (h : Harmonic simp +theorem harmonicAt_smul_const_is_harmonicAt + {f : ℂ → F} + {x : ℂ} + {c : ℝ} + (h : HarmonicAt f x) : + HarmonicAt (c • f) x := by + constructor + · exact ContDiffAt.const_smul c h.1 + · rw [laplace_smul] + have A := Filter.EventuallyEq.const_smul h.2 c + simp at A + assumption + + theorem harmonic_iff_smul_const_is_harmonic {f : ℂ → F} {c : ℝ} (hc : c ≠ 0) : Harmonic f ↔ Harmonic (c • f) := by constructor @@ -171,6 +185,18 @@ theorem harmonic_iff_smul_const_is_harmonic {f : ℂ → F} {c : ℝ} (hc : c exact fun a => harmonic_smul_const_is_harmonic a +theorem harmonicAt_iff_smul_const_is_harmonicAt + {f : ℂ → F} + {x : ℂ} + {c : ℝ} + (hc : c ≠ 0) : + HarmonicAt f x ↔ HarmonicAt (c • f) x := by + constructor + · exact harmonicAt_smul_const_is_harmonicAt + · nth_rewrite 2 [((eq_inv_smul_iff₀ hc).mpr rfl : f = c⁻¹ • c • f)] + exact fun a => harmonicAt_smul_const_is_harmonicAt a + + theorem harmonic_comp_CLM_is_harmonic {f : ℂ → F₁} {l : F₁ →L[ℝ] G} (h : Harmonic f) : Harmonic (l ∘ f) := by diff --git a/Nevanlinna/harmonicAt.examples.lean b/Nevanlinna/harmonicAt.examples.lean new file mode 100644 index 0000000..0dff6b6 --- /dev/null +++ b/Nevanlinna/harmonicAt.examples.lean @@ -0,0 +1,211 @@ +import Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv +import Nevanlinna.complexHarmonic +import Nevanlinna.holomorphicAt + +variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] + + +theorem holomorphicAt_is_harmonicAt + {f : ℂ → F} + {z : ℂ} + (hf : HolomorphicAt f z) : + HarmonicAt f z := by + + let t := {x | HolomorphicAt f x} + have ht : IsOpen t := HolomorphicAt_isOpen f + have hz : z ∈ t := by exact hf + + constructor + · -- ContDiffAt ℝ 2 f z + exact hf.contDiffAt + + · -- Δ f =ᶠ[nhds z] 0 + 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 ℝ hw.CauchyRiemannAt Complex.I] + rw [partialDeriv_smul'₂] + simp + + rw [partialDeriv_commAt hw.contDiffAt Complex.I 1] + rw [partialDeriv_eventuallyEq ℝ hw.CauchyRiemannAt 1] + rw [partialDeriv_smul'₂] + simp + + rw [← smul_assoc] + 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 log_normSq_of_holomorphicAt_is_harmonicAt + {f : ℂ → ℂ} + {z : ℂ} + (h₁f : HolomorphicAt f z) + (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 + + -- Rewrite the log |g|² as Complex.log (g * gc) + suffices hyp : HarmonicAt (Complex.log ∘ ((Complex.conjCLE ∘ g) * g)) z from by + have : Real.log ∘ Complex.normSq ∘ g = Complex.reCLM ∘ Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ g := by + funext x + simp + rw [this] + + have : Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ g = Complex.log ∘ ((Complex.conjCLE ∘ g) * g) := by + funext x + simp + rw [Complex.ofReal_log] + rw [Complex.normSq_eq_conj_mul_self] + exact Complex.normSq_nonneg (g x) + rw [← this] at hyp + apply harmonicAt_comp_CLM_is_harmonicAt hyp + + -- 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.log ∘ Complex.conjCLE ∘ g + Complex.log ∘ g) := by + apply Filter.eventuallyEq_iff_exists_mem.2 + use g⁻¹' (Complex.slitPlane ∩ {0}ᶜ) + constructor + · apply ContinuousAt.preimage_mem_nhds + · exact h₁g.differentiableAt.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_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 + + -- 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 h₁g.differentiableAt.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 + · 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 + constructor + · apply IsOpen.mem_nhds + exact Complex.isOpen_slitPlane + assumption + · exact fun z a => Complex.differentiableAt_log a + exact h₁g + + 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] + apply lem₁ (-f) + · exact HolomorphicAt_neg h₁f + · simpa + · exact (slitPlaneLemma h₂f).resolve_left h₃f + + +theorem logabs_of_holomorphicAt_is_harmonic + {f : ℂ → ℂ} + {z : ℂ} + (h₁f : HolomorphicAt f z) + (h₂f : f z ≠ 0) : + HarmonicAt (fun w ↦ Real.log ‖f w‖) z := by + + -- Suffices: Harmonic (2⁻¹ • Real.log ∘ ⇑Complex.normSq ∘ f) + have : (fun z ↦ Real.log ‖f z‖) = (2 : ℝ)⁻¹ • (Real.log ∘ Complex.normSq ∘ f) := by + funext z + simp + unfold Complex.abs + simp + rw [Real.log_sqrt] + rw [div_eq_inv_mul (Real.log (Complex.normSq (f z))) 2] + exact Complex.normSq_nonneg (f z) + rw [this] + + -- Suffices: Harmonic (Real.log ∘ ⇑Complex.normSq ∘ f) + apply (harmonicAt_iff_smul_const_is_harmonicAt (inv_ne_zero two_ne_zero)).1 + exact log_normSq_of_holomorphicAt_is_harmonicAt h₁f h₂f diff --git a/Nevanlinna/holomorphicAt.lean b/Nevanlinna/holomorphicAt.lean new file mode 100644 index 0000000..e6ae80a --- /dev/null +++ b/Nevanlinna/holomorphicAt.lean @@ -0,0 +1,159 @@ +import Mathlib.Analysis.Complex.TaylorSeries +import Nevanlinna.cauchyRiemann + +variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] +variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] +variable {G : Type*} [NormedAddCommGroup G] [NormedSpace ℂ G] + +def HolomorphicAt (f : E → F) (x : E) : Prop := + ∃ s ∈ nhds x, ∀ z ∈ s, DifferentiableAt ℂ f z + + +theorem HolomorphicAt_iff + {f : E → F} + {x : E} : + 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 + obtain ⟨s, h₁s, h₂s, h₃s⟩ := mem_nhds_iff.1 h₁t + use s + constructor + · assumption + · constructor + · assumption + · intro z hz + exact h₂t z (h₁s hz) + · intro hyp + obtain ⟨s, h₁s, h₂s, hf⟩ := hyp + use s + constructor + · apply (IsOpen.mem_nhds_iff h₁s).2 h₂s + · 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_comp + {g : E → F} + {f : F → G} + {z : E} + (hf : HolomorphicAt f (g z)) + (hg : HolomorphicAt g z) : + HolomorphicAt (f ∘ g) z := by + obtain ⟨UE, h₁UE, h₂UE⟩ := hg + obtain ⟨UF, h₁UF, h₂UF⟩ := hf + use UE ∩ g⁻¹' UF + constructor + · simp + constructor + · assumption + · apply ContinuousAt.preimage_mem_nhds + apply (h₂UE z (mem_of_mem_nhds h₁UE)).continuousAt + assumption + · intro x hx + apply DifferentiableAt.comp + apply h₂UF + exact hx.2 + apply h₂UE + 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 + [CompleteSpace F] + {f : ℂ → F} + {z : ℂ} + {n : ℕ} + (hf : HolomorphicAt f z) : + ContDiffAt ℝ n f z := by + + let t := {x | HolomorphicAt f x} + have ht : IsOpen t := HolomorphicAt_isOpen f + have hz : z ∈ t := by exact hf + + -- ContDiffAt ℝ _ f z + apply ContDiffOn.contDiffAt _ ((IsOpen.mem_nhds_iff ht).2 hz) + suffices h : ContDiffOn ℂ n f t from by + apply ContDiffOn.restrict_scalars ℝ h + apply DifferentiableOn.contDiffOn _ ht + intro w hw + apply DifferentiableAt.differentiableWithinAt + -- DifferentiableAt ℂ f w + let hfw : HolomorphicAt f w := hw + obtain ⟨s, _, h₂s, h₃s⟩ := HolomorphicAt_iff.1 hfw + exact h₃s w h₂s + + +theorem HolomorphicAt.differentiableAt + {f : ℂ → F} + {z : ℂ} + (hf : HolomorphicAt f z) : + DifferentiableAt ℂ f z := by + obtain ⟨s, _, h₂s, h₃s⟩ := HolomorphicAt_iff.1 hf + exact h₃s z h₂s + + +theorem HolomorphicAt.CauchyRiemannAt + {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 + + apply Filter.eventuallyEq_iff_exists_mem.2 + use s + constructor + · exact IsOpen.mem_nhds h₁s hz + · intro w hw + let h := h₂f w hw + -- WARNING This should go to partialDeriv + unfold partialDeriv + simp + conv => + left + rw [DifferentiableAt.fderiv_restrictScalars ℝ h] + simp + rw [← mul_one Complex.I] + rw [← smul_eq_mul] + rw [ContinuousLinearMap.map_smul_of_tower (fderiv ℂ f w) Complex.I 1] + conv => + right + right + rw [DifferentiableAt.fderiv_restrictScalars ℝ h]