PoleCoefficientBounds.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import Mathlib.Analysis.Complex.Liouville
6 import Mathlib.Analysis.Asymptotics.Defs
7 
8 namespace Komorebi.PaperIV
9 noncomputable section
10 open Set Filter Metric Asymptotics
11 open scoped Topology
12 
13 def analyticTaylorCoefficient (f : ℂ → ℂ) (n : ℕ) : ℂ :=
14   iteratedDeriv n f 0 / (n.factorial : ℂ)
15 
16 /-- The exact Cauchy bound after conversion to ordinary Taylor coefficients. -/
17 theorem analyticTaylorCoefficient_norm_le {f : ℂ → ℂ} {R C : ℝ}
18     (hR : 0 < R) (hf : DiffContOnCl ℂ f (ball 0 R))
19     (hC : ∀ z ∈ sphere 0 R, ‖f z‖ ≤ C) (n : ℕ) :
20     ‖analyticTaylorCoefficient f n‖ ≤ C / R ^ n := by
21   have h := Complex.norm_iteratedDeriv_le_of_forall_mem_sphere_norm_le n hR hf hC
22   rw [analyticTaylorCoefficient, norm_div, Complex.norm_natCast]
23   apply (div_le_iff₀ (by positivity : (0 : ℝ) < n.factorial)).mpr
24   simpa only [div_eq_mul_inv, mul_assoc, mul_comm, mul_left_comm] using h
25 
26 /-- Cauchy's estimate supplies the exponential remainder in the nearest-pole
27 expansion once the principal parts have been removed holomorphically. -/
28 theorem analyticTaylorCoefficient_isBigO {f : ℂ → ℂ} {R : ℝ}
29     (hR : 0 < R) (hf : DiffContOnCl ℂ f (ball 0 R)) :
30     (fun n : ℕ => analyticTaylorCoefficient f n) =O[atTop] (fun n => R⁻¹ ^ n) := by
31   have hc : ContinuousOn f (sphere 0 R) :=
32     hf.continuousOn.mono (by simpa only [closure_ball (0 : ℂ) hR.ne'] using! (sphere_subset_closedBall : sphere (0 : ℂ) R ⊆ closedBall 0 R))
33   obtain ⟨C, hC⟩ := (isCompact_sphere (0 : ℂ) R).bddAbove_image hc.norm
34   apply IsBigO.of_bound C
35   apply Eventually.of_forall
36   intro n
37   have hb : ∀ z ∈ sphere (0 : ℂ) R, ‖f z‖ ≤ C := by
38     intro z hz
39     exact hC (mem_image_of_mem (fun z => ‖f z‖) hz)
40   simpa only [norm_pow, Real.norm_eq_abs, abs_inv, abs_of_pos hR, ← inv_pow, div_eq_mul_inv] using
41     analyticTaylorCoefficient_norm_le hR hf hb n
42 
43 /-- Factorial rescaling and the block subsequence preserve the required error
44 bound, including the exact `(N*n)!` normalization of the manuscript. -/
45 theorem analyticTaylorCoefficient_block_error {f : ℂ → ℂ} {R C : ℝ}
46     (hR : 0 < R) (hf : DiffContOnCl ℂ f (ball 0 R))
47     (hC : ∀ z ∈ sphere 0 R, ‖f z‖ ≤ C) (N n : ℕ) :
48     ‖((N * n).factorial : ℂ) * analyticTaylorCoefficient f (N * n)‖ ≤
49       C * ((N * n).factorial : ℝ) * R⁻¹ ^ (N * n) := by
50   rw [norm_mul, Complex.norm_natCast]
51   have h := mul_le_mul_of_nonneg_left (analyticTaylorCoefficient_norm_le hR hf hC (N * n))
52     (show (0 : ℝ) ≤ (N * n).factorial by positivity)
53   simpa only [div_eq_mul_inv, inv_pow, mul_assoc, mul_comm, mul_left_comm] using h
54 
55 end
56 end Komorebi.PaperIV

Back to source controls