Update holomorphic.primitive.lean

Nevanlinna/holomorphic.primitive.lean

@@ -4,67 +4,6 @@ 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]
@@ -149,49 +88,46 @@ theorem integral_divergence₄
 
 theorem integral_divergence₅
   {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
-  (F : ℂ  → ℂ)
+  (F : ℂ  → E)
   (hF : Differentiable ℂ F)
-  (a₁ : ℝ)
+  (lowerLeft upperRight : ℂ) :
-  (a₂ : ℝ)
+  (∫ (x : ℝ) in lowerLeft.re..upperRight.re, F ⟨x, lowerLeft.im⟩)  + Complex.I • ∫ (x : ℝ) in lowerLeft.im..upperRight.im, F ⟨upperRight.re, x⟩ =
-  (b₁ : ℝ)
+  (∫ (x : ℝ) in lowerLeft.re..upperRight.re, F ⟨x, upperRight.im⟩) + Complex.I • ∫ (x : ℝ) in lowerLeft.im..upperRight.im, F ⟨lowerLeft.re,  x⟩ := by
-  (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
-  let h₁g : ContDiff ℝ 1 (Complex.I • F) := by
+    have : -Complex.I • F = fun x ↦ -Complex.I • F x := by rfl
-    have : Complex.I • F = fun x ↦ Complex.I • F x := by rfl
     rw [this]
     apply ContDiff.comp
-    exact contDiff_const_smul Complex.I
+    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
 
-  let A := integral_divergence₄ F g h₁f h₁g a₁ a₂ b₁ b₂
+  have {z : ℂ} : fderiv ℝ F z Complex.I = partialDeriv ℝ _ F z := by rfl
-
+  conv at A in (fderiv ℝ F _) _ => rw [this]
-  have {z : ℂ} : fderiv ℝ F z 1 = partialDeriv ℝ 1 F z := by rfl
+  have {z : ℂ} : fderiv ℝ (-Complex.I • F) z 1 = partialDeriv ℝ _ (-Complex.I • F) z := by rfl
-  conv at A in (fderiv ℝ F _) 1 => rw [this]
+  conv at A in (fderiv ℝ (-Complex.I • F) _) _ => 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 [CauchyRiemann₄ hF]
     rw [partialDeriv_smul'₂]
-    rw [← smul_assoc]
     simp
   simp at A
 
-
+  have {t₁ t₂ t₃ t₄ : E} : 0 = (t₁ - t₂) + t₃ + t₄ → t₁ + t₃ = t₂ - t₄ := by
-
+    intro hyp
-  sorry
+    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