theorem
support_function_unit_ball_eq_dualNorm
{E : Type u}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
(y : Module.Dual ℝ E)
:
Example 2.9 (1): the support function of the closed unit ball of a normed space is the dual norm.
theorem
support_function_lp_unit_ball_eq_conjugate_lp_norm
{n : ℕ}
{p q : ENNReal}
(hpq : p.HolderConjugate q)
(y : Fin n → ℝ)
:
(σ_ {x : Fin n → ℝ | ‖WithLp.toLp p x‖ ≤ 1}) ((dotProductBilin ℝ ℝ) y) = ↑‖WithLp.toLp q y‖
Example 2.9 (2): in ℝ^n with the l_p norm, the support function of the closed unit ball is
the conjugate l_q norm.
theorem
support_function_posDef_unit_ball_eq_sqrt_dotProduct_inv_mulVec
{n : ℕ}
(Q : Matrix (Fin n) (Fin n) ℝ)
(hQ : Q.PosDef)
(y : Fin n → ℝ)
:
Example 2.9 (3): for the norm induced by a positive definite matrix Q, the support function
of the closed unit ball is the Q⁻¹-norm, written here as √(yᵀ Q⁻¹ y).