This commit is contained in:
Stefan Kebekus 2024-06-11 13:28:02 +02:00
parent 5d5d7557c0
commit c3ec40490e
4 changed files with 396 additions and 592 deletions

View File

@ -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₃

View File

@ -163,6 +163,20 @@ theorem harmonic_smul_const_is_harmonic {f : → F} {c : } (h : Harmonic
simp 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) : theorem harmonic_iff_smul_const_is_harmonic {f : → F} {c : } (hc : c ≠ 0) :
Harmonic f ↔ Harmonic (c • f) := by Harmonic f ↔ Harmonic (c • f) := by
constructor 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 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) : theorem harmonic_comp_CLM_is_harmonic {f : → F₁} {l : F₁ →L[] G} (h : Harmonic f) :
Harmonic (l ∘ f) := by Harmonic (l ∘ f) := by

View File

@ -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

View File

@ -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]