theorem
sInf_rightScalarMultiple_indicator_add_one_eq_gauge
{n : ℕ}
{C : Set (Fin n → ℝ)}
(hCne : C.Nonempty)
(hCconv : Convex ℝ C)
(hCabs : ∀ (x : Fin n → ℝ), ∃ (lam : ℝ), 0 ≤ lam ∧ x ∈ (fun (y : Fin n → ℝ) => lam • y) '' C)
(x : Fin n → ℝ)
:
The sInf of right scalar multiples of indicatorFunction C + 1 matches the gauge.
theorem
gauge_posHomogeneousHull_indicator_add_one
{n : ℕ}
{C : Set (Fin n → ℝ)}
(hCne : C.Nonempty)
(hCconv : Convex ℝ C)
(hCabs : ∀ (x : Fin n → ℝ), ∃ (lam : ℝ), 0 ≤ lam ∧ x ∈ (fun (y : Fin n → ℝ) => lam • y) '' C)
:
have h := fun (x : Fin n → ℝ) => indicatorFunction C x + 1;
(∀ (lam : ℝ),
0 ≤ lam →
∀ (x : Fin n → ℝ),
rightScalarMultiple h lam x = indicatorFunction ((fun (y : Fin n → ℝ) => lam • y) '' C) x + ↑lam) ∧ ∀ (x : Fin n → ℝ), sInf {z : EReal | ∃ (lam : ℝ), 0 ≤ lam ∧ z = rightScalarMultiple h lam x} = ↑(gaugeOfConvexSet C x)
Text 5.4.11 (Gauge as a positively homogeneous hull): Let C ⊆ ℝ^n be nonempty and convex,
and assume every x is contained in some nonnegative scaling of C. Define h(x)=δ(x|C)+1.
Then for λ ≥ 0, (h λ)(x)=δ(x|λ C)+λ, and the positively homogeneous convex function
generated by h equals the gauge:
inf { (h λ)(x) | λ ≥ 0 } = inf { λ ≥ 0 | x ∈ λ C } = γ(x|C).
theorem
convexFunctionOn_iSup
{n : ℕ}
{ι : Sort u_1}
{f : ι → (Fin n → ℝ) → EReal}
(hf : ∀ (i : ι), ConvexFunctionOn Set.univ (f i))
:
ConvexFunctionOn Set.univ fun (x : Fin n → ℝ) => ⨆ (i : ι), f i x
Theorem 5.5: The pointwise supremum of an arbitrary collection of convex functions is convex.