From 0f6c905f60d640fa6c607dd753d1d1d4e712645b Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Fri, 14 Jun 2024 10:53:24 +0200 Subject: [PATCH] Update holomorphic.primitive.lean --- Nevanlinna/holomorphic.primitive.lean | 112 ++++++-------------------- 1 file changed, 24 insertions(+), 88 deletions(-) diff --git a/Nevanlinna/holomorphic.primitive.lean b/Nevanlinna/holomorphic.primitive.lean index 4813e2c..579130a 100644 --- a/Nevanlinna/holomorphic.primitive.lean +++ b/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₁ : ℝ) - (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 + (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 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 + 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 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 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 + 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₄ this] + rw [CauchyRiemann₄ hF] rw [partialDeriv_smul'₂] - rw [← smul_assoc] simp simp at A - - - sorry + 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