working

Nevanlinna/holomorphic_primitive2.lean

@@ -21,7 +21,7 @@ theorem primitive_zeroAtBasepoint
 theorem primitive_fderivAtBasepointZero
   {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
   (f : ℂ  → E)
-  (hf : Continuous f) :
+  (hf : ContinuousAt f 0) :
   HasDerivAt (primitive 0 f) (f 0) 0 := by
   unfold primitive
   simp
@@ -253,8 +253,8 @@ theorem primitive_translation
 theorem primitive_hasDerivAtBasepoint
   {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
   {f : ℂ  → E}
-  (hf : Continuous f)
-  (z₀ : ℂ) :
+  (z₀ : ℂ)
+  (hf : ContinuousAt f z₀) :
   HasDerivAt (primitive z₀ f) (f z₀) z₀ := by
 
   let g := f ∘ fun z ↦ z + z₀
@@ -539,81 +539,96 @@ theorem primitive_additivity
 theorem primitive_additivity'
   {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
   (f : ℂ  → E)
-  (hf : Differentiable ℂ f)
-  (z₀ z₁ : ℂ) :
-  primitive z₀ f = fun z ↦ (primitive z₁ f) z + (primitive z₀ f z₁) := by
-
-  nth_rw 1 [← sub_zero (primitive z₀ f)]
-  rw [← primitive_additivity f hf z₀ z₁]
-
-  funext z
-  simp
-  abel
+  (z₀ : ℂ)
+  (R : ℝ)
+  (hf : DifferentiableOn ℂ f (Metric.ball z₀ R))
+  (z₁ : ℂ)
+  (hz₁ : z₁ ∈ (Metric.ball z₀ R))
+  :
+  primitive z₀ f =ᶠ[nhds z₁] fun z ↦ (primitive z₁ f z) + (primitive z₀ f z₁) := by
+  sorry
 
 
 theorem primitive_hasDerivAt
   {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
-  {f : ℂ  → E}
-  (hf : Differentiable ℂ f)
-  (z₀ z : ℂ) :
+  (f : ℂ  → E)
+  (z₀ z : ℂ)
+  (R : ℝ)
+  (hf : DifferentiableOn ℂ f (Metric.ball z₀ R))
+  (hz : z ∈ Metric.ball z₀ R) :
   HasDerivAt (primitive z₀ f) (f z) z := by
-  rw [primitive_additivity' f hf z₀ z]
+
+  let A := primitive_additivity' f z₀ R hf z hz
+  rw [Filter.EventuallyEq.hasDerivAt_iff A]
   rw [← add_zero (f z)]
   apply HasDerivAt.add
   apply primitive_hasDerivAtBasepoint
-  exact hf.continuous
+
+  apply hf.continuousOn.continuousAt
+  apply (IsOpen.mem_nhds_iff Metric.isOpen_ball).2 hz
   apply hasDerivAt_const
 
 
 theorem primitive_differentiable
   {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
   {f : ℂ  → E}
-  (hf : Differentiable ℂ f)
-  (z₀ : ℂ) :
-  Differentiable ℂ (primitive z₀ f) := by
-  intro z
-  exact (primitive_hasDerivAt hf z₀ z).differentiableAt
+  (z₀ : ℂ)
+  (R : ℝ)
+  (hf : DifferentiableOn ℂ f (Metric.ball z₀ R))
+  :
+  DifferentiableOn ℂ (primitive z₀ f) (Metric.ball z₀ R) := by
+  intro z hz
+  apply DifferentiableAt.differentiableWithinAt
+  exact (primitive_hasDerivAt f z₀ z R hf hz).differentiableAt
 
 
 theorem primitive_hasFderivAt
   {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
   {f : ℂ  → E}
-  (hf : Differentiable ℂ f)
-  (z₀ : ℂ) :
-  ∀ z, HasFDerivAt (primitive z₀ f) ((ContinuousLinearMap.lsmul ℂ ℂ).flip (f z)) z := by
-  intro z
+  (z₀ : ℂ)
+  (R : ℝ)
+  (hf : DifferentiableOn ℂ f (Metric.ball z₀ R))
+  :
+  ∀ z ∈ Metric.ball z₀ R, HasFDerivAt (primitive z₀ f) ((ContinuousLinearMap.lsmul ℂ ℂ).flip (f z)) z := by
+  intro z hz
   rw [hasFDerivAt_iff_hasDerivAt]
   simp
-  exact primitive_hasDerivAt hf z₀ z
+  apply primitive_hasDerivAt f z₀ z R hf hz
 
 
 theorem primitive_hasFderivAt'
   {f : ℂ  → ℂ}
-  (hf : Differentiable ℂ f)
-  (z₀ : ℂ) :
-  ∀ z, HasFDerivAt (primitive z₀ f) (ContinuousLinearMap.lsmul ℂ ℂ (f z)) z := by
-  intro z
+  (z₀ : ℂ)
+  (R : ℝ)
+  (hf : DifferentiableOn ℂ f (Metric.ball z₀ R))
+  :
+  ∀ z ∈ Metric.ball z₀ R, HasFDerivAt (primitive z₀ f) (ContinuousLinearMap.lsmul ℂ ℂ (f z)) z := by
+  intro z hz
   rw [hasFDerivAt_iff_hasDerivAt]
   simp
-  exact primitive_hasDerivAt hf z₀ z
+  exact primitive_hasDerivAt f z₀ z R hf hz
 
 
 theorem primitive_fderiv
   {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
   {f : ℂ  → E}
-  (hf : Differentiable ℂ f)
-  (z₀ : ℂ) :
-  ∀ z, (fderiv ℂ (primitive z₀ f) z) = (ContinuousLinearMap.lsmul ℂ ℂ).flip (f z) := by
-  intro z
+  (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
+  intro z hz
   apply HasFDerivAt.fderiv
-  exact primitive_hasFderivAt hf z₀ z
+  exact primitive_hasFderivAt z₀ R hf z hz
 
 
 theorem primitive_fderiv'
   {f : ℂ  → ℂ}
-  (hf : Differentiable ℂ f)
-  (z₀ : ℂ) :
-  ∀ z, (fderiv ℂ (primitive z₀ f) z) = ContinuousLinearMap.lsmul ℂ ℂ (f z) := by
-  intro z
+  (z₀ : ℂ)
+  (R : ℝ)
+  (hf : DifferentiableOn ℂ f (Metric.ball z₀ R))
+  :
+  ∀ z ∈ Metric.ball z₀ R, (fderiv ℂ (primitive z₀ f) z) = ContinuousLinearMap.lsmul ℂ ℂ (f z) := by
+  intro z hz
   apply HasFDerivAt.fderiv
-  exact primitive_hasFderivAt' hf z₀ z
+  exact primitive_hasFderivAt' z₀ R hf z hz