kebekus
/
nevanlinna
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Update holomorphic.primitive.lean

This commit is contained in:
Stefan Kebekus 2024-06-18 09:56:44 +02:00
parent 46ededdde7
commit 2d7e62bb49
1 changed files with 48 additions and 14 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

62
Nevanlinna/holomorphic.primitive.lean
View File

@ -243,14 +243,38 @@ theorem primitive_fderivAtBasepoint
let A := mem_ball_iff_norm.1 hy let A := mem_ball_iff_norm.1 hy
simp at A simp at A
assumption assumption
have h₂y : |y.im| < ε := by
calc |y.im|
_ ≤ Complex.abs y := by apply Complex.abs_im_le_abs
_ < ε := by
let A := mem_ball_iff_norm.1 hy
simp at A
assumption
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 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 apply intervalIntegral.norm_integral_le_of_norm_le_const
intro x hx intro x hx
have h₁x : |x| < ε := by have h₁x : |x| < ε := by
calc |x|
sorry _ ≤ |y.re| := intervalComputation hx
_ < ε := h₁y
apply le_of_lt apply le_of_lt
apply h₃ε { re := x, im := 0 } apply h₃ε { re := x, im := 0 }
rw [mem_ball_iff_norm] rw [mem_ball_iff_norm]
@ -264,16 +288,21 @@ theorem primitive_fderivAtBasepoint
have t₂ : ‖∫ (x : ℝ) in (0)..(y.im), f { re := y.re, im := x } - f 0‖ ≤ (c / (4 : ℝ)) * |y.im - 0| := by 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 apply intervalIntegral.norm_integral_le_of_norm_le_const
intro x hx intro x hx
have h₁x : |x| < ε := by have h₁x : |x| < ε := by
sorry calc |x|
_ ≤ |y.im| := intervalComputation hx
_ < ε := h₂y
apply le_of_lt apply le_of_lt
apply h₃ε { re := y.re, im := x } apply h₃ε { re := y.re, im := x }
simp simp
have : { re := y.re, im := x } = (x : ℂ) := by
rfl calc Complex.abs { re := y.re, im := x }
rw [this] _ ≤ |y.re| + |x| := by
rw [Complex.abs_ofReal] apply Complex.abs_le_abs_re_add_abs_im { re := y.re, im := x }
exact h₁x _ ≤ 2 * ε := 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‖ 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 _ ≤ ‖(∫ (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
@ -282,14 +311,19 @@ theorem primitive_fderivAtBasepoint
simp simp
rw [norm_smul] rw [norm_smul]
simp simp
_ ≤ (c / (4 : ℝ)) * |y.re - 0| + ‖∫ (x : ℝ) in (0)..(y.im), f { re := y.re, im := x } - f 0‖ := by _ ≤ (c / (4 : ℝ)) * |y.re - 0| + (c / (4 : ℝ)) * |y.im - 0| := by
apply add_le_add apply add_le_add
exact t₁ exact t₁
rfl exact t₂
_ ≤ c * ‖y‖ := by sorry _ ≤ (c / (4 : ℝ)) * (|y.re| + |y.im|) := by
simp
rw [mul_add]
sorry _ ≤ c * ‖y‖ := by
apply mul_le_mul
apply div_le_self
exact le_of_lt hc
linarith
sorry
theorem primitive_additivity theorem primitive_additivity