theorem dotProduct_self_nonneg {n : ℕ} (v : Fin n → ℝ) : 0 ≤ v ⬝ᵥ v

Nonnegativity of the dot product of a vector with itself.

theorem range_term_quadraticHalfInner_le (n : ℕ) (x xStar : Fin n → ℝ) : ↑(x ⬝ᵥ xStar) - quadraticHalfInner n x ≤ quadraticHalfInner n xStar

The key inequality for the conjugate of quadraticHalfInner: ⟪x, x*⟫ - (1/2)⟪x, x⟫ ≤ (1/2)⟪x*, x*⟫.

theorem fenchelConjugate_quadraticHalfInner (n : ℕ) : fenchelConjugate n (quadraticHalfInner n) = quadraticHalfInner n

The Fenchel conjugate of w(x) = (1/2)⟪x,x⟫ is itself.

theorem convexFunction_quadraticHalfInner (n : ℕ) : ConvexFunction (quadraticHalfInner n)

The quadratic function w(x) = (1/2)⟪x,x⟫ is convex on ℝ^n.

theorem quadraticHalfInner_le_of_fenchelConjugate_eq_self (n : ℕ) (f : (Fin n → ℝ) → EReal) (hf : fenchelConjugate n f = f) (x : Fin n → ℝ) : quadraticHalfInner n x ≤ f x

If f* = f, then f is pointwise bounded below by w(x) = (1/2)⟪x,x⟫.

theorem fenchelConjugate_eq_self_unique_solution (n : ℕ) : (ConvexFunction (quadraticHalfInner n) ∧ fenchelConjugate n (quadraticHalfInner n) = quadraticHalfInner n) ∧ ∀ (f : (Fin n → ℝ) → EReal), ConvexFunction f → fenchelConjugate n f = f → f = quadraticHalfInner n

Text 12.2.9: The fixed-point identity f* = f for Fenchel conjugation has a unique solution in the class of convex functions on ℝ^n, namely f = w where w(x) = (1/2) * ⟪x, x⟫. Here f* is fenchelConjugate n f.

def constNegInf (n : ℕ) : (Fin n → ℝ) → EReal

Text 12.1.3: Let f_{-∞} and f_{+∞} denote the constant functions on ℝ^n taking values -∞ and +∞ respectively. Then they are conjugate to each other (with conjugation given here by fenchelConjugate), i.e. (f_{-∞})^* = f_{+∞} and (f_{+∞})^* = f_{-∞}.

Equations

• constNegInf n x✝ = ⊥

def constPosInf (n : ℕ) : (Fin n → ℝ) → EReal

The constant function on ℝ^n with value +∞.

Equations

• constPosInf n x✝ = ⊤

theorem fenchelConjugate_constNegInf_apply (n : ℕ) (xStar : Fin n → ℝ) : fenchelConjugate n (constNegInf n) xStar = ⊤

The Fenchel conjugate of the constant -∞ function is pointwise +∞.

theorem fenchelConjugate_constPosInf_apply (n : ℕ) (xStar : Fin n → ℝ) : fenchelConjugate n (constPosInf n) xStar = ⊥

The Fenchel conjugate of the constant +∞ function is pointwise -∞.

theorem fenchelConjugate_constNegInf (n : ℕ) : fenchelConjugate n (constNegInf n) = constPosInf n

For f_{-∞} the constant function x ↦ -∞ on ℝ^n, its Fenchel conjugate is f_{+∞}.

theorem fenchelConjugate_constPosInf (n : ℕ) : fenchelConjugate n (constPosInf n) = constNegInf n

For f_{+∞} the constant function x ↦ +∞ on ℝ^n, its Fenchel conjugate is f_{-∞}.

theorem dotProduct_linearEquiv_symm_eq (n : ℕ) (A AStar : (Fin n → ℝ) ≃ₗ[ℝ] Fin n → ℝ) (hAStar : ∀ (x y : Fin n → ℝ), A x ⬝ᵥ y = x ⬝ᵥ AStar y) (y v : Fin n → ℝ) : A.symm y ⬝ᵥ v = y ⬝ᵥ AStar.symm v

Rewriting a dot product after applying the inverse linear equivalence, using the assumed adjoint relation.

theorem ereal_add_coe_le_coe_iff_cancel (t : EReal) (c μ : ℝ) : t + ↑c ≤ ↑μ ↔ t ≤ ↑(μ - c)

Cancel a finite real constant on the right in an EReal inequality.

theorem affineTransform_pointwise_inequality_iff (n : ℕ) (h : (Fin n → ℝ) → EReal) (A AStar : (Fin n → ℝ) ≃ₗ[ℝ] Fin n → ℝ) (hAStar : ∀ (x y : Fin n → ℝ), A x ⬝ᵥ y = x ⬝ᵥ AStar y) (a aStar : Fin n → ℝ) (α : ℝ) (xStar : Fin n → ℝ) (μ : ℝ) : have b' := AStar.symm (xStar - aStar); have μ' := μ + α - a ⬝ᵥ (xStar - aStar); (∀ (x : Fin n → ℝ), ↑(x ⬝ᵥ xStar - μ) ≤ h (A (x - a)) + ↑(x ⬝ᵥ aStar) + ↑α) ↔ ∀ (y : Fin n → ℝ), ↑(y ⬝ᵥ b' - μ') ≤ h y

Change-of-variables lemma for the affine-minorant characterization used in Theorem 12.3.

theorem fenchelConjugate_affineTransform_le_coe_iff (n : ℕ) (h : (Fin n → ℝ) → EReal) (A AStar : (Fin n → ℝ) ≃ₗ[ℝ] Fin n → ℝ) (hAStar : ∀ (x y : Fin n → ℝ), A x ⬝ᵥ y = x ⬝ᵥ AStar y) (a aStar : Fin n → ℝ) (α : ℝ) (xStar : Fin n → ℝ) (μ : ℝ) : have f := fun (x : Fin n → ℝ) => h (A (x - a)) + ↑(x ⬝ᵥ aStar) + ↑α; have b' := AStar.symm (xStar - aStar); have μ' := μ + α - a ⬝ᵥ (xStar - aStar); fenchelConjugate n f xStar ≤ ↑μ ↔ fenchelConjugate n h b' ≤ ↑μ'

Upper-bound equivalence for the Fenchel conjugate under the affine transformation in Theorem 12.3.

theorem fenchelConjugate_affineTransform (n : ℕ) (h : (Fin n → ℝ) → EReal) (A AStar : (Fin n → ℝ) ≃ₗ[ℝ] Fin n → ℝ) (hAStar : ∀ (x y : Fin n → ℝ), A x ⬝ᵥ y = x ⬝ᵥ AStar y) (a aStar : Fin n → ℝ) (α : ℝ) : have f := fun (x : Fin n → ℝ) => h (A (x - a)) + ↑(x ⬝ᵥ aStar) + ↑α; have αStar := -α - a ⬝ᵥ aStar; fenchelConjugate n f = fun (xStar : Fin n → ℝ) => fenchelConjugate n h (AStar.symm (xStar - aStar)) + ↑(xStar ⬝ᵥ a) + ↑αStar

Theorem 12.3. Let h be a convex function on ℝ^n, and define f(x) = h(A(x - a)) + ⟪x, a^*⟫ + α, where A is a one-to-one linear transformation of ℝ^n, a and a^* are vectors in ℝ^n, and α ∈ ℝ. Then f^*(x^*) = h^*(A^{*-1}(x^* - a^*)) + ⟪x^*, a⟫ + α^*, where A^* is the adjoint of A and α^* = -α - ⟪a, a^*⟫. Here f^* and h^* are represented by fenchelConjugate.

theorem range_term_partialAffine_tucker_simp (n m : ℕ) (α00 : ℝ) (α0 : Fin n → ℝ) (αi0 : Fin m → ℝ) (α : Fin m → Fin n → ℝ) (x xStar : Fin (n + m) → ℝ) : have f := fun (y : Fin (n + m) → ℝ) => if x : ∀ (i : Fin m), y (Fin.natAdd n i) = ∑ j : Fin n, α i j * y (Fin.castAdd m j) - αi0 i then ↑(∑ j : Fin n, α0 j * y (Fin.castAdd m j) - α00) else ⊤; ↑(x ⬝ᵥ xStar) - f x = if x_1 : ∀ (i : Fin m), x (Fin.natAdd n i) = ∑ j : Fin n, α i j * x (Fin.castAdd m j) - αi0 i then ↑(x ⬝ᵥ xStar - (∑ j : Fin n, α0 j * x (Fin.castAdd m j) - α00)) else ⊥

Simplify the Fenchel-conjugate range term for a Tucker-type partial affine function.

Outside the primal constraint set, the function value is ⊤ and the range term is ⊥.

theorem range_term_partialAffine_tucker_real_formula (n m : ℕ) (α00 : ℝ) (α0 : Fin n → ℝ) (αi0 : Fin m → ℝ) (α : Fin m → Fin n → ℝ) (x xStar : Fin (n + m) → ℝ) (hx : ∀ (i : Fin m), x (Fin.natAdd n i) = ∑ j : Fin n, α i j * x (Fin.castAdd m j) - αi0 i) : have xHead := fun (j : Fin n) => x (Fin.castAdd m j); have coeff := fun (j : Fin n) => xStar (Fin.castAdd m j) + ∑ i : Fin m, α i j * xStar (Fin.natAdd n i) - α0 j; have const := α00 - ∑ i : Fin m, αi0 i * xStar (Fin.natAdd n i); x ⬝ᵥ xStar - (∑ j : Fin n, α0 j * xHead j - α00) = ∑ j : Fin n, xHead j * coeff j + const

Expand the real expression ⟪x,x*⟫ - f(x) for a Tucker-type partial affine function under the primal feasibility constraint, grouping the free coordinates x (Fin.castAdd m ·).

theorem tucker_dualConstraint_iff_coeff_eq_zero (n m : ℕ) (α0 : Fin n → ℝ) (α : Fin m → Fin n → ℝ) (xStar : Fin (n + m) → ℝ) : have coeff := fun (j : Fin n) => xStar (Fin.castAdd m j) + ∑ i : Fin m, α i j * xStar (Fin.natAdd n i) - α0 j; (∀ (j : Fin n), xStar (Fin.castAdd m j) = ∑ i : Fin m, -α i j * xStar (Fin.natAdd n i) + α0 j) ↔ ∀ (j : Fin n), coeff j = 0

The dual feasibility constraint in Tucker form is equivalent to vanishing of the coefficients of the free primal variables in the conjugate range term.

theorem exists_head_makes_linear_combo_arbitrarily_large {n : ℕ} (coeff : Fin n → ℝ) (const : ℝ) (hcoeff : ∃ (j : Fin n), coeff j ≠ 0) (μ : ℝ) : ∃ (xHead : Fin n → ℝ), μ ≤ ∑ j : Fin n, xHead j * coeff j + const

If some coefficient in a linear form is nonzero, we can choose the variables to make the form arbitrarily large (even achieving any prescribed value up to a constant shift).