nevanlinna/Nevanlinna/holomorphic_primitive2.lean

import Mathlib.Analysis.Complex.TaylorSeries
import Mathlib.Data.ENNReal.Basic

noncomputable def primitive
  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] :
  ℂ  → (ℂ → E) → (ℂ → E) := by
  intro z₀
  intro f
  exact fun z ↦ (∫ (x : ℝ) in z₀.re..z.re, f ⟨x, z₀.im⟩) + Complex.I • ∫ (x : ℝ) in z₀.im..z.im, f ⟨z.re, x⟩


theorem primitive_zeroAtBasepoint
  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
  (f : ℂ  → E)
  (z₀ : ℂ) :
  (primitive z₀ f) z₀ = 0 := by
  unfold primitive
  simp


theorem primitive_fderivAtBasepointZero
  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
  (f : ℂ  → E)
  (hf : ContinuousAt f 0) :
  HasDerivAt (primitive 0 f) (f 0) 0 := by
  unfold primitive
  simp
  apply hasDerivAt_iff_isLittleO.2
  simp
  rw [Asymptotics.isLittleO_iff]
  intro c hc

  have {z : ℂ} {e : E} : z • e = (∫ (_ : ℝ) in (0)..(z.re), e) + Complex.I • ∫ (_ : ℝ) in (0)..(z.im), e:= by
    simp
    rw [smul_comm]
    rw [← smul_assoc]
    simp
    have : z.re • e = (z.re : ℂ) • e := by exact rfl
    rw [this, ← add_smul]
    simp
  conv =>
    left
    intro x
    left
    arg 1
    arg 2
    rw [this]
  have {A B C D :E} : (A + B) - (C + D) = (A - C) + (B - D) := by
    abel
  have t₀ {r : ℝ} : IntervalIntegrable (fun x => f { re := x, im := 0 }) MeasureTheory.volume 0 r := by
    apply Continuous.intervalIntegrable
    apply Continuous.comp
    exact hf
    have : (fun x => ({ re := x, im := 0 } : ℂ)) = Complex.ofRealLI := by rfl
    rw [this]
    continuity
  have t₁ {r : ℝ} : IntervalIntegrable (fun _ => f 0) MeasureTheory.volume 0 r := by
    apply Continuous.intervalIntegrable
    apply Continuous.comp
    exact hf
    fun_prop
  have t₂ {a b : ℝ} : IntervalIntegrable (fun x_1 => f { re := a, im := x_1 }) MeasureTheory.volume 0 b := by
    apply Continuous.intervalIntegrable
    apply Continuous.comp hf
    have : (Complex.mk a) = (fun x => Complex.I • Complex.ofRealCLM x + { re := a, im := 0 }) := by
      funext x
      apply Complex.ext
      rw [Complex.add_re]
      simp
      simp
    rw [this]
    apply Continuous.add
    continuity
    fun_prop

  have t₃ {a : ℝ} : IntervalIntegrable (fun _ => f 0) MeasureTheory.volume 0 a := by
    apply Continuous.intervalIntegrable
    apply Continuous.comp
    exact hf
    fun_prop
  conv =>
    left
    intro x
    left
    arg 1
    rw [this]
    rw [← smul_sub]
    rw [← intervalIntegral.integral_sub t₀ t₁]
    rw [← intervalIntegral.integral_sub t₂ t₃]
  rw [Filter.eventually_iff_exists_mem]

  let s := f⁻¹' Metric.ball (f 0) (c / (4 : ℝ))
  have h₁s : IsOpen s := IsOpen.preimage hf Metric.isOpen_ball
  have h₂s : 0 ∈ s := by
    apply Set.mem_preimage.mpr
    apply Metric.mem_ball_self
    linarith

  obtain ⟨ε, h₁ε, h₂ε⟩ := Metric.isOpen_iff.1 h₁s 0 h₂s

  have h₃ε : ∀ y ∈ Metric.ball 0 ε, ‖(f y) - (f 0)‖ < (c / (4 : ℝ)) := by
    intro y hy
    apply mem_ball_iff_norm.mp (h₂ε hy)

  use Metric.ball 0 (ε / (4 : ℝ))
  constructor
  · apply Metric.ball_mem_nhds 0
    linarith
  · intro y hy
    have h₁y : |y.re| < ε / 4 := by
      calc |y.re|
      _ ≤ Complex.abs y := by apply Complex.abs_re_le_abs
      _ < ε / 4 := by
        let A := mem_ball_iff_norm.1 hy
        simp at A
        linarith
    have h₂y : |y.im| < ε / 4 := by
      calc |y.im|
      _ ≤ Complex.abs y := by apply Complex.abs_im_le_abs
      _ < ε / 4 := by
        let A := mem_ball_iff_norm.1 hy
        simp at A
        linarith

    have intervalComputation {x' y' : ℝ} (h : x' ∈ Ι 0 y') : |x'| ≤ |y'| := by
      let A := h.1
      let B := h.2
      rcases le_total 0 y' with hy | hy
      · simp [hy] at A
        simp [hy] at B
        rw [abs_of_nonneg hy]
        rw [abs_of_nonneg (le_of_lt A)]
        exact B
      · simp [hy] at A
        simp [hy] at B
        rw [abs_of_nonpos hy]
        rw [abs_of_nonpos]
        linarith [h.1]
        exact B

    have t₁ : ‖(∫ (x : ℝ) in (0)..(y.re), f { re := x, im := 0 } - f 0)‖ ≤ (c / (4 : ℝ)) * |y.re - 0| := by
      apply intervalIntegral.norm_integral_le_of_norm_le_const
      intro x hx

      have h₁x : |x| < ε / 4 := by
        calc |x|
          _ ≤ |y.re| := intervalComputation hx
          _ < ε / 4 := h₁y
      apply le_of_lt
      apply h₃ε { re := x, im := 0 }
      rw [mem_ball_iff_norm]
      simp
      have : { re := x, im := 0 } = (x : ℂ) := by rfl
      rw [this]
      rw [Complex.abs_ofReal]
      linarith

    have t₂ : ‖∫ (x : ℝ) in (0)..(y.im), f { re := y.re, im := x } - f 0‖ ≤ (c / (4 : ℝ)) * |y.im - 0| := by
      apply intervalIntegral.norm_integral_le_of_norm_le_const
      intro x hx

      have h₁x : |x| < ε / 4 := by
        calc |x|
          _ ≤ |y.im| := intervalComputation hx
          _ < ε / 4 := h₂y

      apply le_of_lt
      apply h₃ε { re := y.re, im := x }
      simp

      calc Complex.abs { re := y.re, im := x }
        _ ≤ |y.re| + |x| := by
          apply Complex.abs_le_abs_re_add_abs_im { re := y.re, im := x }
        _ < ε := by
          linarith

    calc ‖(∫ (x : ℝ) in (0)..(y.re), f { re := x, im := 0 } - f 0) + Complex.I • ∫ (x : ℝ) in (0)..(y.im), f { re := y.re, im := x } - f 0‖
      _ ≤ ‖(∫ (x : ℝ) in (0)..(y.re), f { re := x, im := 0 } - f 0)‖ + ‖Complex.I • ∫ (x : ℝ) in (0)..(y.im), f { re := y.re, im := x } - f 0‖ := by
        apply norm_add_le
      _ ≤ ‖(∫ (x : ℝ) in (0)..(y.re), f { re := x, im := 0 } - f 0)‖ + ‖∫ (x : ℝ) in (0)..(y.im), f { re := y.re, im := x } - f 0‖ := by
        simp
        rw [norm_smul]
        simp
      _ ≤ (c / (4 : ℝ)) * |y.re - 0| + (c / (4 : ℝ)) * |y.im - 0| := by
        apply add_le_add
        exact t₁
        exact t₂
      _ ≤ (c / (4 : ℝ)) * (|y.re| + |y.im|) := by
        simp
        rw [mul_add]
      _ ≤ (c / (4 : ℝ)) * (4 * ‖y‖) := by
        have : |y.re| + |y.im| ≤ 4 * ‖y‖ := by
          calc |y.re| + |y.im|
            _ ≤ ‖y‖ + ‖y‖ := by
              apply add_le_add
              apply Complex.abs_re_le_abs
              apply Complex.abs_im_le_abs
            _ ≤ 4 * ‖y‖ := by
              rw [← two_mul]
              apply mul_le_mul
              linarith
              rfl
              exact norm_nonneg y
              linarith

        apply mul_le_mul
        rfl
        exact this
        apply add_nonneg
        apply abs_nonneg
        apply abs_nonneg
        linarith
      _ ≤ c * ‖y‖ := by
        linarith


theorem primitive_translation
  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
  (f : ℂ  → E)
  (z₀ t : ℂ) :
  primitive z₀ (f ∘ fun z ↦ (z - t)) = ((primitive (z₀ - t) f) ∘ fun z ↦ (z - t)) := by
  funext z
  unfold primitive
  simp

  let g : ℝ → E := fun x ↦ f ( {re := x, im := z₀.im - t.im} )
  have {x : ℝ} : f ({ re := x, im := z₀.im } - t) = g (1*x - t.re) := by
    congr 1
    apply Complex.ext <;> simp
  conv =>
    left
    left
    arg 1
    intro x
    rw [this]
  rw [intervalIntegral.integral_comp_mul_sub g one_ne_zero (t.re)]
  simp

  congr 1
  let g : ℝ → E := fun x ↦ f ( {re := z.re - t.re, im := x} )
  have {x : ℝ} : f ({ re := z.re, im := x} - t) = g (1*x - t.im) := by
    congr 1
    apply Complex.ext <;> simp
  conv =>
    left
    arg 1
    intro x
    rw [this]
  rw [intervalIntegral.integral_comp_mul_sub g one_ne_zero (t.im)]
  simp


theorem primitive_hasDerivAtBasepoint
  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
  {f : ℂ  → E}
  (z₀ : ℂ)
  (hf : ContinuousAt f z₀) :
  HasDerivAt (primitive z₀ f) (f z₀) z₀ := by

  let g := f ∘ fun z ↦ z + z₀
  have : Continuous g := by continuity
  let A := primitive_fderivAtBasepointZero g this
  simp at A

  let B := primitive_translation g z₀ z₀
  simp at B
  have : (g ∘ fun z ↦ (z - z₀)) = f := by
    funext z
    dsimp [g]
    simp
  rw [this] at B
  rw [B]
  have : f z₀ = (1 : ℂ) • (f z₀) := by
    exact (MulAction.one_smul (f z₀)).symm
  conv =>
    arg 2
    rw [this]

  apply HasDerivAt.scomp
  simp
  have : g 0 = f z₀ := by simp [g]
  rw [← this]
  exact A
  apply HasDerivAt.sub_const
  have : (fun (x : ℂ) ↦ x) = id := by
    funext x
    simp
  rw [this]
  exact hasDerivAt_id z₀


theorem primitive_additivity
  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
  {f : ℂ  → E}
  {z₀ : ℂ}
  {rx ry : ℝ}
  (hf : DifferentiableOn ℂ f (Metric.ball z₀.re rx ×ℂ Metric.ball z₀.im ry))
  (hry : 0 < ry)
  {z₁ : ℂ}
  (hz₁ : z₁ ∈ (Metric.ball z₀.re rx ×ℂ Metric.ball z₀.im ry))
  :
  ∃ εx > 0, ∃ εy > 0, ∀ z ∈ (Metric.ball z₁.re εx ×ℂ Metric.ball z₁.im εy), (primitive z₀ f z) - (primitive z₁ f z) - (primitive z₀ f z₁) = 0 := by

  let εx := rx - dist z₀.re z₁.re
  have hεx : εx > 0 := by
    sorry
  let εy := ry - dist z₀.im z₁.im
  have hεy : εy > 0 := by
    sorry

  use εx
  use hεx
  use εy
  use hεy

  intro z hz

  unfold primitive

  have : (∫ (x : ℝ) in z₀.re..z.re, f { re := x, im := z₀.im }) = (∫ (x : ℝ) in z₀.re..z₁.re, f { re := x, im := z₀.im }) + (∫ (x : ℝ) in z₁.re..z.re, f { re := x, im := z₀.im }) := by

    rw [intervalIntegral.integral_add_adjacent_intervals]

    -- IntervalIntegrable (fun x => f { re := x, im := z₀.im }) MeasureTheory.volume z₀.re z₁.re
    apply ContinuousOn.intervalIntegrable
    apply ContinuousOn.comp
    exact hf.continuousOn
    have {b : ℝ} : ((fun x => { re := x, im := b }) : ℝ → ℂ) = (fun x => Complex.ofRealCLM x + { re := 0, im := b }) := by
      funext x
      apply Complex.ext
      rw [Complex.add_re]
      simp
      rw [Complex.add_im]
      simp
    apply Continuous.continuousOn
    rw [this]
    continuity
    -- Remains: Set.MapsTo (fun x => { re := x, im := z₀.im }) (Set.uIcc z₀.re z₁.re) (Metric.ball z₀.re rx ×ℂ Metric.ball z₀.im ry)
    intro w hw
    simp
    apply Complex.mem_reProdIm.mpr
    constructor
    · simp
      calc dist w z₀.re
      _ ≤ dist z₁.re z₀.re := by apply Real.dist_right_le_of_mem_uIcc; rwa [Set.uIcc_comm] at hw
      _ < rx := by apply Metric.mem_ball.mp (Complex.mem_reProdIm.1 hz₁).1
    · simpa

    -- IntervalIntegrable (fun x => f { re := x, im := z₀.im }) MeasureTheory.volume z₁.re z.re
    apply ContinuousOn.intervalIntegrable
    apply ContinuousOn.comp
    exact hf.continuousOn
    have {b : ℝ} : ((fun x => { re := x, im := b }) : ℝ → ℂ) = (fun x => Complex.ofRealCLM x + { re := 0, im := b }) := by
      funext x
      apply Complex.ext
      rw [Complex.add_re]
      simp
      rw [Complex.add_im]
      simp
    apply Continuous.continuousOn
    rw [this]
    continuity
    -- Remains: Set.MapsTo (fun x => { re := x, im := z₀.im }) (Set.uIcc z₁.re z.re) (Metric.ball z₀.re rx ×ℂ Metric.ball z₀.im ry)
    intro w hw
    simp
    constructor
    · simp
      calc dist w z₀.re
      _ ≤ dist w z₁.re + dist z₁.re z₀.re := by exact dist_triangle w z₁.re z₀.re
      _ ≤ dist z.re z₁.re + dist z₁.re z₀.re := by
        apply (add_le_add_iff_right (dist z₁.re z₀.re)).mpr
        rw [Set.uIcc_comm] at hw
        exact Real.dist_right_le_of_mem_uIcc hw
      _ < (rx - dist z₀.re z₁.re) + dist z₁.re z₀.re := by
        apply (add_lt_add_iff_right (dist z₁.re z₀.re)).mpr
        apply Metric.mem_ball.1 (Complex.mem_reProdIm.1 hz).1
      _ = rx := by
        rw [dist_comm]
        simp
    · simpa
  rw [this]

  have : (∫ (x : ℝ) in z₀.im..z.im, f { re := z.re, im := x }) = (∫ (x : ℝ) in z₀.im..z₁.im, f { re := z.re, im := x }) + (∫ (x : ℝ) in z₁.im..z.im, f { re := z.re, im := x }) := by
    rw [intervalIntegral.integral_add_adjacent_intervals]

    -- IntervalIntegrable (fun x => f { re := z.re, im := x }) MeasureTheory.volume z₀.im z₁.im
    apply ContinuousOn.intervalIntegrable
    apply ContinuousOn.comp
    exact hf.continuousOn
    apply Continuous.continuousOn
    have {b : ℝ}:  (Complex.mk b) = (fun x => Complex.I • Complex.ofRealCLM x + { re := b, im := 0 }) := by
      funext x
      apply Complex.ext
      rw [Complex.add_re]
      simp
      simp
    rw [this]
    apply Continuous.add
    fun_prop
    fun_prop
    -- Set.MapsTo (Complex.mk z.re) (Set.uIcc z₀.im z₁.im) (Metric.ball z₀.re rx ×ℂ Metric.ball z₀.im ry)
    intro w hw
    constructor
    · simp
      calc dist z.re z₀.re
      _ ≤ dist z.re z₁.re + dist z₁.re z₀.re := by exact dist_triangle z.re z₁.re z₀.re
      _ < (rx - dist z₀.re z₁.re) + dist z₁.re z₀.re := by
        apply (add_lt_add_iff_right (dist z₁.re z₀.re)).mpr
        apply Metric.mem_ball.1 (Complex.mem_reProdIm.1 hz).1
      _ = rx := by
        rw [dist_comm]
        simp
    · simp
      calc dist w z₀.im
      _ ≤ dist z₁.im z₀.im := by rw [Set.uIcc_comm] at hw; exact Real.dist_right_le_of_mem_uIcc hw
      _ < ry := by
        rw [← Metric.mem_ball]
        exact hz₁.2

    -- IntervalIntegrable (fun x => f { re := z.re, im := x }) MeasureTheory.volume z₁.im z.im
    apply ContinuousOn.intervalIntegrable
    apply ContinuousOn.comp
    exact hf.continuousOn
    apply Continuous.continuousOn
    have {b : ℝ}:  (Complex.mk b) = (fun x => Complex.I • Complex.ofRealCLM x + { re := b, im := 0 }) := by
      funext x
      apply Complex.ext
      rw [Complex.add_re]
      simp
      simp
    rw [this]
    apply Continuous.add
    fun_prop
    fun_prop
    -- Set.MapsTo (Complex.mk z.re) (Set.uIcc z₁.im z.im) (Metric.ball z₀.re rx ×ℂ Metric.ball z₀.im ry)
    intro w hw
    constructor
    · simp
      calc dist z.re z₀.re
      _ ≤ dist z.re z₁.re + dist z₁.re z₀.re := by exact dist_triangle z.re z₁.re z₀.re
      _ < (rx - dist z₀.re z₁.re) + dist z₁.re z₀.re := by
        apply (add_lt_add_iff_right (dist z₁.re z₀.re)).mpr
        apply Metric.mem_ball.1 (Complex.mem_reProdIm.1 hz).1
      _ = rx := by
        rw [dist_comm]
        simp
    · simp
      calc dist w z₀.im
      _ ≤ dist w z₁.im + dist z₁.im z₀.im := by exact dist_triangle w z₁.im z₀.im
      _ ≤ dist z.im z₁.im + dist z₁.im z₀.im := by
        apply (add_le_add_iff_right (dist z₁.im z₀.im)).mpr
        rw [Set.uIcc_comm] at hw
        exact Real.dist_right_le_of_mem_uIcc hw
      _ < (ry - dist z₀.im z₁.im) + dist z₁.im z₀.im := by
        apply (add_lt_add_iff_right (dist z₁.im z₀.im)).mpr
        apply Metric.mem_ball.1 (Complex.mem_reProdIm.1 hz).2
      _ = ry := by
        rw [dist_comm]
        simp
  rw [this]

  simp

  have {a b c d e f g h : E} : (a + b) + (c + d) - (e + f) - (g + h) = b + (a - g) - e - f + d  - h + (c) := by
    abel
  rw [this]


  have H' : DifferentiableOn ℂ f (Set.uIcc z₁.re z.re ×ℂ Set.uIcc z₀.im z₁.im) := by
    apply DifferentiableOn.mono hf
    intro x hx
    constructor
    · simp
      calc dist x.re z₀.re
      _ ≤ dist x.re z₁.re + dist z₁.re z₀.re := by exact dist_triangle x.re z₁.re z₀.re
      _ ≤ dist z.re z₁.re + dist z₁.re z₀.re := by
        apply (add_le_add_iff_right (dist z₁.re z₀.re)).mpr
        rw [Set.uIcc_comm] at hx
        apply Real.dist_right_le_of_mem_uIcc (Complex.mem_reProdIm.1 hx).1
      _ < (rx - dist z₀.re z₁.re) + dist z₁.re z₀.re := by
        apply (add_lt_add_iff_right (dist z₁.re z₀.re)).mpr
        apply Metric.mem_ball.1 (Complex.mem_reProdIm.1 hz).1
      _ = rx := by
        rw [dist_comm]
        simp
    · simp
      calc dist x.im z₀.im
      _ ≤ dist z₀.im z₁.im := by rw [dist_comm]; exact Real.dist_left_le_of_mem_uIcc (Complex.mem_reProdIm.1 hx).2
      _ < ry := by
        rw [dist_comm]
        exact Metric.mem_ball.1 (Complex.mem_reProdIm.1 hz₁).2

  let A := Complex.integral_boundary_rect_eq_zero_of_differentiableOn f ⟨z₁.re, z₀.im⟩ ⟨z.re, z₁.im⟩ H'
  have {x : ℝ} {w : ℂ} : ↑x + w.im * Complex.I = { re := x, im := w.im } := by
    apply Complex.ext
    · simp
    · simp
  simp_rw [this] at A
  have {x : ℝ} {w : ℂ} : w.re + x * Complex.I = { re := w.re, im := x } := by
    apply Complex.ext
    · simp
    · simp
  simp_rw [this] at A
  rw [← A]
  abel


theorem primitive_additivity'
  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
  {f : ℂ  → E}
  {z₀ z₁ : ℂ}
  {R : ℝ}
  (hf : DifferentiableOn ℂ f (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

  let ε := R - dist z₀ z₁

  have hε : 0 < ε := by
    dsimp [ε]
    simp
    exact Metric.mem_ball'.mp hz₁

  let rx := dist z₀.re z₁.re + ε/(2 : ℝ)
  let ry := dist z₀.im z₁.im + ε/(2 : ℝ)

  have h'ry : 0 < ry := by
    dsimp [ry]
    apply add_pos_of_nonneg_of_pos
    exact dist_nonneg
    simpa

  have h'f : DifferentiableOn ℂ f (Metric.ball z₀.re rx ×ℂ Metric.ball z₀.im ry) := by
    apply hf.mono
    intro x hx
    simp
    let A := hx.1
    simp at A
    let B := hx.2
    simp at B
    calc dist x z₀
    _ = √((x.re - z₀.re) ^ 2 + (x.im - z₀.im) ^ 2) := by exact Complex.dist_eq_re_im x z₀
    _ =
    sorry

  have h'z₁ : z₁ ∈ (Metric.ball z₀.re rx ×ℂ Metric.ball z₀.im ry) := by
    dsimp [rx, ry]
    constructor
    · rw [dist_comm]; simp; exact hε
    · rw [dist_comm]; simp; exact hε

  obtain ⟨εx, hεx, εy, hεy, hε⟩ := primitive_additivity h'f h'ry h'z₁

  apply Filter.eventuallyEq_iff_exists_mem.2
  use (Metric.ball z₁.re εx ×ℂ Metric.ball z₁.im εy)
  constructor
  · apply IsOpen.mem_nhds
    apply IsOpen.reProdIm
    exact Metric.isOpen_ball
    exact Metric.isOpen_ball
    constructor
    · simpa
    · simpa
  · intro x hx
    simp
    rw [← sub_zero (primitive z₀ f x), ← hε x hx]
    abel


theorem primitive_hasDerivAt
  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
  {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

  let A := primitive_additivity' hf hz
  rw [Filter.EventuallyEq.hasDerivAt_iff A]
  rw [← add_zero (f z)]
  apply HasDerivAt.add
  apply primitive_hasDerivAtBasepoint

  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}
  (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 hf hz).differentiableAt


theorem primitive_hasFderivAt
  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
  {f : ℂ  → E}
  (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
  apply primitive_hasDerivAt hf hz


theorem primitive_hasFderivAt'
  {f : ℂ  → ℂ}
  {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 hz


theorem primitive_fderiv
  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
  {f : ℂ  → E}
  {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 z₀ R hf z hz


theorem primitive_fderiv'
  {f : ℂ  → ℂ}
  {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 hz