theorem recessionFunction_diff_le_sup {n : ℕ} {f : (Fin n → ℝ) → ℝ} {f0_plus : (Fin n → ℝ) → EReal} (hf0_plus : ∀ (y : Fin n → ℝ), f0_plus y = sSup {r : EReal | ∃ x ∈ Set.univ, r = ↑(f (x + y) - f x)}) (x y : Fin n → ℝ) : ↑(f (x + y) - f x) ≤ f0_plus y

Each recession difference is bounded above by f0_plus.

theorem recessionFunction_additive_majorant {n : ℕ} {f : (Fin n → ℝ) → ℝ} {f0_plus : (Fin n → ℝ) → EReal} (hf0_plus : ∀ (y : Fin n → ℝ), f0_plus y = sSup {r : EReal | ∃ x ∈ Set.univ, r = ↑(f (x + y) - f x)}) (x y : Fin n → ℝ) : ↑(f (x + y)) ≤ ↑(f x) + f0_plus y

The recession function controls increments of f.

theorem recessionFunction_le_of_additive_majorant {n : ℕ} {f : (Fin n → ℝ) → ℝ} {f0_plus : (Fin n → ℝ) → EReal} (hf0_plus : ∀ (y : Fin n → ℝ), f0_plus y = sSup {r : EReal | ∃ x ∈ Set.univ, r = ↑(f (x + y) - f x)}) (hne : ∀ (x : Fin n → ℝ), ↑(f x) ≠ ⊥) (h : (Fin n → ℝ) → EReal) : (∀ (z x : Fin n → ℝ), ↑(f z) ≤ ↑(f x) + h (z - x)) → f0_plus ≤ h

Any additive majorant bounds the recession function pointwise.

theorem recessionFunction_least_additive_majorant {n : ℕ} {f : (Fin n → ℝ) → ℝ} {f0_plus : (Fin n → ℝ) → EReal} (hf : ProperConvexFunctionOn Set.univ fun (x : Fin n → ℝ) => ↑(f x)) (hf0_plus : ∀ (y : Fin n → ℝ), f0_plus y = sSup {r : EReal | ∃ x ∈ Set.univ, r = ↑(f (x + y) - f x)}) : (∀ (z x : Fin n → ℝ), ↑(f z) ≤ ↑(f x) + f0_plus (z - x)) ∧ ∀ (h : (Fin n → ℝ) → EReal), (∀ (z x : Fin n → ℝ), ↑(f z) ≤ ↑(f x) + h (z - x)) → f0_plus ≤ h

Corollary 8.5.1. Let f be a proper convex function. Then f0^+ is the least of the functions h such that f(z) ≤ f(x) + h(z - x) for all z and all x. The recession function of f can be viewed in terms of a closure construction when f is a closed proper convex function; the source text continues with "Let g be the positively ..." (truncated).

theorem tendsto_rightScalarMultiple_comp_inv {n : ℕ} {f : (Fin n → ℝ) → EReal} {y : Fin n → ℝ} {l : Filter EReal} : Filter.Tendsto (fun (t : ℝ) => rightScalarMultiple f t y) (nhdsWithin 0 (Set.Ioi 0)) l ↔ Filter.Tendsto (fun (t : ℝ) => rightScalarMultiple f t⁻¹ y) Filter.atTop l

Convert a right-sided limit at 0 into a limit at +∞ via inversion.

theorem rightScalarMultiple_pos_rewrite {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ConvexFunction f) {lam : ℝ} (hlam : 0 < lam) (x : Fin n → ℝ) : rightScalarMultiple f lam x = ↑lam * f (lam⁻¹ • x)

Positive right scalar multiples satisfy the usual scaling formula.

theorem tendsto_rightScalarMultiple_inv_of_ray_limit {n : ℕ} {f : (Fin n → ℝ) → ℝ} {f0_plus : (Fin n → ℝ) → EReal} {y : Fin n → ℝ} (hfconv : ConvexFunction fun (x : Fin n → ℝ) => ↑(f x)) (hlim : Filter.Tendsto (fun (t : ℝ) => ↑((f (t • y) - f 0) / t)) Filter.atTop (nhds (f0_plus y))) : Filter.Tendsto (fun (t : ℝ) => rightScalarMultiple (fun (x : Fin n → ℝ) => ↑(f x)) t⁻¹ y) Filter.atTop (nhds (f0_plus y))

A ray difference-quotient limit yields the inverse right scalar multiple limit.

theorem recessionFunction_limit_rightScalarMultiple {n : ℕ} {f : (Fin n → ℝ) → ℝ} {f0_plus : (Fin n → ℝ) → EReal} (hfclosed : ClosedConvexFunction fun (x : Fin n → ℝ) => ↑(f x)) (hfproper : ProperConvexFunctionOn Set.univ fun (x : Fin n → ℝ) => ↑(f x)) (hf0_plus : ∀ (y : Fin n → ℝ), f0_plus y = sSup {r : EReal | ∃ x ∈ Set.univ, r = ↑(f (x + y) - f x)}) : (∀ y ∈ effectiveDomain Set.univ fun (x : Fin n → ℝ) => ↑(f x), Filter.Tendsto (fun (t : ℝ) => rightScalarMultiple (fun (x : Fin n → ℝ) => ↑(f x)) t y) (nhdsWithin 0 (Set.Ioi 0)) (nhds (f0_plus y))) ∧ ((0 ∈ effectiveDomain Set.univ fun (x : Fin n → ℝ) => ↑(f x)) → ∀ (y : Fin n → ℝ), Filter.Tendsto (fun (t : ℝ) => rightScalarMultiple (fun (x : Fin n → ℝ) => ↑(f x)) t y) (nhdsWithin 0 (Set.Ioi 0)) (nhds (f0_plus y)))

Corollary 8.5.2. If f is a closed proper convex function, then (f0^+)(y) = lim_{λ ↑ 0} (f λ)(y) for every y ∈ dom f. If 0 ∈ dom f, this formula holds for every y ∈ ℝ^n.

theorem ray_antitone_all_iff_nonpos_step {n : ℕ} {f : (Fin n → ℝ) → EReal} {y : Fin n → ℝ} : (∀ (x : Fin n → ℝ), Antitone fun (t : ℝ) => f (x + t • y)) ↔ ∀ (x : Fin n → ℝ) (t : ℝ), 0 ≤ t → f (x + t • y) ≤ f x

Antitone along all base points is equivalent to nonpositive forward steps.

theorem ray_antitone_all_iff_nonpos_step_real {n : ℕ} {f : (Fin n → ℝ) → ℝ} {y : Fin n → ℝ} : (∀ (x : Fin n → ℝ), Antitone fun (t : ℝ) => f (x + t • y)) ↔ ∀ (x : Fin n → ℝ) (t : ℝ), 0 ≤ t → f (x + t • y) ≤ f x

Antitone along all base points is equivalent to nonpositive forward steps (real-valued).

theorem ray_antitone_all_iff_diffquotient_le_zero_real {n : ℕ} {f : (Fin n → ℝ) → ℝ} {y : Fin n → ℝ} : (∀ (x : Fin n → ℝ), Antitone fun (t : ℝ) => f (x + t • y)) ↔ ∀ (x : Fin n → ℝ) (t : ℝ), 0 < t → (f (x + t • y) - f x) / t ≤ 0

Antitone along all base points is equivalent to nonpositive ray difference quotients.

theorem ray_antitone_of_liminf_lt_top_real {n : ℕ} {f : (Fin n → ℝ) → ℝ} (hf : ProperConvexFunctionOn Set.univ fun (x : Fin n → ℝ) => ↑(f x)) {x y : Fin n → ℝ} : Filter.liminf (fun (t : ℝ) => ↑(f (x + t • y))) Filter.atTop < ⊤ → Antitone fun (t : ℝ) => f (x + t • y)

Finite liminf along a ray forces antitone behavior of the ray.

theorem ray_antitone_all_iff_f0plus_le_zero_real {n : ℕ} {f : (Fin n → ℝ) → ℝ} {f0_plus : (Fin n → ℝ) → EReal} (hf : ProperConvexFunctionOn Set.univ fun (x : Fin n → ℝ) => ↑(f x)) (hf0_plus : ∀ (y : Fin n → ℝ), f0_plus y = sSup {r : EReal | ∃ x ∈ Set.univ, r = ↑(f (x + y) - f x)}) {y : Fin n → ℝ} : (∀ (x : Fin n → ℝ), Antitone fun (t : ℝ) => f (x + t • y)) ↔ f0_plus y ≤ 0

All ray functions are antitone iff the recession function is nonpositive.

theorem ray_antitone_extend_closed_real {n : ℕ} {f : (Fin n → ℝ) → ℝ} {y : Fin n → ℝ} (hclosed : ClosedConvexFunction fun (x : Fin n → ℝ) => ↑(f x)) (hx : ∃ x ∈ effectiveDomain Set.univ fun (x : Fin n → ℝ) => ↑(f x), Antitone fun (t : ℝ) => f (x + t • y)) (x : Fin n → ℝ) : Antitone fun (t : ℝ) => f (x + t • y)

For closed convex f, a ray antitone at one base point extends to all base points.

theorem recessionFunction_ray_antitone_iff {n : ℕ} {f : (Fin n → ℝ) → ℝ} {f0_plus : (Fin n → ℝ) → EReal} (hf : ProperConvexFunctionOn Set.univ fun (x : Fin n → ℝ) => ↑(f x)) (hf0_plus : ∀ (y : Fin n → ℝ), f0_plus y = sSup {r : EReal | ∃ x ∈ Set.univ, r = ↑(f (x + y) - f x)}) {y : Fin n → ℝ} : (∀ (x : Fin n → ℝ), Filter.liminf (fun (t : ℝ) => ↑(f (x + t • y))) Filter.atTop < ⊤ → Antitone fun (t : ℝ) => f (x + t • y)) ∧ ((∀ (x : Fin n → ℝ), Antitone fun (t : ℝ) => f (x + t • y)) ↔ f0_plus y ≤ 0) ∧ ((ClosedConvexFunction fun (x : Fin n → ℝ) => ↑(f x)) → (∃ x ∈ effectiveDomain Set.univ fun (x : Fin n → ℝ) => ↑(f x), Antitone fun (t : ℝ) => f (x + t • y)) → ∀ (x : Fin n → ℝ), Antitone fun (t : ℝ) => f (x + t • y))

Theorem 8.6. Let f be a proper convex function, and let y be a vector. If lim_{λ → +∞} inf f (x + λ • y) < +∞ for a given x, then f (x + λ • y) is non-increasing in λ for all real λ. This property holds for every x iff (f0^+)(y) ≤ 0. When f is closed, this property holds for every x if it holds for some x ∈ dom f.

theorem ray_monotone_of_antitone_neg {n : ℕ} {f : (Fin n → ℝ) → ℝ} {y : Fin n → ℝ} : (∀ (x : Fin n → ℝ), Antitone fun (t : ℝ) => f (x + t • -y)) → ∀ (x : Fin n → ℝ), Monotone fun (t : ℝ) => f (x + t • y)

Antitone on the reverse ray yields monotone on the forward ray.

theorem ray_const_iff_antitone_antitone_neg {n : ℕ} {f : (Fin n → ℝ) → ℝ} {y : Fin n → ℝ} : (∀ (x : Fin n → ℝ) (s t : ℝ), f (x + s • y) = f (x + t • y)) ↔ (∀ (x : Fin n → ℝ), Antitone fun (t : ℝ) => f (x + t • y)) ∧ ∀ (x : Fin n → ℝ), Antitone fun (t : ℝ) => f (x + t • -y)

Constancy along rays is equivalent to antitone behavior for y and -y.

theorem liminf_lt_top_of_ray_bounded_above {n : ℕ} {f : (Fin n → ℝ) → ℝ} {x y : Fin n → ℝ} {α : ℝ} (hbound : ∀ (t : ℝ), ↑(f (x + t • y)) ≤ ↑α) : Filter.liminf (fun (t : ℝ) => ↑(f (x + t • y))) Filter.atTop < ⊤

A uniform upper bound on a ray forces a finite liminf.

theorem recessionFunction_ray_const_iff {n : ℕ} {f : (Fin n → ℝ) → ℝ} {f0_plus : (Fin n → ℝ) → EReal} (hf : ProperConvexFunctionOn Set.univ fun (x : Fin n → ℝ) => ↑(f x)) (hf0_plus : ∀ (y : Fin n → ℝ), f0_plus y = sSup {r : EReal | ∃ x ∈ Set.univ, r = ↑(f (x + y) - f x)}) {y : Fin n → ℝ} : ((∀ (x : Fin n → ℝ) (s t : ℝ), f (x + s • y) = f (x + t • y)) ↔ f0_plus y ≤ 0 ∧ f0_plus (-y) ≤ 0) ∧ ((ClosedConvexFunction fun (x : Fin n → ℝ) => ↑(f x)) → (∃ (x : Fin n → ℝ) (α : ℝ), ∀ (t : ℝ), ↑(f (x + t • y)) ≤ ↑α) → f0_plus y ≤ 0 ∧ f0_plus (-y) ≤ 0)

Corollary 8.6.1. Let f be a proper convex function and y a vector. The function λ ↦ f (x + λ • y) is constant on ℝ for every x if and only if (f0^+)(y) ≤ 0 and (f0^+)(-y) ≤ 0. When f is closed, this condition holds if there exists x and α such that f (x + λ • y) ≤ α for all real λ.

theorem convexOn_toReal_on_affine_of_finite {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ConvexFunction f) {M : Set (Fin n → ℝ)} (hMconv : Convex ℝ M) (hfinite : ∀ x ∈ M, f x ≠ ⊥ ∧ f x ≠ ⊤) : ConvexOn ℝ M fun (x : Fin n → ℝ) => (f x).toReal

The toReal of a convex EReal function is convex on any convex set where it is finite.

theorem convexOn_real_antitone_of_bddAbove {g : ℝ → ℝ} (hconv : ConvexOn ℝ Set.univ g) (hbounded : ∃ (α : ℝ), ∀ (t : ℝ), g t ≤ α) : Antitone g

A convex real function bounded above on ℝ is antitone.

theorem convexOn_real_const_of_bddAbove {g : ℝ → ℝ} (hconv : ConvexOn ℝ Set.univ g) (hbounded : ∃ (α : ℝ), ∀ (t : ℝ), g t ≤ α) (s t : ℝ) : g s = g t

A convex real function bounded above on ℝ is constant.

theorem line_const_of_bddAbove_on_affine {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ConvexFunction f) (M : AffineSubspace ℝ (Fin n → ℝ)) (hfinite : ∀ x ∈ ↑M, f x ≠ ⊥ ∧ f x ≠ ⊤) (hbounded : ∃ (α : ℝ), ∀ x ∈ ↑M, f x ≤ ↑α) {x0 x : Fin n → ℝ} (hx0 : x0 ∈ ↑M) (hx : x ∈ ↑M) (s t : ℝ) : f ((AffineMap.lineMap x0 x) s) = f ((AffineMap.lineMap x0 x) t)

A bounded-above convex function is constant along any line in an affine set where it is finite.