Compare commits

...

8 Commits

Author SHA1 Message Date
Stefan Kebekus 83f9aa5d72 Update holomorphic_primitive2.lean 2024-08-07 15:15:03 +02:00
Stefan Kebekus 951c25624e Update holomorphic_primitive2.lean 2024-08-07 13:29:58 +02:00
Stefan Kebekus fc3a4ae3f3 Update holomorphic_primitive2.lean 2024-08-07 13:11:53 +02:00
Stefan Kebekus 656d50e367 Update holomorphic_primitive2.lean 2024-08-07 12:28:36 +02:00
Stefan Kebekus f0b84fcbff Update holomorphic_primitive2.lean 2024-08-07 10:46:08 +02:00
Stefan Kebekus ad5e7c69fd Update holomorphic_primitive2.lean 2024-08-07 09:24:55 +02:00
Stefan Kebekus c3289f89c7 Update holomorphic_primitive2.lean 2024-08-07 09:21:25 +02:00
Stefan Kebekus a2d3793df2 Update holomorphic_primitive2.lean 2024-08-07 09:17:35 +02:00
1 changed files with 179 additions and 58 deletions

View File

@ -20,8 +20,10 @@ theorem primitive_zeroAtBasepoint
theorem primitive_fderivAtBasepointZero
{E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E]
(f : → E)
(hf : ContinuousAt f 0) :
{f : → E}
{R : }
(hR : 0 < R)
(hf : ContinuousOn f (Metric.ball 0 R)) :
HasDerivAt (primitive 0 f) (f 0) 0 := by
unfold primitive
simp
@ -45,20 +47,110 @@ theorem primitive_fderivAtBasepointZero
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
obtain ⟨s, h₁s, h₂s⟩ : ∃ s ⊆ f⁻¹' Metric.ball (f 0) (c / (4 : )), IsOpen s ∧ 0 ∈ s := by
have B : Metric.ball (f 0) (c / 4) ∈ nhds (f 0) := by
apply Metric.ball_mem_nhds (f 0)
linarith
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 t₀ {r : } (hr : r ∈ Metric.ball 0 ε) : IntervalIntegrable (fun x => f { re := x, im := 0 }) MeasureTheory.volume 0 r := 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
have t₁ {r : } : IntervalIntegrable (fun _ => f 0) MeasureTheory.volume 0 r := by
apply Continuous.intervalIntegrable
apply Continuous.comp
exact hf
intro x hx
apply h₂ε.2
simp
constructor
· simp
calc |x|
_ < ε := by
sorry
· simpa
have t₁ {r : } (hr : r ∈ Metric.ball 0 ε) : IntervalIntegrable (fun _ => f 0) MeasureTheory.volume 0 r := by
apply ContinuousOn.intervalIntegrable
apply ContinuousOn.comp
apply hf
fun_prop
intro x hx
simpa
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
@ -78,6 +170,9 @@ theorem primitive_fderivAtBasepointZero
apply Continuous.comp
exact hf
fun_prop
have {A B C D :E} : (A + B) - (C + D) = (A - C) + (B - D) := by
abel
conv =>
left
intro x
@ -85,22 +180,12 @@ theorem primitive_fderivAtBasepointZero
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
@ -148,12 +233,11 @@ theorem primitive_fderivAtBasepointZero
_ < ε / 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
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
@ -166,13 +250,11 @@ theorem primitive_fderivAtBasepointZero
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
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
@ -253,14 +335,21 @@ theorem primitive_translation
theorem primitive_hasDerivAtBasepoint
{E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E]
{f : → E}
{R : }
(z₀ : )
(hf : ContinuousAt f 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 : Continuous g := by continuity
let A := primitive_fderivAtBasepointZero g this
simp at A
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
@ -270,8 +359,7 @@ theorem primitive_hasDerivAtBasepoint
simp
rw [this] at B
rw [B]
have : f z₀ = (1 : ) • (f z₀) := by
exact (MulAction.one_smul (f z₀)).symm
have : f z₀ = (1 : ) • (f z₀) := (MulAction.one_smul (f z₀)).symm
conv =>
arg 2
rw [this]
@ -280,7 +368,7 @@ theorem primitive_hasDerivAtBasepoint
simp
have : g 0 = f z₀ := by simp [g]
rw [← this]
exact A
exact primitive_fderivAtBasepointZero hR hg
apply HasDerivAt.sub_const
have : (fun (x : ) ↦ x) = id := by
funext x
@ -303,10 +391,18 @@ theorem primitive_additivity
let εx := rx - dist z₀.re z₁.re
have hεx : εx > 0 := by
sorry
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
sorry
let A := hz₁.2
simp at A
dsimp [εy]
rw [dist_comm]
simpa
use εx
use hεx
@ -533,7 +629,6 @@ theorem primitive_additivity'
rw [← Complex.dist_eq_re_im]; simp
exact hz₁
obtain ⟨ε, h₁ε, h₂ε⟩ := Metric.isOpen_iff.1 lem₀Ω 0 lem₁Ω
have h'₁ε : 0 < ε := by exact h₁ε
let ε' := (2 : )⁻¹ * ε
@ -571,20 +666,28 @@ theorem primitive_additivity'
simp
rw [Complex.dist_eq_re_im]
have : dist x.re z₀.re < rx := Metric.mem_ball.mp hx.1
have : 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
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
· dsimp [rx]
sorry
· sorry
· 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₀
exact t
_ = d ε := by dsimp [d, rx, ry]
_ < R := by exact h₁ε
@ -625,13 +728,31 @@ theorem primitive_hasDerivAt
rw [Filter.EventuallyEq.hasDerivAt_iff A]
rw [← add_zero (f z)]
apply HasDerivAt.add
apply primitive_hasDerivAtBasepoint
apply hf.continuousOn.continuousAt
apply (IsOpen.mem_nhds_iff Metric.isOpen_ball).2 hz
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_differentiable
{E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E]
{f : → E}