198 lines
7.2 KiB
Plaintext
198 lines
7.2 KiB
Plaintext
import Mathlib.Analysis.Complex.TaylorSeries
|
||
import Mathlib.MeasureTheory.Integral.DivergenceTheorem
|
||
import Mathlib.MeasureTheory.Function.LocallyIntegrable
|
||
import Nevanlinna.cauchyRiemann
|
||
import Nevanlinna.partialDeriv
|
||
|
||
|
||
theorem MeasureTheory.integral2_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, 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 _
|
||
exact DifferentiableAt.hasFDerivAt ((h₁f.differentiable le_rfl) x)
|
||
--
|
||
rw [Set.diff_empty]
|
||
intro 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
|
||
|
||
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 : ℂ → E)
|
||
(hF : Differentiable ℂ F)
|
||
(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 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 _
|
||
exact h₁f
|
||
|
||
let A := integral_divergence₄ (-Complex.I • F) F h₁g h₁f lowerLeft.re upperRight.im upperRight.re lowerLeft.im
|
||
|
||
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₄ hF]
|
||
rw [partialDeriv_smul'₂]
|
||
simp
|
||
simp at A
|
||
|
||
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
|
||
|
||
|
||
noncomputable def primitive
|
||
{E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] :
|
||
ℂ → (ℂ → E) → (ℂ → E) := by
|
||
intro z₀
|
||
intro f
|
||
exact fun z ↦ (∫ (x : ℝ) in z₀.re..z.re, f ⟨x, z₀.im⟩) + Complex.I • ∫ (x : ℝ) in z₀.im..z.im, f ⟨z.re, x⟩
|
||
|
||
|
||
theorem primitive_zeroAtBasepoint
|
||
{E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
|
||
(f : ℂ → E)
|
||
(z₀ : ℂ) :
|
||
(primitive z₀ f) z₀ = 0 := by
|
||
unfold primitive
|
||
simp
|
||
|
||
|
||
theorem primitive_lem1
|
||
{E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] [IsScalarTower ℝ ℂ E]
|
||
(v : E) :
|
||
HasDerivAt (primitive 0 (fun _ ↦ v)) v 0 := by
|
||
unfold primitive
|
||
simp
|
||
|
||
have : (fun (z : ℂ) => z.re • v + Complex.I • z.im • v) = (fun (y : ℂ) => ((fun w ↦ w) y) • v) := by
|
||
funext z
|
||
rw [smul_comm]
|
||
rw [← smul_assoc]
|
||
simp
|
||
have : z.re • v = (z.re : ℂ) • v := by exact rfl
|
||
rw [this, ← add_smul]
|
||
simp
|
||
rw [this]
|
||
|
||
have hc : HasDerivAt (fun (w : ℂ) ↦ w) 1 0 := by
|
||
apply hasDerivAt_id'
|
||
nth_rewrite 2 [← (one_smul ℂ v)]
|
||
exact HasDerivAt.smul_const hc v
|
||
|
||
|
||
|
||
theorem primitive_fderivAtBasepoint
|
||
{E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
|
||
(f : ℂ → E) :
|
||
HasDerivAt (primitive 0 f) (f 0) 0 := by
|
||
unfold primitive
|
||
simp
|
||
apply hasDerivAt_iff_isLittleO.2
|
||
simp
|
||
|
||
sorry
|
||
|
||
|
||
theorem primitive_additivity
|
||
{E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
|
||
(f : ℂ → E)
|
||
(hf : Differentiable ℂ f)
|
||
(z₀ z₁ : ℂ) :
|
||
(primitive z₁ f) = (primitive z₀ f) - (fun z ↦ primitive z₀ f z₁) := by
|
||
|
||
|
||
sorry
|