theorem polarGauge_bipolar_eq_kCl {n : ℕ} {k : (Fin n → ℝ) → EReal} (hk : IsGauge k) : have kCl := fun (x : Fin n → ℝ) => sInf {μ : EReal | ∃ (r : ℝ), μ = ↑r ∧ (x, r) ∈ closure (epigraph Set.univ k)}; polarGauge (polarGauge k) = kCl

The bipolar of a gauge equals the epigraph-closure infimum.

theorem polarGauge_isGauge_isClosed_and_bipolar_eq_closure_epigraph {n : ℕ} {k : (Fin n → ℝ) → EReal} (hk : IsGauge k) : have kPolar := polarGauge k; have kCl := fun (x : Fin n → ℝ) => sInf {μ : EReal | ∃ (r : ℝ), μ = ↑r ∧ (x, r) ∈ closure (epigraph Set.univ k)}; IsGauge kPolar ∧ IsClosed (epigraph Set.univ kPolar) ∧ polarGauge kPolar = kCl ∧ ∀ (C : Set (Fin n → ℝ)), C.Nonempty → Convex ℝ C → (∀ (x : Fin n → ℝ), ∃ (r : ℝ), 0 ≤ r ∧ ∃ y ∈ C, x = r • y) → (k = fun (x : Fin n → ℝ) => ↑(gaugeFunction C x)) → kPolar = supportFunctionEReal C

Theorem 15.1: If k is a gauge function, then its polar k^∘ is a closed gauge function and k^{∘∘} = cl k. Moreover, if k = γ(· | C) for some nonempty convex set C ⊆ ℝ^n that is absorbing, then k^∘ agrees with the support function of C.

In this development, k^∘ is polarGauge k; "closed" is expressed as IsClosed (epigraph univ ·); and cl k is modeled as the extended-real function whose epigraph is the topological closure of epigraph univ k.

theorem epigraphClosureInf_eq_of_isGauge_isClosed_epigraph {n : ℕ} {k : (Fin n → ℝ) → EReal} (hk : IsGauge k) (hclosed : IsClosed (epigraph Set.univ k)) : epigraphClosureInf k = k

A gauge with closed epigraph equals its epigraph-closure infimum.

theorem polarGauge_involutive_of_isGauge_isClosed_epigraph {n : ℕ} {k : (Fin n → ℝ) → EReal} (hk : IsGauge k) (hclosed : IsClosed (epigraph Set.univ k)) : polarGauge (polarGauge k) = k

Closed gauges are fixed by double polarity.

theorem polarGauge_mapsTo_closedGauges {n : ℕ} {k : (Fin n → ℝ) → EReal} : IsGauge k ∧ IsClosed (epigraph Set.univ k) → IsGauge (polarGauge k) ∧ IsClosed (epigraph Set.univ (polarGauge k))

The polar gauge of a closed gauge is again a closed gauge.

theorem polarGauge_bijOn_closedGauges {n : ℕ} : Set.BijOn (fun (k : (Fin n → ℝ) → EReal) => polarGauge k) {k : (Fin n → ℝ) → EReal | IsGauge k ∧ IsClosed (epigraph Set.univ k)} {k : (Fin n → ℝ) → EReal | IsGauge k ∧ IsClosed (epigraph Set.univ k)}

Corollary 15.1.1: The polarity mapping k ↦ k^∘ induces a one-to-one symmetric correspondence on the class of all closed gauges on ℝⁿ. Two closed convex sets containing the origin are polar to each other if and only if their gauge functions are polar to each other.

theorem supportFunctionEReal_sublevel_one_eq_polarSet {n : ℕ} {C : Set (Fin n → ℝ)} : {xStar : Fin n → ℝ | supportFunctionEReal C xStar ≤ 1} = {xStar : Fin n → ℝ | ∀ x ∈ C, x ⬝ᵥ xStar ≤ 1}

The polar set is the ≤ 1 sublevel set of the support function.

theorem polarGauge_gaugeFunction_eq_supportFunctionEReal {n : ℕ} {C : Set (Fin n → ℝ)} (hCne : C.Nonempty) (hCabs : ∀ (x : Fin n → ℝ), ∃ (lam : ℝ), 0 ≤ lam ∧ x ∈ (fun (y : Fin n → ℝ) => lam • y) '' C) : (polarGauge fun (x : Fin n → ℝ) => ↑(gaugeFunction C x)) = supportFunctionEReal C

The polar gauge of a gauge-function equals the support function under absorbing.

theorem supportFunctionEReal_le_gaugeFunction_of_polarSet {n : ℕ} {C D : Set (Fin n → ℝ)} (hDabs : ∀ (x : Fin n → ℝ), ∃ (lam : ℝ), 0 ≤ lam ∧ x ∈ (fun (y : Fin n → ℝ) => lam • y) '' D) (hD : D = {xStar : Fin n → ℝ | ∀ x ∈ C, x ⬝ᵥ xStar ≤ 1}) (xStar : Fin n → ℝ) : supportFunctionEReal C xStar ≤ ↑(gaugeFunction D xStar)

The support function is bounded above by the gauge of a polar set.

theorem supportFunctionEReal_eq_gaugeFunction_of_polarSet {n : ℕ} {C D : Set (Fin n → ℝ)} (hC0 : 0 ∈ C) (hCabs : ∀ (x : Fin n → ℝ), ∃ (lam : ℝ), 0 ≤ lam ∧ x ∈ (fun (y : Fin n → ℝ) => lam • y) '' C) (hDabs : ∀ (x : Fin n → ℝ), ∃ (lam : ℝ), 0 ≤ lam ∧ x ∈ (fun (y : Fin n → ℝ) => lam • y) '' D) (hD : D = {xStar : Fin n → ℝ | ∀ x ∈ C, x ⬝ᵥ xStar ≤ 1}) : supportFunctionEReal C = fun (xStar : Fin n → ℝ) => ↑(gaugeFunction D xStar)

The support function of a polar set agrees with the corresponding gauge function.

theorem closed_convex_sets_polar_iff_gaugeFunctions_polar {n : ℕ} {C D : Set (Fin n → ℝ)} (hC_closed : IsClosed C) (hC_conv : Convex ℝ C) (hC0 : 0 ∈ C) (hCabs : ∀ (x : Fin n → ℝ), ∃ (lam : ℝ), 0 ≤ lam ∧ x ∈ (fun (y : Fin n → ℝ) => lam • y) '' C) (hD_closed : IsClosed D) (hD_conv : Convex ℝ D) (hD0 : 0 ∈ D) (hDabs : ∀ (x : Fin n → ℝ), ∃ (lam : ℝ), 0 ≤ lam ∧ x ∈ (fun (y : Fin n → ℝ) => lam • y) '' D) : D = {xStar : Fin n → ℝ | ∀ x ∈ C, x ⬝ᵥ xStar ≤ 1} ∧ C = {x : Fin n → ℝ | ∀ xStar ∈ D, x ⬝ᵥ xStar ≤ 1} ↔ ((polarGauge fun (x : Fin n → ℝ) => ↑(gaugeFunction C x)) = fun (xStar : Fin n → ℝ) => ↑(gaugeFunction D xStar)) ∧ (polarGauge fun (xStar : Fin n → ℝ) => ↑(gaugeFunction D xStar)) = fun (x : Fin n → ℝ) => ↑(gaugeFunction C x)

Corollary 15.1.1 (sets version): Two closed convex absorbing sets containing the origin are polar to each other if and only if their gauge functions are polar to each other.