English
There exists a bound controlling the norm of circleTransformBoundingFunction on a compact set of w-values.
Русский
Существует ограничение на норму circleTransformBoundingFunction на компактном множестве значений w.
LaTeX
$$$$ \\exists x,\\forall y\\ that\\|circleTransformBoundingFunction(R,z,y)\\| \\le \\|circleTransformBoundingFunction(R,z,x)\\|. $$$$
Lean4
theorem norm_circleTransformBoundingFunction_le {R r : ℝ} (hr : r < R) (hr' : 0 ≤ r) (z : ℂ) :
∃ x : closedBall z r ×ˢ [[0, 2 * π]],
∀ y : closedBall z r ×ˢ [[0, 2 * π]],
‖circleTransformBoundingFunction R z y‖ ≤ ‖circleTransformBoundingFunction R z x‖ :=
by
have cts := continuousOn_norm_circleTransformBoundingFunction hr z
have comp : IsCompact (closedBall z r ×ˢ [[0, 2 * π]]) := by
apply_rules [IsCompact.prod, ProperSpace.isCompact_closedBall z r, isCompact_uIcc]
have none : (closedBall z r ×ˢ [[0, 2 * π]]).Nonempty := (nonempty_closedBall.2 hr').prod nonempty_uIcc
have := IsCompact.exists_isMaxOn comp none (cts.mono <| prod_mono_right (subset_univ _))
simpa [isMaxOn_iff] using this
