import Mathlib.Analysis.Complex.TaylorSeries import Mathlib.Analysis.SpecialFunctions.Integrals import Mathlib.MeasureTheory.Integral.DivergenceTheorem import Mathlib.MeasureTheory.Integral.IntervalIntegral 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_fderivAtBasepointZero {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] (f : ℂ → E) (hf : Continuous f) : HasDerivAt (primitive 0 f) (f 0) 0 := by unfold primitive simp apply hasDerivAt_iff_isLittleO.2 simp rw [Asymptotics.isLittleO_iff] intro c hc have {z : ℂ} {e : E} : z • e = (∫ (_ : ℝ) in (0)..(z.re), e) + Complex.I • ∫ (_ : ℝ) in (0)..(z.im), e:= by simp rw [smul_comm] rw [← smul_assoc] simp have : z.re • e = (z.re : ℂ) • e := by exact rfl rw [this, ← add_smul] simp conv => left intro x left arg 1 arg 2 rw [this] have {A B C D :E} : (A + B) - (C + D) = (A - C) + (B - D) := by abel have t₀ {r : ℝ} : IntervalIntegrable (fun x => f { re := x, im := 0 }) MeasureTheory.volume 0 r := by apply Continuous.intervalIntegrable apply Continuous.comp exact hf have : (fun x => ({ re := x, im := 0 } : ℂ)) = Complex.ofRealLI := by rfl rw [this] continuity have t₁ {r : ℝ} : IntervalIntegrable (fun _ => f 0) MeasureTheory.volume 0 r := by apply Continuous.intervalIntegrable apply Continuous.comp exact hf fun_prop have t₂ {a b : ℝ} : IntervalIntegrable (fun x_1 => f { re := a, im := x_1 }) MeasureTheory.volume 0 b := by apply Continuous.intervalIntegrable apply Continuous.comp exact hf have : ((fun x => { re := a, im := x }) : ℝ → ℂ) = (fun x => { re := a, im := 0 } + { re := 0, im := x }) := by funext x apply Complex.ext rw [Complex.add_re] simp rw [Complex.add_im] simp rw [this] apply Continuous.add fun_prop have : (fun x => { re := 0, im := x } : ℝ → ℂ) = Complex.I • Complex.ofRealCLM := by funext x simp have : (x : ℂ) = {re := x, im := 0} := by rfl rw [this] rw [Complex.I_mul] simp continuity have t₃ {a : ℝ} : IntervalIntegrable (fun _ => f 0) MeasureTheory.volume 0 a := by apply Continuous.intervalIntegrable apply Continuous.comp exact hf fun_prop conv => left intro x left arg 1 rw [this] rw [← smul_sub] rw [← intervalIntegral.integral_sub t₀ t₁] rw [← intervalIntegral.integral_sub t₂ t₃] rw [Filter.eventually_iff_exists_mem] let s := f⁻¹' Metric.ball (f 0) (c / (4 : ℝ)) have h₁s : IsOpen s := IsOpen.preimage hf Metric.isOpen_ball have h₂s : 0 ∈ s := by apply Set.mem_preimage.mpr apply Metric.mem_ball_self linarith obtain ⟨ε, h₁ε, h₂ε⟩ := Metric.isOpen_iff.1 h₁s 0 h₂s have h₃ε : ∀ y ∈ Metric.ball 0 ε, ‖(f y) - (f 0)‖ < (c / (4 : ℝ)) := by intro y hy apply mem_ball_iff_norm.mp (h₂ε hy) use Metric.ball 0 (ε / (4 : ℝ)) constructor · apply Metric.ball_mem_nhds 0 linarith · intro y hy have h₁y : |y.re| < ε / 4 := by calc |y.re| _ ≤ Complex.abs y := by apply Complex.abs_re_le_abs _ < ε / 4 := by let A := mem_ball_iff_norm.1 hy simp at A linarith have h₂y : |y.im| < ε / 4 := by calc |y.im| _ ≤ Complex.abs y := by apply Complex.abs_im_le_abs _ < ε / 4 := by let A := mem_ball_iff_norm.1 hy simp at A linarith have intervalComputation {x' y' : ℝ} (h : x' ∈ Ι 0 y') : |x'| ≤ |y'| := by let A := h.1 let B := h.2 rcases le_total 0 y' with hy | hy · simp [hy] at A simp [hy] at B rw [abs_of_nonneg hy] rw [abs_of_nonneg (le_of_lt A)] exact B · simp [hy] at A simp [hy] at B rw [abs_of_nonpos hy] rw [abs_of_nonpos] linarith [h.1] exact B have t₁ : ‖(∫ (x : ℝ) in (0)..(y.re), f { re := x, im := 0 } - f 0)‖ ≤ (c / (4 : ℝ)) * |y.re - 0| := by apply intervalIntegral.norm_integral_le_of_norm_le_const intro x hx have h₁x : |x| < ε / 4 := by calc |x| _ ≤ |y.re| := intervalComputation hx _ < ε / 4 := h₁y apply le_of_lt apply h₃ε { re := x, im := 0 } rw [mem_ball_iff_norm] simp have : { re := x, im := 0 } = (x : ℂ) := by rfl rw [this] rw [Complex.abs_ofReal] linarith have t₂ : ‖∫ (x : ℝ) in (0)..(y.im), f { re := y.re, im := x } - f 0‖ ≤ (c / (4 : ℝ)) * |y.im - 0| := by apply intervalIntegral.norm_integral_le_of_norm_le_const intro x hx have h₁x : |x| < ε / 4 := by calc |x| _ ≤ |y.im| := intervalComputation hx _ < ε / 4 := h₂y apply le_of_lt apply h₃ε { re := y.re, im := x } simp calc Complex.abs { re := y.re, im := x } _ ≤ |y.re| + |x| := by apply Complex.abs_le_abs_re_add_abs_im { re := y.re, im := x } _ < ε := by linarith calc ‖(∫ (x : ℝ) in (0)..(y.re), f { re := x, im := 0 } - f 0) + Complex.I • ∫ (x : ℝ) in (0)..(y.im), f { re := y.re, im := x } - f 0‖ _ ≤ ‖(∫ (x : ℝ) in (0)..(y.re), f { re := x, im := 0 } - f 0)‖ + ‖Complex.I • ∫ (x : ℝ) in (0)..(y.im), f { re := y.re, im := x } - f 0‖ := by apply norm_add_le _ ≤ ‖(∫ (x : ℝ) in (0)..(y.re), f { re := x, im := 0 } - f 0)‖ + ‖∫ (x : ℝ) in (0)..(y.im), f { re := y.re, im := x } - f 0‖ := by simp rw [norm_smul] simp _ ≤ (c / (4 : ℝ)) * |y.re - 0| + (c / (4 : ℝ)) * |y.im - 0| := by apply add_le_add exact t₁ exact t₂ _ ≤ (c / (4 : ℝ)) * (|y.re| + |y.im|) := by simp rw [mul_add] _ ≤ (c / (4 : ℝ)) * (4 * ‖y‖) := by have : |y.re| + |y.im| ≤ 4 * ‖y‖ := by calc |y.re| + |y.im| _ ≤ ‖y‖ + ‖y‖ := by apply add_le_add apply Complex.abs_re_le_abs apply Complex.abs_im_le_abs _ ≤ 4 * ‖y‖ := by rw [← two_mul] apply mul_le_mul linarith rfl exact norm_nonneg y linarith apply mul_le_mul rfl exact this apply add_nonneg apply abs_nonneg apply abs_nonneg linarith _ ≤ c * ‖y‖ := by linarith theorem primitive_translation {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] (f : ℂ → E) (z₀ t : ℂ) : primitive z₀ (f ∘ fun z ↦ (z - t)) = ((primitive (z₀ - t) f) ∘ fun z ↦ (z - t)) := by funext z unfold primitive simp let g : ℝ → E := fun x ↦ f ( {re := x, im := z₀.im - t.im} ) have {x : ℝ} : f ({ re := x, im := z₀.im } - t) = g (1*x - t.re) := by congr 1 apply Complex.ext <;> simp conv => left left arg 1 intro x rw [this] rw [intervalIntegral.integral_comp_mul_sub g one_ne_zero (t.re)] simp congr 1 let g : ℝ → E := fun x ↦ f ( {re := z.re - t.re, im := x} ) have {x : ℝ} : f ({ re := z.re, im := x} - t) = g (1*x - t.im) := by congr 1 apply Complex.ext <;> simp conv => left arg 1 intro x rw [this] rw [intervalIntegral.integral_comp_mul_sub g one_ne_zero (t.im)] simp theorem primitive_fderivAtBasepoint {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {z₀ : ℂ} (f : ℂ → E) (hf : Continuous f) : HasDerivAt (primitive z₀ f) (f z₀) z₀ := by let g := f ∘ fun z ↦ z + z₀ have : Continuous g := by continuity let A := primitive_fderivAtBasepointZero g this simp at A let B := primitive_translation g z₀ z₀ simp at B have : (g ∘ fun z ↦ (z - z₀)) = f := by funext z dsimp [g] simp rw [this] at B rw [B] have : f z₀ = (1 : ℂ) • (f z₀) := by exact (MulAction.one_smul (f z₀)).symm conv => arg 2 rw [this] apply HasDerivAt.scomp simp have : g 0 = f z₀ := by simp [g] rw [← this] exact A apply HasDerivAt.sub_const have : (fun (x : ℂ) ↦ x) = id := by funext x simp rw [this] exact hasDerivAt_id z₀ lemma integrability₁ {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] (f : ℂ → E) (hf : Differentiable ℂ f) (a₁ a₂ b : ℝ) : IntervalIntegrable (fun x => f { re := x, im := b }) MeasureTheory.volume a₁ a₂ := by apply Continuous.intervalIntegrable apply Continuous.comp exact Differentiable.continuous hf have : ((fun x => { re := x, im := b }) : ℝ → ℂ) = (fun x => Complex.ofRealCLM x + { re := 0, im := b }) := by funext x apply Complex.ext rw [Complex.add_re] simp rw [Complex.add_im] simp rw [this] continuity lemma integrability₂ {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] (f : ℂ → E) (hf : Differentiable ℂ f) (a₁ a₂ b : ℝ) : IntervalIntegrable (fun x => f { re := b, im := x }) MeasureTheory.volume a₁ a₂ := by apply Continuous.intervalIntegrable apply Continuous.comp exact Differentiable.continuous hf have : ((fun x => { re := b, im := x }) : ℝ → ℂ) = (fun x => Complex.I • Complex.ofRealCLM x + { re := b, im := 0 }) := by funext x apply Complex.ext rw [Complex.add_re] simp simp rw [this] apply Continuous.add continuity fun_prop theorem primitive_additivity {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] (f : ℂ → E) (hf : Differentiable ℂ f) (z₀ z₁ : ℂ) : primitive z₀ f = fun z ↦ (primitive z₁ f) z + (primitive z₀ f z₁) := by funext z unfold primitive have : (∫ (x : ℝ) in z₀.re..z.re, f { re := x, im := z₀.im }) = (∫ (x : ℝ) in z₀.re..z₁.re, f { re := x, im := z₀.im }) + (∫ (x : ℝ) in z₁.re..z.re, f { re := x, im := z₀.im }) := by rw [intervalIntegral.integral_add_adjacent_intervals] apply integrability₁ f hf apply integrability₁ f hf rw [this] have : (∫ (x : ℝ) in z₀.im..z.im, f { re := z.re, im := x }) = (∫ (x : ℝ) in z₀.im..z₁.im, f { re := z.re, im := x }) + (∫ (x : ℝ) in z₁.im..z.im, f { re := z.re, im := x }) := by rw [intervalIntegral.integral_add_adjacent_intervals] apply integrability₂ f hf apply integrability₂ f hf rw [this] simp let A := integral_divergence₅ f hf ⟨z₁.re, z₀.im⟩ ⟨z.re, z₁.im⟩ simp at A have {a b c d : E} : (b + a) + (c + d) = (a + c) + (b + d) := by abel rw [this] rw [A] abel theorem primitive_fderiv {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {z₀ z : ℂ} (f : ℂ → E) (hf : Differentiable ℂ f) : HasDerivAt (primitive z₀ f) (f z) z := by rw [primitive_additivity f hf z₀ z] rw [← add_zero (f z)] apply HasDerivAt.add apply primitive_fderivAtBasepoint exact hf.continuous apply hasDerivAt_const