theorem section16_fenchelConjugate_convexFunctionClosure_eq {n : ℕ} (g : (Fin n → ℝ) → EReal) : fenchelConjugate n (convexFunctionClosure g) = fenchelConjugate n g

Taking the convex-function closure does not change the Fenchel conjugate.

theorem section16_closedConvexFunction_fenchelConjugate {n : ℕ} (g : (Fin n → ℝ) → EReal) : ClosedConvexFunction (fenchelConjugate n g)

The Fenchel conjugate is closed and convex.

theorem section16_recessionFunction_fenchelConjugate_proper_posHom {n : ℕ} (f : (Fin n → ℝ) → EReal) (hf : ProperConvexFunctionOn Set.univ f) : ProperConvexFunctionOn Set.univ (recessionFunction (fenchelConjugate n f)) ∧ PositivelyHomogeneous (recessionFunction (fenchelConjugate n f))

The recession function of a Fenchel conjugate is proper and positively homogeneous.

theorem section16_recessionCone_epigraph_eq_epigraph_recessionFunction_fenchelConjugate {n : ℕ} (f : (Fin n → ℝ) → EReal) (hf : ProperConvexFunctionOn Set.univ f) : (epigraph Set.univ (fenchelConjugate n f)).recessionCone = epigraph Set.univ (recessionFunction (fenchelConjugate n f))

The epigraph recession cone of a Fenchel conjugate is the epigraph of its recession function.

theorem section16_infimalConvolutionFamily_fenchelConjugate_closed_and_attained_of_nonempty_iInter_ri {n m : ℕ} (f : Fin m → (Fin n → ℝ) → EReal) (hf : ∀ (i : Fin m), ProperConvexFunctionOn Set.univ (f i)) (hri : (⋂ (i : Fin m), euclideanRelativeInterior n ((fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' effectiveDomain Set.univ (f i))).Nonempty) : (convexFunctionClosure (infimalConvolutionFamily fun (i : Fin m) => fenchelConjugate n (f i)) = infimalConvolutionFamily fun (i : Fin m) => fenchelConjugate n (f i)) ∧ ∀ (xStar : Fin n → ℝ), infimalConvolutionFamily (fun (i : Fin m) => fenchelConjugate n (f i)) xStar = ⊤ ∨ ∃ (xStarFamily : Fin m → Fin n → ℝ), ∑ i : Fin m, xStarFamily i = xStar ∧ ∑ i : Fin m, fenchelConjugate n (f i) (xStarFamily i) = infimalConvolutionFamily (fun (i : Fin m) => fenchelConjugate n (f i)) xStar

Closedness and attainment for the infimal convolution of conjugates under the ri condition.