Compare commits

...

2 Commits

Author SHA1 Message Date
Stefan Kebekus 4642c017c7 working… 2024-08-08 14:26:53 +02:00
Stefan Kebekus 75ce3b31ef working 2024-08-08 13:32:15 +02:00
5 changed files with 1284 additions and 1261 deletions

View File

@ -3,28 +3,51 @@ import Nevanlinna.holomorphic_examples
theorem harmonic_meanValue theorem harmonic_meanValue
{f : } {f : }
(hf : ∀ z, HarmonicAt f z) {z : }
(R : ) (ρ R : )
(hR : R > 0) : (hR : R > 0)
(∫ (x : ) in (0)..2 * Real.pi, f (circleMap 0 R x)) = 2 * Real.pi * f 0 (hρ : ρ > R)
(hf : ∀ x ∈ Metric.ball z ρ , HarmonicAt f x)
:
(∫ (x : ) in (0)..2 * Real.pi, f (circleMap z R x)) = 2 * Real.pi * f z
:= by := by
obtain ⟨F, h₁F, h₂F⟩ := harmonic_is_realOfHolomorphic hf obtain ⟨F, h₁F, h₂F⟩ := harmonic_is_realOfHolomorphic (gt_trans hρ hR) hf
have regF : Differentiable F := fun z ↦ HolomorphicAt.differentiableAt (h₁F z) have hrρ : Metric.ball z R ⊆ Metric.ball z ρ := by
intro x hx
exact gt_trans hρ hx
have : (∮ (z : ) in C(0, R), z⁻¹ • F z) = (2 * ↑Real.pi * Complex.I) • F 0 := by have reg₀F : DifferentiableOn F (Metric.ball z ρ) := by
intro x hx
apply DifferentiableAt.differentiableWithinAt
apply HolomorphicAt.differentiableAt (h₁F x _)
exact hx
have reg₁F : DifferentiableOn F (Metric.ball z R) := by
intro x hx
apply DifferentiableAt.differentiableWithinAt
apply HolomorphicAt.differentiableAt (h₁F x _)
exact hrρ hx
have : (∮ (x : ) in C(z, R), (x - z)⁻¹ • F x) = (2 * ↑Real.pi * Complex.I) • F z := by
let s : Set := ∅ let s : Set := ∅
let hs : s.Countable := Set.countable_empty let hs : s.Countable := Set.countable_empty
let _ : := 0 let _ : := 0
let hw : (0 : ) ∈ Metric.ball 0 R := Metric.mem_ball_self hR have hw : (z : ) ∈ Metric.ball z R := Metric.mem_ball_self hR
let hc : ContinuousOn F (Metric.closedBall 0 R) := by have hc : ContinuousOn F (Metric.closedBall z R) := by
apply Continuous.continuousOn apply reg₀F.continuousOn.mono
exact regF.continuous intro x hx
let hd : ∀ x ∈ Metric.ball 0 R \ s, DifferentiableAt F x := by simp at hx
intro x _ simp
exact regF x linarith
have hd : ∀ x ∈ Metric.ball z R \ s, DifferentiableAt F x := by
intro x hx
let A := reg₁F x hx.1
apply A.differentiableAt
apply (IsOpen.mem_nhds_iff ?hs).mpr
exact hx.1
exact Metric.isOpen_ball
let CIF := Complex.circleIntegral_sub_inv_smul_of_differentiable_on_off_countable hs hw hc hd let CIF := Complex.circleIntegral_sub_inv_smul_of_differentiable_on_off_countable hs hw hc hd
simp at CIF simp at CIF
assumption assumption
@ -32,7 +55,7 @@ theorem harmonic_meanValue
unfold circleIntegral at this unfold circleIntegral at this
simp_rw [deriv_circleMap] at this simp_rw [deriv_circleMap] at this
have t₁ {θ : } : (circleMap 0 R θ * Complex.I) • (circleMap 0 R θ)⁻¹ • F (circleMap 0 R θ) = Complex.I • F (circleMap 0 R θ) := by have t₁ {θ : } : (circleMap 0 R θ * Complex.I) • (circleMap 0 R θ)⁻¹ • F (circleMap z R θ) = Complex.I • F (circleMap z R θ) := by
rw [← smul_assoc] rw [← smul_assoc]
congr 1 congr 1
simp simp

View File

@ -1,6 +1,6 @@
import Nevanlinna.complexHarmonic import Nevanlinna.complexHarmonic
import Nevanlinna.holomorphicAt import Nevanlinna.holomorphicAt
import Nevanlinna.holomorphic_primitive2 import Nevanlinna.holomorphic_primitive
import Nevanlinna.mathlibAddOn import Nevanlinna.mathlibAddOn

File diff suppressed because it is too large Load Diff

View File

@ -1,846 +0,0 @@
import Mathlib.Analysis.Complex.TaylorSeries
import Mathlib.Data.ENNReal.Basic
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}
{R : }
(hR : 0 < R)
(hf : ContinuousOn f (Metric.ball 0 R)) :
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]
obtain ⟨s, h₁s, h₂s⟩ : ∃ s ⊆ f⁻¹' Metric.ball (f 0) (c / (4 : )), IsOpen s ∧ 0 ∈ s := by
apply eventually_nhds_iff.mp
apply continuousAt_def.1
apply Continuous.continuousAt
fun_prop
apply continuousAt_def.1
apply hf.continuousAt
exact Metric.ball_mem_nhds 0 hR
apply Metric.ball_mem_nhds (f 0)
simpa
obtain ⟨ε, h₁ε, h₂ε⟩ : ∃ ε > 0, (Metric.ball 0 ε) × (Metric.ball 0 ε) ⊆ s ∧ (Metric.ball 0 ε) × (Metric.ball 0 ε) ⊆ Metric.ball 0 R := by
obtain ⟨ε', h₁ε', h₂ε'⟩ : ∃ ε' > 0, Metric.ball 0 ε' ⊆ s ∩ Metric.ball 0 R := by
apply Metric.mem_nhds_iff.mp
apply IsOpen.mem_nhds
apply IsOpen.inter
exact h₂s.1
exact Metric.isOpen_ball
constructor
· exact h₂s.2
· simpa
use (2 : )⁻¹ * ε'
constructor
· simpa
· constructor
· intro x hx
apply (h₂ε' _).1
simp
calc Complex.abs x
_ ≤ |x.re| + |x.im| := Complex.abs_le_abs_re_add_abs_im x
_ < (2 : )⁻¹ * ε' + |x.im| := by
apply (add_lt_add_iff_right |x.im|).mpr
have : x.re ∈ Metric.ball 0 (2⁻¹ * ε') := (Complex.mem_reProdIm.1 hx).1
simp at this
exact this
_ < (2 : )⁻¹ * ε' + (2 : )⁻¹ * ε' := by
apply (add_lt_add_iff_left ((2 : )⁻¹ * ε')).mpr
have : x.im ∈ Metric.ball 0 (2⁻¹ * ε') := (Complex.mem_reProdIm.1 hx).2
simp at this
exact this
_ = ε' := by
rw [← add_mul]
abel_nf
simp
· intro x hx
apply (h₂ε' _).2
simp
calc Complex.abs x
_ ≤ |x.re| + |x.im| := Complex.abs_le_abs_re_add_abs_im x
_ < (2 : )⁻¹ * ε' + |x.im| := by
apply (add_lt_add_iff_right |x.im|).mpr
have : x.re ∈ Metric.ball 0 (2⁻¹ * ε') := (Complex.mem_reProdIm.1 hx).1
simp at this
exact this
_ < (2 : )⁻¹ * ε' + (2 : )⁻¹ * ε' := by
apply (add_lt_add_iff_left ((2 : )⁻¹ * ε')).mpr
have : x.im ∈ Metric.ball 0 (2⁻¹ * ε') := (Complex.mem_reProdIm.1 hx).2
simp at this
exact this
_ = ε' := by
rw [← add_mul]
abel_nf
simp
have h₃ε : ∀ y ∈ (Metric.ball 0 ε) × (Metric.ball 0 ε), ‖(f y) - (f 0)‖ < (c / (4 : )) := by
intro y hy
apply mem_ball_iff_norm.mp
apply h₁s
exact h₂ε.1 hy
have intervalComputation_uIcc {x' y' : } (h : x' ∈ Set.uIcc 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
rwa [abs_of_nonneg A, abs_of_nonneg hy]
· simp [hy] at A
simp [hy] at B
rw [abs_of_nonpos hy]
rw [abs_of_nonpos]
linarith [h.1]
exact B
rw [Filter.eventually_iff_exists_mem]
use Metric.ball 0 (ε / (4 : ))
constructor
· apply Metric.ball_mem_nhds 0
linarith
· intro y hy
have {A B C D :E} : (A + B) - (C + D) = (A - C) + (B - D) := by
abel
rw [this]
rw [← smul_sub]
have t₀ : IntervalIntegrable (fun x => f { re := x, im := 0 }) MeasureTheory.volume 0 y.re := by
apply ContinuousOn.intervalIntegrable
apply ContinuousOn.comp
exact hf
have : (fun x => ({ re := x, im := 0 } : )) = Complex.ofRealLI := by rfl
rw [this]
apply Continuous.continuousOn
continuity
intro x hx
apply h₂ε.2
simp
constructor
· simp
calc |x|
_ ≤ |y.re| := by apply intervalComputation_uIcc hx
_ ≤ Complex.abs y := by exact Complex.abs_re_le_abs y
_ < ε / 4 := by simp at hy; assumption
_ < ε := by linarith
· simpa
have t₁ : IntervalIntegrable (fun _ => f 0) MeasureTheory.volume 0 y.re := by
apply ContinuousOn.intervalIntegrable
apply ContinuousOn.comp
apply hf
fun_prop
intro x _
simpa
rw [← intervalIntegral.integral_sub t₀ t₁]
have t₂ : IntervalIntegrable (fun x_1 => f { re := y.re, im := x_1 }) MeasureTheory.volume 0 y.im := by
apply ContinuousOn.intervalIntegrable
apply ContinuousOn.comp
exact hf
have : (Complex.mk y.re) = (fun x => Complex.I • Complex.ofRealCLM x + { re := y.re, im := 0 }) := by
funext x
apply Complex.ext
rw [Complex.add_re]
simp
simp
rw [this]
apply ContinuousOn.add
apply Continuous.continuousOn
continuity
fun_prop
intro x hx
apply h₂ε.2
constructor
· simp
calc |y.re|
_ ≤ Complex.abs y := by exact Complex.abs_re_le_abs y
_ < ε / 4 := by simp at hy; assumption
_ < ε := by linarith
· simp
calc |x|
_ ≤ |y.im| := by apply intervalComputation_uIcc hx
_ ≤ Complex.abs y := by exact Complex.abs_im_le_abs y
_ < ε / 4 := by simp at hy; assumption
_ < ε := by linarith
have t₃ : IntervalIntegrable (fun _ => f 0) MeasureTheory.volume 0 y.im := by
apply ContinuousOn.intervalIntegrable
apply ContinuousOn.comp
exact hf
fun_prop
intro x _
apply h₂ε.2
simp
constructor
· simpa
· simpa
rw [← intervalIntegral.integral_sub t₂ t₃]
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 }
constructor
· simp
linarith
· simp
exact h₁ε
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 }
constructor
· simp
linarith
· simp
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_hasDerivAtBasepoint
{E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E]
{f : → E}
{R : }
(z₀ : )
(hR : 0 < R)
(hf : ContinuousOn f (Metric.ball z₀ R)) :
HasDerivAt (primitive z₀ f) (f z₀) z₀ := by
let g := f ∘ fun z ↦ z + z₀
have hg : ContinuousOn g (Metric.ball 0 R) := by
apply ContinuousOn.comp
fun_prop
fun_prop
intro x hx
simp
simp at hx
assumption
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₀) := (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 primitive_fderivAtBasepointZero hR hg
apply HasDerivAt.sub_const
have : (fun (x : ) ↦ x) = id := by
funext x
simp
rw [this]
exact hasDerivAt_id z₀
theorem primitive_additivity
{E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E]
{f : → E}
{z₀ : }
{rx ry : }
(hf : DifferentiableOn f (Metric.ball z₀.re rx × Metric.ball z₀.im ry))
(hry : 0 < ry)
{z₁ : }
(hz₁ : z₁ ∈ (Metric.ball z₀.re rx × Metric.ball z₀.im ry))
:
∃ εx > 0, ∃ εy > 0, ∀ z ∈ (Metric.ball z₁.re εx × Metric.ball z₁.im εy), (primitive z₀ f z) - (primitive z₁ f z) - (primitive z₀ f z₁) = 0 := by
let εx := rx - dist z₀.re z₁.re
have hεx : εx > 0 := by
let A := hz₁.1
simp at A
dsimp [εx]
rw [dist_comm]
simpa
let εy := ry - dist z₀.im z₁.im
have hεy : εy > 0 := by
let A := hz₁.2
simp at A
dsimp [εy]
rw [dist_comm]
simpa
use εx
use hεx
use εy
use hεy
intro z hz
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]
-- IntervalIntegrable (fun x => f { re := x, im := z₀.im }) MeasureTheory.volume z₀.re z₁.re
apply ContinuousOn.intervalIntegrable
apply ContinuousOn.comp
exact hf.continuousOn
have {b : } : ((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
apply Continuous.continuousOn
rw [this]
continuity
-- Remains: Set.MapsTo (fun x => { re := x, im := z₀.im }) (Set.uIcc z₀.re z₁.re) (Metric.ball z₀.re rx × Metric.ball z₀.im ry)
intro w hw
simp
apply Complex.mem_reProdIm.mpr
constructor
· simp
calc dist w z₀.re
_ ≤ dist z₁.re z₀.re := by apply Real.dist_right_le_of_mem_uIcc; rwa [Set.uIcc_comm] at hw
_ < rx := by apply Metric.mem_ball.mp (Complex.mem_reProdIm.1 hz₁).1
· simpa
-- IntervalIntegrable (fun x => f { re := x, im := z₀.im }) MeasureTheory.volume z₁.re z.re
apply ContinuousOn.intervalIntegrable
apply ContinuousOn.comp
exact hf.continuousOn
have {b : } : ((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
apply Continuous.continuousOn
rw [this]
continuity
-- Remains: Set.MapsTo (fun x => { re := x, im := z₀.im }) (Set.uIcc z₁.re z.re) (Metric.ball z₀.re rx × Metric.ball z₀.im ry)
intro w hw
simp
constructor
· simp
calc dist w z₀.re
_ ≤ dist w z₁.re + dist z₁.re z₀.re := by exact dist_triangle w z₁.re z₀.re
_ ≤ dist z.re z₁.re + dist z₁.re z₀.re := by
apply (add_le_add_iff_right (dist z₁.re z₀.re)).mpr
rw [Set.uIcc_comm] at hw
exact Real.dist_right_le_of_mem_uIcc hw
_ < (rx - dist z₀.re z₁.re) + dist z₁.re z₀.re := by
apply (add_lt_add_iff_right (dist z₁.re z₀.re)).mpr
apply Metric.mem_ball.1 (Complex.mem_reProdIm.1 hz).1
_ = rx := by
rw [dist_comm]
simp
· simpa
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]
-- IntervalIntegrable (fun x => f { re := z.re, im := x }) MeasureTheory.volume z₀.im z₁.im
apply ContinuousOn.intervalIntegrable
apply ContinuousOn.comp
exact hf.continuousOn
apply Continuous.continuousOn
have {b : }: (Complex.mk b) = (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
fun_prop
fun_prop
-- Set.MapsTo (Complex.mk z.re) (Set.uIcc z₀.im z₁.im) (Metric.ball z₀.re rx × Metric.ball z₀.im ry)
intro w hw
constructor
· simp
calc dist z.re z₀.re
_ ≤ dist z.re z₁.re + dist z₁.re z₀.re := by exact dist_triangle z.re z₁.re z₀.re
_ < (rx - dist z₀.re z₁.re) + dist z₁.re z₀.re := by
apply (add_lt_add_iff_right (dist z₁.re z₀.re)).mpr
apply Metric.mem_ball.1 (Complex.mem_reProdIm.1 hz).1
_ = rx := by
rw [dist_comm]
simp
· simp
calc dist w z₀.im
_ ≤ dist z₁.im z₀.im := by rw [Set.uIcc_comm] at hw; exact Real.dist_right_le_of_mem_uIcc hw
_ < ry := by
rw [← Metric.mem_ball]
exact hz₁.2
-- IntervalIntegrable (fun x => f { re := z.re, im := x }) MeasureTheory.volume z₁.im z.im
apply ContinuousOn.intervalIntegrable
apply ContinuousOn.comp
exact hf.continuousOn
apply Continuous.continuousOn
have {b : }: (Complex.mk b) = (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
fun_prop
fun_prop
-- Set.MapsTo (Complex.mk z.re) (Set.uIcc z₁.im z.im) (Metric.ball z₀.re rx × Metric.ball z₀.im ry)
intro w hw
constructor
· simp
calc dist z.re z₀.re
_ ≤ dist z.re z₁.re + dist z₁.re z₀.re := by exact dist_triangle z.re z₁.re z₀.re
_ < (rx - dist z₀.re z₁.re) + dist z₁.re z₀.re := by
apply (add_lt_add_iff_right (dist z₁.re z₀.re)).mpr
apply Metric.mem_ball.1 (Complex.mem_reProdIm.1 hz).1
_ = rx := by
rw [dist_comm]
simp
· simp
calc dist w z₀.im
_ ≤ dist w z₁.im + dist z₁.im z₀.im := by exact dist_triangle w z₁.im z₀.im
_ ≤ dist z.im z₁.im + dist z₁.im z₀.im := by
apply (add_le_add_iff_right (dist z₁.im z₀.im)).mpr
rw [Set.uIcc_comm] at hw
exact Real.dist_right_le_of_mem_uIcc hw
_ < (ry - dist z₀.im z₁.im) + dist z₁.im z₀.im := by
apply (add_lt_add_iff_right (dist z₁.im z₀.im)).mpr
apply Metric.mem_ball.1 (Complex.mem_reProdIm.1 hz).2
_ = ry := by
rw [dist_comm]
simp
rw [this]
simp
have {a b c d e f g h : E} : (a + b) + (c + d) - (e + f) - (g + h) = b + (a - g) - e - f + d - h + (c) := by
abel
rw [this]
have H' : DifferentiableOn f (Set.uIcc z₁.re z.re × Set.uIcc z₀.im z₁.im) := by
apply DifferentiableOn.mono hf
intro x hx
constructor
· simp
calc dist x.re z₀.re
_ ≤ dist x.re z₁.re + dist z₁.re z₀.re := by exact dist_triangle x.re z₁.re z₀.re
_ ≤ dist z.re z₁.re + dist z₁.re z₀.re := by
apply (add_le_add_iff_right (dist z₁.re z₀.re)).mpr
rw [Set.uIcc_comm] at hx
apply Real.dist_right_le_of_mem_uIcc (Complex.mem_reProdIm.1 hx).1
_ < (rx - dist z₀.re z₁.re) + dist z₁.re z₀.re := by
apply (add_lt_add_iff_right (dist z₁.re z₀.re)).mpr
apply Metric.mem_ball.1 (Complex.mem_reProdIm.1 hz).1
_ = rx := by
rw [dist_comm]
simp
· simp
calc dist x.im z₀.im
_ ≤ dist z₀.im z₁.im := by rw [dist_comm]; exact Real.dist_left_le_of_mem_uIcc (Complex.mem_reProdIm.1 hx).2
_ < ry := by
rw [dist_comm]
exact Metric.mem_ball.1 (Complex.mem_reProdIm.1 hz₁).2
let A := Complex.integral_boundary_rect_eq_zero_of_differentiableOn f ⟨z₁.re, z₀.im⟩ ⟨z.re, z₁.im⟩ H'
have {x : } {w : } : ↑x + w.im * Complex.I = { re := x, im := w.im } := by
apply Complex.ext
· simp
· simp
simp_rw [this] at A
have {x : } {w : } : w.re + x * Complex.I = { re := w.re, im := x } := by
apply Complex.ext
· simp
· simp
simp_rw [this] at A
rw [← A]
abel
theorem primitive_additivity'
{E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E]
{f : → E}
{z₀ z₁ : }
{R : }
(hf : DifferentiableOn f (Metric.ball z₀ R))
(hz₁ : z₁ ∈ Metric.ball z₀ R)
:
primitive z₀ f =ᶠ[nhds z₁] fun z ↦ (primitive z₁ f z) + (primitive z₀ f z₁) := by
let d := fun ε ↦ √((dist z₁.re z₀.re + ε) ^ 2 + (dist z₁.im z₀.im + ε) ^ 2)
have h₀d : Continuous d := by continuity
have h₁d : ∀ ε, 0 ≤ d ε := fun ε ↦ Real.sqrt_nonneg ((dist z₁.re z₀.re + ε) ^ 2 + (dist z₁.im z₀.im + ε) ^ 2)
obtain ⟨ε, h₀ε, h₁ε⟩ : ∃ ε > 0, d ε < R := by
let Omega := d⁻¹' Metric.ball 0 R
have lem₀Ω : IsOpen Omega := IsOpen.preimage h₀d Metric.isOpen_ball
have lem₁Ω : 0 ∈ Omega := by
dsimp [Omega, d]; simp
have : dist z₁.re z₀.re = |z₁.re - z₀.re| := by exact rfl
rw [this]
have : dist z₁.im z₀.im = |z₁.im - z₀.im| := by exact rfl
rw [this]
simp
rw [← Complex.dist_eq_re_im]; simp
exact hz₁
obtain ⟨ε, h₁ε, h₂ε⟩ := Metric.isOpen_iff.1 lem₀Ω 0 lem₁Ω
let ε' := (2 : )⁻¹ * ε
have h₀ε' : ε' ∈ Omega := by
apply h₂ε
dsimp [ε']; simp
have : |ε| = ε := by apply abs_of_pos h₁ε
rw [this]
apply (inv_mul_lt_iff zero_lt_two).mpr
linarith
have h₁ε' : 0 < ε' := by
apply Real.mul_pos _ h₁ε
apply inv_pos.mpr
exact zero_lt_two
use ε'
constructor
· exact h₁ε'
· dsimp [Omega] at h₀ε'; simp at h₀ε'
rwa [abs_of_nonneg (h₁d ε')] at h₀ε'
let rx := dist z₁.re z₀.re + ε
let ry := dist z₁.im z₀.im + ε
have h'ry : 0 < ry := by
dsimp [ry]
apply add_pos_of_nonneg_of_pos
exact dist_nonneg
simpa
have h'f : DifferentiableOn f (Metric.ball z₀.re rx × Metric.ball z₀.im ry) := by
apply hf.mono
intro x hx
simp
rw [Complex.dist_eq_re_im]
have t₀ : dist x.re z₀.re < rx := Metric.mem_ball.mp hx.1
have t₁ : dist x.im z₀.im < ry := Metric.mem_ball.mp hx.2
have t₂ : √((x.re - z₀.re) ^ 2 + (x.im - z₀.im) ^ 2) < √( rx ^ 2 + ry ^ 2) := by
rw [Real.sqrt_lt_sqrt_iff]
apply add_lt_add
· rw [sq_lt_sq]
dsimp [dist] at t₀
nth_rw 2 [abs_of_nonneg]
assumption
apply add_nonneg dist_nonneg (le_of_lt h₀ε)
· rw [sq_lt_sq]
dsimp [dist] at t₁
nth_rw 2 [abs_of_nonneg]
assumption
apply add_nonneg dist_nonneg (le_of_lt h₀ε)
apply add_nonneg
exact sq_nonneg (x.re - z₀.re)
exact sq_nonneg (x.im - z₀.im)
calc √((x.re - z₀.re) ^ 2 + (x.im - z₀.im) ^ 2)
_ < √( rx ^ 2 + ry ^ 2) := by
exact t₂
_ = d ε := by dsimp [d, rx, ry]
_ < R := by exact h₁ε
have h'z₁ : z₁ ∈ (Metric.ball z₀.re rx × Metric.ball z₀.im ry) := by
dsimp [rx, ry]
constructor
· simp; exact h₀ε
· simp; exact h₀ε
obtain ⟨εx, hεx, εy, hεy, hε⟩ := primitive_additivity h'f h'ry h'z₁
apply Filter.eventuallyEq_iff_exists_mem.2
use (Metric.ball z₁.re εx × Metric.ball z₁.im εy)
constructor
· apply IsOpen.mem_nhds
apply IsOpen.reProdIm
exact Metric.isOpen_ball
exact Metric.isOpen_ball
constructor
· simpa
· simpa
· intro x hx
simp
rw [← sub_zero (primitive z₀ f x), ← hε x hx]
abel
theorem primitive_hasDerivAt
{E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E]
{f : → E}
{z₀ z : }
{R : }
(hf : DifferentiableOn f (Metric.ball z₀ R))
(hz : z ∈ Metric.ball z₀ R) :
HasDerivAt (primitive z₀ f) (f z) z := by
let A := primitive_additivity' hf hz
rw [Filter.EventuallyEq.hasDerivAt_iff A]
rw [← add_zero (f z)]
apply HasDerivAt.add
let R' := R - dist z z₀
have h₀R' : 0 < R' := by
dsimp [R']
simp
exact hz
have h₁R' : Metric.ball z R' ⊆ Metric.ball z₀ R := by
intro x hx
simp
calc dist x z₀
_ ≤ dist x z + dist z z₀ := dist_triangle x z z₀
_ < R' + dist z z₀ := by
refine add_lt_add_right ?bc (dist z z₀)
exact hx
_ = R := by
dsimp [R']
simp
apply primitive_hasDerivAtBasepoint
exact h₀R'
apply ContinuousOn.mono hf.continuousOn h₁R'
apply hasDerivAt_const
theorem primitive_differentiableOn
{E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E]
{f : → E}
{z₀ : }
{R : }
(hf : DifferentiableOn f (Metric.ball z₀ R))
:
DifferentiableOn (primitive z₀ f) (Metric.ball z₀ R) := by
intro z hz
apply DifferentiableAt.differentiableWithinAt
exact (primitive_hasDerivAt hf hz).differentiableAt
theorem primitive_hasFderivAt
{E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E]
{f : → E}
(z₀ : )
(R : )
(hf : DifferentiableOn f (Metric.ball z₀ R))
:
∀ z ∈ Metric.ball z₀ R, HasFDerivAt (primitive z₀ f) ((ContinuousLinearMap.lsmul ).flip (f z)) z := by
intro z hz
rw [hasFDerivAt_iff_hasDerivAt]
simp
apply primitive_hasDerivAt hf hz
theorem primitive_hasFderivAt'
{f : }
{z₀ : }
{R : }
(hf : DifferentiableOn f (Metric.ball z₀ R))
:
∀ z ∈ Metric.ball z₀ R, HasFDerivAt (primitive z₀ f) (ContinuousLinearMap.lsmul (f z)) z := by
intro z hz
rw [hasFDerivAt_iff_hasDerivAt]
simp
exact primitive_hasDerivAt hf hz
theorem primitive_fderiv
{E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E]
{f : → E}
{z₀ : }
{R : }
(hf : DifferentiableOn f (Metric.ball z₀ R))
:
∀ z ∈ Metric.ball z₀ R, (fderiv (primitive z₀ f) z) = (ContinuousLinearMap.lsmul ).flip (f z) := by
intro z hz
apply HasFDerivAt.fderiv
exact primitive_hasFderivAt z₀ R hf z hz
theorem primitive_fderiv'
{f : }
{z₀ : }
{R : }
(hf : DifferentiableOn f (Metric.ball z₀ R))
:
∀ z ∈ Metric.ball z₀ R, (fderiv (primitive z₀ f) z) = ContinuousLinearMap.lsmul (f z) := by
intro z hz
apply HasFDerivAt.fderiv
exact primitive_hasFderivAt' hf z hz

View File

@ -0,0 +1,666 @@
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.partialDeriv
import Nevanlinna.cauchyRiemann
/-
noncomputable def partialDeriv
{E : Type*} [NormedAddCommGroup E] [NormedSpace E]
{F : Type*} [NormedAddCommGroup F] [NormedSpace F] : E → (E → F) → (E → F) :=
fun v ↦ (fun f ↦ (fun w ↦ fderiv f w v))
theorem partialDeriv_compContLinAt
{E : Type*} [NormedAddCommGroup E] [NormedSpace E]
{F : Type*} [NormedAddCommGroup F] [NormedSpace F]
{G : Type*} [NormedAddCommGroup G] [NormedSpace G]
{f : E → F}
{l : F →L[] G}
{v : E}
{x : E}
(h : DifferentiableAt f x) :
(partialDeriv v (l ∘ f)) x = (l ∘ partialDeriv v f) x:= by
unfold partialDeriv
rw [fderiv.comp x (ContinuousLinearMap.differentiableAt l) h]
simp
theorem partialDeriv_compCLE
{E : Type*} [NormedAddCommGroup E] [NormedSpace E]
{F : Type*} [NormedAddCommGroup F] [NormedSpace F]
{G : Type*} [NormedAddCommGroup G] [NormedSpace G]
{f : E → F}
{l : F ≃L[] G} {v : E} : partialDeriv v (l ∘ f) = l ∘ partialDeriv v f := by
funext x
by_cases hyp : DifferentiableAt f x
· let lCLM : F →L[] G := l
suffices shyp : partialDeriv v (lCLM ∘ f) x = (lCLM ∘ partialDeriv v f) x from by tauto
apply partialDeriv_compContLinAt
exact hyp
· unfold partialDeriv
rw [fderiv_zero_of_not_differentiableAt]
simp
rw [fderiv_zero_of_not_differentiableAt]
simp
exact hyp
rw [ContinuousLinearEquiv.comp_differentiableAt_iff]
exact hyp
theorem partialDeriv_smul'₂
{E : Type*} [NormedAddCommGroup E] [NormedSpace E]
{F : Type*} [NormedAddCommGroup F] [NormedSpace F]
{f : E → F} {a : } {v : E} :
partialDeriv v (a • f) = a • partialDeriv v f := by
funext w
by_cases ha : a = 0
· unfold partialDeriv
have : a • f = fun y ↦ a • f y := by rfl
rw [this, ha]
simp
· -- Now a is not zero. We present scalar multiplication with a as a continuous linear equivalence.
let smulCLM : F ≃L[] F :=
{
toFun := fun x ↦ a • x
map_add' := fun x y => DistribSMul.smul_add a x y
map_smul' := fun m x => (smul_comm ((RingHom.id ) m) a x).symm
invFun := fun x ↦ a⁻¹ • x
left_inv := by
intro x
simp
rw [← smul_assoc, smul_eq_mul, mul_comm, mul_inv_cancel ha, one_smul]
right_inv := by
intro x
simp
rw [← smul_assoc, smul_eq_mul, mul_inv_cancel ha, one_smul]
continuous_toFun := continuous_const_smul a
continuous_invFun := continuous_const_smul a⁻¹
}
have : a • f = smulCLM ∘ f := by tauto
rw [this]
rw [partialDeriv_compCLE]
tauto
theorem CauchyRiemann₄
{F : Type*} [NormedAddCommGroup F] [NormedSpace F]
{f : → F} :
(Differentiable f) → partialDeriv Complex.I f = Complex.I • partialDeriv 1 f := by
intro h
unfold partialDeriv
conv =>
left
intro w
rw [DifferentiableAt.fderiv_restrictScalars (h w)]
simp
rw [← mul_one Complex.I]
rw [← smul_eq_mul]
conv =>
right
right
intro w
rw [DifferentiableAt.fderiv_restrictScalars (h w)]
funext w
simp
-/
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 Complex.I F z := by rfl
conv at A in (fderiv F _) _ => rw [this]
have {z : } : fderiv (-Complex.I • F) z 1 = partialDeriv 1 (-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 hf
have : (Complex.mk a) = (fun x => Complex.I • Complex.ofRealCLM x + { re := a, im := 0 }) := by
funext x
apply Complex.ext
rw [Complex.add_re]
simp
simp
rw [this]
apply Continuous.add
continuity
fun_prop
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_hasDerivAtBasepoint
{E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E]
{f : → E}
(hf : Continuous f)
(z₀ : ) :
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 : (Complex.mk b) = (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_hasDerivAt
{E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E]
{f : → E}
(hf : Differentiable f)
(z₀ z : ) :
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_hasDerivAtBasepoint
exact hf.continuous
apply hasDerivAt_const
theorem primitive_differentiable
{E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E]
{f : → E}
(hf : Differentiable f)
(z₀ : ) :
Differentiable (primitive z₀ f) := by
intro z
exact (primitive_hasDerivAt hf z₀ z).differentiableAt
theorem primitive_hasFderivAt
{E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E]
{f : → E}
(hf : Differentiable f)
(z₀ : ) :
∀ z, HasFDerivAt (primitive z₀ f) ((ContinuousLinearMap.lsmul ).flip (f z)) z := by
intro z
rw [hasFDerivAt_iff_hasDerivAt]
simp
exact primitive_hasDerivAt hf z₀ z
theorem primitive_hasFderivAt'
{f : }
(hf : Differentiable f)
(z₀ : ) :
∀ z, HasFDerivAt (primitive z₀ f) (ContinuousLinearMap.lsmul (f z)) z := by
intro z
rw [hasFDerivAt_iff_hasDerivAt]
simp
exact primitive_hasDerivAt hf z₀ z
theorem primitive_fderiv
{E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E]
{f : → E}
(hf : Differentiable f)
(z₀ : ) :
∀ z, (fderiv (primitive z₀ f) z) = (ContinuousLinearMap.lsmul ).flip (f z) := by
intro z
apply HasFDerivAt.fderiv
exact primitive_hasFderivAt hf z₀ z
theorem primitive_fderiv'
{f : }
(hf : Differentiable f)
(z₀ : ) :
∀ z, (fderiv (primitive z₀ f) z) = ContinuousLinearMap.lsmul (f z) := by
intro z
apply HasFDerivAt.fderiv
exact primitive_hasFderivAt' hf z₀ z