254 lines
7.2 KiB
Plaintext
254 lines
7.2 KiB
Plaintext
import Nevanlinna.complexHarmonic
|
||
import Nevanlinna.holomorphicAt
|
||
import Nevanlinna.holomorphic_primitive
|
||
import Nevanlinna.mathlibAddOn
|
||
|
||
|
||
theorem CauchyRiemann₆
|
||
{E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]
|
||
{F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F]
|
||
{f : E → F}
|
||
{z : E} :
|
||
(DifferentiableAt ℂ f z) ↔ (DifferentiableAt ℝ f z) ∧ ∀ e, partialDeriv ℝ (Complex.I • e) f z = Complex.I • partialDeriv ℝ e f z := by
|
||
constructor
|
||
|
||
· -- Direction "→"
|
||
intro h
|
||
constructor
|
||
· exact DifferentiableAt.restrictScalars ℝ h
|
||
· unfold partialDeriv
|
||
conv =>
|
||
intro e
|
||
left
|
||
rw [DifferentiableAt.fderiv_restrictScalars ℝ h]
|
||
simp
|
||
rw [← mul_one Complex.I]
|
||
rw [← smul_eq_mul]
|
||
conv =>
|
||
intro e
|
||
right
|
||
right
|
||
rw [DifferentiableAt.fderiv_restrictScalars ℝ h]
|
||
simp
|
||
|
||
· -- Direction "←"
|
||
intro ⟨h₁, h₂⟩
|
||
apply (differentiableAt_iff_restrictScalars ℝ h₁).2
|
||
|
||
use {
|
||
toFun := fderiv ℝ f z
|
||
map_add' := fun x y => ContinuousLinearMap.map_add (fderiv ℝ f z) x y
|
||
map_smul' := by
|
||
simp
|
||
intro m x
|
||
have : m = m.re + m.im • Complex.I := by simp
|
||
rw [this, add_smul, add_smul, ContinuousLinearMap.map_add]
|
||
congr
|
||
simp
|
||
rw [smul_assoc, smul_assoc, ContinuousLinearMap.map_smul (fderiv ℝ f z) m.2]
|
||
congr
|
||
exact h₂ x
|
||
}
|
||
rfl
|
||
|
||
|
||
theorem CauchyRiemann₇
|
||
{F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F]
|
||
{f : ℂ → F}
|
||
{z : ℂ} :
|
||
(DifferentiableAt ℂ f z) ↔ (DifferentiableAt ℝ f z) ∧ partialDeriv ℝ Complex.I f z = Complex.I • partialDeriv ℝ 1 f z := by
|
||
constructor
|
||
· intro hf
|
||
constructor
|
||
· exact (CauchyRiemann₆.1 hf).1
|
||
· let A := (CauchyRiemann₆.1 hf).2 1
|
||
simp at A
|
||
exact A
|
||
· intro ⟨h₁, h₂⟩
|
||
apply CauchyRiemann₆.2
|
||
constructor
|
||
· exact h₁
|
||
· intro e
|
||
have : Complex.I • e = e • Complex.I := by
|
||
rw [smul_eq_mul, smul_eq_mul]
|
||
exact CommMonoid.mul_comm Complex.I e
|
||
rw [this]
|
||
have : e = e.re + e.im • Complex.I := by simp
|
||
rw [this, add_smul, partialDeriv_add₁, partialDeriv_add₁]
|
||
simp
|
||
rw [← smul_eq_mul]
|
||
have : partialDeriv ℝ ((e.re : ℝ) • Complex.I) f = partialDeriv ℝ ((e.re : ℂ) • Complex.I) f := by rfl
|
||
rw [← this, partialDeriv_smul₁ ℝ]
|
||
have : (e.re : ℂ) = (e.re : ℝ) • (1 : ℂ) := by simp
|
||
rw [this, partialDeriv_smul₁ ℝ]
|
||
have : partialDeriv ℝ ((e.im : ℂ) * Complex.I) f = partialDeriv ℝ ((e.im : ℝ) • Complex.I) f := by rfl
|
||
rw [this, partialDeriv_smul₁ ℝ]
|
||
simp
|
||
rw [h₂]
|
||
rw [smul_comm]
|
||
congr
|
||
rw [mul_assoc]
|
||
simp
|
||
nth_rw 2 [smul_comm]
|
||
rw [← smul_assoc]
|
||
simp
|
||
have : - (e.im : ℂ) = (-e.im : ℝ) • (1 : ℂ) := by simp
|
||
rw [this, partialDeriv_smul₁ ℝ]
|
||
simp
|
||
|
||
|
||
|
||
|
||
/-
|
||
|
||
A harmonic, real-valued function on ℂ is the real part of a suitable holomorphic
|
||
function.
|
||
|
||
-/
|
||
|
||
theorem harmonic_is_realOfHolomorphic
|
||
{f : ℂ → ℝ}
|
||
(hf : ∀ z, HarmonicAt f z) :
|
||
∃ F : ℂ → ℂ, (∀ z, HolomorphicAt F z) ∧ (Complex.reCLM ∘ F = f) := by
|
||
|
||
let f_1 : ℂ → ℂ := Complex.ofRealCLM ∘ (partialDeriv ℝ 1 f)
|
||
let f_I : ℂ → ℂ := Complex.ofRealCLM ∘ (partialDeriv ℝ Complex.I f)
|
||
|
||
let g : ℂ → ℂ := f_1 - Complex.I • f_I
|
||
|
||
have reg₂f : ContDiff ℝ 2 f := by
|
||
apply contDiff_iff_contDiffAt.mpr
|
||
intro z
|
||
exact (hf z).1
|
||
|
||
have reg₁f_1 : ContDiff ℝ 1 f_1 := by
|
||
apply contDiff_iff_contDiffAt.mpr
|
||
intro z
|
||
dsimp [f_1]
|
||
apply ContDiffAt.continuousLinearMap_comp
|
||
exact partialDeriv_contDiffAt ℝ (hf z).1 1
|
||
|
||
have reg₁f_I : ContDiff ℝ 1 f_I := by
|
||
apply contDiff_iff_contDiffAt.mpr
|
||
intro z
|
||
dsimp [f_I]
|
||
apply ContDiffAt.continuousLinearMap_comp
|
||
exact partialDeriv_contDiffAt ℝ (hf z).1 Complex.I
|
||
|
||
have reg₁g : ContDiff ℝ 1 g := by
|
||
dsimp [g]
|
||
apply ContDiff.sub
|
||
exact reg₁f_1
|
||
apply ContDiff.const_smul'
|
||
exact reg₁f_I
|
||
|
||
have reg₁ : Differentiable ℂ g := by
|
||
intro z
|
||
apply CauchyRiemann₇.2
|
||
constructor
|
||
· apply Differentiable.differentiableAt
|
||
apply ContDiff.differentiable
|
||
exact reg₁g
|
||
rfl
|
||
· dsimp [g]
|
||
rw [partialDeriv_sub₂, partialDeriv_sub₂]
|
||
simp
|
||
dsimp [f_1, f_I]
|
||
rw [partialDeriv_smul'₂, partialDeriv_smul'₂]
|
||
rw [partialDeriv_compContLin, partialDeriv_compContLin, partialDeriv_compContLin, partialDeriv_compContLin]
|
||
rw [mul_sub]
|
||
simp
|
||
rw [← mul_assoc]
|
||
simp
|
||
rw [add_comm, sub_eq_add_neg]
|
||
congr 1
|
||
· rw [partialDeriv_comm reg₂f Complex.I 1]
|
||
· let A := Filter.EventuallyEq.eq_of_nhds (hf z).2
|
||
simp at A
|
||
unfold Complex.laplace at A
|
||
conv =>
|
||
right
|
||
right
|
||
rw [← sub_zero (partialDeriv ℝ 1 (partialDeriv ℝ 1 f) z)]
|
||
rw [← A]
|
||
simp
|
||
|
||
--Differentiable ℝ (partialDeriv ℝ _ f)
|
||
repeat
|
||
apply ContDiff.differentiable
|
||
apply contDiff_iff_contDiffAt.mpr
|
||
exact fun w ↦ partialDeriv_contDiffAt ℝ (hf w).1 _
|
||
apply le_rfl
|
||
-- Differentiable ℝ f_1
|
||
exact reg₁f_1.differentiable le_rfl
|
||
-- Differentiable ℝ (Complex.I • f_I)
|
||
apply Differentiable.const_smul'
|
||
exact reg₁f_I.differentiable le_rfl
|
||
-- Differentiable ℝ f_1
|
||
exact reg₁f_1.differentiable le_rfl
|
||
-- Differentiable ℝ (Complex.I • f_I)
|
||
apply Differentiable.const_smul'
|
||
exact reg₁f_I.differentiable le_rfl
|
||
|
||
let F := fun z ↦ (primitive 0 g) z + f 0
|
||
|
||
have regF : Differentiable ℂ F := by
|
||
apply Differentiable.add
|
||
apply primitive_differentiable reg₁
|
||
simp
|
||
|
||
have pF'' : ∀ x, (fderiv ℝ F x) = ContinuousLinearMap.lsmul ℝ ℂ (g x) := by
|
||
intro x
|
||
rw [DifferentiableAt.fderiv_restrictScalars ℝ (regF x)]
|
||
dsimp [F]
|
||
rw [fderiv_add_const]
|
||
rw [primitive_fderiv']
|
||
exact rfl
|
||
exact reg₁
|
||
|
||
use F
|
||
|
||
constructor
|
||
· -- ∀ (z : ℂ), HolomorphicAt F z
|
||
intro z
|
||
apply HolomorphicAt_iff.2
|
||
use Set.univ
|
||
constructor
|
||
· exact isOpen_const
|
||
· constructor
|
||
· simp
|
||
· intro w _
|
||
exact regF w
|
||
· -- (F z).re = f z
|
||
have A := reg₂f.differentiable one_le_two
|
||
have B : Differentiable ℝ (Complex.reCLM ∘ F) := by
|
||
apply Differentiable.comp
|
||
exact ContinuousLinearMap.differentiable Complex.reCLM
|
||
exact Differentiable.restrictScalars ℝ regF
|
||
have C : (F 0).re = f 0 := by
|
||
dsimp [F]
|
||
rw [primitive_zeroAtBasepoint]
|
||
simp
|
||
|
||
apply eq_of_fderiv_eq B A _ 0 C
|
||
|
||
intro x
|
||
rw [fderiv.comp]
|
||
simp
|
||
apply ContinuousLinearMap.ext
|
||
intro w
|
||
simp
|
||
rw [pF'']
|
||
dsimp [g, f_1, f_I, partialDeriv]
|
||
simp
|
||
have : w = w.re • 1 + w.im • Complex.I := by simp
|
||
nth_rw 3 [this]
|
||
rw [(fderiv ℝ f x).map_add]
|
||
rw [(fderiv ℝ f x).map_smul, (fderiv ℝ f x).map_smul]
|
||
rw [smul_eq_mul, smul_eq_mul]
|
||
ring
|
||
-- DifferentiableAt ℝ (⇑Complex.reCLM) (F x)
|
||
fun_prop
|
||
-- DifferentiableAt ℝ F x
|
||
exact regF.restrictScalars ℝ x
|