theorem exists_unit_apply_gt_of_lt_norm {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : StrongDual ℝ E} {L : NNReal} (hLt : ↑L < ‖s‖) : ∃ (u : E), ‖u‖ = 1 ∧ ↑L < s u

Helper for Proposition 6.1: if a continuous dual vector has norm strictly larger than L, then some unit vector evaluates strictly larger than L under that functional.

theorem fenchel_maximand_nat_smul_lower_bound {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : E → ℝ) (L : NNReal) (hgrowth : ∀ (x : E), f x ≤ f 0 + ↑L * ‖x‖) {s : StrongDual ℝ E} {u : E} (hu : ‖u‖ = 1) (n : ℕ) : ↑n * (s u - ↑L) - f 0 ≤ s (↑n • u) - f (↑n • u)

Helper for Proposition 6.1: along a unit ray, the Fenchel maximand is bounded below by the linear function with slope s u - L.

theorem strongFenchelConjugate_eq_top_of_unit_apply_gt_radius {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : E → ℝ) (L : NNReal) (hgrowth : ∀ (x : E), f x ≤ f 0 + ↑L * ‖x‖) {s : StrongDual ℝ E} {u : E} (hu : ‖u‖ = 1) (hsu : ↑L < s u) : strongFenchelConjugate f s = ⊤

Helper for Proposition 6.1: if some unit vector evaluates above the radius L, then the continuous-dual Fenchel conjugate is infinite at that functional.

theorem dom_fenchelConjugate_subset_closedBall_of_upper_linear_growth {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : E → ℝ) (L : NNReal) (hgrowth : ∀ (x : E), f x ≤ f 0 + ↑L * ‖x‖) : extendedRealEffectiveDomain (strongFenchelConjugate f) ⊆ Metric.closedBall 0 ↑L

Proposition 6.1: if a real-valued function is bounded above by f 0 + L ‖x‖, then the finite-value domain of its Fenchel conjugate on the continuous dual is contained in the closed dual ball of radius L.

theorem dom_fenchelConjugate_bounded_of_upper_linear_growth {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : E → ℝ) (L : NNReal) (hgrowth : ∀ (x : E), f x ≤ f 0 + ↑L * ‖x‖) : Bornology.IsBounded (extendedRealEffectiveDomain (strongFenchelConjugate f))

The finite-value domain of the conjugate is bounded under the same upper linear-growth hypothesis.