English
If f is bounded by C on the circle, then the norm of the circle integral is at most 2π|R|C.
Русский
Если функция f ограничена на окружности нормой ≤ C, то нормa кругового интеграла не превосходит 2π|R|C.
LaTeX
$$$\\|\\oint z in C(c,R), f(z)\\| \\le 2\\pi\\,|R|\\,C$ given $\\forall z\\in sphere c|R|,\\; \\|f(z)\\| \\le C$$$
Lean4
theorem norm_integral_le_of_norm_le_const' {f : ℂ → E} {c : ℂ} {R C : ℝ} (hf : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ C) :
‖∮ z in C(c, R), f z‖ ≤ 2 * π * |R| * C :=
calc
‖∮ z in C(c, R), f z‖ ≤ |R| * C * |2 * π - 0| :=
intervalIntegral.norm_integral_le_of_norm_le_const fun θ _ =>
calc
‖deriv (circleMap c R) θ • f (circleMap c R θ)‖ = |R| * ‖f (circleMap c R θ)‖ := by simp [norm_smul]
_ ≤ |R| * C := mul_le_mul_of_nonneg_left (hf _ <| circleMap_mem_sphere' _ _ _) (abs_nonneg _)
_ = 2 * π * |R| * C := by rw [sub_zero, _root_.abs_of_pos Real.two_pi_pos]; ac_rfl
