English
The radius of convergence of the Cauchy power series is bounded below by R; in particular, as a function of R, the radius satisfies ↑R ≤ radius of cauchyPowerSeries f c R.
Русский
Радиус сходимости ряда Коши имеет нижнюю границу, равную R; радиус ряда не меньше R.
LaTeX
$$$$ \\uparrow R \\le \\operatorname{radius} \\big( cauchyPowerSeries\\ f\\ c\\ R \\big). $$$$
Lean4
theorem norm_cauchyPowerSeries_le (f : ℂ → E) (c : ℂ) (R : ℝ) (n : ℕ) :
‖cauchyPowerSeries f c R n‖ ≤ ((2 * π)⁻¹ * ∫ θ : ℝ in 0..2 * π, ‖f (circleMap c R θ)‖) * |R|⁻¹ ^ n :=
calc
‖cauchyPowerSeries f c R n‖
_ = (2 * π)⁻¹ * ‖∮ z in C(c, R), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z‖ := by
simp [cauchyPowerSeries, norm_smul, Real.pi_pos.le]
_ ≤
(2 * π)⁻¹ *
∫ θ in 0..2 * π,
‖deriv (circleMap c R) θ • (circleMap c R θ - c)⁻¹ ^ n • (circleMap c R θ - c)⁻¹ • f (circleMap c R θ)‖ :=
(mul_le_mul_of_nonneg_left (intervalIntegral.norm_integral_le_integral_norm Real.two_pi_pos.le)
(by simp [Real.pi_pos.le]))
_ = (2 * π)⁻¹ * (|R|⁻¹ ^ n * (|R| * (|R|⁻¹ * ∫ x : ℝ in 0..2 * π, ‖f (circleMap c R x)‖))) := by
simp [norm_smul, mul_left_comm |R|]
_ ≤ ((2 * π)⁻¹ * ∫ θ : ℝ in 0..2 * π, ‖f (circleMap c R θ)‖) * |R|⁻¹ ^ n :=
by
rcases eq_or_ne R 0 with (rfl | hR)
· cases n <;> simp [-mul_inv_rev]
· rw [mul_inv_cancel_left₀, mul_assoc, mul_comm (|R|⁻¹ ^ n)]
rwa [Ne, _root_.abs_eq_zero]
