Update holomorphic_primitive2.lean

This commit is contained in:
Stefan Kebekus 2024-08-07 12:28:36 +02:00
parent f0b84fcbff
commit 656d50e367
1 changed files with 15 additions and 14 deletions

View File

@ -20,8 +20,9 @@ theorem primitive_zeroAtBasepoint
theorem primitive_fderivAtBasepointZero
{E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E]
(f : → E)
(hf : ContinuousAt f 0) :
{f : → E}
{R : }
(hf : ContinuousOn f (Metric.ball 0 R)) :
HasDerivAt (primitive 0 f) (f 0) 0 := by
unfold primitive
simp
@ -277,19 +278,20 @@ theorem primitive_translation
theorem primitive_hasDerivAtBasepoint
{E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E]
{f : → E}
{R : }
(z₀ : )
(hf : ContinuousAt f z₀) :
(hf : ContinuousOn f (Metric.ball z₀ R)) :
HasDerivAt (primitive z₀ f) (f z₀) z₀ := by
let g := f ∘ fun z ↦ z + z₀
have : ContinuousAt g 0 := by
apply ContinuousAt.comp
simpa
apply ContinuousAt.add
exact fun ⦃U⦄ a => a
exact continuousAt_const
let A := primitive_fderivAtBasepointZero g this
simp at A
have hg : ContinuousOn g (Metric.ball 0 R) := by
apply ContinuousOn.comp
fun_prop
fun_prop
intro x hx
simp
simp at hx
assumption
let B := primitive_translation g z₀ z₀
simp at B
@ -299,8 +301,7 @@ theorem primitive_hasDerivAtBasepoint
simp
rw [this] at B
rw [B]
have : f z₀ = (1 : ) • (f z₀) := by
exact (MulAction.one_smul (f z₀)).symm
have : f z₀ = (1 : ) • (f z₀) := (MulAction.one_smul (f z₀)).symm
conv =>
arg 2
rw [this]
@ -309,7 +310,7 @@ theorem primitive_hasDerivAtBasepoint
simp
have : g 0 = f z₀ := by simp [g]
rw [← this]
exact A
exact primitive_fderivAtBasepointZero hg
apply HasDerivAt.sub_const
have : (fun (x : ) ↦ x) = id := by
funext x