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

working

This commit is contained in:
Stefan Kebekus 2024-08-05 13:47:20 +02:00
parent c041cff4ad
commit 854b7ef492
1 changed files with 18 additions and 19 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

37
Nevanlinna/holomorphic_primitive2.lean
View File

@ -538,12 +538,11 @@ theorem primitive_additivity
theorem primitive_additivity' theorem primitive_additivity'
{E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
(f : ℂ → E) {f : ℂ → E}
(z₀ : ℂ) {z₀ z₁ : ℂ}
(R : ℝ) {R : ℝ}
(hf : DifferentiableOn ℂ f (Metric.ball z₀ R)) (hf : DifferentiableOn ℂ f (Metric.ball z₀ R))
(z₁ : ℂ) (hz₁ : z₁ ∈ Metric.ball z₀ R)
(hz₁ : z₁ ∈ (Metric.ball z₀ R))
: :
primitive z₀ f =ᶠ[nhds z₁] fun z ↦ (primitive z₁ f z) + (primitive z₀ f z₁) := by primitive z₀ f =ᶠ[nhds z₁] fun z ↦ (primitive z₁ f z) + (primitive z₀ f z₁) := by
sorry sorry
@ -551,14 +550,14 @@ theorem primitive_additivity'
theorem primitive_hasDerivAt theorem primitive_hasDerivAt
{E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
(f : ℂ → E) {f : ℂ → E}
(z₀ z : ℂ) {z₀ z : ℂ}
(R : ℝ) {R : ℝ}
(hf : DifferentiableOn ℂ f (Metric.ball z₀ R)) (hf : DifferentiableOn ℂ f (Metric.ball z₀ R))
(hz : z ∈ Metric.ball z₀ R) : (hz : z ∈ Metric.ball z₀ R) :
HasDerivAt (primitive z₀ f) (f z) z := by HasDerivAt (primitive z₀ f) (f z) z := by
let A := primitive_additivity' f z₀ R hf z hz let A := primitive_additivity' hf hz
rw [Filter.EventuallyEq.hasDerivAt_iff A] rw [Filter.EventuallyEq.hasDerivAt_iff A]
rw [← add_zero (f z)] rw [← add_zero (f z)]
apply HasDerivAt.add apply HasDerivAt.add
@ -579,7 +578,7 @@ theorem primitive_differentiable
DifferentiableOn ℂ (primitive z₀ f) (Metric.ball z₀ R) := by DifferentiableOn ℂ (primitive z₀ f) (Metric.ball z₀ R) := by
intro z hz intro z hz
apply DifferentiableAt.differentiableWithinAt apply DifferentiableAt.differentiableWithinAt
exact (primitive_hasDerivAt f z₀ z R hf hz).differentiableAt exact (primitive_hasDerivAt hf hz).differentiableAt
theorem primitive_hasFderivAt theorem primitive_hasFderivAt
@ -593,27 +592,27 @@ theorem primitive_hasFderivAt
intro z hz intro z hz
rw [hasFDerivAt_iff_hasDerivAt] rw [hasFDerivAt_iff_hasDerivAt]
simp simp
apply primitive_hasDerivAt f z₀ z R hf hz apply primitive_hasDerivAt hf hz
theorem primitive_hasFderivAt' theorem primitive_hasFderivAt'
{f : ℂ → ℂ} {f : ℂ → ℂ}
(z₀ : ℂ) {z₀ : ℂ}
(R : ℝ) {R : ℝ}
(hf : DifferentiableOn ℂ f (Metric.ball z₀ R)) (hf : DifferentiableOn ℂ f (Metric.ball z₀ R))
: :
∀ z ∈ Metric.ball z₀ R, HasFDerivAt (primitive z₀ f) (ContinuousLinearMap.lsmul ℂ ℂ (f z)) z := by ∀ z ∈ Metric.ball z₀ R, HasFDerivAt (primitive z₀ f) (ContinuousLinearMap.lsmul ℂ ℂ (f z)) z := by
intro z hz intro z hz
rw [hasFDerivAt_iff_hasDerivAt] rw [hasFDerivAt_iff_hasDerivAt]
simp simp
exact primitive_hasDerivAt f z₀ z R hf hz exact primitive_hasDerivAt hf hz
theorem primitive_fderiv theorem primitive_fderiv
{E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
{f : ℂ → E} {f : ℂ → E}
(z₀ : ℂ) {z₀ : ℂ}
(R : ℝ) {R : ℝ}
(hf : DifferentiableOn ℂ f (Metric.ball z₀ R)) (hf : DifferentiableOn ℂ f (Metric.ball z₀ R))
: :
∀ z ∈ Metric.ball z₀ R, (fderiv ℂ (primitive z₀ f) z) = (ContinuousLinearMap.lsmul ℂ ℂ).flip (f z) := by ∀ z ∈ Metric.ball z₀ R, (fderiv ℂ (primitive z₀ f) z) = (ContinuousLinearMap.lsmul ℂ ℂ).flip (f z) := by
@ -624,11 +623,11 @@ theorem primitive_fderiv
theorem primitive_fderiv' theorem primitive_fderiv'
{f : ℂ → ℂ} {f : ℂ → ℂ}
(z₀ : ℂ) {z₀ : ℂ}
(R : ℝ) {R : ℝ}
(hf : DifferentiableOn ℂ f (Metric.ball z₀ R)) (hf : DifferentiableOn ℂ f (Metric.ball z₀ R))
: :
∀ z ∈ Metric.ball z₀ R, (fderiv ℂ (primitive z₀ f) z) = ContinuousLinearMap.lsmul ℂ ℂ (f z) := by ∀ z ∈ Metric.ball z₀ R, (fderiv ℂ (primitive z₀ f) z) = ContinuousLinearMap.lsmul ℂ ℂ (f z) := by
intro z hz intro z hz
apply HasFDerivAt.fderiv apply HasFDerivAt.fderiv
exact primitive_hasFderivAt' z₀ R hf z hz exact primitive_hasFderivAt' hf z hz