theorem image_add_subset_of_add_mem {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} {y : EuclideanSpace ℝ (Fin n)} (h : ∀ x ∈ C, x + y ∈ C) : (fun (x : EuclideanSpace ℝ (Fin n)) => x + y) '' C ⊆ C

If every x ∈ C satisfies x + y ∈ C, then the translation of C by y stays in C.

theorem subset_image_add_of_sub_mem {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} {y : EuclideanSpace ℝ (Fin n)} (h : ∀ x ∈ C, x + -y ∈ C) : C ⊆ (fun (x : EuclideanSpace ℝ (Fin n)) => x + y) '' C

If every x ∈ C satisfies x - y ∈ C, then C is contained in its translation by y.

theorem add_mem_of_image_eq {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} {y : EuclideanSpace ℝ (Fin n)} (hEq : (fun (x : EuclideanSpace ℝ (Fin n)) => x + y) '' C = C) : (∀ x ∈ C, x + y ∈ C) ∧ ∀ x ∈ C, x + -y ∈ C

If C is invariant under translation by y, then C is closed under adding y and -y.

theorem linealitySpace_eq_translation {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hCne : C.Nonempty) (hCconv : Convex ℝ C) : -C.recessionCone ∩ C.recessionCone = {y : EuclideanSpace ℝ (Fin n) | (fun (x : EuclideanSpace ℝ (Fin n)) => x + y) '' C = C}

Theorem 8.4.5. For any non-empty convex set C, the lineality space lin(C) = (-0^+ C) ∩ 0^+ C equals { y ∈ ℝ^n | C + y = C }.

noncomputable def Set.rank {n : ℕ} (C : Set (EuclideanSpace ℝ (Fin n))) : ℕ

Definiton 8.4.6. Let C be a non-empty convex set with lineality space L = lin(C). The rank of C is defined by rank(C) = dim(C) - dim(L).

Equations

• C.rank = Module.finrank ℝ ↥(affineSpan ℝ C).direction - Module.finrank ℝ ↥(Submodule.span ℝ (-C.recessionCone ∩ C.recessionCone))

theorem properConvexFunctionOn_nonempty {n : ℕ} {C : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → EReal} (hf : ProperConvexFunctionOn C f) : C.Nonempty

Proper convexity implies the domain is nonempty.

theorem diffQuotient_set_nonempty {n : ℕ} {C : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → ℝ} (hf : ProperConvexFunctionOn C fun (x : Fin n → ℝ) => ↑(f x)) (y : Fin n → ℝ) : {r : EReal | ∃ x ∈ C, r = ↑(f (x + y) - f x)}.Nonempty

The difference-quotient set used in the recession formula is nonempty.

theorem recessionFunction_zero {n : ℕ} {C : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → ℝ} {f0_plus : (Fin n → ℝ) → EReal} (hf : ProperConvexFunctionOn C fun (x : Fin n → ℝ) => ↑(f x)) (hf0_plus : ∀ (y : Fin n → ℝ), f0_plus y = sSup {r : EReal | ∃ x ∈ C, r = ↑(f (x + y) - f x)}) : f0_plus 0 = 0

The recession formula forces f0_plus 0 = 0.

theorem recessionFunction_ne_bot {n : ℕ} {C : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → ℝ} {f0_plus : (Fin n → ℝ) → EReal} (hf : ProperConvexFunctionOn C fun (x : Fin n → ℝ) => ↑(f x)) (hf0_plus : ∀ (y : Fin n → ℝ), f0_plus y = sSup {r : EReal | ∃ x ∈ C, r = ↑(f (x + y) - f x)}) (y : Fin n → ℝ) : f0_plus y ≠ ⊥

The recession formula prevents f0_plus from taking the value ⊥.

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

The recession formula gives a pointwise inequality characterization.

theorem recessionFunction_epigraph_nonempty {n : ℕ} {C : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → ℝ} {f0_plus : (Fin n → ℝ) → EReal} (hf : ProperConvexFunctionOn C fun (x : Fin n → ℝ) => ↑(f x)) (hf0_plus : ∀ (y : Fin n → ℝ), f0_plus y = sSup {r : EReal | ∃ x ∈ C, r = ↑(f (x + y) - f x)}) : (epigraph Set.univ f0_plus).Nonempty

The epigraph of the recession function is nonempty, witnessed at the origin.

theorem convexOn_real_of_convexFunctionOn_ereal_univ {n : ℕ} {C : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → ℝ} (hC : C = Set.univ) (hf : ProperConvexFunctionOn C fun (x : Fin n → ℝ) => ↑(f x)) : ConvexOn ℝ Set.univ f

Proper convexity on the whole space gives real-valued convexity on Set.univ.

theorem recessionFunction_ray_bound_real {n : ℕ} {C : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → ℝ} (hC : C = Set.univ) (hf : ProperConvexFunctionOn C fun (x : Fin n → ℝ) => ↑(f x)) {y : Fin n → ℝ} {v : ℝ} : (∀ (x : Fin n → ℝ), f (x + y) - f x ≤ v) → ∀ t > 0, ∀ (x : Fin n → ℝ), f (x + t • y) - f x ≤ t * v

A convex real function with bounded unit increments along y has bounded increments at all positive scales.

theorem recessionFunction_ray_bound {n : ℕ} {C : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → ℝ} (hC : C = Set.univ) (hf : ProperConvexFunctionOn C fun (x : Fin n → ℝ) => ↑(f x)) {y : Fin n → ℝ} {v : ℝ} : (∀ (x : Fin n → ℝ), ↑(f (x + y) - f x) ≤ ↑v) → ∀ t > 0, ∀ (x : Fin n → ℝ), ↑(f (x + t • y) - f x) ≤ ↑(t * v)

The ray bound rewritten in EReal form for the recession function.

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

A pointwise bound on f0_plus is equivalent to bounds on all ray difference quotients.

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

Subadditivity of the recession formula when the domain is the whole space.

theorem recessionFunction_convex_univ {n : ℕ} {C : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → ℝ} {f0_plus : (Fin n → ℝ) → EReal} (hC : C = Set.univ) (hf : ProperConvexFunctionOn C fun (x : Fin n → ℝ) => ↑(f x)) (hf0_plus : ∀ (y : Fin n → ℝ), f0_plus y = sSup {r : EReal | ∃ x ∈ C, r = ↑(f (x + y) - f x)}) (hpos : PositivelyHomogeneous f0_plus) : ConvexFunctionOn Set.univ f0_plus

Convexity of the recession function on Set.univ from subadditivity and pos. homogeneity.

theorem differenceQuotient_monotone {n : ℕ} {C : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → ℝ} (hC : C = Set.univ) (hf : ProperConvexFunctionOn C fun (x : Fin n → ℝ) => ↑(f x)) (x y : Fin n → ℝ) : Monotone fun (t : { t : ℝ // 0 < t }) => (f (x + ↑t • y) - f x) / ↑t

Along a fixed ray, the difference quotient is monotone in the step length.

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

Rewrite the recession formula as an iSup over base points.

theorem recessionFunction_lsc_of_closed {n : ℕ} {C : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → ℝ} {f0_plus : (Fin n → ℝ) → EReal} (hC : C = Set.univ) (hf0_plus : ∀ (y : Fin n → ℝ), f0_plus y = sSup {r : EReal | ∃ x ∈ C, r = ↑(f (x + y) - f x)}) (hclosed : ClosedConvexFunction fun (x : Fin n → ℝ) => ↑(f x)) : LowerSemicontinuous f0_plus

Closedness of f implies lower semicontinuity of the recession function.

theorem closed_embedded_epigraph {n : ℕ} {f : (Fin n → ℝ) → EReal} (hls : LowerSemicontinuous f) : have C := ⇑(appendAffineEquiv n 1) '' ((fun (p : (Fin n → ℝ) × ℝ) => ((EuclideanSpace.equiv (Fin n) ℝ).symm p.1, (EuclideanSpace.equiv (Fin 1) ℝ).symm fun (x : Fin 1) => p.2)) '' epigraph Set.univ f); IsClosed C

The embedded epigraph is closed when f is lower semicontinuous.

theorem embedded_epigraph_add_smul {n : ℕ} : have eN := (EuclideanSpace.equiv (Fin n) ℝ).symm.toAffineEquiv; have e1 := ((ContinuousLinearEquiv.funUnique (Fin 1) ℝ ℝ).symm.toLinearEquiv ≪≫ₗ (EuclideanSpace.equiv (Fin 1) ℝ).symm.toLinearEquiv).toAffineEquiv; have g := eN.prodCongr e1; have embed := fun (p : (Fin n → ℝ) × ℝ) => (appendAffineEquiv n 1) (g p); have dir := fun (q : (Fin n → ℝ) × ℝ) => (appendAffineEquiv n 1).linear (g.linear q); ∀ (p q : (Fin n → ℝ) × ℝ) (t : ℝ), embed (p + t • q) = embed p + t • dir q

The embedded epigraph map sends affine rays to affine rays.

theorem ray_bound_extend_closed {n : ℕ} {f : (Fin n → ℝ) → ℝ} {x0 y : Fin n → ℝ} {v : ℝ} (hclosed : ClosedConvexFunction fun (x : Fin n → ℝ) => ↑(f x)) (hbound : ∀ t > 0, (f (x0 + t • y) - f x0) / t ≤ v) (x : Fin n → ℝ) (t : ℝ) : 0 < t → (f (x + t • y) - f x) / t ≤ v

A ray bound at one base point extends to all base points for closed convex f.

theorem ray_sSup_eq_of_closed {n : ℕ} {C : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → ℝ} {f0_plus : (Fin n → ℝ) → EReal} (hC : C = Set.univ) (hf : ProperConvexFunctionOn C fun (x : Fin n → ℝ) => ↑(f x)) (hf0_plus : ∀ (y : Fin n → ℝ), f0_plus y = sSup {r : EReal | ∃ x ∈ C, r = ↑(f (x + y) - f x)}) (hpos : PositivelyHomogeneous f0_plus) (hclosed : ClosedConvexFunction fun (x : Fin n → ℝ) => ↑(f x)) (x y : Fin n → ℝ) : f0_plus y = sSup {r : EReal | ∃ (t : ℝ), 0 < t ∧ r = ↑((f (x + t • y) - f x) / t)}

Closed convexity makes the ray supremum independent of the base point.

theorem ray_limit_monotone {n : ℕ} {C : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → ℝ} {f0_plus : (Fin n → ℝ) → EReal} (hC : C = Set.univ) (hf : ProperConvexFunctionOn C fun (x : Fin n → ℝ) => ↑(f x)) (hf0_plus : ∀ (y : Fin n → ℝ), f0_plus y = sSup {r : EReal | ∃ x ∈ C, r = ↑(f (x + y) - f x)}) (hpos : PositivelyHomogeneous f0_plus) (hclosed : ClosedConvexFunction fun (x : Fin n → ℝ) => ↑(f x)) (x y : Fin n → ℝ) : Filter.Tendsto (fun (t : ℝ) => ↑((f (x + t • y) - f x) / t)) Filter.atTop (nhds (f0_plus y))

Along a fixed ray, the difference quotient converges to f0_plus.