theorem section13_span_linearitySpace_fenchelConjugate_eq_orthogonal_direction_affineSpan_effectiveDomain {n : ℕ} (f : (Fin n → ℝ) → EReal) (hf : ProperConvexFunctionOn Set.univ f) : Submodule.span ℝ (linearitySpace (fenchelConjugate n f)) = orthogonalComplement n (affineSpan ℝ (effectiveDomain Set.univ f)).direction

Theorem 13.4 (primal part): for proper convex f, the linearity space of f* is the orthogonal complement of the direction of affineSpan (dom f).

theorem linearitySpace_fenchelConjugate_eq_orthogonal_direction_affineSpan_effectiveDomain_and_dual {n : ℕ} (f : (Fin n → ℝ) → EReal) (hf : ProperConvexFunctionOn Set.univ f) : have domF := effectiveDomain Set.univ f; have domFstar := effectiveDomain Set.univ (fenchelConjugate n f); Submodule.span ℝ (linearitySpace (fenchelConjugate n f)) = orthogonalComplement n (affineSpan ℝ domF).direction ∧ (ClosedConvexFunction f → (affineSpan ℝ domFstar).direction = orthogonalComplement n (Submodule.span ℝ (linearitySpace f)) ∧ Module.finrank ℝ ↥(Submodule.span ℝ (linearitySpace (fenchelConjugate n f))) = n - Module.finrank ℝ ↥(affineSpan ℝ domF).direction ∧ Module.finrank ℝ ↥(affineSpan ℝ domFstar).direction = n - Module.finrank ℝ ↥(Submodule.span ℝ (linearitySpace f)))

Theorem 13.4: Let f be a proper convex function on ℝ^n. The linearity space of f^* is the orthogonal complement of the subspace parallel to aff (dom f). Dually, if f is closed, the subspace parallel to aff (dom f^*) is the orthogonal complement of the linearity space of f, and one has

linearity f^* = n - dimension f, and dimension f^* = n - linearity f.