working
This commit is contained in:
Stefan Kebekus
parent
c3ec40490e
commit
f43fd50528
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Reference in New Issue