theorem section16_fenchelConjugate_norm_sub_eq_indicator_add_dot {n : ℕ} (a : Fin n → ℝ) : (fenchelConjugate n fun (x : Fin n → ℝ) => ↑‖x - a‖) = fun (xStar : Fin n → ℝ) => (if l1Norm xStar ≤ 1 then 0 else ⊤) + ↑(a ⬝ᵥ xStar)

The conjugate of x ↦ ‖x - a‖ is the unit-ball indicator plus a linear term.

theorem section16_properConvexFunctionOn_norm_sub {n : ℕ} (a : Fin n → ℝ) : ProperConvexFunctionOn Set.univ fun (x : Fin n → ℝ) => ↑‖x - a‖

Translating the norm preserves proper convexity on Set.univ.

theorem section16_closure_effectiveDomain_norm_sub_eq_univ {n : ℕ} (a : Fin n → ℝ) : closure (effectiveDomain Set.univ fun (x : Fin n → ℝ) => ↑‖x - a‖) = Set.univ

The effective domain of x ↦ ‖x - a‖ is all of ℝ^n.

theorem section16_fenchelConjugate_sSup_norm_sub_points_eq_sInf {n m : ℕ} (a : Fin m → Fin n → ℝ) (hm : 0 < m) : have f := fun (x : Fin n → ℝ) => sSup (Set.range fun (i : Fin m) => ↑‖x - a i‖); ∀ (xStar : Fin n → ℝ), have S := {r : EReal | ∃ (lam : Fin m → ℝ) (xStar_i : Fin m → Fin n → ℝ), (∀ (i : Fin m), 0 ≤ lam i) ∧ ∑ i : Fin m, lam i = 1 ∧ ∑ i : Fin m, lam i • xStar_i i = xStar ∧ (∀ (i : Fin m), l1Norm (xStar_i i) ≤ 1) ∧ r = ↑(∑ i : Fin m, lam i * a i ⬝ᵥ xStar_i i)}; fenchelConjugate n f xStar = sInf S ∧ (S.Nonempty → ∃ r ∈ S, sInf S = r)

Text 16.5.1: Let f(x) = max { ‖x - aᵢ‖ | i = 1, …, m }, where a₁, …, aₘ ∈ ℝⁿ.

For each x⋆, the conjugate f⋆(x⋆) is the minimum of

λ₁ ⟪a₁, x₁⋆⟫ + ⋯ + λₘ ⟪aₘ, xₘ⋆⟫

over all xᵢ⋆ and λᵢ satisfying

• λ₁ x₁⋆ + ⋯ + λₘ xₘ⋆ = x⋆,
• ‖xᵢ⋆‖ ≤ 1,
• λᵢ ≥ 0 and λ₁ + ⋯ + λₘ = 1.