89 lines
2.8 KiB
Plaintext
89 lines
2.8 KiB
Plaintext
import Mathlib.Data.Fin.Tuple.Basic
|
||
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.Data.Complex.Module
|
||
import Mathlib.Data.Complex.Order
|
||
import Mathlib.Data.Complex.Exponential
|
||
import Mathlib.Analysis.RCLike.Basic
|
||
import Mathlib.Topology.Algebra.InfiniteSum.Module
|
||
import Mathlib.Topology.Instances.RealVectorSpace
|
||
import Nevanlinna.cauchyRiemann
|
||
import Nevanlinna.partialDeriv
|
||
|
||
|
||
noncomputable def Complex.laplace : (ℂ → ℂ) → (ℂ → ℂ) := by
|
||
intro f
|
||
let fx := partialDeriv ℝ 1 f
|
||
let fxx := partialDeriv ℝ 1 fx
|
||
let fy := partialDeriv ℝ Complex.I f
|
||
let fyy := partialDeriv ℝ Complex.I fy
|
||
exact fxx + fyy
|
||
|
||
|
||
def Harmonic (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
|