nevanlinna/Nevanlinna/holomorphic.primitive.lean

import Mathlib.Analysis.Complex.TaylorSeries
import Mathlib.MeasureTheory.Integral.DivergenceTheorem
import Mathlib.MeasureTheory.Integral.IntervalIntegral
import Mathlib.MeasureTheory.Function.LocallyIntegrable
import Nevanlinna.cauchyRiemann
import Nevanlinna.partialDeriv


theorem MeasureTheory.integral2_divergence₃
  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
  (f g : ℝ × ℝ → E)
  (h₁f : ContDiff ℝ 1 f)
  (h₁g : ContDiff ℝ 1 g)
  (a₁ : ℝ)
  (a₂ : ℝ)
  (b₁ : ℝ)
  (b₂ : ℝ) :
  ∫ (x : ℝ) in a₁..b₁, ∫ (y : ℝ) in a₂..b₂, ((fderiv ℝ f) (x, y)) (1, 0) + ((fderiv ℝ g) (x, y)) (0, 1) = (((∫ (x : ℝ) in a₁..b₁, g (x, b₂)) - ∫ (x : ℝ) in a₁..b₁, g (x, a₂)) + ∫ (y : ℝ) in a₂..b₂, f (b₁, y)) - ∫ (y : ℝ) in a₂..b₂, f (a₁, y) := by

  apply integral2_divergence_prod_of_hasFDerivWithinAt_off_countable f g (fderiv ℝ f) (fderiv ℝ g) a₁ a₂ b₁ b₂ ∅
  exact Set.countable_empty
  -- ContinuousOn f (Set.uIcc a₁ b₁ ×ˢ Set.uIcc a₂ b₂)
  exact h₁f.continuous.continuousOn
  --
  exact h₁g.continuous.continuousOn
  --
  rw [Set.diff_empty]
  intro x _
  exact DifferentiableAt.hasFDerivAt ((h₁f.differentiable le_rfl) x)
  --
  rw [Set.diff_empty]
  intro y _
  exact DifferentiableAt.hasFDerivAt ((h₁g.differentiable le_rfl) y)
  --
  apply ContinuousOn.integrableOn_compact
  apply IsCompact.prod
  exact isCompact_uIcc
  exact isCompact_uIcc
  apply ContinuousOn.add
  apply Continuous.continuousOn
  exact Continuous.clm_apply (ContDiff.continuous_fderiv h₁f le_rfl) continuous_const
  apply Continuous.continuousOn
  exact Continuous.clm_apply (ContDiff.continuous_fderiv h₁g le_rfl) continuous_const


theorem integral_divergence₄
  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
  (f g : ℂ  → E)
  (h₁f : ContDiff ℝ 1 f)
  (h₁g : ContDiff ℝ 1 g)
  (a₁ : ℝ)
  (a₂ : ℝ)
  (b₁ : ℝ)
  (b₂ : ℝ) :
  ∫ (x : ℝ) in a₁..b₁, ∫ (y : ℝ) in a₂..b₂, ((fderiv ℝ f) ⟨x, y⟩ ) 1 + ((fderiv ℝ g) ⟨x, y⟩) Complex.I = (((∫ (x : ℝ) in a₁..b₁, g ⟨x, b₂⟩) - ∫ (x : ℝ) in a₁..b₁, g ⟨x, a₂⟩) + ∫ (y : ℝ) in a₂..b₂, f ⟨b₁, y⟩) - ∫ (y : ℝ) in a₂..b₂, f ⟨a₁, y⟩ := by

  let fr : ℝ × ℝ → E := f ∘ Complex.equivRealProdCLM.symm
  let gr : ℝ × ℝ → E := g ∘ Complex.equivRealProdCLM.symm

  have sfr {x y : ℝ} : f { re := x, im := y } = fr (x, y) := by exact rfl
  have sgr {x y : ℝ} : g { re := x, im := y } = gr (x, y) := by exact rfl
  repeat (conv in f { re := _, im := _ } => rw [sfr])
  repeat (conv in g { re := _, im := _ } => rw [sgr])

  have sfr' {x y : ℝ} {z : ℂ} : (fderiv ℝ f { re := x, im := y }) z = fderiv ℝ fr (x, y) (Complex.equivRealProdCLM z) := by
    rw [fderiv.comp]
    rw [Complex.equivRealProdCLM.symm.fderiv]
    tauto
    apply Differentiable.differentiableAt
    exact h₁f.differentiable le_rfl
    exact Complex.equivRealProdCLM.symm.differentiableAt
  conv in ⇑(fderiv ℝ f { re := _, im := _ }) _ => rw [sfr']

  have sgr' {x y : ℝ} {z : ℂ} : (fderiv ℝ g { re := x, im := y }) z = fderiv ℝ gr (x, y) (Complex.equivRealProdCLM z) := by
    rw [fderiv.comp]
    rw [Complex.equivRealProdCLM.symm.fderiv]
    tauto
    apply Differentiable.differentiableAt
    exact h₁g.differentiable le_rfl
    exact Complex.equivRealProdCLM.symm.differentiableAt
  conv in ⇑(fderiv ℝ g { re := _, im := _ }) _ => rw [sgr']

  apply MeasureTheory.integral2_divergence₃ fr gr _ _ a₁ a₂ b₁ b₂
  -- ContDiff ℝ 1 fr
  exact (ContinuousLinearEquiv.contDiff_comp_iff (ContinuousLinearEquiv.symm Complex.equivRealProdCLM)).mpr h₁f
  -- ContDiff ℝ 1 gr
  exact (ContinuousLinearEquiv.contDiff_comp_iff (ContinuousLinearEquiv.symm Complex.equivRealProdCLM)).mpr h₁g


theorem integral_divergence₅
  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
  (F : ℂ  → E)
  (hF : Differentiable ℂ F)
  (lowerLeft upperRight : ℂ) :
  (∫ (x : ℝ) in lowerLeft.re..upperRight.re, F ⟨x, lowerLeft.im⟩)  + Complex.I • ∫ (x : ℝ) in lowerLeft.im..upperRight.im, F ⟨upperRight.re, x⟩ =
  (∫ (x : ℝ) in lowerLeft.re..upperRight.re, F ⟨x, upperRight.im⟩) + Complex.I • ∫ (x : ℝ) in lowerLeft.im..upperRight.im, F ⟨lowerLeft.re,  x⟩ := by

  let h₁f : ContDiff ℝ 1 F :=  (hF.contDiff : ContDiff ℂ 1 F).restrict_scalars ℝ

  let h₁g : ContDiff ℝ 1 (-Complex.I • F) := by
    have : -Complex.I • F = fun x ↦ -Complex.I • F x := by rfl
    rw [this]
    apply ContDiff.comp
    exact contDiff_const_smul _
    exact h₁f

  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
  conv at A in (fderiv ℝ F _) _ => rw [this]
  have {z : ℂ} : fderiv ℝ (-Complex.I • F) z 1 = partialDeriv ℝ _ (-Complex.I • F) z := by rfl
  conv at A in (fderiv ℝ (-Complex.I • F) _) _ => rw [this]
  conv at A =>
    left
    arg 1
    intro x
    arg 1
    intro y
    rw [CauchyRiemann₄ hF]
    rw [partialDeriv_smul'₂]
    simp
  simp at A

  have {t₁ t₂ t₃ t₄ : E} : 0 = (t₁ - t₂) + t₃ + t₄ → t₁ + t₃ = t₂ - t₄ := by
    intro hyp
    calc
      t₁ + t₃ = t₁ + t₃ - 0 := by rw [sub_zero (t₁ + t₃)]
      _ = t₁ + t₃ - (t₁ - t₂ + t₃ + t₄) := by rw [hyp]
      _ = t₂ - t₄ := by abel
  let B := this A
  repeat
    rw [intervalIntegral.integral_symm lowerLeft.im upperRight.im] at B
  simp at B
  exact B


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_lem1
  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] [IsScalarTower ℝ ℂ E]
  (v : E) :
  HasDerivAt (primitive 0 (fun _ ↦ v)) v 0 := by
  unfold primitive
  simp

  have : (fun (z : ℂ) => z.re • v + Complex.I • z.im • v) = (fun (y : ℂ) => ((fun w ↦ w)  y) • v) := by
    funext z
    rw [smul_comm]
    rw [← smul_assoc]
    simp
    have : z.re • v = (z.re : ℂ) • v := by exact rfl
    rw [this, ← add_smul]
    simp
  rw [this]

  have hc : HasDerivAt (fun (w : ℂ) ↦ w) 1 0 := by
    apply hasDerivAt_id'
  nth_rewrite 2 [← (one_smul ℂ v)]
  exact HasDerivAt.smul_const hc v



theorem primitive_fderivAtBasepointZero
  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
  (f : ℂ  → E)
  (hf : Continuous f) :
  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
    exact hf
    have : ((fun x => { re := a, im := x }) : ℝ → ℂ) = (fun x => { re := a, im := 0 } + { re := 0, im := x }) := by
      funext x
      apply Complex.ext
      rw [Complex.add_re]
      simp
      rw [Complex.add_im]
      simp
    rw [this]
    apply Continuous.add
    fun_prop
    have : (fun x => { re := 0, im := x } : ℝ → ℂ) = Complex.I • Complex.ofRealCLM := by
      funext x
      simp
      have : (x : ℂ) = {re := x, im := 0} := by rfl
      rw [this]
      rw [Complex.I_mul]
      simp
    continuity

  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_additivity
  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
  (f : ℂ  → E)
  (hf : Differentiable ℂ f)
  (z₀ z₁ : ℂ) :
  (primitive z₁ f) = (primitive z₀ f) - (fun z ↦ primitive z₀ f z₁) := by


  sorry