English
If f is bounded by C on the circle and the circle integral is taken, then the norm of the integral is bounded by 2π R C.
Русский
Если f ограничена на окружности нормой ≤ C, то норма интеграла не превышает 2πRC.
LaTeX
$$$\\|\\oint z in C(c,R), f z\\| \\le 2\\pi\\,R\\,C$$$
Lean4
/-- If `f` is continuous on the circle `|z - c| = R`, `R > 0`, the `‖f z‖` is less than or equal to
`C : ℝ` on this circle, and this norm is strictly less than `C` at some point `z` of the circle,
then `‖∮ z in C(c, R), f z‖ < 2 * π * R * C`. -/
theorem norm_integral_lt_of_norm_le_const_of_lt {f : ℂ → E} {c : ℂ} {R C : ℝ} (hR : 0 < R)
(hc : ContinuousOn f (sphere c R)) (hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C) (hlt : ∃ z ∈ sphere c R, ‖f z‖ < C) :
‖∮ z in C(c, R), f z‖ < 2 * π * R * C :=
by
rw [← _root_.abs_of_pos hR, ← image_circleMap_Ioc] at hlt
rcases hlt with ⟨_, ⟨θ₀, hmem, rfl⟩, hlt⟩
calc
‖∮ z in C(c, R), f z‖ ≤ ∫ θ in 0..2 * π, ‖deriv (circleMap c R) θ • f (circleMap c R θ)‖ :=
intervalIntegral.norm_integral_le_integral_norm Real.two_pi_pos.le
_ < ∫ _ in 0..2 * π, R * C :=
by
simp only [deriv_circleMap, norm_smul, norm_mul, norm_circleMap_zero, abs_of_pos hR, norm_I, mul_one]
refine
intervalIntegral.integral_lt_integral_of_continuousOn_of_le_of_exists_lt Real.two_pi_pos ?_ continuousOn_const
(fun θ _ => ?_) ⟨θ₀, Ioc_subset_Icc_self hmem, ?_⟩
·
exact
continuousOn_const.mul
(hc.comp (continuous_circleMap _ _).continuousOn fun θ _ => circleMap_mem_sphere _ hR.le _).norm
· exact mul_le_mul_of_nonneg_left (hf _ <| circleMap_mem_sphere _ hR.le _) hR.le
· gcongr
_ = 2 * π * R * C := by simp [mul_assoc]; ring
