kebekus
/
nevanlinna
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Working

This commit is contained in:
Stefan Kebekus 2024-05-07 16:50:57 +02:00
parent b5cf426b7f
commit e45017277a
2 changed files with 22 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
Nevanlinna/complexHarmonic.lean
View File

@ -39,9 +39,9 @@ theorem holomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f) :
· -- Laplace of f is zero · -- Laplace of f is zero
unfold Complex.laplace unfold Complex.laplace
rw [CauchyRiemann₄ h] rw [CauchyRiemann₄ h]
rw [partialDeriv_smul fI_is_real_differentiable] rw [partialDeriv_smul₂ fI_is_real_differentiable]
rw [partialDeriv_comm f_is_real_C2 Complex.I 1] rw [partialDeriv_comm f_is_real_C2 Complex.I 1]
rw [CauchyRiemann₄ h] rw [CauchyRiemann₄ h]
rw [partialDeriv_smul fI_is_real_differentiable] rw [partialDeriv_smul₂ fI_is_real_differentiable]
rw [← smul_assoc] rw [← smul_assoc]
simp simp

23
Nevanlinna/partialDeriv.lean
View File

@ -14,7 +14,24 @@ noncomputable def Real.partialDeriv : ℂ → (ℂ → ℂ) → (ℂ → ℂ) :=
fun v ↦ (fun f ↦ (fun w ↦ fderiv ℝ f w v)) fun v ↦ (fun f ↦ (fun w ↦ fderiv ℝ f w v))
theorem partialDeriv_smul {f : ℂ → ℂ} {a v : ℂ} (h : Differentiable ℝ f) : Real.partialDeriv v (a • f) = a • Real.partialDeriv v f := by
theorem partialDeriv_smul₁ {f : ℂ → ℂ} {a : ℝ} {v : ℂ} : Real.partialDeriv (a • v) f = a • Real.partialDeriv v f := by
unfold Real.partialDeriv
conv =>
left
intro w
rw [map_smul]
theorem partialDeriv_add₁ {f : ℂ → ℂ} {v₁ v₂ : ℂ} : Real.partialDeriv (v₁ + v₂) f = (Real.partialDeriv v₁ f) + (Real.partialDeriv v₂ f) := by
unfold Real.partialDeriv
conv =>
left
intro w
rw [map_add]
theorem partialDeriv_smul₂ {f : ℂ → ℂ} {a v : ℂ} (h : Differentiable ℝ f) : Real.partialDeriv v (a • f) = a • Real.partialDeriv v f := by
unfold Real.partialDeriv unfold Real.partialDeriv
have : a • f = fun y ↦ a • f y := by rfl have : a • f = fun y ↦ a • f y := by rfl
@ -26,7 +43,7 @@ theorem partialDeriv_smul {f : ℂ → ℂ} {a v : ℂ} (h : Differentiable ℝ
rw [fderiv_const_smul (h w)] rw [fderiv_const_smul (h w)]
theorem partialDeriv_add {f₁ f₂ : ℂ → ℂ} {v : ℂ} (h₁ : Differentiable ℝ f₁) (h₂ : Differentiable ℝ f₂) : Real.partialDeriv v (f₁ + f₂) = (Real.partialDeriv v f₁) + (Real.partialDeriv v f₂) := by theorem partialDeriv_add₂ {f₁ f₂ : ℂ → ℂ} {v : ℂ} (h₁ : Differentiable ℝ f₁) (h₂ : Differentiable ℝ f₂) : Real.partialDeriv v (f₁ + f₂) = (Real.partialDeriv v f₁) + (Real.partialDeriv v f₂) := by
unfold Real.partialDeriv unfold Real.partialDeriv
have : f₁ + f₂ = fun y ↦ f₁ y + f₂ y := by rfl have : f₁ + f₂ = fun y ↦ f₁ y + f₂ y := by rfl
@ -38,7 +55,7 @@ theorem partialDeriv_add {f₁ f₂ : ℂ → ℂ} {v : ℂ} (h₁ : Differentia
rw [fderiv_add (h₁ w) (h₂ w)] rw [fderiv_add (h₁ w) (h₂ w)]
theorem partialDeriv_compLin {f : ℂ → ℂ} {l : ℂ →L[ℝ] ℂ} {v : ℂ} (h : Differentiable ℝ f) : Real.partialDeriv v (l ∘ f) = l ∘ Real.partialDeriv v f := by theorem partialDeriv_compContLin {f : ℂ → ℂ} {l : ℂ →L[ℝ] ℂ} {v : ℂ} (h : Differentiable ℝ f) : Real.partialDeriv v (l ∘ f) = l ∘ Real.partialDeriv v f := by
unfold Real.partialDeriv unfold Real.partialDeriv
conv => conv =>