theorem polarSetProd_bipolar_eq_closure_of_convex_zeroMem {n : ℕ} (C : Set ((Fin n → ℝ) × ℝ)) (hCconv : Convex ℝ C) (hC0 : 0 ∈ C) : polarSetProd (polarSetProd C) = closure C

Bipolarity for polarSetProd, using the closed convex bipolar theorem.

theorem hbot_of_nonneg {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf_nonneg : ∀ (x : Fin n → ℝ), 0 ≤ f x) (x : Fin n → ℝ) : f x ≠ ⊥

Nonnegativity rules out the value ⊥.

theorem mu_nonneg_of_vertReflect_mem_polarSetProd_epigraph {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf0 : f 0 = 0) {xStar : Fin n → ℝ} {μ : ℝ} (hmem : vertReflect (xStar, μ) ∈ polarSetProd (epigraph Set.univ f)) : 0 ≤ μ

If a reflected point lies in the polar of the epigraph and f 0 = 0, then the height is nonnegative.