theorem section16_fenchelConjugate_precomp_eq_top_of_improper_of_exists_mem_ri {n m : ℕ} (A : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin m)) (g : (Fin m → ℝ) → EReal) (hg : ConvexFunction g) (hri : ∃ (x : EuclideanSpace ℝ (Fin n)), A x ∈ euclideanRelativeInterior m ((fun (z : EuclideanSpace ℝ (Fin m)) => z.ofLp) ⁻¹' effectiveDomain Set.univ g)) (hproper : ¬ProperConvexFunctionOn Set.univ g) : (fenchelConjugate n fun (x : Fin n → ℝ) => g (A (WithLp.toLp 2 x)).ofLp) = constPosInf n ∧ fenchelConjugate m g = constPosInf m

In the improper case, the conjugates are identically ⊤.

theorem section16_convexFunctionClosure_precomp_eq_precomp_convexFunctionClosure_of_exists_mem_ri {n m : ℕ} (A : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin m)) {g : (Fin m → ℝ) → EReal} (hgproper : ProperConvexFunctionOn Set.univ g) (hri : ∃ (x : EuclideanSpace ℝ (Fin n)), A x ∈ euclideanRelativeInterior m ((fun (z : EuclideanSpace ℝ (Fin m)) => z.ofLp) ⁻¹' effectiveDomain Set.univ g)) : (convexFunctionClosure fun (x : Fin n → ℝ) => g (A (WithLp.toLp 2 x)).ofLp) = fun (x : (i : Fin n) → (fun (x : Fin n) => ℝ) i) => convexFunctionClosure g (A (WithLp.toLp 2 x)).ofLp

Closure commutes with linear precomposition under a relative-interior preimage point.

theorem section16_adjointImage_closed_and_attained_of_exists_mem_ri_effectiveDomain {n m : ℕ} (A : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin m)) (g : (Fin m → ℝ) → EReal) (hgproper : ProperConvexFunctionOn Set.univ g) (hri : ∃ (x : EuclideanSpace ℝ (Fin n)), A x ∈ euclideanRelativeInterior m ((fun (z : EuclideanSpace ℝ (Fin m)) => z.ofLp) ⁻¹' effectiveDomain Set.univ g)) : have Aadj := LinearMap.adjoint A; have gStar := fenchelConjugate m g; have h := fun (xStar : Fin n → ℝ) => sInf ((fun (yStar : EuclideanSpace ℝ (Fin m)) => gStar yStar.ofLp) '' {yStar : EuclideanSpace ℝ (Fin m) | Aadj yStar = WithLp.toLp 2 xStar}); convexFunctionClosure h = h ∧ ∀ (xStar : Fin n → ℝ), h xStar = ⊤ ∨ ∃ (yStar : EuclideanSpace ℝ (Fin m)), Aadj yStar = WithLp.toLp 2 xStar ∧ gStar yStar.ofLp = h xStar

Closedness and attainment for the adjoint-image infimum under the ri condition.

theorem section16_properConvexFunctionOn_indicatorFunction_of_exists_mem_ri {n m : ℕ} (A : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin m)) (D : Set (Fin m → ℝ)) (hD : Convex ℝ D) (hri : ∃ (x : EuclideanSpace ℝ (Fin n)), A x ∈ euclideanRelativeInterior m ((fun (z : EuclideanSpace ℝ (Fin m)) => z.ofLp) ⁻¹' D)) : ProperConvexFunctionOn Set.univ (indicatorFunction D) ∧ ∃ (x : EuclideanSpace ℝ (Fin n)), A x ∈ euclideanRelativeInterior m ((fun (z : EuclideanSpace ℝ (Fin m)) => z.ofLp) ⁻¹' effectiveDomain Set.univ (indicatorFunction D))

Properness and ri-compatibility for indicator functions under a feasible point.

theorem section16_indicator_precomp_eq_indicator_preimage {n m : ℕ} (A : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin m)) (D : Set (Fin m → ℝ)) : (fun (x : Fin n → ℝ) => indicatorFunction D (A (WithLp.toLp 2 x)).ofLp) = indicatorFunction ((fun (x : Fin n → ℝ) => (A (WithLp.toLp 2 x)).ofLp) ⁻¹' D)

Precomposition of an indicator is the indicator of a preimage set.