Update holomorphic.primitive.lean

Nevanlinna/holomorphic.primitive.lean

@@ -38,6 +38,7 @@ theorem MeasureTheory.integral2_divergence_prod_of_hasFDerivWithinAt_off_countab
     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)
@@ -65,7 +66,7 @@ theorem MeasureTheory.integral2_divergence_prod_of_hasFDerivWithinAt_off_countab
   assumption
 
 
-theorem MeasureTheory.integral2_divergence_prod_of_hasFDerivWithinAt_off_countable₃
+theorem MeasureTheory.integral2_divergence₃
   {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
   (f g : ℝ × ℝ → E)
   (h₁f : ContDiff ℝ 1 f)
@@ -84,11 +85,11 @@ theorem MeasureTheory.integral2_divergence_prod_of_hasFDerivWithinAt_off_countab
   exact h₁g.continuous.continuousOn
   --
   rw [Set.diff_empty]
-  intro x h₁x
+  intro x _
   exact DifferentiableAt.hasFDerivAt ((h₁f.differentiable le_rfl) x)
   --
   rw [Set.diff_empty]
-  intro y h₁y
+  intro y _
   exact DifferentiableAt.hasFDerivAt ((h₁g.differentiable le_rfl) y)
   --
   apply ContinuousOn.integrableOn_compact
@@ -103,7 +104,7 @@ theorem MeasureTheory.integral2_divergence_prod_of_hasFDerivWithinAt_off_countab
 
 
 theorem integral_divergence₄
-  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
+  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
   (f g : ℂ  → E)
   (h₁f : ContDiff ℝ 1 f)
   (h₁g : ContDiff ℝ 1 g)
@@ -113,27 +114,76 @@ theorem integral_divergence₄
   (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
 
-  apply integral2_divergence_prod_of_hasFDerivWithinAt_off_countable f g (fderiv ℝ f) (fderiv ℝ g) a₁ a₂ b₁ b₂ ∅
+  let fr : ℝ × ℝ → E := f ∘ Complex.equivRealProdCLM.symm
-  exact Set.countable_empty
+  let gr : ℝ × ℝ → E := g ∘ Complex.equivRealProdCLM.symm
-  -- ContinuousOn f (Set.uIcc a₁ b₁ ×ˢ Set.uIcc a₂ b₂)
+
-  exact h₁f.continuous.continuousOn
+  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
-  exact h₁g.continuous.continuousOn
+  repeat (conv in f { re := _, im := _ } => rw [sfr])
-  --
+  repeat (conv in g { re := _, im := _ } => rw [sgr])
-  rw [Set.diff_empty]
+
-  intro x h₁x
+  have sfr' {x y : ℝ} {z : ℂ} : (fderiv ℝ f { re := x, im := y }) z = fderiv ℝ fr (x, y) (Complex.equivRealProdCLM z) := by
-  exact DifferentiableAt.hasFDerivAt ((h₁f.differentiable le_rfl) x)
+    rw [fderiv.comp]
-  --
+    rw [Complex.equivRealProdCLM.symm.fderiv]
-  rw [Set.diff_empty]
+    tauto
-  intro y h₁y
+    apply Differentiable.differentiableAt
-  exact DifferentiableAt.hasFDerivAt ((h₁g.differentiable le_rfl) y)
+    exact h₁f.differentiable le_rfl
-  --
+    exact Complex.equivRealProdCLM.symm.differentiableAt
-  apply ContinuousOn.integrableOn_compact
+  conv in ⇑(fderiv ℝ f { re := _, im := _ }) _ => rw [sfr']
-  apply IsCompact.prod
+
-  exact isCompact_uIcc
+  have sgr' {x y : ℝ} {z : ℂ} : (fderiv ℝ g { re := x, im := y }) z = fderiv ℝ gr (x, y) (Complex.equivRealProdCLM z) := by
-  exact isCompact_uIcc
+    rw [fderiv.comp]
-  apply ContinuousOn.add
+    rw [Complex.equivRealProdCLM.symm.fderiv]
-  apply Continuous.continuousOn
+    tauto
-  exact Continuous.clm_apply (ContDiff.continuous_fderiv h₁f le_rfl) continuous_const
+    apply Differentiable.differentiableAt
-  apply Continuous.continuousOn
+    exact h₁g.differentiable le_rfl
-  exact Continuous.clm_apply (ContDiff.continuous_fderiv h₁g le_rfl) continuous_const
+    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 f := F
+  let h₁f : ContDiff ℝ 1 f := by sorry
+  let g := Complex.I • F
+  let h₁g : ContDiff ℝ 1 g := by sorry
+
+  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