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

Working…

This commit is contained in:
Stefan Kebekus 2024-06-19 08:20:36 +02:00
parent 50591a54c2
commit 7a281ff514
2 changed files with 4 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
Nevanlinna/cauchyRiemann.lean
View File

@ -44,8 +44,10 @@ theorem CauchyRiemann₃ : (DifferentiableAt ℂ f z)
simp simp
theorem CauchyRiemann₄ {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] {f : ℂ → F} : (Differentiable ℂ f) theorem CauchyRiemann₄
→ partialDeriv ℝ Complex.I f = Complex.I • partialDeriv ℝ 1 f := by {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F]
{f : ℂ → F} :
(Differentiable ℂ f) → partialDeriv ℝ Complex.I f = Complex.I • partialDeriv ℝ 1 f := by
intro h intro h
unfold partialDeriv unfold partialDeriv

3
Nevanlinna/holomorphic.primitive.lean
View File

@ -4,9 +4,7 @@ import Mathlib.MeasureTheory.Integral.DivergenceTheorem
import Mathlib.MeasureTheory.Integral.IntervalIntegral import Mathlib.MeasureTheory.Integral.IntervalIntegral
import Mathlib.MeasureTheory.Function.LocallyIntegrable import Mathlib.MeasureTheory.Function.LocallyIntegrable
import Nevanlinna.cauchyRiemann import Nevanlinna.cauchyRiemann
import Nevanlinna.partialDeriv
theorem MeasureTheory.integral2_divergence₃ theorem MeasureTheory.integral2_divergence₃
@ -108,7 +106,6 @@ theorem integral_divergence₅
exact h₁f exact h₁f
let A := integral_divergence₄ (-Complex.I • F) F h₁g h₁f lowerLeft.re upperRight.im upperRight.re lowerLeft.im let A := integral_divergence₄ (-Complex.I • F) F h₁g h₁f lowerLeft.re upperRight.im upperRight.re lowerLeft.im
have {z : ℂ} : fderiv ℝ F z Complex.I = partialDeriv ℝ _ F z := by rfl have {z : ℂ} : fderiv ℝ F z Complex.I = partialDeriv ℝ _ F z := by rfl
conv at A in (fderiv ℝ F _) _ => rw [this] conv at A in (fderiv ℝ F _) _ => rw [this]
have {z : ℂ} : fderiv ℝ (-Complex.I • F) z 1 = partialDeriv ℝ _ (-Complex.I • F) z := by rfl have {z : ℂ} : fderiv ℝ (-Complex.I • F) z 1 = partialDeriv ℝ _ (-Complex.I • F) z := by rfl