nevanlinna/Nevanlinna/complexHarmonic.lean

402 lines
13 KiB
Plaintext
Raw Normal View History

2024-04-30 08:20:57 +02:00
import Mathlib.Analysis.Complex.Basic
2024-05-02 09:48:26 +02:00
import Mathlib.Analysis.Complex.TaylorSeries
2024-04-30 08:20:57 +02:00
import Mathlib.Analysis.Calculus.LineDeriv.Basic
import Mathlib.Analysis.Calculus.ContDiff.Defs
import Mathlib.Analysis.Calculus.FDeriv.Basic
2024-05-02 21:09:38 +02:00
import Mathlib.Analysis.Calculus.FDeriv.Symmetric
2024-05-15 15:03:16 +02:00
import Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
2024-05-08 08:27:12 +02:00
import Mathlib.Data.Complex.Module
import Mathlib.Data.Complex.Order
import Mathlib.Data.Complex.Exponential
2024-05-15 15:03:16 +02:00
import Mathlib.Data.Fin.Tuple.Basic
2024-05-08 08:27:12 +02:00
import Mathlib.Analysis.RCLike.Basic
import Mathlib.Topology.Algebra.InfiniteSum.Module
import Mathlib.Topology.Instances.RealVectorSpace
2024-04-30 08:20:57 +02:00
import Nevanlinna.cauchyRiemann
2024-05-13 09:23:08 +02:00
import Nevanlinna.laplace
2024-05-07 09:49:56 +02:00
import Nevanlinna.partialDeriv
2024-05-07 07:08:23 +02:00
2024-05-13 09:23:08 +02:00
variable {F : Type*} [NormedAddCommGroup F] [NormedSpace F]
2024-05-16 21:46:01 +02:00
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-04-30 08:20:57 +02:00
2024-05-13 09:23:08 +02:00
def Harmonic (f : → F) : Prop :=
2024-04-30 08:20:57 +02:00
(ContDiff 2 f) ∧ (∀ z, Complex.laplace f z = 0)
2024-05-03 12:23:09 +02:00
2024-05-18 12:13:30 +02:00
def HarmonicOn (f : → F) (s : Set ) : Prop :=
(ContDiffOn 2 f s) ∧ (∀ z ∈ s, Complex.laplace f z = 0)
theorem HarmonicOn_of_locally_HarmonicOn {f : → F} {s : Set } (h : ∀ x ∈ s, ∃ (u : Set ), IsOpen u ∧ x ∈ u ∧ HarmonicOn f (s ∩ u)) :
HarmonicOn f s := by
constructor
· apply contDiffOn_of_locally_contDiffOn
intro x xHyp
2024-05-30 16:20:06 +02:00
obtain ⟨u, uHyp⟩ := h x xHyp
2024-05-18 12:13:30 +02:00
use u
2024-05-29 16:33:32 +02:00
exact ⟨ uHyp.1, ⟨uHyp.2.1, uHyp.2.2.1⟩⟩
2024-05-18 12:13:30 +02:00
· intro x xHyp
2024-05-30 16:20:06 +02:00
obtain ⟨u, uHyp⟩ := h x xHyp
2024-05-18 12:13:30 +02:00
exact (uHyp.2.2.2) x ⟨xHyp, uHyp.2.1⟩
2024-05-30 16:20:06 +02:00
theorem HarmonicOn_congr {f₁ f₂ : → F} {s : Set } (hs : IsOpen s) (hf₁₂ : ∀ x ∈ s, f₁ x = f₂ x) :
HarmonicOn f₁ s ↔ HarmonicOn f₂ s := by
constructor
· intro h₁
constructor
· apply ContDiffOn.congr h₁.1
intro x hx
rw [eq_comm]
exact hf₁₂ x hx
· intro z hz
have : f₁ =ᶠ[nhds z] f₂ := by
unfold Filter.EventuallyEq
unfold Filter.Eventually
simp
2024-05-30 17:02:15 +02:00
refine mem_nhds_iff.mpr ?_
use s
constructor
· exact hf₁₂
· constructor
· exact hs
· exact hz
2024-05-30 16:20:06 +02:00
rw [← laplace_eventuallyEq this]
exact h₁.2 z hz
· intro h₁
constructor
· apply ContDiffOn.congr h₁.1
intro x hx
exact hf₁₂ x hx
· intro z hz
2024-05-30 17:02:15 +02:00
have : f₁ =ᶠ[nhds z] f₂ := by
unfold Filter.EventuallyEq
unfold Filter.Eventually
simp
refine mem_nhds_iff.mpr ?_
use s
constructor
· exact hf₁₂
· constructor
· exact hs
· exact hz
2024-05-30 16:20:06 +02:00
rw [laplace_eventuallyEq this]
exact h₁.2 z hz
2024-05-17 12:31:36 +02:00
theorem harmonic_add_harmonic_is_harmonic {f₁ f₂ : → F} (h₁ : Harmonic f₁) (h₂ : Harmonic f₂) :
2024-05-17 10:09:14 +02:00
Harmonic (f₁ + f₂) := by
constructor
· exact ContDiff.add h₁.1 h₂.1
· rw [laplace_add h₁.1 h₂.1]
simp
intro z
rw [h₁.2 z, h₂.2 z]
simp
2024-05-30 17:02:15 +02:00
theorem harmonicOn_add_harmonicOn_is_harmonicOn {f₁ f₂ : → F} {s : Set } (hs : IsOpen s) (h₁ : HarmonicOn f₁ s) (h₂ : HarmonicOn f₂ s) :
HarmonicOn (f₁ + f₂) s := by
constructor
· exact ContDiffOn.add h₁.1 h₂.1
· rw [laplace_add h₁.1 h₂.1]
simp
intro z
rw [h₁.2 z, h₂.2 z]
simp
2024-05-17 12:31:36 +02:00
theorem harmonic_smul_const_is_harmonic {f : → F} {c : } (h : Harmonic f) :
Harmonic (c • f) := by
constructor
· exact ContDiff.const_smul c h.1
· rw [laplace_smul h.1]
dsimp
intro z
rw [h.2 z]
simp
theorem harmonic_iff_smul_const_is_harmonic {f : → F} {c : } (hc : c ≠ 0) :
Harmonic f ↔ Harmonic (c • f) := by
constructor
· exact harmonic_smul_const_is_harmonic
· nth_rewrite 2 [((eq_inv_smul_iff₀ hc).mpr rfl : f = c⁻¹ • c • f)]
exact fun a => harmonic_smul_const_is_harmonic a
2024-05-17 09:19:24 +02:00
theorem harmonic_comp_CLM_is_harmonic {f : → F₁} {l : F₁ →L[] G} (h : Harmonic f) :
2024-05-16 21:46:01 +02:00
Harmonic (l ∘ f) := by
constructor
· -- Continuous differentiability
apply ContDiff.comp
exact ContinuousLinearMap.contDiff l
2024-05-17 09:19:24 +02:00
exact h.1
2024-05-16 21:46:01 +02:00
· rw [laplace_compContLin]
simp
intro z
rw [h.2 z]
simp
2024-05-17 09:19:24 +02:00
exact ContDiff.restrict_scalars h.1
2024-05-16 21:46:01 +02:00
2024-05-30 10:41:10 +02:00
theorem harmonicOn_comp_CLM_is_harmonicOn {f : → F₁} {s : Set } {l : F₁ →L[] G} (hs : IsOpen s) (h : HarmonicOn f s) :
2024-05-18 12:13:30 +02:00
HarmonicOn (l ∘ f) s := by
constructor
· -- Continuous differentiability
apply ContDiffOn.continuousLinearMap_comp
exact h.1
2024-05-29 16:33:32 +02:00
· -- Vanishing of Laplace
2024-05-18 12:13:30 +02:00
intro z zHyp
2024-05-30 10:41:10 +02:00
rw [laplace_compContLinAt]
simp
2024-05-18 12:13:30 +02:00
rw [h.2 z]
simp
assumption
2024-05-30 10:41:10 +02:00
apply ContDiffOn.contDiffAt h.1
exact IsOpen.mem_nhds hs zHyp
2024-05-29 16:33:32 +02:00
2024-05-16 21:46:01 +02:00
theorem harmonic_iff_comp_CLE_is_harmonic {f : → F₁} {l : F₁ ≃L[] G₁} :
Harmonic f ↔ Harmonic (l ∘ f) := by
constructor
· have : l ∘ f = (l : F₁ →L[] G₁) ∘ f := by rfl
rw [this]
exact harmonic_comp_CLM_is_harmonic
2024-05-17 09:05:15 +02:00
· have : f = (l.symm : G₁ →L[] F₁) ∘ l ∘ f := by
2024-05-16 21:46:01 +02:00
funext z
unfold Function.comp
simp
nth_rewrite 2 [this]
exact harmonic_comp_CLM_is_harmonic
theorem holomorphic_is_harmonic {f : → F₁} (h : Differentiable f) :
2024-05-06 17:01:10 +02:00
Harmonic f := by
-- f is real C²
have f_is_real_C2 : ContDiff 2 f :=
ContDiff.restrict_scalars (Differentiable.contDiff h)
2024-05-08 15:59:56 +02:00
have fI_is_real_differentiable : Differentiable (partialDeriv 1 f) := by
exact (partialDeriv_contDiff f_is_real_C2 1).differentiable (Submonoid.oneLE.proof_2 ℕ∞)
2024-04-30 08:20:57 +02:00
constructor
2024-05-06 09:01:43 +02:00
· -- f is two times real continuously differentiable
2024-05-06 17:01:10 +02:00
exact f_is_real_C2
2024-04-30 08:20:57 +02:00
· -- Laplace of f is zero
unfold Complex.laplace
2024-05-07 07:08:23 +02:00
rw [CauchyRiemann₄ h]
2024-05-08 07:15:34 +02:00
2024-05-08 08:32:06 +02:00
-- 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.
2024-05-17 09:19:24 +02:00
have : ∀ v, ∀ s : , ∀ g : → F₁, Differentiable g → partialDeriv v (s • g) = s • (partialDeriv v g) := by
2024-05-08 08:27:12 +02:00
intro v s g hg
2024-05-08 08:32:06 +02:00
-- Present scalar multiplication as a continuous -linear map. This is
-- horrible, there must be better ways to do that.
2024-05-17 09:19:24 +02:00
let sMuls : F₁ →L[] F₁ :=
2024-05-08 08:27:12 +02:00
{
2024-05-17 09:19:24 +02:00
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
2024-05-08 08:27:12 +02:00
}
2024-05-08 07:15:34 +02:00
2024-05-08 08:32:06 +02:00
-- Bring the goal into a form that is recognized by
-- partialDeriv_compContLin.
2024-05-08 08:27:12 +02:00
have : s • g = sMuls ∘ g := by rfl
rw [this]
2024-05-08 08:32:06 +02:00
2024-05-08 15:59:56 +02:00
rw [partialDeriv_compContLin hg]
2024-05-08 08:27:12 +02:00
rfl
2024-05-08 07:15:34 +02:00
2024-05-08 08:27:12 +02:00
rw [this]
2024-05-07 10:16:23 +02:00
rw [partialDeriv_comm f_is_real_C2 Complex.I 1]
rw [CauchyRiemann₄ h]
2024-05-08 08:27:12 +02:00
rw [this]
2024-05-07 10:16:23 +02:00
rw [← smul_assoc]
2024-05-02 21:09:38 +02:00
simp
2024-05-08 08:27:12 +02:00
-- 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
2024-05-13 09:23:08 +02:00
2024-05-16 21:46:01 +02:00
theorem re_of_holomorphic_is_harmonic {f : } (h : Differentiable f) :
2024-05-13 09:23:08 +02:00
Harmonic (Complex.reCLM ∘ f) := by
2024-05-16 21:46:01 +02:00
apply harmonic_comp_CLM_is_harmonic
exact holomorphic_is_harmonic h
2024-05-13 09:23:08 +02:00
2024-05-16 21:46:01 +02:00
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
2024-05-17 09:05:15 +02:00
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
2024-05-18 12:13:30 +02:00
theorem log_normSq_of_holomorphicOn_is_harmonicOn
{f : }
{s : Set }
2024-05-30 10:41:10 +02:00
(hs : IsOpen s)
2024-05-18 12:13:30 +02:00
(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
2024-05-30 10:41:10 +02:00
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)
2024-05-18 12:13:30 +02:00
2024-05-30 10:41:10 +02:00
suffices hyp : HarmonicOn (Complex.log ∘ (((starRingEnd ) ∘ f) * f)) s from by
2024-05-18 12:13:30 +02:00
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₃
2024-05-30 10:49:16 +02:00
have : ∀ z ∈ s, (Complex.log ∘ (⇑(starRingEnd ) ∘ f * f)) z = (Complex.log ∘ ⇑(starRingEnd ) ∘ f + Complex.log ∘ f) z := by
intro z hz
2024-05-18 12:13:30 +02:00
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
2024-05-30 10:49:16 +02:00
exact Complex.slitPlane_arg_ne_pi (h₃ z hz)
2024-05-18 12:13:30 +02:00
simp
tauto
rw [this]
simp
constructor
· exact Real.pi_pos
· exact Real.pi_nonneg
2024-05-30 10:49:16 +02:00
exact (AddEquivClass.map_ne_zero_iff starRingAut).mpr (h₂ z hz)
exact h₂ z hz
2024-05-30 17:02:15 +02:00
rw [HarmonicOn_congr hs this]
2024-05-30 16:20:06 +02:00
simp
2024-05-18 12:13:30 +02:00
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
2024-05-16 21:46:01 +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
2024-05-17 12:31:36 +02:00
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))
2024-05-16 21:46:01 +02:00
2024-05-17 12:31:36 +02:00
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
2024-05-16 21:46:01 +02:00
2024-05-17 10:09:14 +02:00
-- 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]
2024-05-13 10:10:10 +02:00
2024-05-17 10:09:14 +02:00
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]
2024-05-16 21:46:01 +02:00
simp
2024-05-17 10:09:14 +02:00
constructor
· exact Real.pi_pos
· exact Real.pi_nonneg
exact (AddEquivClass.map_ne_zero_iff starRingAut).mpr (h₂ z)
2024-05-16 21:46:01 +02:00
exact h₂ z
2024-05-17 10:09:14 +02:00
rw [this]
2024-05-13 09:23:08 +02:00
2024-05-17 10:09:14 +02:00
apply harmonic_add_harmonic_is_harmonic
have : Complex.log ∘ ⇑(starRingEnd ) ∘ f = Complex.conjCLE ∘ Complex.log ∘ f := by
2024-05-16 21:46:01 +02:00
funext z
unfold Function.comp
rw [Complex.log_conj]
rfl
exact Complex.slitPlane_arg_ne_pi (h₃ z)
2024-05-17 10:09:14 +02:00
rw [this]
rw [← harmonic_iff_comp_CLE_is_harmonic]
2024-05-13 10:10:10 +02:00
2024-05-17 10:09:14 +02:00
repeat
apply holomorphic_is_harmonic
2024-05-13 10:10:10 +02:00
intro z
2024-05-17 10:09:14 +02:00
apply DifferentiableAt.comp
exact Complex.differentiableAt_log (h₃ z)
exact h₁ z
2024-05-14 09:47:46 +02:00
theorem logabs_of_holomorphic_is_harmonic
{f : }
(h₁ : Differentiable f)
2024-05-15 10:09:22 +02:00
(h₂ : ∀ z, f z ≠ 0)
(h₃ : ∀ z, f z ∈ Complex.slitPlane) :
2024-05-14 09:47:46 +02:00
Harmonic (fun z ↦ Real.log ‖f z‖) := by
2024-05-17 12:31:36 +02:00
-- Suffices: Harmonic (2⁻¹ • Real.log ∘ ⇑Complex.normSq ∘ f)
have : (fun z ↦ Real.log ‖f z‖) = (2 : )⁻¹ • (Real.log ∘ Complex.normSq ∘ f) := by
2024-05-16 10:01:15 +02:00
funext z
2024-05-15 15:03:16 +02:00
simp
2024-05-17 12:31:36 +02:00
unfold Complex.abs
2024-05-15 21:17:42 +02:00
simp
2024-05-17 12:31:36 +02:00
rw [Real.log_sqrt]
rw [div_eq_inv_mul (Real.log (Complex.normSq (f z))) 2]
exact Complex.normSq_nonneg (f z)
rw [this]
2024-05-16 09:19:45 +02:00
2024-05-17 12:31:36 +02:00
-- Suffices: Harmonic (Real.log ∘ ⇑Complex.normSq ∘ f)
apply (harmonic_iff_smul_const_is_harmonic (inv_ne_zero two_ne_zero)).1
2024-05-16 09:19:45 +02:00
2024-05-17 12:31:36 +02:00
exact log_normSq_of_holomorphic_is_harmonic h₁ h₂ h₃