267 lines
8.1 KiB
Plaintext
267 lines
8.1 KiB
Plaintext
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.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.Analysis.RCLike.Basic
|
||
import Mathlib.Topology.Algebra.InfiniteSum.Module
|
||
import Mathlib.Topology.Instances.RealVectorSpace
|
||
import Nevanlinna.cauchyRiemann
|
||
import Nevanlinna.laplace
|
||
import Nevanlinna.partialDeriv
|
||
|
||
variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
|
||
|
||
|
||
def Harmonic (f : ℂ → F) : Prop :=
|
||
(ContDiff ℝ 2 f) ∧ (∀ z, Complex.laplace f z = 0)
|
||
|
||
|
||
theorem holomorphic_is_harmonic {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 : ℂ → ℂ, 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 : ℂ →L[ℝ] ℂ :=
|
||
{
|
||
toFun := fun x ↦ s * x
|
||
map_add' := by
|
||
intro x y
|
||
ring
|
||
map_smul' := by
|
||
intro m x
|
||
simp
|
||
ring
|
||
}
|
||
|
||
-- 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 re_of_holomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f) :
|
||
Harmonic (Complex.reCLM ∘ f) := by
|
||
|
||
constructor
|
||
· -- Continuous differentiability
|
||
apply ContDiff.comp
|
||
exact ContinuousLinearMap.contDiff Complex.reCLM
|
||
exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff h)
|
||
· rw [laplace_compContLin]
|
||
simp
|
||
intro z
|
||
rw [(holomorphic_is_harmonic h).right z]
|
||
simp
|
||
exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff h)
|
||
|
||
|
||
theorem im_of_holomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f) :
|
||
Harmonic (Complex.imCLM ∘ f) := by
|
||
|
||
constructor
|
||
· -- Continuous differentiability
|
||
apply ContDiff.comp
|
||
exact ContinuousLinearMap.contDiff Complex.imCLM
|
||
exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff h)
|
||
· rw [laplace_compContLin]
|
||
simp
|
||
intro z
|
||
rw [(holomorphic_is_harmonic h).right z]
|
||
simp
|
||
exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff h)
|
||
|
||
|
||
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
|
||
|
||
-- f is real C²
|
||
have f_is_real_C2 : ContDiff ℝ 2 f :=
|
||
ContDiff.restrict_scalars ℝ (Differentiable.contDiff h₁)
|
||
|
||
-- The norm square is z * z.conj
|
||
have normSq_conj : ∀ (z : ℂ), (starRingEnd ℂ) z * z = ↑‖z‖ ^ 2 := Complex.conj_mul'
|
||
|
||
-- The norm square is real C²
|
||
have normSq_is_real_C2 : ContDiff ℝ 2 Complex.normSq := by
|
||
unfold Complex.normSq
|
||
simp
|
||
conv =>
|
||
arg 3
|
||
intro x
|
||
rw [← Complex.reCLM_apply, ← Complex.imCLM_apply]
|
||
apply ContDiff.add
|
||
apply ContDiff.mul
|
||
apply ContinuousLinearMap.contDiff Complex.reCLM
|
||
apply ContinuousLinearMap.contDiff Complex.reCLM
|
||
apply ContDiff.mul
|
||
apply ContinuousLinearMap.contDiff Complex.imCLM
|
||
apply ContinuousLinearMap.contDiff Complex.imCLM
|
||
|
||
constructor
|
||
· -- logabs f is real C²
|
||
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]
|
||
|
||
have : (2 : ℝ)⁻¹ • (Real.log ∘ Complex.normSq ∘ f) = (fun z ↦ (2 : ℝ)⁻¹ • ((Real.log ∘ ⇑Complex.normSq ∘ f) z)) := by
|
||
simp
|
||
rw [this]
|
||
|
||
apply contDiff_iff_contDiffAt.2
|
||
intro z
|
||
|
||
apply ContDiffAt.const_smul
|
||
apply ContDiffAt.comp
|
||
apply Real.contDiffAt_log.2
|
||
simp
|
||
exact h₂ z
|
||
apply ContDiffAt.comp
|
||
exact ContDiff.contDiffAt normSq_is_real_C2
|
||
exact ContDiff.contDiffAt f_is_real_C2
|
||
|
||
· -- Laplace vanishes
|
||
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]
|
||
rw [laplace_smul]
|
||
simp
|
||
|
||
have : ∀ (z : ℂ), Complex.laplace (Real.log ∘ ⇑Complex.normSq ∘ f) z = 0 ↔ Complex.laplace (Complex.ofRealCLM ∘ Real.log ∘ ⇑Complex.normSq ∘ f) z = 0 := by
|
||
intro z
|
||
rw [laplace_compContLin]
|
||
simp
|
||
sorry
|
||
conv =>
|
||
intro z
|
||
rw [this z]
|
||
|
||
have : Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ f = Complex.log ∘ Complex.ofRealCLM ∘ Complex.normSq ∘ f := by
|
||
unfold Function.comp
|
||
funext z
|
||
apply Complex.ofReal_log
|
||
exact Complex.normSq_nonneg (f z)
|
||
rw [this]
|
||
|
||
have : Complex.ofRealCLM ∘ ⇑Complex.normSq ∘ f = ((starRingEnd ℂ) ∘ f) * f := by
|
||
funext z
|
||
simp
|
||
exact Complex.normSq_eq_conj_mul_self
|
||
rw [this]
|
||
|
||
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]
|
||
rw [laplace_add]
|
||
|
||
have : Differentiable ℂ (Complex.log ∘ f) := by
|
||
intro z
|
||
apply DifferentiableAt.comp
|
||
exact Complex.differentiableAt_log (h₃ z)
|
||
exact h₁ z
|
||
|
||
have : Complex.laplace (Complex.log ∘ f) = 0 := by
|
||
let A := holomorphic_is_harmonic this
|
||
funext z
|
||
exact A.2 z
|
||
rw [this]
|
||
simp
|
||
|
||
have : Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f = ⇑(starRingEnd ℂ) ∘ Complex.log ∘ f := by
|
||
funext z
|
||
unfold Function.comp
|
||
rw [Complex.log_conj]
|
||
exact Complex.slitPlane_arg_ne_pi (h₃ z)
|
||
rw [this]
|
||
|
||
have : ⇑(starRingEnd ℂ) ∘ Complex.log ∘ f = Complex.conjCLE ∘ Complex.log ∘ f := by
|
||
rfl
|
||
rw [this]
|
||
have : ContDiff ℝ 2 (Complex.log ∘ f) := by sorry
|
||
have : Complex.laplace (⇑Complex.imCLM ∘ f) = ⇑Complex.imCLM ∘ Complex.laplace (f) := by
|
||
apply laplace_compContLin
|
||
|
||
sorry
|
||
rw [laplace_compContLin this]
|
||
|
||
sorry
|
||
|
||
sorry
|
||
sorry
|