nevanlinna/Nevanlinna/holomorphic.primitive.lean

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

/-
variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]
variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F]
variable {G : Type*} [NormedAddCommGroup G] [NormedSpace ℂ G] [CompleteSpace G]

noncomputable def Complex.primitive
  (f : ℂ → F) : ℂ → F :=
  fun z ↦ ∫ t : ℝ in (0)..1, z • f (t * z)
-/



theorem MeasureTheory.integral2_divergence_prod_of_hasFDerivWithinAt_off_countable₁
  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
  (f : ℝ × ℝ → E)
  (g : ℝ × ℝ → E)
  (f' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E)
  (g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E)
  (a₁ : ℝ)
  (a₂ : ℝ)
  (b₁ : ℝ)
  (b₂ : ℝ)
  (s : Set (ℝ × ℝ))
  (hs : s.Countable)
  (Hcf : ContinuousOn f (Set.uIcc a₁ b₁ ×ˢ Set.uIcc a₂ b₂))
  (Hcg : ContinuousOn g (Set.uIcc a₁ b₁ ×ˢ Set.uIcc a₂ b₂))
  (Hdf : ∀ x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂) \ s, HasFDerivAt f (f' x) x)
  (Hdg : ∀ x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂) \ s, HasFDerivAt g (g' x) x)
  (Hi : MeasureTheory.IntegrableOn (fun (x : ℝ × ℝ) => (f' x) (1, 0) + (g' x) (0, 1)) (Set.uIcc a₁ b₁ ×ˢ Set.uIcc a₂ b₂) MeasureTheory.volume) :
  ∫ (x : ℝ) in a₁..b₁, ∫ (y : ℝ) in a₂..b₂, (f' (x, y)) (1, 0) + (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
  exact
    integral2_divergence_prod_of_hasFDerivWithinAt_off_countable f g f' g' a₁ a₂ b₁ b₂ s hs Hcf Hcg
      Hdf Hdg Hi


theorem MeasureTheory.integral2_divergence_prod_of_hasFDerivWithinAt_off_countable₂
  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
  (f : ℝ × ℝ → E)
  (g : ℝ × ℝ → E)
  (f' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E)
  (g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E)
  (a₁ : ℝ)
  (a₂ : ℝ)
  (b₁ : ℝ)
  (b₂ : ℝ)
  (Hcf : ContinuousOn f (Set.uIcc a₁ b₁ ×ˢ Set.uIcc a₂ b₂))
  (Hcg : ContinuousOn g (Set.uIcc a₁ b₁ ×ˢ Set.uIcc a₂ b₂))
  (Hdf : ∀ x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂), HasFDerivAt f (f' x) x)
  (Hdg : ∀ x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂), HasFDerivAt g (g' x) x)
  (Hi : MeasureTheory.IntegrableOn (fun (x : ℝ × ℝ) => (f' x) (1, 0) + (g' x) (0, 1)) (Set.uIcc a₁ b₁ ×ˢ Set.uIcc a₂ b₂) MeasureTheory.volume) :
  ∫ (x : ℝ) in a₁..b₁, ∫ (y : ℝ) in a₂..b₂, (f' (x, y)) (1, 0) + (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 f' g' a₁ a₂ b₁ b₂ ∅
  exact Set.countable_empty
  assumption
  assumption
  rwa [Set.diff_empty]
  rwa [Set.diff_empty]
  assumption


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 : ℂ  → ℂ)
  (hF : Differentiable ℂ F)
  (a₁ : ℝ)
  (a₂ : ℝ)
  (b₁ : ℝ)
  (b₂ : ℝ) :
  (∫ (x : ℝ) in a₁..b₁, Complex.I • F { re := x, im := b₂ }) +
  (∫ (y : ℝ) in a₂..b₂, F { re := b₁, im := y })
  =
  (∫ (x : ℝ) in a₁..b₁, Complex.I • F { re := x, im := a₂ }) +
  (∫ (y : ℝ) in a₂..b₂, F { re := a₁, im := y }) := by

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

  let g := Complex.I • F
  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 Complex.I
    exact h₁f


  let A := integral_divergence₄ F g h₁f h₁g a₁ a₂ b₁ b₂

  have {z : ℂ} : fderiv ℝ F z 1 = partialDeriv ℝ 1 F z := by rfl
  conv at A in (fderiv ℝ F _) 1 => rw [this]
  have {z : ℂ} : fderiv ℝ g z Complex.I = partialDeriv ℝ Complex.I g z := by rfl
  conv at A in (fderiv ℝ g _) Complex.I => rw [this]

  have : Differentiable ℂ g := by sorry
  conv at A =>
    left
    arg 1
    intro x
    arg 1
    intro y
    rw [CauchyRiemann₄ this]
    rw [partialDeriv_smul'₂]
    rw [← smul_assoc]
    simp
  simp at A



  sorry