theorem epigraph_polarConvex_subset_vertReflect_preimage_polarSetProd_epigraph {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf_nonneg : ∀ (x : Fin n → ℝ), 0 ≤ f x) : epigraph Set.univ (polarConvex f) ⊆ vertReflect ⁻¹' polarSetProd (epigraph Set.univ f)

Epigraph points of the polar map to the product polar via vertical reflection.

theorem vertReflect_preimage_polarSetProd_epigraph_subset_epigraph_polarConvex {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf_nonneg : ∀ (x : Fin n → ℝ), 0 ≤ f x) (hf0 : f 0 = 0) : vertReflect ⁻¹' polarSetProd (epigraph Set.univ f) ⊆ epigraph Set.univ (polarConvex f)

Reflected product-polar points are in the epigraph of the polar.

theorem epigraph_polarConvex_mem_iff_vertReflect_mem_polarSetProd_epigraph {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf_nonneg : ∀ (x : Fin n → ℝ), 0 ≤ f x) (hf0 : f 0 = 0) (p : (Fin n → ℝ) × ℝ) : p ∈ epigraph Set.univ (polarConvex f) ↔ vertReflect p ∈ polarSetProd (epigraph Set.univ f)

Epigraph identity for the polar convex function.

theorem epigraph_bipolar_polarConvex_eq_closure_epigraph {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf_conv : ConvexFunctionOn Set.univ f) (hf_nonneg : ∀ (x : Fin n → ℝ), 0 ≤ f x) (hf0 : f 0 = 0) : epigraph Set.univ (polarConvex (polarConvex f)) = closure (epigraph Set.univ f)

Bipolar epigraph of the polar convex function.

theorem polarConvex_nonneg_closedConvex_and_bipolar_eq_convexFunctionClosure {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf_conv : ConvexFunctionOn Set.univ f) (hf_nonneg : ∀ (x : Fin n → ℝ), 0 ≤ f x) (hf0 : f 0 = 0) : have fPolar := polarConvex f; (∀ (xStar : Fin n → ℝ), 0 ≤ fPolar xStar) ∧ ClosedConvexFunction fPolar ∧ fPolar 0 = 0 ∧ polarConvex fPolar = convexFunctionClosure f

theorem convexFunctionOn_univ_of_closedConvexFunction {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf_closed : ClosedConvexFunction f) : ConvexFunctionOn Set.univ f

A closed convex function is convex on univ.

theorem polarConvex_mem_subtype_nonneg_closedConvex_zero {n : ℕ} (f : { g : (Fin n → ℝ) → EReal // (∀ (x : Fin n → ℝ), 0 ≤ g x) ∧ ClosedConvexFunction g ∧ g 0 = 0 }) : (∀ (x : Fin n → ℝ), 0 ≤ polarConvex (↑f) x) ∧ ClosedConvexFunction (polarConvex ↑f) ∧ polarConvex (↑f) 0 = 0

polarConvex preserves nonnegativity, closed convexity, and vanishing at 0 on the subtype.

theorem polarConvex_involutive_on_subtype {n : ℕ} (f : { g : (Fin n → ℝ) → EReal // (∀ (x : Fin n → ℝ), 0 ≤ g x) ∧ ClosedConvexFunction g ∧ g 0 = 0 }) : polarConvex (polarConvex ↑f) = ↑f

polarConvex is involutive on the nonnegative closed convex subclass with f 0 = 0.