Constraint polytopes and finite convex decompositions

Adapted for Lean Pool from the Apache-2.0 upstream formalization, with module-system, Mathlib API, and compilation changes.

def OlevskiiGram.constraintPolytope {n : Type u_1} {ι : Type u_2} [Fintype n] (a : ι → n → ℝ) : Set (n → ℝ)

The constraint polytope cut out by the inequalities |⟪x,a_j⟫| ≤ 1.

Equations

• OlevskiiGram.constraintPolytope a = {x : n → ℝ | ∀ (j : ι), |OlevskiiGram.realDot x (a j)| ≤ 1}

def OlevskiiGram.activeConstraintVectors {n : Type u_1} {ι : Type u_2} [Fintype n] (a : ι → n → ℝ) (x : n → ℝ) : Set (n → ℝ)

The vectors whose constraints are active at x.

Equations

• OlevskiiGram.activeConstraintVectors a x = {v : n → ℝ | ∃ (j : ι), v = a j ∧ |OlevskiiGram.realDot x (a j)| = 1}

def OlevskiiGram.activeConstraintSpan {n : Type u_1} {ι : Type u_2} [Fintype n] (a : ι → n → ℝ) (x : n → ℝ) : Submodule ℝ (n → ℝ)

The span of the active constraint vectors at x.

Equations

• OlevskiiGram.activeConstraintSpan a x = Submodule.span ℝ (OlevskiiGram.activeConstraintVectors a x)

noncomputable def OlevskiiGram.activeConstraintIndexSet {n : Type u_1} {ι : Type u_2} [Fintype n] [Fintype ι] (a : ι → n → ℝ) (x : n → ℝ) : Finset ι

The finite set of indices whose constraints are active at x.

Equations

• OlevskiiGram.activeConstraintIndexSet a x = {j : ι | |OlevskiiGram.realDot x (a j)| = 1}

noncomputable def OlevskiiGram.activeConstraintCount {n : Type u_1} {ι : Type u_2} [Fintype n] [Fintype ι] (a : ι → n → ℝ) (x : n → ℝ) : ℕ

The number of active constraints at x.

Equations

• OlevskiiGram.activeConstraintCount a x = (OlevskiiGram.activeConstraintIndexSet a x).card

theorem OlevskiiGram.mem_activeConstraintIndexSet_iff {n : Type u_1} {ι : Type u_2} [Fintype n] [Fintype ι] (a : ι → n → ℝ) (x : n → ℝ) (j : ι) : j ∈ activeConstraintIndexSet a x ↔ |realDot x (a j)| = 1

Membership in the finite active-index set is exactly activity of the constraint.

theorem OlevskiiGram.activeConstraintCount_lt_of_subset_and_new {n : Type u_1} {ι : Type u_2} [Fintype n] [Fintype ι] (a : ι → n → ℝ) (x y : n → ℝ) (hsubset : activeConstraintIndexSet a x ⊆ activeConstraintIndexSet a y) {jNew : ι} (hjOld : jNew ∉ activeConstraintIndexSet a x) (hjNew : jNew ∈ activeConstraintIndexSet a y) : activeConstraintCount a x < activeConstraintCount a y

Adding one genuinely new active index strictly increases the active count.

theorem OlevskiiGram.activeConstraintCount_lt_of_old_active_and_new {n : Type u_1} {ι : Type u_2} [Fintype n] [Fintype ι] (a : ι → n → ℝ) (x y : n → ℝ) {jNew : ι} (hold : ∀ (j : ι), |realDot x (a j)| = 1 → |realDot y (a j)| = 1) (hjOldInactive : |realDot x (a jNew)| ≠ 1) (hjNewActive : |realDot y (a jNew)| = 1) : activeConstraintCount a x < activeConstraintCount a y

If all old active constraints remain active and one inactive constraint becomes active, then the active count strictly increases.

def OlevskiiGram.IsConstraintPolytopeMaximizer {n : Type u_1} {ι : Type u_2} [Fintype n] (a : ι → n → ℝ) (Φ : (n → ℝ) → ℝ) (x : n → ℝ) : Prop

Predicate for a point maximizing Φ on the constraint polytope.

Equations

• OlevskiiGram.IsConstraintPolytopeMaximizer a Φ x = (x ∈ OlevskiiGram.constraintPolytope a ∧ ∀ y ∈ OlevskiiGram.constraintPolytope a, Φ y ≤ Φ x)

theorem OlevskiiGram.realDot_add {ι : Type u_1} [Fintype ι] (x y z : ι → ℝ) : realDot (x + y) z = realDot x z + realDot y z

Linearity of the finite real dot product in its first argument.

theorem OlevskiiGram.realDot_smul {ι : Type u_1} [Fintype ι] (c : ℝ) (x y : ι → ℝ) : realDot (c • x) y = c * realDot x y

Homogeneity of the finite real dot product in its first argument.

theorem OlevskiiGram.realDot_add_right {ι : Type u_1} [Fintype ι] (x y z : ι → ℝ) : realDot x (y + z) = realDot x y + realDot x z

Linearity of the finite real dot product in its second argument.

theorem OlevskiiGram.realDot_smul_right {ι : Type u_1} [Fintype ι] (c : ℝ) (x y : ι → ℝ) : realDot x (c • y) = c * realDot x y

Homogeneity of the finite real dot product in its second argument.

def OlevskiiGram.realDotLinearFunctional {ι : Type u_1} [Fintype ι] (x : ι → ℝ) : (ι → ℝ) →ₗ[ℝ] ℝ

The dot product with a fixed first argument, as a linear functional.

Equations

• OlevskiiGram.realDotLinearFunctional x = { toFun := fun (y : ι → ℝ) => OlevskiiGram.realDot x y, map_add' := ⋯, map_smul' := ⋯ }

theorem OlevskiiGram.realDot_self_eq_zero {ι : Type u_1} [Fintype ι] {x : ι → ℝ} : realDot x x = 0 ↔ x = 0

A vector with zero dot product against itself is zero.

noncomputable def OlevskiiGram.dualRepresenter {ι : Type u_1} (φ : (ι → ℝ) →ₗ[ℝ] ℝ) : ι → ℝ

The coordinate vector representing a linear functional via realDot.

Equations

• OlevskiiGram.dualRepresenter φ i = φ (Pi.single i 1)

theorem OlevskiiGram.realDot_dualRepresenter {ι : Type u_1} [Fintype ι] (φ : (ι → ℝ) →ₗ[ℝ] ℝ) (x : ι → ℝ) : realDot (dualRepresenter φ) x = φ x

Every linear functional on a finite coordinate space is represented by realDot.

theorem OlevskiiGram.dualRepresenter_ne_zero {ι : Type u_1} [Finite ι] {φ : (ι → ℝ) →ₗ[ℝ] ℝ} : φ ≠ 0 → dualRepresenter φ ≠ 0

A nonzero functional has a nonzero realDot representer.

theorem OlevskiiGram.continuous_realDot_left {ι : Type u_1} [Fintype ι] (y : ι → ℝ) : Continuous fun (x : ι → ℝ) => realDot x y

Continuity of the finite real dot product as a function of its first argument.

def OlevskiiGram.constraintLinearMap {n : Type u_1} {ι : Type u_2} [Fintype n] (a : ι → n → ℝ) : (n → ℝ) →ₗ[ℝ] ι → ℝ

The linear map collecting all constraint functionals.

Equations

• OlevskiiGram.constraintLinearMap a = { toFun := fun (x : n → ℝ) (j : ι) => OlevskiiGram.realDot x (a j), map_add' := ⋯, map_smul' := ⋯ }

theorem OlevskiiGram.constraintLinearMap_injective_of_span {n : Type u_1} {ι : Type u_2} [Fintype n] (a : ι → n → ℝ) (hspan : Submodule.span ℝ (Set.range a) = ⊤) : Function.Injective ⇑(constraintLinearMap a)

If the constraint vectors span, then the constraint map is injective.

theorem OlevskiiGram.exists_nonzero_annihilating_activeSpan {n : Type u_1} {ι : Type u_2} [Fintype n] (a : ι → n → ℝ) (x : n → ℝ) (hproper : activeConstraintSpan a x ≠ ⊤) : ∃ (h : n → ℝ), h ≠ 0 ∧ ∀ (j : ι), |realDot x (a j)| = 1 → realDot h (a j) = 0

If the active span is proper, there is a nonzero direction annihilating every active constraint vector under realDot.

theorem OlevskiiGram.activeConstraint_stays_active_along_annihilating_direction {n : Type u_1} {ι : Type u_2} [Fintype n] (a : ι → n → ℝ) (x h : n → ℝ) (hh : ∀ (j : ι), |realDot x (a j)| = 1 → realDot h (a j) = 0) {j : ι} (hj : |realDot x (a j)| = 1) (t : ℝ) : |realDot (x + t • h) (a j)| = 1

Active constraints remain active along a direction annihilating them.

theorem OlevskiiGram.abs_add_mul_le_one_of_abs_lt_one {u v : ℝ} (hu : |u| < 1) : ∃ (δ : ℝ), 0 < δ ∧ ∀ (t : ℝ), |t| ≤ δ → |u + t * v| ≤ 1

A strict scalar inequality has a positive interval of perturbative room.

theorem OlevskiiGram.inactiveConstraint_has_room {n : Type u_1} {ι : Type u_2} [Fintype n] (a : ι → n → ℝ) (x h : n → ℝ) {j : ι} (hj : |realDot x (a j)| < 1) : ∃ (δ : ℝ), 0 < δ ∧ ∀ (t : ℝ), |t| ≤ δ → |realDot (x + t • h) (a j)| ≤ 1

A single inactive constraint has a positive interval of allowed motion.

theorem OlevskiiGram.constraintPolytope_has_local_line_segment {n : Type u_1} {ι : Type u_2} [Fintype n] [Finite ι] (a : ι → n → ℝ) (x h : n → ℝ) (hx : x ∈ constraintPolytope a) (hh : ∀ (j : ι), |realDot x (a j)| = 1 → realDot h (a j) = 0) : ∃ (δ : ℝ), 0 < δ ∧ ∀ (t : ℝ), |t| ≤ δ → x + t • h ∈ constraintPolytope a

If a direction annihilates every active constraint, then a small whole segment around the base point remains in the constraint polytope.

theorem OlevskiiGram.constraintPolytope_zero_mem {n : Type u_1} {ι : Type u_2} [Fintype n] (a : ι → n → ℝ) : 0 ∈ constraintPolytope a

The constraint polytope always contains the origin.

theorem OlevskiiGram.constraintPolytope_isClosed {n : Type u_1} {ι : Type u_2} [Fintype n] (a : ι → n → ℝ) : IsClosed (constraintPolytope a)

The constraint polytope is closed.

theorem OlevskiiGram.constraintPolytope_isBounded {n : Type u_1} {ι : Type u_2} [Fintype n] [Finite ι] (a : ι → n → ℝ) (hspan : Submodule.span ℝ (Set.range a) = ⊤) : Bornology.IsBounded (constraintPolytope a)

Under the spanning hypothesis, the constraint polytope is bounded.

theorem OlevskiiGram.constraintPolytope_isCompact {n : Type u_1} {ι : Type u_2} [Fintype n] [Finite ι] (a : ι → n → ℝ) (hspan : Submodule.span ℝ (Set.range a) = ⊤) : IsCompact (constraintPolytope a)

Under the spanning hypothesis, the constraint polytope is compact.

theorem OlevskiiGram.exists_constraintPolytope_maximizer {n : Type u_1} {ι : Type u_2} [Fintype n] [Finite ι] (a : ι → n → ℝ) (Φ : (n → ℝ) → ℝ) (hspan : Submodule.span ℝ (Set.range a) = ⊤) (hcont : Continuous Φ) : ∃ x₀ ∈ constraintPolytope a, ∀ x ∈ constraintPolytope a, Φ x ≤ Φ x₀

A continuous function on the constraint polytope attains its maximum.

theorem OlevskiiGram.activeConstraintCount_le_card {n : Type u_1} {ι : Type u_2} [Fintype n] [Fintype ι] (a : ι → n → ℝ) (x : n → ℝ) : activeConstraintCount a x ≤ Fintype.card ι

The number of active constraints is bounded by the total number of constraints.

theorem OlevskiiGram.exists_constraintPolytope_maximizer_max_active {n : Type u_1} {ι : Type u_2} [Fintype n] [Fintype ι] (a : ι → n → ℝ) (Φ : (n → ℝ) → ℝ) (hspan : Submodule.span ℝ (Set.range a) = ⊤) (hcont : Continuous Φ) : ∃ (x₀ : n → ℝ), IsConstraintPolytopeMaximizer a Φ x₀ ∧ ∀ (x : n → ℝ), IsConstraintPolytopeMaximizer a Φ x → activeConstraintCount a x ≤ activeConstraintCount a x₀

There is a maximizer whose number of active constraints is maximal.

theorem OlevskiiGram.constraintPolytope_convex {n : Type u_1} {ι : Type u_2} [Fintype n] (a : ι → n → ℝ) : Convex ℝ (constraintPolytope a)

The constraint polytope is convex.

theorem OlevskiiGram.endpoints_are_maximizers_of_convex_combination {n : Type u_1} {ι : Type u_2} [Fintype n] (a : ι → n → ℝ) (Φ : (n → ℝ) → ℝ) {x₀ xPlus xMinus : n → ℝ} {c d : ℝ} (hconv : ConvexOn ℝ (constraintPolytope a) Φ) (hx₀max : IsConstraintPolytopeMaximizer a Φ x₀) (hxPlus : xPlus ∈ constraintPolytope a) (hxMinus : xMinus ∈ constraintPolytope a) (hc : 0 < c) (hd : 0 < d) (hcd : c + d = 1) (hcomb : x₀ = c • xPlus + d • xMinus) : IsConstraintPolytopeMaximizer a Φ xPlus ∧ IsConstraintPolytopeMaximizer a Φ xMinus

If a maximizer is a genuine convex combination of two feasible endpoints, then both endpoints are maximizers.

theorem OlevskiiGram.exists_constraint_not_annihilated_of_span {n : Type u_1} {ι : Type u_2} [Fintype n] (a : ι → n → ℝ) (hspan : Submodule.span ℝ (Set.range a) = ⊤) {h : n → ℝ} (hhne : h ≠ 0) : ∃ (j : ι), realDot h (a j) ≠ 0

Some spanning constraint has nonzero pairing with every nonzero direction.

noncomputable def OlevskiiGram.endpointTimeBound (u v : ℝ) : ℝ

The positive endpoint time for the scalar inequality |u + t v| ≤ 1.

Equations

• OlevskiiGram.endpointTimeBound u v = if 0 < v then (1 - u) / v else (-1 - u) / v

theorem OlevskiiGram.endpointTimeBound_pos {u v : ℝ} (hu : |u| < 1) (hv : v ≠ 0) : 0 < endpointTimeBound u v

For a strictly inactive scalar constraint with nonzero derivative, the endpoint time is positive.

theorem OlevskiiGram.abs_add_mul_le_one_of_le_endpointTimeBound {u v t : ℝ} (hu : |u| ≤ 1) (htnonneg : 0 ≤ t) (htle : t ≤ endpointTimeBound u v) : |u + t * v| ≤ 1

If 0 ≤ t is below the scalar endpoint time, then the corresponding scalar constraint remains feasible.

theorem OlevskiiGram.abs_add_endpointTimeBound_mul_eq_one {u v : ℝ} (hv : v ≠ 0) : |u + endpointTimeBound u v * v| = 1

At the scalar endpoint time, the scalar constraint is active.

theorem OlevskiiGram.activeEndpointWithNewActiveConstraint {n : Type u_1} {ι : Type u_2} [Fintype n] [Finite ι] (a : ι → n → ℝ) (hspan : Submodule.span ℝ (Set.range a) = ⊤) (x₀ h : n → ℝ) : h ≠ 0 → (∀ (j : ι), |realDot x₀ (a j)| = 1 → realDot h (a j) = 0) → ∀ (δ : ℝ), 0 < δ → (∀ (t : ℝ), |t| ≤ δ → x₀ + t • h ∈ constraintPolytope a) → ∃ (xPlus : n → ℝ) (xMinus : n → ℝ) (c : ℝ) (d : ℝ) (jNew : ι), xPlus ∈ constraintPolytope a ∧ xMinus ∈ constraintPolytope a ∧ 0 < c ∧ 0 < d ∧ c + d = 1 ∧ x₀ = c • xPlus + d • xMinus ∧ (∀ (j : ι), |realDot x₀ (a j)| = 1 → |realDot xPlus (a j)| = 1) ∧ |realDot x₀ (a jNew)| ≠ 1 ∧ |realDot xPlus (a jNew)| = 1

Endpoint construction in the active-constraint maximizer lemma.

All compactness, local-motion, and convexity/maximizer consequences have been separated out. This lemma proves the remaining endpoint/geometric part: from a nonzero feasible perturbation direction, one can find feasible endpoints whose convex combination is the base point, all old active constraints remain active at one endpoint, and one genuinely new constraint becomes active there.

theorem OlevskiiGram.activeEndpointWithMoreActiveConstraints {n : Type u_1} {ι : Type u_2} [Fintype n] [Fintype ι] (a : ι → n → ℝ) (hspan : Submodule.span ℝ (Set.range a) = ⊤) (x₀ h : n → ℝ) : h ≠ 0 → (∀ (j : ι), |realDot x₀ (a j)| = 1 → realDot h (a j) = 0) → ∀ (δ : ℝ), 0 < δ → (∀ (t : ℝ), |t| ≤ δ → x₀ + t • h ∈ constraintPolytope a) → ∃ (xPlus : n → ℝ) (xMinus : n → ℝ) (c : ℝ) (d : ℝ), xPlus ∈ constraintPolytope a ∧ xMinus ∈ constraintPolytope a ∧ 0 < c ∧ 0 < d ∧ c + d = 1 ∧ x₀ = c • xPlus + d • xMinus ∧ activeConstraintCount a x₀ < activeConstraintCount a xPlus

The endpoint construction implies the active-count increase used downstream.

theorem OlevskiiGram.activeEndpointContradiction {n : Type u_1} {ι : Type u_2} [Fintype n] [Fintype ι] (a : ι → n → ℝ) (Φ : (n → ℝ) → ℝ) (hspan : Submodule.span ℝ (Set.range a) = ⊤) (hconv : ConvexOn ℝ (constraintPolytope a) Φ) (x₀ : n → ℝ) : IsConstraintPolytopeMaximizer a Φ x₀ → (∀ (x : n → ℝ), IsConstraintPolytopeMaximizer a Φ x → activeConstraintCount a x ≤ activeConstraintCount a x₀) → ∀ (h : n → ℝ), h ≠ 0 → (∀ (j : ι), |realDot x₀ (a j)| = 1 → realDot h (a j) = 0) → ∀ (δ : ℝ), 0 < δ → (∀ (t : ℝ), |t| ≤ δ → x₀ + t • h ∈ constraintPolytope a) → False

Endpoint contradiction after proving the endpoint maximizer fact from convexity.

theorem OlevskiiGram.activePerturbationContradiction {n : Type u_1} {ι : Type u_2} [Fintype n] [Fintype ι] (a : ι → n → ℝ) (Φ : (n → ℝ) → ℝ) (hspan : Submodule.span ℝ (Set.range a) = ⊤) (hconv : ConvexOn ℝ (constraintPolytope a) Φ) (x₀ : n → ℝ) : IsConstraintPolytopeMaximizer a Φ x₀ → (∀ (x : n → ℝ), IsConstraintPolytopeMaximizer a Φ x → activeConstraintCount a x ≤ activeConstraintCount a x₀) → ∀ (h : n → ℝ), h ≠ 0 → (∀ (j : ι), |realDot x₀ (a j)| = 1 → realDot h (a j) = 0) → False

The perturbation contradiction, reduced to the endpoint part after proving there is positive room to move inside the polytope.

theorem OlevskiiGram.activeSpanTopOfMaximalActiveMaximizer {n : Type u_1} {ι : Type u_2} [Fintype n] [Fintype ι] (a : ι → n → ℝ) (Φ : (n → ℝ) → ℝ) (hspan : Submodule.span ℝ (Set.range a) = ⊤) (hconv : ConvexOn ℝ (constraintPolytope a) Φ) (x₀ : n → ℝ) : IsConstraintPolytopeMaximizer a Φ x₀ → (∀ (x : n → ℝ), IsConstraintPolytopeMaximizer a Φ x → activeConstraintCount a x ≤ activeConstraintCount a x₀) → activeConstraintSpan a x₀ = ⊤

A maximal-active-cardinality maximizer has full active span via the endpoint perturbation argument.

theorem OlevskiiGram.activeConstraintMaximizer {n : Type u_1} {ι : Type u_2} [Fintype n] [Finite ι] (a : ι → n → ℝ) (Φ : (n → ℝ) → ℝ) (hspan : Submodule.span ℝ (Set.range a) = ⊤) (hcont : Continuous Φ) (hconv : ConvexOn ℝ (constraintPolytope a) Φ) : ∃ x₀ ∈ constraintPolytope a, (∀ x ∈ constraintPolytope a, Φ x ≤ Φ x₀) ∧ activeConstraintSpan a x₀ = ⊤

The active-constraint maximizer lemma, proved using the perturbation argument.

theorem OlevskiiGram.supportFunctionSeparation {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (K L : Set V) (hKcpt : IsCompact K) (hLcpt : IsCompact L) (hLconv : Convex ℝ L) (hLnonempty : L.Nonempty) (hsupport : ∀ (a : V), sSup ((fun (x : V) => inner ℝ a x) '' K) ≤ sSup ((fun (y : V) => inner ℝ a y) '' L)) : K ⊆ L

A compact set lies in a nonempty compact convex set when its support function is smaller.

theorem OlevskiiGram.realMatrix_star_eq_transpose {n : Type u_1} (A : Matrix n n ℝ) : star A = A.transpose

Over the real numbers, matrix star is just transpose.

theorem OlevskiiGram.matrixInner_eq_trace_transpose_mul {n : Type u_1} [Fintype n] [DecidableEq n] (A G : Matrix n n ℝ) : inner ℝ A G = (A.transpose * G).trace

For the matrix inner product induced by the identity positive matrix, the Frobenius pairing is the trace pairing against the transpose.

theorem OlevskiiGram.matrixInner_realRankOne_eq_realQuadraticForm {n : Type u_1} [Fintype n] [DecidableEq n] (A : Matrix n n ℝ) (q : n → ℝ) : inner ℝ A (realRankOne q) = realQuadraticForm A q

The Frobenius support value of a rank-one cube matrix is the associated quadratic form.

noncomputable def OlevskiiGram.realSymmPart {d : Type u_1} (A : Matrix d d ℝ) : Matrix d d ℝ

The symmetric part of a real square matrix.

Equations

• OlevskiiGram.realSymmPart A i j = (A i j + A j i) / 2

def OlevskiiGram.realRankOneCubeSet (d : Type u_1) : Set (Matrix d d ℝ)

Rank-one cube matrices, as a subset of the ambient real matrix space.

Equations

• OlevskiiGram.realRankOneCubeSet d = {R : Matrix d d ℝ | ∃ (q : d → ℝ), OlevskiiGram.InRealUnitCube q ∧ R = OlevskiiGram.realRankOne q}

def OlevskiiGram.matrixToEuclidean {d : Type u_1} (A : Matrix d d ℝ) : EuclideanSpace ℝ (d × d)

Flatten a matrix into the Euclidean coordinate space indexed by pairs.

Equations

• OlevskiiGram.matrixToEuclidean A = WithLp.toLp 2 fun (ij : d × d) => A ij.1 ij.2

def OlevskiiGram.euclideanToMatrix {d : Type u_1} (v : EuclideanSpace ℝ (d × d)) : Matrix d d ℝ

Unflatten a Euclidean vector indexed by pairs into a matrix.

Equations

• OlevskiiGram.euclideanToMatrix v i j = v.ofLp (i, j)

def OlevskiiGram.realRankOneCubeEuclideanSet (d : Type u_1) : Set (EuclideanSpace ℝ (d × d))

Rank-one cube matrices, flattened into Euclidean space.

Equations

• OlevskiiGram.realRankOneCubeEuclideanSet d = (fun (A : Matrix d d ℝ) => OlevskiiGram.matrixToEuclidean A) '' OlevskiiGram.realRankOneCubeSet d

theorem OlevskiiGram.isCompact_realUnitCube {d : Type u_1} : IsCompact {q : d → ℝ | InRealUnitCube q}

The coordinate cube [-1,1]^d is compact.

theorem OlevskiiGram.continuous_matrixToEuclidean_realRankOne {d : Type u_1} : Continuous fun (q : d → ℝ) => matrixToEuclidean (realRankOne q)

The rank-one flattening map is continuous on the real cube ambient space.

theorem OlevskiiGram.isCompact_realRankOneCubeEuclideanSet {d : Type u_1} : IsCompact (realRankOneCubeEuclideanSet d)

The flattened rank-one cube image is compact.

def OlevskiiGram.barycentricImageSet {E : Type u_1} [AddCommMonoid E] [Module ℝ E] (s : Set E) (k : ℕ) : Set E

The set of barycentres of k points of s, with weights in the standard simplex.

Equations

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

def OlevskiiGram.finiteBarycentricHull {E : Type u_1} [AddCommGroup E] [Module ℝ E] (s : Set E) : Set E

A finite-dimensional Caratheodory-sized union of barycentric images.

Equations

• OlevskiiGram.finiteBarycentricHull s = ⋃ (k : Fin (Module.finrank ℝ E + 2)), OlevskiiGram.barycentricImageSet s ↑k

theorem OlevskiiGram.isCompact_barycentricImageSet {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} (hs : IsCompact s) (k : ℕ) : IsCompact (barycentricImageSet s k)

Barycentric images of compact sets are compact.

theorem OlevskiiGram.mem_barycentricImageSet_of_finset_convexHull {E : Type u_1} [AddCommGroup E] [Module ℝ E] {s : Set E} {t : Finset E} {x : E} (hts : ↑t ⊆ s) (hx : x ∈ (convexHull ℝ) ↑t) : x ∈ barycentricImageSet s (Fintype.card ↥t)

Membership in the convex hull of a finite subset gives an explicit barycentric image point.

theorem OlevskiiGram.convexHull_eq_finiteBarycentricHull {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (s : Set E) : (convexHull ℝ) s = finiteBarycentricHull s

In finite dimension, the convex hull is the Caratheodory-sized barycentric union.

theorem OlevskiiGram.isCompact_convexHull_of_isCompact {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} (hs : IsCompact s) : IsCompact ((convexHull ℝ) s)

The convex hull of a compact set in finite-dimensional real space is compact.

theorem OlevskiiGram.isClosed_convexHull_of_isCompact {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} (hs : IsCompact s) : IsClosed ((convexHull ℝ) s)

The convex hull of a compact set in finite-dimensional real space is closed.

theorem OlevskiiGram.closedConvexHull_eq_convexHull_of_isCompact {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} (hs : IsCompact s) : (closedConvexHull ℝ) s = (convexHull ℝ) s

For compact sets in finite dimension, closed convex hull equals convex hull.

theorem OlevskiiGram.euclideanToMatrix_matrixToEuclidean {d : Type u_1} (A : Matrix d d ℝ) : euclideanToMatrix (matrixToEuclidean A) = A

Flattening and then unflattening a matrix gives the original matrix.

theorem OlevskiiGram.matrixToEuclidean_euclideanToMatrix {d : Type u_1} (v : EuclideanSpace ℝ (d × d)) : matrixToEuclidean (euclideanToMatrix v) = v

Unflattening and then flattening a Euclidean matrix-vector gives the original vector.

theorem OlevskiiGram.realSymmetric_realSymmPart {d : Type u_1} (A : Matrix d d ℝ) : RealSymmetric (realSymmPart A)

The symmetric part is symmetric.

theorem OlevskiiGram.realSymmetric_realRankOne {d : Type u_1} (q : d → ℝ) : RealSymmetric (realRankOne q)

Rank-one real matrices are symmetric.

theorem OlevskiiGram.trace_mul_eq_trace_transpose_mul_of_realSymmetric_right {d : Type u_1} [Fintype d] (A T : Matrix d d ℝ) (hT : RealSymmetric T) : (A * T).trace = (A.transpose * T).trace

Against a symmetric right factor, A and Aᵀ have the same trace pairing.

theorem OlevskiiGram.trace_realSymmPart_mul_eq_average {d : Type u_1} [Fintype d] (A T : Matrix d d ℝ) : (realSymmPart A * T).trace = ((A * T).trace + (A.transpose * T).trace) / 2

The trace pairing with the symmetric part is the average of the two trace pairings.

theorem OlevskiiGram.trace_transpose_mul_eq_trace_realSymmPart_mul_of_realSymmetric {d : Type u_1} [Fintype d] (A T : Matrix d d ℝ) (hT : RealSymmetric T) : (A.transpose * T).trace = (realSymmPart A * T).trace

A symmetric right factor only sees the symmetric part of the left factor.

theorem OlevskiiGram.realQuadraticForm_transpose {d : Type u_1} [Fintype d] (A : Matrix d d ℝ) (q : d → ℝ) : realQuadraticForm A.transpose q = realQuadraticForm A q

The quadratic form of a transpose agrees with the original quadratic form.

theorem OlevskiiGram.realQuadraticForm_realSymmPart_eq_average {d : Type u_1} [Fintype d] (A : Matrix d d ℝ) (q : d → ℝ) : realQuadraticForm (realSymmPart A) q = (realQuadraticForm A q + realQuadraticForm A.transpose q) / 2

The quadratic form of the symmetric part is the average of the two transpose forms.

theorem OlevskiiGram.realQuadraticForm_realSymmPart {d : Type u_1} [Fintype d] (A : Matrix d d ℝ) (q : d → ℝ) : realQuadraticForm (realSymmPart A) q = realQuadraticForm A q

Quadratic forms only see the symmetric part of a real matrix.

theorem OlevskiiGram.inner_matrixToEuclidean_eq_trace_transpose_mul {d : Type u_1} [Fintype d] (A T : Matrix d d ℝ) : inner ℝ (matrixToEuclidean A) (matrixToEuclidean T) = (A.transpose * T).trace

The Euclidean inner product of flattened matrices is the trace pairing.

theorem OlevskiiGram.inner_matrixToEuclidean_realRankOne_eq_realQuadraticForm {d : Type u_1} [Fintype d] (A : Matrix d d ℝ) (q : d → ℝ) : inner ℝ (matrixToEuclidean A) (matrixToEuclidean (realRankOne q)) = realQuadraticForm A q

The flattened support value of a rank-one matrix is the quadratic form.

theorem OlevskiiGram.realSymmetric_isHermitian {n : Type u_1} (A : Matrix n n ℝ) : RealSymmetric A → A.IsHermitian

A real symmetric matrix is Hermitian in Mathlib's matrix sense.

theorem OlevskiiGram.realSymmetric_of_isHermitian {n : Type u_1} (A : Matrix n n ℝ) : A.IsHermitian → RealSymmetric A

A real Hermitian matrix is symmetric in entrywise real coordinates.

theorem OlevskiiGram.realSymmetric_cfc {n : Type u_1} [Fintype n] [DecidableEq n] (A : Matrix n n ℝ) (hSym : RealSymmetric A) (f : ℝ → ℝ) : RealSymmetric (⋯.cfc f)

The explicit Hermitian matrix functional calculus preserves real symmetry.

theorem OlevskiiGram.realPSD_posSemidef {n : Type u_1} [Fintype n] (A : Matrix n n ℝ) : RealSymmetric A → RealPSD A → A.PosSemidef

The real quadratic-form PSD predicate implies Mathlib's matrix PSD predicate.

theorem OlevskiiGram.realPSD_of_posSemidef {n : Type u_1} [Fintype n] (A : Matrix n n ℝ) : A.PosSemidef → RealPSD A

Mathlib's matrix PSD predicate implies nonnegativity of the real quadratic form.

theorem OlevskiiGram.realPSD_cfc_of_nonneg_spectrum {n : Type u_1} [Fintype n] [DecidableEq n] (A : Matrix n n ℝ) (hSym : RealSymmetric A) (f : ℝ → ℝ) (hf : ∀ x ∈ spectrum ℝ A, 0 ≤ f x) : RealPSD (⋯.cfc f)

If a real function is nonnegative on the spectrum, its Hermitian matrix functional calculus is positive semidefinite in the project's quadratic-form sense.

theorem OlevskiiGram.trace_cfc_eq_sum_eigenvalues {n : Type u_1} [Fintype n] [DecidableEq n] (A : Matrix n n ℝ) (hA : A.IsHermitian) (f : ℝ → ℝ) : (hA.cfc f).trace = ∑ i : n, f (hA.eigenvalues i)

Trace of the explicit Hermitian matrix functional calculus.

theorem OlevskiiGram.posPart_eq_cfc_posPart {n : Type u_1} [Fintype n] [DecidableEq n] (A : Matrix n n ℝ) (hA : A.IsHermitian) : A⁺ = hA.cfc fun (x : ℝ) => x⁺

Mathlib's CFC positive part agrees with the explicit Hermitian matrix cfc.

theorem OlevskiiGram.trace_posPart_eq_sum_posPart_eigenvalues {n : Type u_1} [Fintype n] [DecidableEq n] (A : Matrix n n ℝ) (hA : A.IsHermitian) : A⁺.trace = ∑ i : n, (hA.eigenvalues i)⁺

Trace of the CFC positive part as the sum of positive eigenvalue parts.

theorem OlevskiiGram.trace_posPart_eq_sum_eigenvalues₀ {n : Type u_1} [Fintype n] [DecidableEq n] (A : Matrix n n ℝ) (hSym : RealSymmetric A) : A⁺.trace = ∑ i : Fin (Fintype.card n), (⋯.eigenvalues₀ i)⁺

Trace of the CFC positive part, indexed by Mathlib's canonical sorted eigenvalue list.

theorem OlevskiiGram.realSymmetric_one {n : Type u_1} [DecidableEq n] : RealSymmetric 1

The identity matrix is real symmetric.

theorem OlevskiiGram.realSymmetric_one_sub {n : Type u_1} [DecidableEq n] (G : Matrix n n ℝ) : RealSymmetric G → RealSymmetric (1 - G)

Symmetry is preserved by subtracting from the identity.

theorem OlevskiiGram.realPSD_zero {n : Type u_1} [Fintype n] : RealPSD 0

The zero matrix is real positive semidefinite.

theorem OlevskiiGram.realPSD_one {n : Type u_1} [Fintype n] [DecidableEq n] : RealPSD 1

The identity matrix is real positive semidefinite.

theorem OlevskiiGram.realLoewnerBetweenZeroAndOne_one {n : Type u_1} [Fintype n] [DecidableEq n] : RealLoewnerBetweenZeroAndOne 1

The identity matrix satisfies 0 ≤ I ≤ I.

theorem OlevskiiGram.positiveSemidefinite_trace_mul_nonneg {n : Type u_1} [Fintype n] (B C : Matrix n n ℝ) : RealSymmetric B → RealSymmetric C → RealPSD B → RealPSD C → 0 ≤ (B * C).trace

The trace of a product of two real PSD matrices is nonnegative.

theorem OlevskiiGram.trace_mul_realConvexCombination {n : Type u_1} [Fintype n] {m : ℕ} (A G : Matrix n n ℝ) (p : Fin m → ℝ) (q : Fin m → n → ℝ) (hentry : ∀ (a b : n), G a b = ∑ r : Fin m, p r * q r a * q r b) : (A * G).trace = ∑ r : Fin m, p r * realQuadraticForm A (q r)

Trace pairing with a finite convex combination of rank-one matrices.

def OlevskiiGram.HasPositivePartSupportFunction {n : Type u_1} [Fintype n] [DecidableEq n] (A Apos : Matrix n n ℝ) : Prop

The support-function property expected from the positive spectral part of A.

For the paper proof, Apos is instantiated as the positive spectral part of A; this predicate packages the required support-function property.

Equations

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

theorem OlevskiiGram.hasPositivePartSupportFunction_of_realPSD {n : Type u_1} [Fintype n] [DecidableEq n] (A : Matrix n n ℝ) : RealSymmetric A → RealPSD A → HasPositivePartSupportFunction A A

For a positive semidefinite test matrix, the support function over 0 ≤ G ≤ I is attained at G = I.

theorem OlevskiiGram.supportUpperBound_of_posNegDecomposition {n : Type u_1} [Fintype n] [DecidableEq n] (A Apos Aneg : Matrix n n ℝ) (hAeq : A = Apos - Aneg) (hAposSym : RealSymmetric Apos) (hAnegSym : RealSymmetric Aneg) (hAposPSD : RealPSD Apos) (hAnegPSD : RealPSD Aneg) (G : Matrix n n ℝ) : RealSymmetric G → RealLoewnerBetweenZeroAndOne G → (A * G).trace ≤ Apos.trace

Upper-bound half of the positive/negative spectral-part support-function argument. This is enough for the convex-hull separation proof once Ball--Prodromou supplies a cube vector with quadratic value at least Apos.trace.

theorem OlevskiiGram.supportUpperBound_cfc_posPart {n : Type u_1} [Fintype n] [DecidableEq n] (A : Matrix n n ℝ) (hSym : RealSymmetric A) (G : Matrix n n ℝ) : RealSymmetric G → RealLoewnerBetweenZeroAndOne G → (A * G).trace ≤ A⁺.trace

For a real symmetric matrix, Mathlib's CFC positive part gives the support upper bound over the Loewner interval 0 ≤ G ≤ I.

theorem OlevskiiGram.hasPositivePartSupportFunction_of_posNegProjection {n : Type u_1} [Fintype n] [DecidableEq n] (A Apos Aneg Ppos : Matrix n n ℝ) (hAeq : A = Apos - Aneg) (hAposSym : RealSymmetric Apos) (hAnegSym : RealSymmetric Aneg) (hAposPSD : RealPSD Apos) (hAnegPSD : RealPSD Aneg) (hPposSym : RealSymmetric Ppos) (hPposBetween : RealLoewnerBetweenZeroAndOne Ppos) (hApos_mul_Ppos : Apos * Ppos = Apos) (hAneg_mul_Ppos : Aneg * Ppos = 0) : HasPositivePartSupportFunction A Apos

Abstract positive/negative spectral-part criterion for the support-function property. The remaining spectral task is to provide Apos, Aneg, and Ppos satisfying these hypotheses for a real symmetric matrix A.

def OlevskiiGram.HasRealConvexDecomposition (d : Type u_1) [Fintype d] [DecidableEq d] : Prop

The real convex-decomposition theorem as an explicit property.

This packages the substantial mathematical statement that every real symmetric matrix with 0 ≤ T ≤ I should be a finite convex combination of rank-one matrices q qᵀ with q ∈ [-1,1]^d. It is established below by hasRealConvexDecomposition.

Equations

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

theorem OlevskiiGram.cubeQuadraticMaximum {n : Type u_1} [Fintype n] [DecidableEq n] (A Apos : Matrix n n ℝ) : HasRealConvexDecomposition n → HasPositivePartSupportFunction A Apos → ∃ (x : n → ℝ), InRealUnitCube x ∧ Apos.trace ≤ realQuadraticForm A x

The cube quadratic maximum follows from the support-function maximizer and the real convex decomposition.