From a9f1c3eaa60420ad527f1c529a808113897b9295 Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Wed, 12 Jun 2024 12:30:08 +0200 Subject: [PATCH] Update holomorphic.primitive.lean --- Nevanlinna/holomorphic.primitive.lean | 106 +++++++++++++++++++------- 1 file changed, 78 insertions(+), 28 deletions(-) diff --git a/Nevanlinna/holomorphic.primitive.lean b/Nevanlinna/holomorphic.primitive.lean index 60b12bd..07b8d1d 100644 --- a/Nevanlinna/holomorphic.primitive.lean +++ b/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₂ ∅ - 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 + 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 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