119 lines
2.9 KiB
Plaintext
119 lines
2.9 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 Nevanlinna.cauchyRiemann
|
||
|
||
noncomputable def Complex.laplace : (ℂ → ℂ) → (ℂ → ℂ) := by
|
||
intro f
|
||
|
||
let fx := fun w ↦ (fderiv ℝ f w) 1
|
||
let fxx := fun w ↦ (fderiv ℝ fx w) 1
|
||
let fy := fun w ↦ (fderiv ℝ f w) Complex.I
|
||
let fyy := fun w ↦ (fderiv ℝ fy w) Complex.I
|
||
exact fun z ↦ (fxx z) + (fyy z)
|
||
|
||
|
||
def Harmonic (f : ℂ → ℂ) : Prop :=
|
||
(ContDiff ℝ 2 f) ∧ (∀ z, Complex.laplace f z = 0)
|
||
|
||
#check second_derivative_symmetric
|
||
|
||
lemma zwoDiff (f : ℝ × ℝ → ℝ) (h : ContDiff ℝ 2 f) : ∀ z a b : ℂ, 0 = 1 := by
|
||
intro z a b
|
||
|
||
let fx := fun w ↦ (fderiv ℝ f w) 1
|
||
let fxx := fun w ↦ (fderiv ℝ fx w) 1
|
||
let f2 := (fderiv ℝ (fun w => fderiv ℝ f w) z) 1 1
|
||
|
||
have : iteratedFDeriv ℝ (1 + 1) f = 0 := by
|
||
rw [iteratedFDeriv_succ_eq_comp_left]
|
||
|
||
simp
|
||
sorry
|
||
|
||
have : f2 = fxx z := by
|
||
dsimp [f2, fxx, fx]
|
||
|
||
sorry
|
||
|
||
sorry
|
||
|
||
|
||
lemma derivSymm (f : ℂ → ℂ) (h : Differentiable ℝ f) :
|
||
∀ z a b : ℂ, (fderiv ℝ (fun w => fderiv ℝ f w) z) a b = (fderiv ℝ (fun w => fderiv ℝ f w) z) b a := by
|
||
intro z a b
|
||
|
||
let f' := fun w => (fderiv ℝ f w)
|
||
have h₀ : ∀ y, HasFDerivAt f (f' y) y := by
|
||
exact fun y => DifferentiableAt.hasFDerivAt (h y)
|
||
|
||
let f'' := (fderiv ℝ f' z)
|
||
have h₁ : HasFDerivAt f' f'' z := by
|
||
apply DifferentiableAt.hasFDerivAt
|
||
sorry
|
||
|
||
let A := second_derivative_symmetric h₀ h₁ a b
|
||
dsimp [f'', f'] at A
|
||
apply A
|
||
|
||
theorem re_comp_holomorphic_is_harmonic (f : ℂ → ℂ) :
|
||
Differentiable ℂ f → Harmonic f := by
|
||
|
||
intro h
|
||
|
||
constructor
|
||
· -- Complex.reCLM ∘ f is two times real continuously differentiable
|
||
exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff h)
|
||
|
||
· -- Laplace of f is zero
|
||
intro z
|
||
unfold Complex.laplace
|
||
|
||
simp
|
||
|
||
conv =>
|
||
left
|
||
right
|
||
arg 1
|
||
arg 2
|
||
intro z
|
||
rw [CauchyRiemann₁ (h z)]
|
||
|
||
have t₀ : ∀ z, DifferentiableAt ℝ (fun w => (fderiv ℝ f w) 1) z := by
|
||
intro z
|
||
|
||
sorry
|
||
|
||
have t₁ : ∀ x, (fderiv ℝ (fun w => Complex.I * (fderiv ℝ f w) 1) z) x
|
||
= Complex.I * ((fderiv ℝ (fun w => (fderiv ℝ f w) 1) z) x) := by
|
||
intro x
|
||
rw [fderiv_const_mul]
|
||
simp
|
||
exact t₀ z
|
||
rw [t₁]
|
||
|
||
have t₂₀ : Differentiable ℝ f := by sorry
|
||
have t₂ : (fderiv ℝ (fun w => (fderiv ℝ f w) 1) z) Complex.I
|
||
= (fderiv ℝ (fun w => (fderiv ℝ f w) Complex.I) z) 1 := by
|
||
let A := derivSymm f t₂₀ z 1 Complex.I
|
||
|
||
sorry
|
||
rw [t₂]
|
||
|
||
conv =>
|
||
left
|
||
right
|
||
arg 2
|
||
arg 1
|
||
arg 2
|
||
intro z
|
||
rw [CauchyRiemann₁ (h z)]
|
||
|
||
rw [t₁]
|
||
|
||
rw [← mul_assoc]
|
||
simp
|