From f43fd505288f4ed8889524eaf35d7d12eaca5436 Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Tue, 11 Jun 2024 17:18:24 +0200 Subject: [PATCH] working --- Nevanlinna/holomorphic.primitive.lean | 139 ++++++++++++++++++++++++++ Nevanlinna/holomorphicAt.lean | 14 +-- 2 files changed, 140 insertions(+), 13 deletions(-) create mode 100644 Nevanlinna/holomorphic.primitive.lean diff --git a/Nevanlinna/holomorphic.primitive.lean b/Nevanlinna/holomorphic.primitive.lean new file mode 100644 index 0000000..60b12bd --- /dev/null +++ b/Nevanlinna/holomorphic.primitive.lean @@ -0,0 +1,139 @@ +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_prod_of_hasFDerivWithinAt_off_countable₃ + {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 h₁x + exact DifferentiableAt.hasFDerivAt ((h₁f.differentiable le_rfl) x) + -- + rw [Set.diff_empty] + intro y h₁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 + + 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 h₁x + exact DifferentiableAt.hasFDerivAt ((h₁f.differentiable le_rfl) x) + -- + rw [Set.diff_empty] + intro y h₁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 diff --git a/Nevanlinna/holomorphicAt.lean b/Nevanlinna/holomorphicAt.lean index e6ae80a..b7d7cdd 100644 --- a/Nevanlinna/holomorphicAt.lean +++ b/Nevanlinna/holomorphicAt.lean @@ -143,17 +143,5 @@ theorem HolomorphicAt.CauchyRiemannAt · exact IsOpen.mem_nhds h₁s hz · intro w hw let h := h₂f w hw - -- WARNING This should go to partialDeriv unfold partialDeriv - simp - conv => - left - rw [DifferentiableAt.fderiv_restrictScalars ℝ h] - simp - rw [← mul_one Complex.I] - rw [← smul_eq_mul] - rw [ContinuousLinearMap.map_smul_of_tower (fderiv ℂ f w) Complex.I 1] - conv => - right - right - rw [DifferentiableAt.fderiv_restrictScalars ℝ h] + apply CauchyRiemann₅ h