theorem hzero_two {n : ℕ} {f1_0_plus f2_0_plus : (Fin n → ℝ) → EReal} (hpos : ∀ (z : Fin n → ℝ), z ≠ 0 → f1_0_plus z + f2_0_plus (-z) > 0) (z : Fin 2 → Fin n → ℝ) : ∑ i : Fin 2, (if i = 0 then f1_0_plus else f2_0_plus) (z i) ≤ 0 → ∑ i : Fin 2, (if i = 0 then f1_0_plus else f2_0_plus) (-z i) > 0 → ∑ i : Fin 2, z i ≠ 0

In the two-function case, the zero-sum condition in the family corollary follows from the positivity hypothesis on f1_0_plus and f2_0_plus.

theorem extract_two_attainer {n : ℕ} {f1 f2 : (Fin n → ℝ) → EReal} {x : Fin n → ℝ} {x' : Fin 2 → Fin n → ℝ} (hsum : ∑ i : Fin 2, x' i = x) : ∑ i : Fin 2, (if i = 0 then f1 else f2) (x' i) = f1 (x - x' 1) + f2 (x' 1)

For Fin 2, a decomposition x = x' 0 + x' 1 rewrites the sum over the family into the binary form.

theorem infimalConvolution_closed_proper_convex_recession {n : ℕ} {f1 f2 f1_0_plus f2_0_plus : (Fin n → ℝ) → EReal} (hclosed1 : ClosedConvexFunction f1) (hclosed2 : ClosedConvexFunction f2) (hproper1 : ProperConvexFunctionOn Set.univ f1) (hproper2 : ProperConvexFunctionOn Set.univ f2) (hpos : ∀ (z : Fin n → ℝ), z ≠ 0 → f1_0_plus z + f2_0_plus (-z) > 0) (hrec1 : (epigraph Set.univ f1).recessionCone = epigraph Set.univ f1_0_plus) (hrec2 : (epigraph Set.univ f2).recessionCone = epigraph Set.univ f2_0_plus) (hpos1 : PositivelyHomogeneous f1_0_plus) (hpos2 : PositivelyHomogeneous f2_0_plus) (hproper0_1 : ProperConvexFunctionOn Set.univ f1_0_plus) (hproper0_2 : ProperConvexFunctionOn Set.univ f2_0_plus) : ClosedConvexFunction (infimalConvolution f1 f2) ∧ ProperConvexFunctionOn Set.univ (infimalConvolution f1 f2) ∧ ∀ (x : Fin n → ℝ), ∃ (y : Fin n → ℝ), infimalConvolution f1 f2 x = f1 (x - y) + f2 y

Corollary 9.2.2. Let f1 and f2 be closed proper convex functions on ℝ^n such that (f1 0+)(z) + (f2 0+)(-z) > 0 for all z ≠ 0. Then infimalConvolution f1 f2 is a closed proper convex function, and for each x the infimum in (f1 square f2)(x) = inf_y { f1 (x - y) + f2 y } is attained by some y.

theorem infimalConvolution_indicator_neg_eq_sInf_translate {n : ℕ} {f : (Fin n → ℝ) → EReal} {C : Set (Fin n → ℝ)} (hproper : ProperConvexFunctionOn Set.univ f) (x : Fin n → ℝ) : infimalConvolution (indicatorFunction (-C)) f x = sInf {z : EReal | ∃ y ∈ (fun (c : Fin n → ℝ) => c + x) '' C, z = f y}

Rewrite the infimal convolution with an indicator as an infimum over the translate.

theorem closedConvexFunction_indicator_neg {n : ℕ} {C : Set (Fin n → ℝ)} (hCne : C.Nonempty) (hCclosed : IsClosed C) (hCconvex : Convex ℝ C) : ClosedConvexFunction (indicatorFunction (-C)) ∧ ProperConvexFunctionOn Set.univ (indicatorFunction (-C))

The indicator of a closed convex nonempty set is closed and proper.

theorem recessionCone_smul_pos_fin {n : ℕ} {C : Set (Fin n → ℝ)} {y : Fin n → ℝ} (hy : y ∈ C.recessionCone) {t : ℝ} (ht : 0 < t) : t • y ∈ C.recessionCone

Positive scaling preserves membership in the recession cone.

theorem recessionCone_convex_fin {n : ℕ} {C : Set (Fin n → ℝ)} (hCconvex : Convex ℝ C) : Convex ℝ C.recessionCone

The recession cone of a convex set is convex (finite-dimensional version).

theorem indicator_recession_posHom_proper {n : ℕ} {C : Set (Fin n → ℝ)} (hCconvex : Convex ℝ C) : PositivelyHomogeneous (indicatorFunction (-C.recessionCone)) ∧ ProperConvexFunctionOn Set.univ (indicatorFunction (-C.recessionCone))

The indicator of the recession cone is positively homogeneous and proper.

theorem recessionCone_epigraph_indicator_neg {n : ℕ} {C : Set (Fin n → ℝ)} (hCne : C.Nonempty) : (epigraph Set.univ (indicatorFunction (-C))).recessionCone = epigraph Set.univ (indicatorFunction (-C.recessionCone))

The recession cone of the indicator epigraph is the epigraph of the recession indicator.

theorem indicator_recession_hpos_from_noCommon {n : ℕ} {f0_plus : (Fin n → ℝ) → EReal} {C : Set (Fin n → ℝ)} (hproper0 : ProperConvexFunctionOn Set.univ f0_plus) (hnoCommon : ∀ (z : Fin n → ℝ), z ≠ 0 → (EuclideanSpace.equiv (Fin n) ℝ).symm z ∈ (⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' C).recessionCone → f0_plus z > 0) (z : Fin n → ℝ) : z ≠ 0 → indicatorFunction (-C.recessionCone) z + f0_plus (-z) > 0

Positivity from a recession-direction separation hypothesis.

theorem infimalConvolution_indicator_neg_example {n : ℕ} {f f0_plus : (Fin n → ℝ) → EReal} {C : Set (Fin n → ℝ)} (hclosed : ClosedConvexFunction f) (hproper : ProperConvexFunctionOn Set.univ f) (hrec2 : (epigraph Set.univ f).recessionCone = epigraph Set.univ f0_plus) (hpos2 : PositivelyHomogeneous f0_plus) (hproper0_2 : ProperConvexFunctionOn Set.univ f0_plus) (hCne : C.Nonempty) (hCclosed : IsClosed C) (hCconvex : Convex ℝ C) (hnoCommon : ∀ (z : Fin n → ℝ), z ≠ 0 → (EuclideanSpace.equiv (Fin n) ℝ).symm z ∈ (⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' C).recessionCone → f0_plus z > 0) : (infimalConvolution (indicatorFunction (-C)) f = fun (x : Fin n → ℝ) => sInf {z : EReal | ∃ y ∈ (fun (c : Fin n → ℝ) => c + x) '' C, z = f y}) ∧ ClosedConvexFunction (infimalConvolution (indicatorFunction (-C)) f) ∧ ∀ (x : Fin n → ℝ), ∃ y ∈ (fun (c : Fin n → ℝ) => c + x) '' C, infimalConvolution (indicatorFunction (-C)) f x = f y

Example 9.2.2.2. For f = f₂ closed proper convex and f₁ the indicator function of -C with C nonempty closed convex, (f₁ □ f)(x) = inf { δ(x - y | -C) + f(y) | y ∈ ℝ^n } and equals inf { f(y) | y ∈ (C + x) }. If f and C have no common direction of recession, then the infimum over the translate C + x is attained for each x, and the resulting function of x is lower semicontinuous and convex.

def coordinatewiseInfSet {n : ℕ} (f : (Fin n → ℝ) → EReal) (x : Fin n → ℝ) : Set EReal

The set of values of f above a point x in the coordinatewise order.

Equations

• coordinatewiseInfSet f x = {z : EReal | ∃ (y : Fin n → ℝ), x ≤ y ∧ z = f y}

theorem coordinatewiseInfSet_mono {n : ℕ} {f : (Fin n → ℝ) → EReal} {x x' : Fin n → ℝ} (hxx' : x ≤ x') : coordinatewiseInfSet f x' ⊆ coordinatewiseInfSet f x

A larger base point yields a smaller coordinatewise infimum set.

theorem coordinatewiseInf_le_self {n : ℕ} {f : (Fin n → ℝ) → EReal} (x : Fin n → ℝ) : sInf (coordinatewiseInfSet f x) ≤ f x

The coordinatewise infimum is bounded above by f.

theorem coordinatewiseInf_monotone {n : ℕ} {f : (Fin n → ℝ) → EReal} : Monotone fun (x : Fin n → ℝ) => sInf (coordinatewiseInfSet f x)

The coordinatewise infimum is monotone.

theorem coordinatewiseInf_greatest {n : ℕ} {f h : (Fin n → ℝ) → EReal} (hle : ∀ (x : Fin n → ℝ), h x ≤ f x) (hmono : Monotone h) (x : Fin n → ℝ) : h x ≤ sInf (coordinatewiseInfSet f x)

Any monotone minorant of f lies below the coordinatewise infimum.

theorem nonnegOrthant_closed_convex_nonempty {n : ℕ} : (Set.Ici 0).Nonempty ∧ IsClosed (Set.Ici 0) ∧ Convex ℝ (Set.Ici 0)

The non-negative orthant is nonempty, closed, and convex.

theorem image_add_nonnegOrthant_eq_ge {n : ℕ} (x : Fin n → ℝ) : (fun (c : Fin n → ℝ) => c + x) '' Set.Ici 0 = {y : Fin n → ℝ | x ≤ y}

Translating the non-negative orthant by x gives the coordinatewise upper set.

theorem recessionCone_nonnegOrthant_subset {n : ℕ} : (Set.Ici 0).recessionCone ⊆ Set.Ici 0

The recession cone of the non-negative orthant lies in the orthant.

theorem hnoCommon_of_hnoNonneg {n : ℕ} {f0_plus : (Fin n → ℝ) → EReal} (hnoNonneg : ∀ (z : Fin n → ℝ), z ≠ 0 → (∀ (i : Fin n), 0 ≤ z i) → f0_plus z > 0) (z : Fin n → ℝ) : z ≠ 0 → (EuclideanSpace.equiv (Fin n) ℝ).symm z ∈ (⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' Set.Ici 0).recessionCone → f0_plus z > 0

Nonnegative recession directions yield the no-common-recession hypothesis.

theorem coordinatewiseInfSet_eq_translate {n : ℕ} {f : (Fin n → ℝ) → EReal} (x : Fin n → ℝ) : coordinatewiseInfSet f x = {z : EReal | ∃ y ∈ (fun (c : Fin n → ℝ) => c + x) '' Set.Ici 0, z = f y}

The coordinatewise infimum set is the translate-based infimum set.

theorem coordinatewiseInfimum_closed_proper_convex {n : ℕ} {f f0_plus : (Fin n → ℝ) → EReal} (hclosed : ClosedConvexFunction f) (hproper : ProperConvexFunctionOn Set.univ f) (hrec2 : (epigraph Set.univ f).recessionCone = epigraph Set.univ f0_plus) (hpos2 : PositivelyHomogeneous f0_plus) (hproper0_2 : ProperConvexFunctionOn Set.univ f0_plus) (hnoNonneg : ∀ (z : Fin n → ℝ), z ≠ 0 → (∀ (i : Fin n), 0 ≤ z i) → f0_plus z > 0) : have g := fun (x : Fin n → ℝ) => sInf (coordinatewiseInfSet f x); ClosedConvexFunction g ∧ ProperConvexFunctionOn Set.univ g ∧ (∀ (x : Fin n → ℝ), ∃ (y : Fin n → ℝ), x ≤ y ∧ g x = f y) ∧ (∀ (x : Fin n → ℝ), g x ≤ f x) ∧ Monotone g ∧ ∀ (h : (Fin n → ℝ) → EReal), (∀ (x : Fin n → ℝ), h x ≤ f x) → Monotone h → ∀ (x : Fin n → ℝ), h x ≤ g x

Example 9.2.2.3. Taking C to be the non-negative orthant of ℝ^n, we have C + x = { y | y ≥ x } for each x. If f is a closed proper convex function on ℝ^n whose recession cone contains no non-negative non-zero vectors, then the infimum in g(x) = inf { f(y) | y ≥ x } is attained for each x, and g is a closed proper convex function. Moreover, g is the greatest function with g ≤ f and g coordinatewise non-decreasing.

theorem finset_sum_ne_bot_of_forall {α : Type u_1} (s : Finset α) (f : α → EReal) (h : ∀ a ∈ s, f a ≠ ⊥) : s.sum f ≠ ⊥

Non-⊥ is preserved by finite sums.

theorem finset_sum_ne_top_of_forall {α : Type u_1} (s : Finset α) (f : α → EReal) (h : ∀ a ∈ s, f a ≠ ⊤) : s.sum f ≠ ⊤

Non-⊤ is preserved by finite sums.

theorem effectiveDomain_sum_eq_iInter_univ {n m : ℕ} {f : Fin m → (Fin n → ℝ) → EReal} (hnotbot : ∀ (i : Fin m) (x : Fin n → ℝ), f i x ≠ ⊥) : (effectiveDomain Set.univ fun (x : Fin n → ℝ) => ∑ i : Fin m, f i x) = ⋂ (i : Fin m), effectiveDomain Set.univ (f i)

The effective domain of a finite sum is the intersection of the effective domains, assuming no summand takes the value ⊥.