theorem normConjugate_eq_zero_of_norm_le_one {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {y : StrongDual ℝ E} (hy : ‖y‖ ≤ 1) : conjugate_function (fun (x : E) => ↑‖x‖) ↑y = 0

Helper for Proposition 4.18: if ‖y‖ ≤ 1, then the defining supremum for the conjugate of x ↦ ‖x‖ is bounded above by 0 and attained at x = 0.

theorem exists_eval_sub_norm_pos_of_one_lt_norm {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {y : StrongDual ℝ E} (hy : 1 < ‖y‖) : ∃ (x : E), 0 < y x - ‖x‖

Helper for Proposition 4.18: if ‖y‖ > 1, then some vector gives a positive gap y x - ‖x‖.

theorem normConjugateIntegrand_natSmul {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] (y : StrongDual ℝ E) (x : E) (n : ℕ) : ↑(y (↑n • x)) - ↑‖↑n • x‖ = ↑(↑n * (y x - ‖x‖))

Helper for Proposition 4.18: along the ray ((n : ℝ) • x), the conjugate integrand is the real scalar n * (y x - ‖x‖) viewed in EReal.

theorem normConjugate_eq_top_of_one_lt_norm {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {y : StrongDual ℝ E} (hy : 1 < ‖y‖) : conjugate_function (fun (x : E) => ↑‖x‖) ↑y = ⊤

Helper for Proposition 4.18: if ‖y‖ > 1, then the defining supremum for the conjugate of x ↦ ‖x‖ is unbounded above and therefore equals ⊤.

theorem norm_conjugate_eq_extendedIndicator_closedBall {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] : (fun (y : StrongDual ℝ E) => conjugate_function (fun (x : E) => ↑‖x‖) ↑y) = δ_ (Metric.closedBall 0 1)

Proposition 4.18: the Fenchel conjugate of the norm x ↦ ‖x‖ is the extended-real-valued indicator of the closed unit ball in the dual space.

theorem norm_conjugate_apply_eq_extendedIndicator_closedBall {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] (y : StrongDual ℝ E) : conjugate_function (fun (x : E) => ↑‖x‖) ↑y = (δ_ (Metric.closedBall 0 1)) y

Pointwise form of Proposition 4.18 on the continuous-dual bridge from conjugate_function.

theorem norm_conjugate_eq_if_norm_le_one {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] (y : StrongDual ℝ E) : conjugate_function (fun (x : E) => ↑‖x‖) ↑y = if ‖y‖ ≤ 1 then 0 else ⊤

The conjugate of the norm is 0 on the dual closed unit ball and ∞ outside it.