norm_two_pi_i_inv_smul_integral_le_of_norm_le_const

English

The norm of (2π i)^{-1} times the circle integral is at most R·C, under the usual hypotheses about f on the circle.

Русский

Норма $ (2\\pi i)^{-1} \\cdot$ кругового интеграла не превосходит $R C$ при обычных предположениях о f на окружности.

LaTeX

$$$\\| (2\\pi i)^{-1} \\oint z in C(c,R) f(z)\\| \\le R C$ under appropriate conditions on f.$$

Lean4

theorem norm_two_pi_i_inv_smul_integral_le_of_norm_le_const {f : ℂ → E} {c : ℂ} {R C : ℝ} (hR : 0 ≤ R)
    (hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C) : ‖(2 * π * I : ℂ)⁻¹ • ∮ z in C(c, R), f z‖ ≤ R * C :=
  by
  have : ‖(2 * π * I : ℂ)⁻¹‖ = (2 * π)⁻¹ := by simp [Real.pi_pos.le]
  rw [norm_smul, this, ← div_eq_inv_mul, div_le_iff₀ Real.two_pi_pos, mul_comm (R * C), ← mul_assoc]
  exact norm_integral_le_of_norm_le_const hR hf

Похожие утверждения