English
The polar of a closed ball equals the closed ball of inverse radius: polar(ClosedBall(0,r)) = ClosedBall(0, r^{-1}).
Русский
Поляр замкнутого шара равна замкнутому шару с обратным радиусом: polar(замкнутый шар) = замкнутый шар радиуса 1/r.
LaTeX
$$$\\operatorname{polar}(0, r) = \\overline{B}^*(0, r^{-1})$$$
Lean4
/-- The `polar` of closed ball in a normed space `E` is the closed ball of the dual with inverse
radius. -/
theorem polar_closedBall {𝕜 E : Type*} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {r : ℝ} (hr : 0 < r) :
StrongDual.polar 𝕜 (closedBall (0 : E) r) = closedBall (0 : StrongDual 𝕜 E) r⁻¹ :=
by
refine Subset.antisymm ?_ (closedBall_inv_subset_polar_closedBall 𝕜)
intro x' h
simp only [mem_closedBall_zero_iff]
refine ContinuousLinearMap.opNorm_le_of_ball hr (inv_nonneg.mpr hr.le) fun z _ => ?_
simpa only [one_div] using LinearMap.bound_of_ball_bound' hr 1 x'.toLinearMap h z
