theorem fenchelConjugate_partialAffine_tucker (n m : ℕ) (hn : 0 < n) (hm : 0 < m) (α00 : ℝ) (α0 : Fin n → ℝ) (αi0 : Fin m → ℝ) (α : Fin m → Fin n → ℝ) : have f := fun (x : Fin (n + m) → ℝ) => if x_1 : ∀ (i : Fin m), x (Fin.natAdd n i) = ∑ j : Fin n, α i j * x (Fin.castAdd m j) - αi0 i then ↑(∑ j : Fin n, α0 j * x (Fin.castAdd m j) - α00) else ⊤; have fStar := fun (xStar : Fin (n + m) → ℝ) => if x : ∀ (j : Fin n), xStar (Fin.castAdd m j) = ∑ i : Fin m, -α i j * xStar (Fin.natAdd n i) + α0 j then ↑(∑ i : Fin m, -αi0 i * xStar (Fin.natAdd n i) + α00) else ⊤; fenchelConjugate (n + m) f = fStar

Text 12.3.1: Let f be an n-dimensional partial affine function on ℝ^N with 0 < n < N and m = N - n, given (after a partition of coordinates x = (ξ₁, …, ξ_N)) by a Tucker-type representation:

f(x) = (∑_{j=1}^n α₀ⱼ ξⱼ - α₀₀) if ξ_{n+i} = ∑_{j=1}^n αᵢⱼ ξⱼ - αᵢ₀ for i = 1, …, m, and f(x) = +∞ otherwise.

Then the conjugate f* is:

f*(x*) = (∑_{i=1}^m β₀ᵢ ξ*_{n+i} - β₀₀) if ξ*ⱼ = ∑_{i=1}^m βⱼᵢ ξ*_{n+i} - βⱼ₀ for j = 1, …, n, and f*(x*) = +∞ otherwise, where βⱼᵢ = -αᵢⱼ for all i ∈ {0, …, m}, j ∈ {0, …, n}.

noncomputable def quadraticHalfLinear (n : ℕ) (Q : (Fin n → ℝ) →ₗ[ℝ] Fin n → ℝ) : (Fin n → ℝ) → EReal

The quadratic extended-real function associated to a linear map Q on ℝ^n, x ↦ (1/2) * ⟪x, Q x⟫. Here the inner product is written as the dot product ⬝ᵥ on coordinates x : Fin n → ℝ.

Equations

• quadraticHalfLinear n Q x = ↑(1 / 2 * x ⬝ᵥ Q x)

def IsSymmetricWrtOrthogonalSet {α : Type u_1} (n : ℕ) (G : Set ((Fin n → ℝ) ≃ₗᵢ[ℝ] Fin n → ℝ)) (f : (Fin n → ℝ) → α) : Prop

A function f on ℝ^n is symmetric with respect to a set G of orthogonal linear transformations if it is invariant under every element of G, i.e. f (g x) = f x for all g ∈ G and all x.

Equations

• IsSymmetricWrtOrthogonalSet n G f = ∀ g ∈ G, ∀ (x : Fin n → ℝ), f (g x) = f x

theorem dotProduct_orthogonal_symm_apply {n : ℕ} (g : (Fin n → ℝ) ≃ₗᵢ[ℝ] Fin n → ℝ) (hg : ∀ (x y : Fin n → ℝ), g x ⬝ᵥ g y = x ⬝ᵥ y) (x y : Fin n → ℝ) : g x ⬝ᵥ y = x ⬝ᵥ g.symm y

If g preserves dot products, then g.symm is the adjoint of g for the dot product.

theorem fenchelConjugate_precomp_orthogonal (n : ℕ) (f : (Fin n → ℝ) → EReal) (g : (Fin n → ℝ) ≃ₗᵢ[ℝ] Fin n → ℝ) (hAStar : ∀ (x y : Fin n → ℝ), g x ⬝ᵥ y = x ⬝ᵥ g.symm y) : (fenchelConjugate n fun (x : Fin n → ℝ) => f (g x)) = fun (xStar : Fin n → ℝ) => fenchelConjugate n f (g xStar)

The Fenchel conjugate commutes with precomposition by an "orthogonal" map (for the dot product), with the inverse appearing on the dual side.

theorem fenchelConjugate_biconjugate_eq_of_closedConvex (n : ℕ) (f : (Fin n → ℝ) → EReal) (hf_closed : LowerSemicontinuous f) (hf_convex : ConvexFunction f) (hf_ne_bot : ∀ (x : Fin n → ℝ), f x ≠ ⊥) : fenchelConjugate n (fenchelConjugate n f) = f

A lower semicontinuous convex function that never takes the value -∞ equals its Fenchel biconjugate.

theorem isSymmetricWrtOrthogonalSet_fenchelConjugate_of_isSymmetricWrtOrthogonalSet (n : ℕ) (G : Set ((Fin n → ℝ) ≃ₗᵢ[ℝ] Fin n → ℝ)) (f : (Fin n → ℝ) → EReal) (hG : ∀ g ∈ G, ∀ (x y : Fin n → ℝ), g x ⬝ᵥ g y = x ⬝ᵥ y) : IsSymmetricWrtOrthogonalSet n G f → IsSymmetricWrtOrthogonalSet n G (fenchelConjugate n f)

If f is invariant under a set G of dot-product-orthogonal maps, then its Fenchel conjugate is invariant under G.

theorem isSymmetricWrtOrthogonalSet_iff_isSymmetricWrtOrthogonalSet_fenchelConjugate (n : ℕ) (G : Set ((Fin n → ℝ) ≃ₗᵢ[ℝ] Fin n → ℝ)) (f : (Fin n → ℝ) → EReal) (hf_closed : LowerSemicontinuous f) (hf_convex : ConvexFunction f) (hf_ne_bot : ∀ (x : Fin n → ℝ), f x ≠ ⊥) (hG : ∀ g ∈ G, ∀ (x y : Fin n → ℝ), g x ⬝ᵥ g y = x ⬝ᵥ y) : IsSymmetricWrtOrthogonalSet n G f ↔ IsSymmetricWrtOrthogonalSet n G (fenchelConjugate n f)

Corollary 12.3.1. A closed convex function f is symmetric with respect to a given set G of orthogonal linear transformations if and only if f* is symmetric with respect to G.

theorem Q_Q'_apply_eq_of_mem_L {n : ℕ} (Q Q' P_L : (Fin n → ℝ) →ₗ[ℝ] Fin n → ℝ) (L : Submodule ℝ (Fin n → ℝ)) (hQQ' : Q ∘ₗ Q' = P_L) (hP_L_id : ∀ xStar ∈ L, P_L xStar = xStar) {xStar : Fin n → ℝ} (hxStar : xStar ∈ L) : Q (Q' xStar) = xStar

If P_L acts as the identity on L and Q ∘ Q' = P_L, then Q (Q' xStar) = xStar on L.

theorem range_term_quadraticHalfLinear_le_on_L {n : ℕ} (Q Q' P_L : (Fin n → ℝ) →ₗ[ℝ] Fin n → ℝ) (L : Submodule ℝ (Fin n → ℝ)) (hQQ' : Q ∘ₗ Q' = P_L) (hP_L_id : ∀ xStar ∈ L, P_L xStar = xStar) (hQsymm : ∀ (x y : Fin n → ℝ), Q x ⬝ᵥ y = x ⬝ᵥ Q y) (hQpsd : ∀ (x : Fin n → ℝ), 0 ≤ x ⬝ᵥ Q x) {xStar : Fin n → ℝ} (hxStar : xStar ∈ L) (x : Fin n → ℝ) : ↑(x ⬝ᵥ xStar) - quadraticHalfLinear n Q x ≤ quadraticHalfLinear n Q' xStar

Completed-square inequality for the range term of the quadratic function x ↦ (1/2) * (x ⬝ᵥ Q x) when xStar ∈ L = range(Q).

theorem fenchelConjugate_quadraticHalfLinear_pseudoinverse (n : ℕ) (Q Q' P_L : (Fin n → ℝ) →ₗ[ℝ] Fin n → ℝ) (L : Submodule ℝ (Fin n → ℝ)) (hL : L = LinearMap.range Q) (hQQ' : Q ∘ₗ Q' = P_L) (_hQ'Q : Q' ∘ₗ Q = P_L) (hP_L_id : ∀ xStar ∈ L, P_L xStar = xStar) (hQsymm : ∀ (x y : Fin n → ℝ), Q x ⬝ᵥ y = x ⬝ᵥ Q y) (hQpsd : ∀ (x : Fin n → ℝ), 0 ≤ x ⬝ᵥ Q x) : fenchelConjugate n (quadraticHalfLinear n Q) = fun (xStar : Fin n → ℝ) => if xStar ∈ L then quadraticHalfLinear n Q' xStar else ⊤

Text 12.3.2: Let Q be a symmetric positive semi-definite n × n matrix and consider the quadratic convex function h(x) = (1/2) * ⟪x, Qx⟫. Let L = range(Q) and let Q' be the Moore–Penrose pseudoinverse, characterized by Q Q' = Q' Q = P_L where P_L is the orthogonal projection onto L. Then the conjugate function h* has the piecewise form h*(x*) = (1/2) * ⟪x*, Q' x*⟫ for x* ∈ L and h*(x*) = +∞ for x* ∉ L. (If Q is nonsingular, then L = ℝ^n and Q' = Q⁻¹.)

def IsPartialQuadraticConvexFunction (n : ℕ) (f : (Fin n → ℝ) → EReal) : Prop

Text 12.3.3: A proper convex function f on ℝ^n is a partial quadratic convex function if it can be written as f = q + δ(· | M), where q is a finite quadratic convex function and M is an affine set. Moreover, f is partial quadratic iff, after an affine change of coordinates, it has the form x ↦ h (A (x - a)) + ⟪x, a*⟫ + α, where h is an elementary partial quadratic convex function, A is a bijective linear map, and a, a* ∈ ℝ^n, α ∈ ℝ.

Equations

• One or more equations did not get rendered due to their size.

def IsElementaryPartialQuadraticConvexFunction (n : ℕ) (h : (Fin n → ℝ) → EReal) : Prop

Text 12.3.3 (elementary model): An elementary partial quadratic convex function is a prototype partial quadratic convex function given by a diagonal quadratic form plus the indicator of a linear subspace.

Equations

• One or more equations did not get rendered due to their size.

theorem exists_mem_affineSubspace_of_proper_of_eq_indicator {n : ℕ} {f r : (Fin n → ℝ) → EReal} {M : AffineSubspace ℝ (Fin n → ℝ)} (hfprop : ProperConvexFunctionOn Set.univ f) (hr_ne_bot : ∀ (x : Fin n → ℝ), r x ≠ ⊥) (hfEq : f = fun (x : Fin n → ℝ) => r x + indicatorFunction (↑M) x) : ∃ (a : Fin n → ℝ), a ∈ M

If a proper convex function can be written as r + δ(· | M), then the affine subspace M must be nonempty. This is extracted by taking a point in the (nonempty) epigraph of f and observing that off M the indicator term forces f = ⊤.

theorem indicatorFunction_affineSubspace_eq_indicator_direction_sub {n : ℕ} (M : AffineSubspace ℝ (Fin n → ℝ)) {a : Fin n → ℝ} (ha : a ∈ M) (x : Fin n → ℝ) : indicatorFunction (↑M) x = indicatorFunction (↑M.direction) (x - a)

Re-center the indicator of an affine subspace at a base point: translating by a ∈ M turns δ(· | M) into the indicator of the direction submodule M.direction.

theorem dotProduct_eq_inner_euclideanSpace (n : ℕ) (x y : Fin n → ℝ) : x ⬝ᵥ y = inner ℝ ((EuclideanSpace.equiv (Fin n) ℝ).symm x) ((EuclideanSpace.equiv (Fin n) ℝ).symm y)

Convert dot products on Fin n → ℝ into inner products on EuclideanSpace ℝ (Fin n) via EuclideanSpace.equiv. This is the bridge that allows the use of spectral-theorem APIs.

theorem linearMap_symmPart_dotProduct_preserves_quadratic {n : ℕ} (Q : (Fin n → ℝ) →ₗ[ℝ] Fin n → ℝ) : ∃ (Qs : (Fin n → ℝ) →ₗ[ℝ] Fin n → ℝ), (∀ (x y : Fin n → ℝ), Qs x ⬝ᵥ y = x ⬝ᵥ Qs y) ∧ ∀ (x : Fin n → ℝ), x ⬝ᵥ Qs x = x ⬝ᵥ Q x

Replace a linear map by its dot-product symmetric part without changing the associated quadratic form x ↦ x ⬝ᵥ Q x. This is implemented by transporting to EuclideanSpace and symmetrizing using the adjoint.

theorem indicatorFunction_submodule_comap_linearEquiv {n : ℕ} (L : Submodule ℝ (Fin n → ℝ)) (A : (Fin n → ℝ) ≃ₗ[ℝ] Fin n → ℝ) (v : Fin n → ℝ) : indicatorFunction (↑(Submodule.comap (↑A) L)) v = indicatorFunction (↑L) (A v)

Transporting an indicator function along a linear equivalence using Submodule.comap.

theorem quadraticHalfLinear_translate_of_dotProduct_symmetric {n : ℕ} (Q : (Fin n → ℝ) →ₗ[ℝ] Fin n → ℝ) (hQsymm : ∀ (x y : Fin n → ℝ), Q x ⬝ᵥ y = x ⬝ᵥ Q y) (a x : Fin n → ℝ) : quadraticHalfLinear n Q x = quadraticHalfLinear n Q (x - a) + ↑(x ⬝ᵥ Q a) + ↑(-(1 / 2) * a ⬝ᵥ Q a)

Translation identity for the quadratic term when Q is symmetric with respect to the dot product. This is the algebraic step used to rewrite a quadratic form in x in terms of x-a, plus a linear term and a constant.

theorem exists_linearEquiv_diagonalize_psd_dotProduct {n : ℕ} (Q : (Fin n → ℝ) →ₗ[ℝ] Fin n → ℝ) (hQsymm : ∀ (x y : Fin n → ℝ), Q x ⬝ᵥ y = x ⬝ᵥ Q y) (hpsd : ∀ (x : Fin n → ℝ), 0 ≤ x ⬝ᵥ Q x) : ∃ (A : (Fin n → ℝ) ≃ₗ[ℝ] Fin n → ℝ) (d : Fin n → ℝ), (∀ (i : Fin n), 0 ≤ d i) ∧ ∀ (x : Fin n → ℝ), x ⬝ᵥ Q x = ∑ i : Fin n, d i * A x i ^ 2

Diagonalize a dot-product symmetric positive semidefinite linear operator on ℝ^n by transporting to EuclideanSpace and applying the spectral theorem.