theorem infimalConvolution_eq_sInf_epigraph_add {n : ℕ} (f1 f2 : (Fin n → ℝ) → EReal) (x : Fin n → ℝ) : infimalConvolution f1 f2 x = sInf {z : EReal | ∃ (x1 : Fin n → ℝ) (x2 : Fin n → ℝ), x1 + x2 = x ∧ z = f1 x1 + f2 x2}

Text 5.4.1.6: For any functions f_1 and f_2 from R^n to [-infty, +infty] (not necessarily convex nor proper), (f_1 □ f_2)(x) can be defined directly in terms of addition of epigraphs: (f_1 □ f_2)(x) = inf { μ | (x, μ) ∈ (epi f_1 + epi f_2) }.

noncomputable def rightScalarMultiple {n : ℕ} (f : (Fin n → ℝ) → EReal) (lam : ℝ) : (Fin n → ℝ) → EReal

Text 5.4.2: Let f : R^n → R ∪ {+infty} be convex and lam ∈ [0, +infty). Define the right scalar multiple f lam to be the convex function obtained from Theorem 5.3 by taking F = lam (epi f) ⊆ R^{n+1}.

Equations

• rightScalarMultiple f lam x = sInf ((fun (μ : ℝ) => ↑μ) '' {μ : ℝ | (x, μ) ∈ (fun (p : (Fin n → ℝ) × ℝ) => lam • p) '' epigraph Set.univ f})

theorem mem_image_smul_epigraph_iff {n : ℕ} {f : (Fin n → ℝ) → EReal} {lam : ℝ} (hlam : 0 < lam) {x : Fin n → ℝ} {μ : ℝ} : (x, μ) ∈ (fun (p : (Fin n → ℝ) × ℝ) => lam • p) '' epigraph Set.univ f ↔ f (lam⁻¹ • x) ≤ ↑(μ / lam)

Membership in the scaled epigraph fiber for positive scaling.

theorem sInf_image_real_univ : sInf ((fun (μ : ℝ) => ↑μ) '' Set.univ) = ⊥

The infimum of all real coercions in EReal is ⊥.

theorem sInf_fiber_smul_eq {n : ℕ} {f : (Fin n → ℝ) → EReal} {lam : ℝ} (hlam : 0 < lam) (x : Fin n → ℝ) : sInf ((fun (μ : ℝ) => ↑μ) '' {μ : ℝ | (x, μ) ∈ (fun (p : (Fin n → ℝ) × ℝ) => lam • p) '' epigraph Set.univ f}) = ↑lam * f (lam⁻¹ • x)

The infimum over a scaled epigraph fiber equals the scaled value of f.

theorem image_zero_smul_epigraph_eq_singleton {n : ℕ} {f : (Fin n → ℝ) → EReal} (hne : (epigraph Set.univ f).Nonempty) : (fun (p : (Fin n → ℝ) × ℝ) => 0 • p) '' epigraph Set.univ f = {0}

The zero scaling of a nonempty epigraph is the singleton {(0,0)}.

theorem rightScalarMultiple_zero_eval {n : ℕ} {f : (Fin n → ℝ) → EReal} (hne : (epigraph Set.univ f).Nonempty) (x : Fin n → ℝ) : rightScalarMultiple f 0 x = if x = 0 then 0 else ⊤

Evaluate the zero scalar multiple when the epigraph is nonempty.

theorem rightScalarMultiple_pos {n : ℕ} {f : (Fin n → ℝ) → EReal} {lam : ℝ} (_hf : ConvexFunctionOn Set.univ f) (hlam : 0 < lam) (x : Fin n → ℝ) : rightScalarMultiple f lam x = ↑lam * f (lam⁻¹ • x)

Text 5.4.3 (i): Let f be convex on ℝ^n. If λ > 0, then for all x, (f λ)(x) = λ f (λ^{-1} x).

theorem rightScalarMultiple_zero_eq_indicator {n : ℕ} {f : (Fin n → ℝ) → EReal} (_hf : ConvexFunctionOn Set.univ f) (hfinite : ∃ (x : Fin n → ℝ), f x ≠ ⊤) : rightScalarMultiple f 0 = indicatorFunction {0}

Text 5.4.3 (ii): Let f be convex on ℝ^n. If λ = 0 and f is not identically +∞, then for all x, (f 0)(x) = δ(x | 0). (Trivially, if f ≡ +∞ then f 0 = f.)

theorem positivelyHomogeneous_iff {n : ℕ} {f : (Fin n → ℝ) → EReal} : PositivelyHomogeneous f ↔ ∀ (x : Fin n → ℝ) (α : ℝ), 0 < α → f (α • x) = ↑α * f x

Text 5.4.4: A function f : ℝ^n → ℝ ∪ {+∞} is positively homogeneous if f (α x) = α f x for all x and all α > 0.

theorem smul_inv_smul_simplify {n : ℕ} {lam : ℝ} {x : Fin n → ℝ} (hne : lam ≠ 0) : lam⁻¹ • lam • x = x

Simplify lam⁻¹ • (lam • x) when lam ≠ 0.

theorem rightScalarMultiple_eq_self_of_posHom {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ConvexFunctionOn Set.univ f) (hpos : PositivelyHomogeneous f) (lam : ℝ) : 0 < lam → rightScalarMultiple f lam = f

If f is positively homogeneous, all positive right scalar multiples equal f.

theorem posHom_of_rightScalarMultiple_eq_self {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ConvexFunctionOn Set.univ f) (hscale : ∀ (lam : ℝ), 0 < lam → rightScalarMultiple f lam = f) : PositivelyHomogeneous f

If every positive right scalar multiple equals f, then f is positively homogeneous.

theorem positivelyHomogeneous_iff_rightScalarMultiple_eq {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ConvexFunctionOn Set.univ f) : PositivelyHomogeneous f ↔ ∀ (lam : ℝ), 0 < lam → rightScalarMultiple f lam = f

Text 5.4.5 (Characterization via right scalar multiplication): A convex function f is positively homogeneous if and only if f λ = f for every λ > 0, where f λ denotes the right scalar multiple.

def convexConeGeneratedEpigraph {n : ℕ} (h : (Fin n → ℝ) → EReal) : Set ((Fin n → ℝ) × ℝ)

Text 5.4.6 (Cone generated by an epigraph): Let h : ℝ^n → ℝ ∪ {+∞} be convex. The convex cone generated by epi h is the smallest convex cone F ⊆ ℝ^{n+1} containing epi h. Equivalently, F = cone (epi h) := conv ({0} ∪ ⋃_{λ > 0} λ • (epi h)).

Equations

• convexConeGeneratedEpigraph h = Set.insert 0 ↑(ConvexCone.hull ℝ (epigraph Set.univ h))

noncomputable def positivelyHomogeneousConvexFunctionGenerated {n : ℕ} (h : (Fin n → ℝ) → EReal) : (Fin n → ℝ) → EReal

Text 5.4.7 (Positively homogeneous convex function generated by h): Let h : ℝ^n → ℝ ∪ {+∞} be convex and let F = cone (epi h) ⊆ ℝ^{n+1}. Define f x = inf { μ | (x, μ) ∈ F } (as in Theorem 5.3). The function f is called the positively homogeneous convex function generated by h.

Equations

• positivelyHomogeneousConvexFunctionGenerated h x = sInf ((fun (μ : ℝ) => ↑μ) '' {μ : ℝ | (x, μ) ∈ convexConeGeneratedEpigraph h})

theorem smul_mem_convexConeGeneratedEpigraph {n : ℕ} {h : (Fin n → ℝ) → EReal} {t : ℝ} (ht : 0 < t) {p : (Fin n → ℝ) × ℝ} : p ∈ convexConeGeneratedEpigraph h → t • p ∈ convexConeGeneratedEpigraph h

The generated epigraph is closed under positive scaling.

theorem add_mem_convexConeGeneratedEpigraph {n : ℕ} {h : (Fin n → ℝ) → EReal} {p q : (Fin n → ℝ) × ℝ} : p ∈ convexConeGeneratedEpigraph h → q ∈ convexConeGeneratedEpigraph h → p + q ∈ convexConeGeneratedEpigraph h

The generated epigraph is closed under addition.

def convexCone_generatedEpigraph {n : ℕ} (h : (Fin n → ℝ) → EReal) : ConvexCone ℝ ((Fin n → ℝ) × ℝ)

The generated epigraph forms a convex cone.

Equations

• convexCone_generatedEpigraph h = { carrier := convexConeGeneratedEpigraph h, smul_mem' := ⋯, add_mem' := ⋯ }

theorem ereal_mul_le_mul_of_pos_left_general {t : ℝ} (ht : 0 < t) {x y : EReal} (h : x ≤ y) : ↑t * x ≤ ↑t * y

Multiplying by a positive real preserves order in EReal.

theorem ereal_mul_inv_smul {t : ℝ} (ht : 0 < t) (x : EReal) : ↑t * ((↑t)⁻¹ * x) = x

Positive scaling by t and t⁻¹ cancels on EReal.

theorem sInf_image_real_smul {S : Set ℝ} {t : ℝ} (ht : 0 < t) : sInf ((fun (μ : ℝ) => ↑μ) '' (t • S)) = ↑t * sInf ((fun (μ : ℝ) => ↑μ) '' S)

Scaling a real set scales the infimum of its EReal image.

theorem posHom_of_inf_section_of_cone {n : ℕ} {F : Set ((Fin n → ℝ) × ℝ)} (hcone : ∀ (t : ℝ), 0 < t → (fun (p : (Fin n → ℝ) × ℝ) => t • p) '' F ⊆ F) : PositivelyHomogeneous fun (x : Fin n → ℝ) => sInf ((fun (μ : ℝ) => ↑μ) '' {μ : ℝ | (x, μ) ∈ F})

The inf-section of a set closed under positive scaling is positively homogeneous.

theorem add_mem_epigraph_of_posHom_convex {n : ℕ} {f : (Fin n → ℝ) → EReal} (hpos : PositivelyHomogeneous f) (hconv : ConvexFunctionOn Set.univ f) {p q : (Fin n → ℝ) × ℝ} (hp : p ∈ epigraph Set.univ f) (hq : q ∈ epigraph Set.univ f) : p + q ∈ epigraph Set.univ f

The epigraph of a convex positively homogeneous function is closed under addition.

def convexCone_epigraph_of_posHom_convex {n : ℕ} {f : (Fin n → ℝ) → EReal} (hpos : PositivelyHomogeneous f) (hconv : ConvexFunctionOn Set.univ f) : ConvexCone ℝ ((Fin n → ℝ) × ℝ)

The epigraph of a convex positively homogeneous function is a convex cone.

Equations

• convexCone_epigraph_of_posHom_convex hpos hconv = { carrier := epigraph Set.univ f, smul_mem' := ⋯, add_mem' := ⋯ }

theorem le_of_epigraph_subset_inf_section {n : ℕ} {h : (Fin n → ℝ) → EReal} {F : Set ((Fin n → ℝ) × ℝ)} (hF : epigraph Set.univ h ⊆ F) : (fun (x : Fin n → ℝ) => sInf ((fun (μ : ℝ) => ↑μ) '' {μ : ℝ | (x, μ) ∈ F})) ≤ h

If epigraph h ⊆ F, then the inf-section of F is dominated by h.

theorem cone_minimality_epigraph_u {n : ℕ} {h u : (Fin n → ℝ) → EReal} (hu_pos : PositivelyHomogeneous u) (hu_conv : ConvexFunctionOn Set.univ u) (hu0 : u 0 ≤ 0) (hu_le : u ≤ h) : convexConeGeneratedEpigraph h ⊆ epigraph Set.univ u

Minimality of the generated cone inside any epigraph majorant.

theorem maximality_posHomogeneousHull {n : ℕ} {h : (Fin n → ℝ) → EReal} (_hh : ConvexFunctionOn Set.univ h) : have f := positivelyHomogeneousConvexFunctionGenerated h; (∃ (C : ConvexCone ℝ ((Fin n → ℝ) × ℝ)), ↑C = epigraph Set.univ f ∧ 0 ∈ epigraph Set.univ f) ∧ (ConvexFunctionOn Set.univ f ∧ PositivelyHomogeneous f ∧ f 0 ≤ 0 ∧ f ≤ h) ∧ ∀ (u : (Fin n → ℝ) → EReal), PositivelyHomogeneous u → ConvexFunctionOn Set.univ u → u 0 ≤ 0 → u ≤ h → u ≤ f

Text 5.4.8 (Maximality of the positively homogeneous hull): Let h be convex on ℝ^n, and let f be the positively homogeneous convex function generated by h. Then: (i) epi f is a convex cone in ℝ^{n+1} containing the origin. (ii) f is convex and positively homogeneous, and satisfies f(0) ≤ 0 and f ≤ h. (iii) (Greatest such minorant) If u is any positively homogeneous convex function with u(0) ≤ 0 and u ≤ h, then u ≤ f.

theorem mem_convexConeGeneratedEpigraph_iff {n : ℕ} {h : (Fin n → ℝ) → EReal} (hh : ConvexFunctionOn Set.univ h) {p : (Fin n → ℝ) × ℝ} : p ∈ convexConeGeneratedEpigraph h ↔ p = 0 ∨ ∃ (lam : ℝ), 0 < lam ∧ p ∈ (fun (q : (Fin n → ℝ) × ℝ) => lam • q) '' epigraph Set.univ h

Membership in the generated cone is either zero or a positive scaling of the epigraph, for convex h.

theorem rightScalarMultiple_set_eq_insert {n : ℕ} {h : (Fin n → ℝ) → EReal} (x : Fin n → ℝ) : {z : EReal | ∃ (lam : ℝ), 0 ≤ lam ∧ z = rightScalarMultiple h lam x} = Set.insert (rightScalarMultiple h 0 x) {z : EReal | ∃ (lam : ℝ), 0 < lam ∧ z = rightScalarMultiple h lam x}

The λ ≥ 0 right-scalar-multiple values are obtained by inserting the λ = 0 value.

theorem sInf_rightScalarMultiple_pos_le_zero {n : ℕ} {h : (Fin n → ℝ) → EReal} (hh : ConvexFunctionOn Set.univ h) (h0 : h 0 < ⊤) : sInf {z : EReal | ∃ (lam : ℝ), 0 < lam ∧ z = rightScalarMultiple h lam 0} ≤ 0

If h 0 < ⊤, then the infimum of positive right scalar multiples at 0 is ≤ 0.