From 7e6fc7bacdb2473efd9bbc9d1ef3939c2e9a78f3 Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Tue, 18 Jun 2024 11:21:58 +0200 Subject: [PATCH] Update holomorphic.primitive.lean --- Nevanlinna/holomorphic.primitive.lean | 104 +++++++++++++++++++------- 1 file changed, 79 insertions(+), 25 deletions(-) diff --git a/Nevanlinna/holomorphic.primitive.lean b/Nevanlinna/holomorphic.primitive.lean index c18e1af..7619a12 100644 --- a/Nevanlinna/holomorphic.primitive.lean +++ b/Nevanlinna/holomorphic.primitive.lean @@ -175,7 +175,7 @@ theorem primitive_lem1 -theorem primitive_fderivAtBasepoint +theorem primitive_fderivAtBasepointZero {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] (f : ℂ → E) (hf : Continuous f) : @@ -187,7 +187,7 @@ theorem primitive_fderivAtBasepoint rw [Asymptotics.isLittleO_iff] intro c hc - have {z : ℂ} {e : E} : z • e = (∫ (x : ℝ) in (0)..(z.re), e) + Complex.I • ∫ (x : ℝ) in (0)..(z.im), e:= by + 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] @@ -204,10 +204,46 @@ theorem primitive_fderivAtBasepoint 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 sorry - have t₁ {r : ℝ} :IntervalIntegrable (fun x => f 0) MeasureTheory.volume 0 r := by sorry - have t₂ {a b : ℝ}: IntervalIntegrable (fun x_1 => f { re := a, im := x_1 }) MeasureTheory.volume 0 b := by sorry - have t₃ {a : ℝ} : IntervalIntegrable (fun x => f 0) MeasureTheory.volume 0 a := by sorry + 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 @@ -232,24 +268,25 @@ theorem primitive_fderivAtBasepoint intro y hy apply mem_ball_iff_norm.mp (h₂ε hy) - use Metric.ball 0 ε + use Metric.ball 0 (ε / (4 : ℝ)) constructor - · exact Metric.ball_mem_nhds 0 h₁ε + · apply Metric.ball_mem_nhds 0 + linarith · intro y hy - have h₁y : |y.re| < ε := by + have h₁y : |y.re| < ε / 4 := by calc |y.re| _ ≤ Complex.abs y := by apply Complex.abs_re_le_abs - _ < ε := by + _ < ε / 4 := by let A := mem_ball_iff_norm.1 hy simp at A - assumption - have h₂y : |y.im| < ε := by + linarith + have h₂y : |y.im| < ε / 4 := by calc |y.im| _ ≤ Complex.abs y := by apply Complex.abs_im_le_abs - _ < ε := by + _ < ε / 4 := by let A := mem_ball_iff_norm.1 hy simp at A - assumption + linarith have intervalComputation {x' y' : ℝ} (h : x' ∈ Ι 0 y') : |x'| ≤ |y'| := by let A := h.1 @@ -271,10 +308,10 @@ theorem primitive_fderivAtBasepoint apply intervalIntegral.norm_integral_le_of_norm_le_const intro x hx - have h₁x : |x| < ε := by + have h₁x : |x| < ε / 4 := by calc |x| _ ≤ |y.re| := intervalComputation hx - _ < ε := h₁y + _ < ε / 4 := h₁y apply le_of_lt apply h₃ε { re := x, im := 0 } rw [mem_ball_iff_norm] @@ -282,17 +319,16 @@ theorem primitive_fderivAtBasepoint have : { re := x, im := 0 } = (x : ℂ) := by rfl rw [this] rw [Complex.abs_ofReal] - exact h₁x - + 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| < ε := by + have h₁x : |x| < ε / 4 := by calc |x| _ ≤ |y.im| := intervalComputation hx - _ < ε := h₂y + _ < ε / 4 := h₂y apply le_of_lt apply h₃ε { re := y.re, im := x } @@ -301,7 +337,7 @@ theorem primitive_fderivAtBasepoint 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 } - _ ≤ 2 * ε := by + _ < ε := 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‖ @@ -318,12 +354,30 @@ theorem primitive_fderivAtBasepoint _ ≤ (c / (4 : ℝ)) * (|y.re| + |y.im|) := by simp rw [mul_add] - _ ≤ c * ‖y‖ := by + _ ≤ (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 - apply div_le_self - exact le_of_lt hc + rfl + exact this + apply add_nonneg + apply abs_nonneg + apply abs_nonneg + linarith + _ ≤ c * ‖y‖ := by linarith - sorry theorem primitive_additivity