English
There exists a bound B such that for all w within ball around c of radius r<R, the norm of circleTransformBoundingFunction is bounded by B.
Русский
Существует предел B, такой что для всех w внутри ball(c,r) с r<R, нормa circleTransformBoundingFunction не превосходит B.
LaTeX
$$$$ \\exists B, \\exists \\varepsilon>0,\\ \\forall y\\in \\text{ball}(x,\\varepsilon),\\ \\|\\text{circleTransformBoundingFunction}(R,z,y)\\| \\le B. $$$$
Lean4
theorem continuousOn_norm_circleTransformBoundingFunction {R r : ℝ} (hr : r < R) (z : ℂ) :
ContinuousOn ((‖·‖) ∘ circleTransformBoundingFunction R z) (closedBall z r ×ˢ univ) :=
by
have : ContinuousOn (circleTransformBoundingFunction R z) (closedBall z r ×ˢ univ) :=
by
apply_rules [ContinuousOn.smul, continuousOn_const]
· simp only [deriv_circleMap]
apply_rules [ContinuousOn.mul, (continuous_circleMap 0 R).comp_continuousOn continuousOn_snd, continuousOn_const]
· simpa only [inv_pow] using continuousOn_prod_circle_transform_function hr
exact this.norm
