nevanlinna/Nevanlinna/complexHarmonic.examples.lean

470 lines
15 KiB
Plaintext
Raw Normal View History

2024-06-03 13:59:10 +02:00
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
2024-06-03 17:32:33 +02:00
import Mathlib.Topology.Defs.Filter
2024-06-03 13:59:10 +02:00
import Mathlib.Topology.Instances.RealVectorSpace
import Nevanlinna.cauchyRiemann
import Nevanlinna.laplace
import Nevanlinna.complexHarmonic
2024-06-05 12:03:05 +02:00
import Nevanlinna.holomorphic
2024-06-03 13:59:10 +02:00
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₁]
2024-06-05 12:03:05 +02:00
#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
2024-06-03 13:59:10 +02:00
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₃
2024-06-03 17:32:33 +02:00
theorem log_normSq_of_holomorphicOn_is_harmonicOn
{f : }
{s : Set }
(hs : IsOpen s)
(h₁ : DifferentiableOn f s)
2024-06-03 18:45:31 +02:00
(h₂ : ∀ z ∈ s, f z ≠ 0) :
2024-06-03 17:32:33 +02:00
HarmonicOn (Real.log ∘ Complex.normSq ∘ f) s := by
2024-06-04 10:27:46 +02:00
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
2024-06-03 17:32:33 +02:00
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
2024-06-03 18:45:31 +02:00
intro z hz
apply hz.1
2024-06-03 17:32:33 +02:00
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₂
2024-06-03 18:45:31 +02:00
constructor
· exact hs₂
· constructor
2024-06-03 18:53:55 +02:00
· constructor
2024-06-04 10:27:46 +02:00
· apply Or.resolve_left (slitPlaneLemma (h₂ z hz)) hfz
· exact hz
2024-06-03 18:45:31 +02:00
· 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₂
2024-06-03 17:32:33 +02:00
2024-06-03 13:59:10 +02:00
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₃