norm_integral_le_of_norm_le_const

English

Under similar hypotheses as above, the bound remains valid with the usual absolute value appearing as |R| in place of R, since |R| = R when R ≥ 0.

Русский

При аналогичных условиях верхняя граница сохраняется, поскольку |R|=R при R≥0.

LaTeX

$$$\\|\\oint z in C(c,R), f z\\| \\le 2\\pi\\,|R|\\,C$ and hence equals $2\\pi R C$ when R≥0.$$

Lean4

theorem norm_integral_le_of_norm_le_const {f : ℂ → E} {c : ℂ} {R C : ℝ} (hR : 0 ≤ R)
    (hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C) : ‖∮ z in C(c, R), f z‖ ≤ 2 * π * R * C :=
  have : |R| = R := abs_of_nonneg hR
  calc
    ‖∮ z in C(c, R), f z‖ ≤ 2 * π * |R| * C := norm_integral_le_of_norm_le_const' <| by rwa [this]
    _ = 2 * π * R * C := by rw [this]

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