theorem
epigraph_polarGauge_eq_preimage_innerDualCone_H2
{n : ℕ}
{k : (Fin n → ℝ) → EReal}
(hk : IsGauge k)
(xStar : Fin n → ℝ)
(μ : ℝ)
:
(xStar, μ) ∈ epigraph Set.univ (polarGauge k) ↔ let E₂ := EuclideanSpace ℝ (Fin n);
let H₂ := WithLp 2 (E₂ × ℝ);
have eH := eH_transport_to_H2 n;
have σ₂ := fun (p : H₂) => WithLp.toLp 2 (-p.ofLp.1, p.ofLp.2);
have S₂ := ⇑eH.symm '' epigraph Set.univ k;
σ₂ (eH.symm (xStar, μ)) ∈ ↑(ProperCone.innerDual S₂)
Epigraph of the polar gauge as a sign-flipped inner-dual cone in H₂.