English
The operator norm of the nth coefficient of the Cauchy power series is bounded by a constant times the average norm of f over the circle, scaled by |R|^{-n}.
Русский
Норма-независимый предел коэффициента ряда ограничен константой, зависящей от среднеквадратичного значения f по окружности, умноженной на |R|^{-n}.
LaTeX
$$$$ \\| cauchyPowerSeries\\ f\\ c\\ R\\ n \\| \\le (2\\pi)^{-1} \\Big( \\int_0^{2\\pi} \\| f( circleMap\\ c\\ R\\ \\theta) \\| \\, d\\theta \\Big) \\cdot |R|^{-n}. $$$$
Lean4
theorem le_radius_cauchyPowerSeries (f : ℂ → E) (c : ℂ) (R : ℝ≥0) : ↑R ≤ (cauchyPowerSeries f c R).radius :=
by
refine
(cauchyPowerSeries f c R).le_radius_of_bound ((2 * π)⁻¹ * ∫ θ : ℝ in 0..2 * π, ‖f (circleMap c R θ)‖) fun n => ?_
refine (mul_le_mul_of_nonneg_right (norm_cauchyPowerSeries_le _ _ _ _) (pow_nonneg R.coe_nonneg _)).trans ?_
rw [abs_of_nonneg R.coe_nonneg]
rcases eq_or_ne (R ^ n : ℝ) 0 with hR | hR
· rw_mod_cast [hR, mul_zero]
exact
mul_nonneg (inv_nonneg.2 Real.two_pi_pos.le)
(intervalIntegral.integral_nonneg Real.two_pi_pos.le fun _ _ => norm_nonneg _)
· rw [inv_pow]
have : (R : ℝ) ^ n ≠ 0 := by norm_cast at hR ⊢
rw [inv_mul_cancel_right₀ this]
