def Function.linealitySpace' {n : ℕ} (f0_plus : (Fin n → ℝ) → EReal) : Set (Fin n → ℝ)

Definition 8.9.0. The lineality space of f0_plus on ℝ^n.

Equations

• Function.linealitySpace' f0_plus = {y : Fin n → ℝ | f0_plus (-y) = -f0_plus y}

def Function.IsAffineDirection {n : ℕ} (f0_plus : (Fin n → ℝ) → EReal) (y : Fin n → ℝ) : Prop

Definition 8.9.1. The directions of the vectors in the lineality space of f are called directions in which f is affine.

Equations

• Function.IsAffineDirection f0_plus y = (y ∈ Function.linealitySpace' f0_plus)

def Function.lineality {n : ℕ} (f0_plus : (Fin n → ℝ) → EReal) : ℕ

Definition 8.9.2. The dimension of the lineality space of f is the lineality of f.

Equations

• Function.lineality f0_plus = Module.finrank ℝ ↥(Submodule.span ℝ (Function.linealitySpace' f0_plus))

def Function.rank {n : ℕ} (f0_plus : (Fin n → ℝ) → EReal) (dim_f : ℕ) : ℕ

Definition 8.9.2. The rank of f is defined to be the dimension of f minus the lineality of f.

Equations

• Function.rank f0_plus dim_f = dim_f - Function.lineality f0_plus

theorem rank_eq_zero_le_lineality {n : ℕ} {f0_plus : (Fin n → ℝ) → EReal} {dim_f : ℕ} (h : Function.rank f0_plus dim_f = 0) : dim_f ≤ Function.lineality f0_plus

Rank zero forces dim_f to be at most the lineality.

theorem properConvexFunctionOn_effectiveDomain_nonempty {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ProperConvexFunctionOn Set.univ f) : (effectiveDomain Set.univ f).Nonempty

Proper convexity implies the effective domain is nonempty.

theorem not_mem_effectiveDomain_of_not_mem_affineSpan {n : ℕ} {f : (Fin n → ℝ) → EReal} {x : Fin n → ℝ} (hx : x ∉ affineSpan ℝ (effectiveDomain Set.univ f)) : x ∉ effectiveDomain Set.univ f

Points outside the affine span of the effective domain are not in the effective domain.

theorem linealitySpace_value_real {n : ℕ} {f0_plus : (Fin n → ℝ) → EReal} (hf0_plus : ProperConvexFunctionOn Set.univ f0_plus) {y : Fin n → ℝ} (hy : y ∈ Function.linealitySpace' f0_plus) : ∃ (v : ℝ), f0_plus y = ↑v

Values of the recession function are finite on its lineality space.

theorem lineality_span_eq_affineSpan_direction_of_rank_zero {n : ℕ} {f f0_plus : (Fin n → ℝ) → EReal} {dim_f : ℕ} (hdim : dim_f = Module.finrank ℝ ↥(affineSpan ℝ (effectiveDomain Set.univ f)).direction) (hrank : Function.rank f0_plus dim_f = 0) (hspan : Submodule.span ℝ (Function.linealitySpace' f0_plus) ≤ (affineSpan ℝ (effectiveDomain Set.univ f)).direction) : Submodule.span ℝ (Function.linealitySpace' f0_plus) = (affineSpan ℝ (effectiveDomain Set.univ f)).direction

Rank zero identifies the affine-span direction with the span of the lineality space, provided the inclusion is available.

theorem mem_direction_affineSpan_of_mem_effectiveDomain_add {n : ℕ} {f : (Fin n → ℝ) → EReal} {x0 y : Fin n → ℝ} (hx0 : x0 ∈ effectiveDomain Set.univ f) (hx0y : x0 + y ∈ effectiveDomain Set.univ f) : y ∈ (affineSpan ℝ (effectiveDomain Set.univ f)).direction

If x0 and x0 + y are in the effective domain, then y is a direction of its affine span.

theorem lineality_mem_effectiveDomain_of_additive_majorant {n : ℕ} {f f0_plus : (Fin n → ℝ) → EReal} (hf0_plus : ProperConvexFunctionOn Set.univ f0_plus) (hmaj : ∀ (x y : Fin n → ℝ), f (x + y) ≤ f x + f0_plus y) {x0 : Fin n → ℝ} (hx0 : x0 ∈ effectiveDomain Set.univ f) (y : Fin n → ℝ) : y ∈ Function.linealitySpace' f0_plus → x0 + y ∈ effectiveDomain Set.univ f

Additive majorants keep lineality directions inside the effective domain.

theorem lineality_span_le_direction_affineSpan {n : ℕ} {f f0_plus : (Fin n → ℝ) → EReal} {x0 : Fin n → ℝ} (hx0 : x0 ∈ effectiveDomain Set.univ f) (hmem : ∀ y ∈ Function.linealitySpace' f0_plus, x0 + y ∈ effectiveDomain Set.univ f) : Submodule.span ℝ (Function.linealitySpace' f0_plus) ≤ (affineSpan ℝ (effectiveDomain Set.univ f)).direction

If lineality directions preserve the effective domain, then their span lies in the direction of the affine span of the effective domain.

theorem mem_affineSpan_iff_vsub_mem_direction {n : ℕ} {s : Set (Fin n → ℝ)} {x0 x : Fin n → ℝ} (hx0 : x0 ∈ affineSpan ℝ s) : x ∈ affineSpan ℝ s ↔ x -ᵥ x0 ∈ (affineSpan ℝ s).direction

Membership in the affine span is equivalent to membership in the translated direction.

theorem lineality_neg {n : ℕ} {f0_plus : (Fin n → ℝ) → EReal} {y : Fin n → ℝ} (hy : y ∈ Function.linealitySpace' f0_plus) : -y ∈ Function.linealitySpace' f0_plus

Lineality is symmetric under negation.

theorem lineality_add {n : ℕ} {f0_plus : (Fin n → ℝ) → EReal} (hf0_plus : ProperConvexFunctionOn Set.univ f0_plus) (hpos : PositivelyHomogeneous f0_plus) {y1 y2 : Fin n → ℝ} (hy1 : y1 ∈ Function.linealitySpace' f0_plus) : f0_plus (y1 + y2) = f0_plus y1 + f0_plus y2

Lineality directions give additivity of f0_plus.

theorem lineality_zero_of_nonempty {n : ℕ} {f0_plus : (Fin n → ℝ) → EReal} (hf0_plus : ProperConvexFunctionOn Set.univ f0_plus) (hpos : PositivelyHomogeneous f0_plus) (hne : (Function.linealitySpace' f0_plus).Nonempty) : f0_plus 0 = 0

If the lineality space is nonempty, then f0_plus 0 = 0.

theorem lineality_span_neg_eq {n : ℕ} {f0_plus : (Fin n → ℝ) → EReal} (hf0_plus : ProperConvexFunctionOn Set.univ f0_plus) (hpos : PositivelyHomogeneous f0_plus) (hne : (Function.linealitySpace' f0_plus).Nonempty) (y : Fin n → ℝ) : y ∈ Submodule.span ℝ (Function.linealitySpace' f0_plus) → f0_plus (-y) = -f0_plus y

The lineality relation extends to the linear span of the lineality space.

theorem linealitySpace_linear_on_span {n : ℕ} {f0_plus : (Fin n → ℝ) → EReal} (hf0_plus : ProperConvexFunctionOn Set.univ f0_plus) (hpos : PositivelyHomogeneous f0_plus) (hne : (Function.linealitySpace' f0_plus).Nonempty) : ∃ (aL : ↥(Submodule.span ℝ (Function.linealitySpace' f0_plus)) →ₗ[ℝ] ℝ), ∀ (y : ↥(Submodule.span ℝ (Function.linealitySpace' f0_plus))), f0_plus ↑y = ↑(aL y)

On the span of its lineality space, f0_plus agrees with a linear functional.

theorem properConvexFunction_rank_zero_affine_on_affineSpan {n : ℕ} {f f0_plus : (Fin n → ℝ) → EReal} {dim_f : ℕ} (hf : ProperConvexFunctionOn Set.univ f) (hf0_plus : ProperConvexFunctionOn Set.univ f0_plus) (hpos : PositivelyHomogeneous f0_plus) (hmaj : ∀ (x y : Fin n → ℝ), f (x + y) ≤ f x + f0_plus y) (hdim : dim_f = Module.finrank ℝ ↥(affineSpan ℝ (effectiveDomain Set.univ f)).direction) (hrank : Function.rank f0_plus dim_f = 0) : ∃ (g : (Fin n → ℝ) →ᵃ[ℝ] ℝ), ∀ x ∈ ↑(affineSpan ℝ (effectiveDomain Set.univ f)), f x = ↑(g x)

Rank zero should force affine behavior on the affine span of the effective domain.

theorem properConvexFunction_rank_zero_partialAffine {n : ℕ} {f f0_plus : (Fin n → ℝ) → EReal} {dim_f : ℕ} (hf : ProperConvexFunctionOn Set.univ f) (hf0_plus : ProperConvexFunctionOn Set.univ f0_plus) (hpos : PositivelyHomogeneous f0_plus) (hmaj : ∀ (x y : Fin n → ℝ), f (x + y) ≤ f x + f0_plus y) (hdim : dim_f = Module.finrank ℝ ↥(affineSpan ℝ (effectiveDomain Set.univ f)).direction) (hrank : Function.rank f0_plus dim_f = 0) : ∃ (S : AffineSubspace ℝ (Fin n → ℝ)) (g : (Fin n → ℝ) →ᵃ[ℝ] ℝ), (∀ x ∈ ↑S, f x = ↑(g x)) ∧ ∀ x ∉ ↑S, f x = ⊤

Theorem 8.9.3. The proper convex functions of rank 0 are the partial affine functions, i.e. the functions which agree with an affine function along a certain affine set and are ⊤ elsewhere.

theorem rank_eq_dim_iff_lineality_eq_zero {n : ℕ} {f0_plus : (Fin n → ℝ) → EReal} {dim_f : ℕ} (hle : Function.lineality f0_plus ≤ dim_f) : Function.rank f0_plus dim_f = dim_f ↔ Function.lineality f0_plus = 0

Rank equals dimension iff the lineality is zero, provided the lineality is bounded.

theorem lineality_eq_zero_iff_no_nonzero_affineDirection {n : ℕ} {f0_plus : (Fin n → ℝ) → EReal} : Function.lineality f0_plus = 0 ↔ ¬∃ (y : Fin n → ℝ), y ≠ 0 ∧ Function.IsAffineDirection f0_plus y

Lineality zero iff there is no nonzero affine direction.

theorem closedProperConvexFunction_rank_eq_dim_iff_not_affineLine {n : ℕ} {f f0_plus : (Fin n → ℝ) → EReal} {dim_f : ℕ} (_hfclosed : ClosedConvexFunction fun (x : Fin n → ℝ) => f ((EuclideanSpace.equiv (Fin n) ℝ).symm x).ofLp) (_hfproper : ProperConvexFunctionOn Set.univ f) (hle : Function.lineality f0_plus ≤ dim_f) : Function.rank f0_plus dim_f = dim_f ↔ ¬∃ (y : Fin n → ℝ), y ≠ 0 ∧ Function.IsAffineDirection f0_plus y

Theorem 8.9.4. A closed proper convex function f has rank f = dim f if and only if it is not affine along any line in dom f.

theorem indicatorFunction_linealitySpace'_iff {n : ℕ} {S : Set (Fin n → ℝ)} {y : Fin n → ℝ} : y ∈ Function.linealitySpace' (indicatorFunction S) ↔ y ∈ S ∧ -y ∈ S

The lineality space of an indicator function consists of points in the set and its negation.

theorem Set.linealitySpace_eq_inter_of_recessionCone_eq {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hcone : C.recessionCone = C) : C.linealitySpace = C ∩ -C

If the recession cone equals the set, then the lineality space is C ∩ -C.

theorem linealitySpace_indicatorFunction_image_eq {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} : Function.linealitySpace' (indicatorFunction (⇑(EuclideanSpace.equiv (Fin n) ℝ) '' C)) = ⇑(EuclideanSpace.equiv (Fin n) ℝ) '' (C ∩ -C)

The lineality space of the indicator function of the image of C is the image of C ∩ -C.

theorem finrank_span_image_linearEquiv {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] [FiniteDimensional ℝ V] [FiniteDimensional ℝ W] (e : V ≃ₗ[ℝ] W) (S : Set V) : Module.finrank ℝ ↥(Submodule.span ℝ (⇑e '' S)) = Module.finrank ℝ ↥(Submodule.span ℝ S)

Finrank of the span is preserved under a linear equivalence.

theorem convexSet_rank_eq_indicatorFunction_rank {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (_hC : Convex ℝ C) (hcone : C.recessionCone = C) : C.rank = Function.rank (fun (x : Fin n → ℝ) => indicatorFunction (⇑(EuclideanSpace.equiv (Fin n) ℝ) '' C) x) (Module.finrank ℝ ↥(affineSpan ℝ C).direction)

Theorem 8.9.5. The rank of a convex set C equals the rank of its indicator function.