noncomputable def indicatorFunction {n : ℕ} (C : Set (Fin n → ℝ)) : (Fin n → ℝ) → EReal

Defintion 4.8.1: For a set C ⊆ ℝ^n, the indicator function δ(· | C) is 0 on C and +∞ outside C.

Equations

• indicatorFunction C x = if x ∈ C then 0 else ⊤

theorem indicatorFunction_lt_top_iff_mem {n : ℕ} {C : Set (Fin n → ℝ)} {x : Fin n → ℝ} : indicatorFunction C x < ⊤ ↔ x ∈ C

The indicator function is finite exactly on the set.

theorem effectiveDomain_indicatorFunction_eq {n : ℕ} (C : Set (Fin n → ℝ)) : effectiveDomain Set.univ (indicatorFunction C) = C

The effective domain of the indicator function is the original set.

theorem convexFunction_indicator_of_convex {n : ℕ} {C : Set (Fin n → ℝ)} (hC : Convex ℝ C) : ConvexFunction (indicatorFunction C)

The indicator function of a convex set is convex.

theorem convex_iff_convexFunction_indicatorFunction {n : ℕ} (C : Set (Fin n → ℝ)) : Convex ℝ C ↔ ConvexFunction (indicatorFunction C)

Remark 4.8.1: The epigraph of the indicator function is a half-cylinder with cross-section C. Clearly C is a convex set iff δ(· | C) is a convex function on ℝ^n.

noncomputable def supportFunction {n : ℕ} (C : Set (Fin n → ℝ)) : (Fin n → ℝ) → ℝ

Defintion 4.8.2: The support function delta*(· | C) of a convex set C in R^n is defined by delta*(x | C) = sup {dotProduct x y | y ∈ C}.

Equations

• supportFunction C x = sSup {r : ℝ | ∃ y ∈ C, r = x ⬝ᵥ y}

noncomputable def gaugeFunction {n : ℕ} (C : Set (Fin n → ℝ)) : (Fin n → ℝ) → ℝ

Defintion 4.8.2: The gauge gamma(· | C) is defined by gamma(x | C) = inf {lambda >= 0 | x ∈ lambda C}, for C ≠ ∅.

Equations

• gaugeFunction C x = sInf {r : ℝ | 0 ≤ r ∧ ∃ y ∈ C, x = r • y}

noncomputable def distanceFunction {n : ℕ} (C : Set (Fin n → ℝ)) : (Fin n → ℝ) → ℝ

Defintion 4.8.3: The (Euclidean) distance function d(·, C) is defined by d(x, C) = inf { |x - y| | y ∈ C }.

Equations

• distanceFunction C x = Metric.infDist x C