theorem section16_dotProduct_add_left {n : ℕ} (u v w : Fin n → ℝ) : (u + v) ⬝ᵥ w = u ⬝ᵥ w + v ⬝ᵥ w

Dot product is additive in the left argument.

theorem section16_range_fenchelConjugate_translate {n : ℕ} (h : (Fin n → ℝ) → EReal) (a xStar : Fin n → ℝ) : (Set.range fun (x : Fin n → ℝ) => ↑(x ⬝ᵥ xStar) - h (x - a)) = (fun (z : EReal) => z + ↑(a ⬝ᵥ xStar)) '' Set.range fun (y : Fin n → ℝ) => ↑(y ⬝ᵥ xStar) - h y

Translate the Fenchel conjugate range under x ↦ x - a.

theorem section16_fenchelConjugate_translate {n : ℕ} (h : (Fin n → ℝ) → EReal) (a : Fin n → ℝ) : (fenchelConjugate n fun (x : Fin n → ℝ) => h (x - a)) = fun (xStar : Fin n → ℝ) => fenchelConjugate n h xStar + ↑(a ⬝ᵥ xStar)

Text 16.0.1: Basic operations on a convex function and their effect on the Fenchel conjugate.

• If h is translated by a, i.e. f x = h (x - a), then f* x* = h* x* + ⟪a, x*⟫.
• If a linear functional is added, i.e. f x = h x + ⟪x, a*⟫, then f* x* = h* (x* - a*).
• For a real constant α, the conjugate of h + α is h* - α.

As a special case, for a set C, the support function of the translate C + a is supportFunctionEReal C + ⟪a, ·⟫, since the support function is the conjugate of the indicator function.

theorem section16_affine_piece_add_linear {n : ℕ} (h : (Fin n → ℝ) → EReal) (aStar x xStar : Fin n → ℝ) : ↑(x ⬝ᵥ xStar) - (h x + ↑(x ⬝ᵥ aStar)) = ↑(x ⬝ᵥ (xStar - aStar)) - h x

Rewriting the affine piece after adding a linear functional.

theorem section16_range_fenchelConjugate_add_linear {n : ℕ} (h : (Fin n → ℝ) → EReal) (aStar xStar : Fin n → ℝ) : (Set.range fun (x : Fin n → ℝ) => ↑(x ⬝ᵥ xStar) - (h x + ↑(x ⬝ᵥ aStar))) = Set.range fun (x : Fin n → ℝ) => ↑(x ⬝ᵥ (xStar - aStar)) - h x

Range rewrite for adding a linear functional inside fenchelConjugate.

theorem section16_fenchelConjugate_add_linear {n : ℕ} (h : (Fin n → ℝ) → EReal) (aStar : Fin n → ℝ) : (fenchelConjugate n fun (x : Fin n → ℝ) => h x + ↑(x ⬝ᵥ aStar)) = fun (xStar : Fin n → ℝ) => fenchelConjugate n h (xStar - aStar)

theorem section16_affine_piece_add_const {n : ℕ} (h : (Fin n → ℝ) → EReal) (α : ℝ) (x xStar : Fin n → ℝ) : ↑(x ⬝ᵥ xStar) - (h x + ↑α) = ↑(x ⬝ᵥ xStar) - h x + ↑(-α)

Rewriting the affine piece after adding a constant.

theorem section16_range_fenchelConjugate_add_const {n : ℕ} (h : (Fin n → ℝ) → EReal) (α : ℝ) (xStar : Fin n → ℝ) : (Set.range fun (x : Fin n → ℝ) => ↑(x ⬝ᵥ xStar) - (h x + ↑α)) = (fun (z : EReal) => z + ↑(-α)) '' Set.range fun (x : Fin n → ℝ) => ↑(x ⬝ᵥ xStar) - h x

Range rewrite for adding a constant inside fenchelConjugate.

theorem section16_fenchelConjugate_add_const {n : ℕ} (h : (Fin n → ℝ) → EReal) (α : ℝ) : (fenchelConjugate n fun (x : Fin n → ℝ) => h x + ↑α) = fun (xStar : Fin n → ℝ) => fenchelConjugate n h xStar - ↑α

theorem section16_supportFunctionEReal_translate {n : ℕ} (C : Set (Fin n → ℝ)) (a : Fin n → ℝ) : supportFunctionEReal ((fun (x : Fin n → ℝ) => x + a) '' C) = fun (xStar : Fin n → ℝ) => supportFunctionEReal C xStar + ↑(a ⬝ᵥ xStar)

theorem section16_polar_eq_sublevel_deltaStar {n : ℕ} (C : Set (Fin n → ℝ)) : {xStar : Fin n → ℝ | ∀ x ∈ C, x ⬝ᵥ xStar ≤ 1} = {xStar : Fin n → ℝ | supportFunctionEReal C xStar ≤ 1}

Text 16.0.2: The polar of a convex set C is a ≤ 1 level set of the support function δ^*(· | C), namely

C^∘ = {x^* | δ^*(x^* | C) ≤ 1}.

theorem section16_fenchelConjugate_const_zero {n : ℕ} : (fenchelConjugate n fun (x : Fin n → ℝ) => 0) = indicatorFunction {0}

The conjugate of the constant zero function is the indicator of {0}.

theorem section16_fenchelConjugate_precomp_smul {n : ℕ} (f : (Fin n → ℝ) → EReal) {lam : ℝ} (hlam : lam ≠ 0) : (fenchelConjugate n fun (x : Fin n → ℝ) => f (lam⁻¹ • x)) = fun (xStar : Fin n → ℝ) => fenchelConjugate n f (lam • xStar)

Scaling precomposition inside a Fenchel conjugate.

theorem section16_fenchelConjugate_indicator_singleton_zero {n : ℕ} : fenchelConjugate n (indicatorFunction {0}) = fun (x : Fin n → ℝ) => 0

The conjugate of the singleton indicator is the constant zero function.

theorem section16_fenchelConjugate_scaling {n : ℕ} (f : (Fin n → ℝ) → EReal) (hf : ProperConvexFunctionOn Set.univ f) {lam : ℝ} (hlam : 0 ≤ lam) : (fenchelConjugate n fun (x : Fin n → ℝ) => ↑lam * f x) = rightScalarMultiple (fenchelConjugate n f) lam ∧ fenchelConjugate n (rightScalarMultiple f lam) = fun (xStar : Fin n → ℝ) => ↑lam * fenchelConjugate n f xStar

Theorem 16.1: For any proper convex function f, one has (λ f)^* = f^* λ and (f λ)^* = λ f^*, 0 ≤ λ < ∞.

Here f^* is the Fenchel conjugate fenchelConjugate n f, λ f is pointwise multiplication x ↦ (λ : EReal) * f x, and f λ is the right scalar multiple rightScalarMultiple f λ.

theorem section16_image_dotProduct_smul_set {n : ℕ} (C : Set (Fin n → ℝ)) (lam : ℝ) (xStar : Fin n → ℝ) : (fun (x : Fin n → ℝ) => x ⬝ᵥ xStar) '' (lam • C) = lam • (fun (x : Fin n → ℝ) => x ⬝ᵥ xStar) '' C

Scaling the dot-product image-set commutes with set scaling.

theorem section16_deltaStar_scaling {n : ℕ} (C : Set (Fin n → ℝ)) {lam : ℝ} (hlam : 0 ≤ lam) : deltaStar (lam • C) = fun (xStar : Fin n → ℝ) => lam * deltaStar C xStar

Corollary 16.1.1. For any non-empty convex set C, one has δ^*(x^* | λ C) = λ δ^*(x^* | C), 0 ≤ λ < ∞.

theorem section16_mem_inv_smul_set_iff {n : ℕ} {lam : ℝ} (hlam0 : lam ≠ 0) (S : Set (Fin n → ℝ)) (x : Fin n → ℝ) : x ∈ lam⁻¹ • S ↔ lam • x ∈ S

Membership in an inverse-scaled set can be rewritten using the original scaling.

theorem section16_polar_smul_iff {n : ℕ} (C : Set (Fin n → ℝ)) {lam : ℝ} (xStar : Fin n → ℝ) : (∀ x ∈ lam • C, x ⬝ᵥ xStar ≤ 1) ↔ ∀ x ∈ C, x ⬝ᵥ lam • xStar ≤ 1

The polar inequality for a scaled set is equivalent to a scaled dual variable.

theorem section16_polar_scaling {n : ℕ} (C : Set (Fin n → ℝ)) {lam : ℝ} (hlam : 0 < lam) : {xStar : Fin n → ℝ | ∀ x ∈ lam • C, x ⬝ᵥ xStar ≤ 1} = lam⁻¹ • {xStar : Fin n → ℝ | ∀ x ∈ C, x ⬝ᵥ xStar ≤ 1}

Corollary 16.1.2. For any non-empty convex set C one has (λ C)^∘ = λ^{-1} C^∘ for 0 < λ < ∞.

theorem section16_intrinsicInterior_submodule_eq {n : ℕ} (L : Submodule ℝ (Fin n → ℝ)) : intrinsicInterior ℝ ↑L = ↑L

The intrinsic interior of a submodule (as a set) is the submodule itself.

theorem section16_nonempty_preimage_inter_ri_preimage_iff_not_disjoint_intrinsicInterior {n : ℕ} (L : Submodule ℝ (Fin n → ℝ)) (C : Set (Fin n → ℝ)) : ((fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' ↑L ∩ euclideanRelativeInterior n ((fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' C)).Nonempty ↔ ¬Disjoint (intrinsicInterior ℝ ↑L) (intrinsicInterior ℝ C)

Nonempty intersection in Euclidean space corresponds to non-disjoint intrinsic interiors.

theorem section16_sInf_sSup_image_dotProduct_submodule {n : ℕ} (L : Submodule ℝ (Fin n → ℝ)) (b : Fin n → ℝ) : (sInf ((fun (x : Fin n → ℝ) => ↑(x ⬝ᵥ b)) '' ↑L) = if b ∈ orthogonalComplement n L then 0 else ⊥) ∧ sSup ((fun (x : Fin n → ℝ) => ↑(x ⬝ᵥ b)) '' ↑L) = if b ∈ orthogonalComplement n L then 0 else ⊤

The dot-product image over a submodule has sInf/sSup determined by orthogonality.

theorem section16_sInf_lt_zero_iff_sSup_neg_gt_zero {n : ℕ} (C : Set (Fin n → ℝ)) (b : Fin n → ℝ) : 0 > sInf ((fun (x : Fin n → ℝ) => ↑(x ⬝ᵥ b)) '' C) ↔ sSup ((fun (x : Fin n → ℝ) => ↑(x ⬝ᵥ -b)) '' C) > 0

Negating the dual variable swaps the sign of the dot-product infimum condition.

theorem section16_exists_hyperplaneSeparatesProperly_submodule_effectiveDomain_iff_exists_orthogonal_recession_ineq {n : ℕ} (L : Submodule ℝ (Fin n → ℝ)) (f : (Fin n → ℝ) → EReal) (hf : ProperConvexFunctionOn Set.univ f) : (∃ (H : Set (Fin n → ℝ)), HyperplaneSeparatesProperly n H (↑L) (effectiveDomain Set.univ f)) ↔ ∃ xStar ∈ orthogonalComplement n L, recessionFunction (fenchelConjugate n f) xStar ≤ 0 ∧ recessionFunction (fenchelConjugate n f) (-xStar) > 0

Proper separation of a submodule and an effective domain in terms of recession inequalities.

theorem section16_subspace_meets_ri_effectiveDomain_iff_not_exists_orthogonal_recession_ineq {n : ℕ} (L : Submodule ℝ (Fin n → ℝ)) (f : (Fin n → ℝ) → EReal) (hf : ProperConvexFunctionOn Set.univ f) : ((fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' ↑L ∩ euclideanRelativeInterior n ((fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' effectiveDomain Set.univ f)).Nonempty ↔ ¬∃ xStar ∈ orthogonalComplement n L, recessionFunction (fenchelConjugate n f) xStar ≤ 0 ∧ recessionFunction (fenchelConjugate n f) (-xStar) > 0

Lemma 16.2. Let L be a subspace of ℝ^n and let f be a proper convex function. Then L meets ri (dom f) if and only if there exists no vector xStar ∈ L^⊥ such that (f^*0^+)(xStar) ≤ 0 and (f^*0^+)(-xStar) > 0.

Here dom f is the effective domain effectiveDomain univ f, ri is euclideanRelativeInterior, and (f^*0^+) is represented as recessionFunction (fenchelConjugate n f).

noncomputable def section16_coordLinearMap {n m : ℕ} (A : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin m)) : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] Fin m → ℝ

Coordinate form of a Euclidean linear map, viewed as a map into Fin m → ℝ.

Equations

• section16_coordLinearMap A = ↑(EuclideanSpace.equiv (Fin m) ℝ).toLinearEquiv ∘ₗ A

theorem section16_nonempty_preimage_range_inter_ri_effectiveDomain_iff {n m : ℕ} (A : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin m)) (g : (Fin m → ℝ) → EReal) : ((fun (z : EuclideanSpace ℝ (Fin m)) => z.ofLp) ⁻¹' ↑(LinearMap.range (section16_coordLinearMap A)) ∩ euclideanRelativeInterior m ((fun (z : EuclideanSpace ℝ (Fin m)) => z.ofLp) ⁻¹' effectiveDomain Set.univ g)).Nonempty ↔ ∃ (x : EuclideanSpace ℝ (Fin n)), A x ∈ euclideanRelativeInterior m ((fun (z : EuclideanSpace ℝ (Fin m)) => z.ofLp) ⁻¹' effectiveDomain Set.univ g)

Convert the range-preimage intersection into an explicit witness.

theorem section16_mem_orthogonalComplement_range_iff_adjoint_eq_zero {n m : ℕ} (A : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin m)) (yStar : EuclideanSpace ℝ (Fin m)) : yStar.ofLp ∈ orthogonalComplement m (LinearMap.range (section16_coordLinearMap A)) ↔ (LinearMap.adjoint A) yStar = 0

Characterize the orthogonal complement of a range via the adjoint.

theorem section16_exists_orthogonalComplement_range_recession_iff_exists_adjoint_eq_zero_recession {n m : ℕ} (A : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin m)) (g : (Fin m → ℝ) → EReal) : (∃ xStar ∈ orthogonalComplement m (LinearMap.range (section16_coordLinearMap A)), recessionFunction (fenchelConjugate m g) xStar ≤ 0 ∧ recessionFunction (fenchelConjugate m g) (-xStar) > 0) ↔ ∃ (yStar : EuclideanSpace ℝ (Fin m)), (LinearMap.adjoint A) yStar = 0 ∧ recessionFunction (fenchelConjugate m g) yStar.ofLp ≤ 0 ∧ recessionFunction (fenchelConjugate m g) (-yStar.ofLp) > 0

Rewrite orthogonality over the range in an existential statement.