The Ball--Prodromou cube quadratic maximum

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

theorem OlevskiiGram.parsevalFrame_span_top {n : Type u_1} {ι : Type u_2} [Fintype n] [Fintype ι] (u : ι → n → ℝ) (hparseval : ∀ (x : n → ℝ) (i : n), ∑ j : ι, realDot x (u j) * u j i = x i) : Submodule.span ℝ (Set.range u) = ⊤

A Parseval family spans the whole coordinate space. This is the frame identity used in the Ball--Prodromou proof.

theorem OlevskiiGram.parsevalFrame_realDot_self {n : Type u_1} {ι : Type u_2} [Fintype n] [Fintype ι] (u : ι → n → ℝ) (hparseval : ∀ (x : n → ℝ) (i : n), ∑ j : ι, realDot x (u j) * u j i = x i) (x : n → ℝ) : realDot x x = ∑ j : ι, realDot x (u j) ^ 2

Parseval identity for the squared norm expressed using realDot.

theorem OlevskiiGram.activeConstraintCount_ge_card_of_span_top {n : Type u_1} {ι : Type u_2} [Fintype n] [Fintype ι] (u : ι → n → ℝ) (x : n → ℝ) (hspan : activeConstraintSpan u x = ⊤) : Fintype.card n ≤ activeConstraintCount u x

If the active constraints span the whole coordinate space, then at least dim constraints are active.

theorem OlevskiiGram.activeConstraint_sum_sq_eq_count {n : Type u_1} {ι : Type u_2} [Fintype n] [Fintype ι] (u : ι → n → ℝ) (x : n → ℝ) : ∑ j ∈ activeConstraintIndexSet u x, realDot x (u j) ^ 2 = ↑(activeConstraintCount u x)

On the active set, the squared frame coefficients sum to the active count.

theorem OlevskiiGram.parsevalFrame_active_norm_lower {n : Type u_1} {ι : Type u_2} [Fintype n] [Fintype ι] (u : ι → n → ℝ) (hparseval : ∀ (x : n → ℝ) (i : n), ∑ j : ι, realDot x (u j) * u j i = x i) (x : n → ℝ) (hspan : activeConstraintSpan u x = ⊤) : ↑(Fintype.card n) ≤ realDot x x

The norm-lower step in Ball--Prodromou: a Parseval family and a point whose active constraints span force dim ≤ ‖x‖².

theorem OlevskiiGram.exists_parseval_polytope_point_norm_ge_card {n : Type u_1} {ι : Type u_2} [Fintype n] [Fintype ι] (u : ι → n → ℝ) (hparseval : ∀ (x : n → ℝ) (i : n), ∑ j : ι, realDot x (u j) * u j i = x i) : ∃ (w : n → ℝ), (∀ (j : ι), |realDot w (u j)| ≤ 1) ∧ ↑(Fintype.card n) ≤ realDot w w

Existence form of the Ball--Prodromou norm-lower step. This is obtained from the active-constraint maximizer already proved in RealConvex.lean.

def OlevskiiGram.weightedSquareSum {n : Type u_1} [Fintype n] (c x : n → ℝ) : ℝ

Weighted diagonal quadratic form used for the Ball--Prodromou functions Φ_m.

Equations

• OlevskiiGram.weightedSquareSum c x = ∑ i : n, c i * x i ^ 2

theorem OlevskiiGram.continuous_weightedSquareSum {n : Type u_1} [Fintype n] (c : n → ℝ) : Continuous (weightedSquareSum c)

The finite weighted diagonal quadratic form is continuous.

theorem OlevskiiGram.convexOn_weightedSquareSum_nonneg {n : Type u_1} [Fintype n] (c : n → ℝ) (hc : ∀ (i : n), 0 ≤ c i) : ConvexOn ℝ Set.univ (weightedSquareSum c)

A weighted diagonal quadratic form with nonnegative weights is convex.

theorem OlevskiiGram.convexOn_constraintPolytope_weightedSquareSum_nonneg {n : Type u_1} {ι : Type u_2} [Fintype n] (u : ι → n → ℝ) (c : n → ℝ) (hc : ∀ (i : n), 0 ≤ c i) : ConvexOn ℝ (constraintPolytope u) (weightedSquareSum c)

The same convexity statement restricted to a constraint polytope, in the exact shape needed by activeConstraintMaximizer.

theorem OlevskiiGram.exists_parseval_weightedSquareSum_maximizer {n : Type u_1} {ι : Type u_2} [Fintype n] [Fintype ι] (u : ι → n → ℝ) (hparseval : ∀ (x : n → ℝ) (i : n), ∑ j : ι, realDot x (u j) * u j i = x i) (c : n → ℝ) (hc : ∀ (i : n), 0 ≤ c i) : ∃ w ∈ constraintPolytope u, (∀ y ∈ constraintPolytope u, weightedSquareSum c y ≤ weightedSquareSum c w) ∧ activeConstraintSpan u w = ⊤ ∧ ↑(Fintype.card n) ≤ realDot w w

For a Parseval family, every nonnegative weighted diagonal quadratic has a maximizer on the constraint polytope whose active constraints span and whose norm has the Ball--Prodromou lower bound.

def OlevskiiGram.bpPhiWeights (s : ℕ → ℝ) (m : ℕ) : Fin (m + 1) → ℝ

The coefficient vector for the Ball--Prodromou functional Φ_m(x) = ∑_{i<m} (s_i - s_m) x_i^2 on Fin (m+1).

Equations

• OlevskiiGram.bpPhiWeights s m i = if ↑i < m then s ↑i - s m else 0

theorem OlevskiiGram.bpPhiWeights_nonneg (s : ℕ → ℝ) (m : ℕ) (hmono : ∀ i < m, s m ≤ s i) (i : Fin (m + 1)) : 0 ≤ bpPhiWeights s m i

The Ball--Prodromou coefficient vector is nonnegative under eigenvalue monotonicity.

theorem OlevskiiGram.bpPhiWeights_last (s : ℕ → ℝ) (m : ℕ) : bpPhiWeights s m ⟨m, ⋯⟩ = 0

The last coefficient in bpPhiWeights is zero.

theorem OlevskiiGram.bpPhiWeights_of_lt (s : ℕ → ℝ) {i m : ℕ} (hi : i < m) : bpPhiWeights s m ⟨i, ⋯⟩ = s i - s m

A coefficient before the last index has the expected spectral-gap value.

theorem OlevskiiGram.exists_bpPhiMaximizer {m : ℕ} {ι : Type u_1} [Fintype ι] (u : ι → Fin (m + 1) → ℝ) (hparseval : ∀ (x : Fin (m + 1) → ℝ) (i : Fin (m + 1)), ∑ j : ι, realDot x (u j) * u j i = x i) (s : ℕ → ℝ) (hmono : ∀ i < m, s m ≤ s i) : ∃ w ∈ constraintPolytope u, (∀ y ∈ constraintPolytope u, weightedSquareSum (bpPhiWeights s m) y ≤ weightedSquareSum (bpPhiWeights s m) w) ∧ activeConstraintSpan u w = ⊤ ∧ ↑(m + 1) ≤ realDot w w

The active-constraint maximizer specialized to the Ball--Prodromou functional on Fin (m+1).

theorem OlevskiiGram.realDot_self_fin_eq_sum_univ {n : ℕ} (x : Fin n → ℝ) : realDot x x = ∑ i : Fin n, x i ^ 2

Coordinate form of realDot x x on Fin n.

theorem OlevskiiGram.weightedSquareSum_bpPhiWeights (s : ℕ → ℝ) (m : ℕ) (x : Fin (m + 1) → ℝ) : weightedSquareSum (bpPhiWeights s m) x = ∑ i : Fin m, (s ↑i - s m) * x i.castSucc ^ 2

bpPhiWeights turns weightedSquareSum into the expected prefix sum.

def OlevskiiGram.dropLastConstraints {ι : Type u_1} {m : ℕ} (u : ι → Fin (m + 1) → ℝ) : ι → Fin m → ℝ

Drop the last coordinate from each constraint vector.

Equations

• OlevskiiGram.dropLastConstraints u j i = u j i.castSucc

def OlevskiiGram.extendByZero {m : ℕ} (x : Fin m → ℝ) : Fin (m + 1) → ℝ

Extend a vector by a zero final coordinate.

Equations

• OlevskiiGram.extendByZero x = Fin.snoc x 0

@[simp]

theorem OlevskiiGram.extendByZero_castSucc {m : ℕ} (x : Fin m → ℝ) (i : Fin m) : extendByZero x i.castSucc = x i

@[simp]

theorem OlevskiiGram.extendByZero_last {m : ℕ} (x : Fin m → ℝ) : extendByZero x (Fin.last m) = 0

theorem OlevskiiGram.weightedSquareSum_bpPhiWeights_extendByZero (s : ℕ → ℝ) (m : ℕ) (x : Fin m → ℝ) : weightedSquareSum (bpPhiWeights s m) (extendByZero x) = ∑ i : Fin m, (s ↑i - s m) * x i ^ 2

The previous Ball--Prodromou functional evaluated on a zero-extension.

theorem OlevskiiGram.realDot_extendByZero_dropLastConstraints {ι : Type u_1} {m : ℕ} (u : ι → Fin (m + 1) → ℝ) (x : Fin m → ℝ) (j : ι) : realDot (extendByZero x) (u j) = realDot x (dropLastConstraints u j)

The dot product of a zero-extension with a full constraint vector is the dot product against the truncated constraint vector.

theorem OlevskiiGram.parseval_dropLastConstraints {ι : Type u_1} [Fintype ι] {m : ℕ} (u : ι → Fin (m + 1) → ℝ) (hparseval : ∀ (x : Fin (m + 1) → ℝ) (i : Fin (m + 1)), ∑ j : ι, realDot x (u j) * u j i = x i) (x : Fin m → ℝ) (i : Fin m) : ∑ j : ι, realDot x (dropLastConstraints u j) * dropLastConstraints u j i = x i

Truncating the final coordinate preserves the Parseval identity.

theorem OlevskiiGram.extendByZero_mem_constraintPolytope {ι : Type u_1} {m : ℕ} (u : ι → Fin (m + 1) → ℝ) {x : Fin m → ℝ} (hx : x ∈ constraintPolytope (dropLastConstraints u)) : extendByZero x ∈ constraintPolytope u

The TeX inclusion C_{m-1} ⊆ C_m: a feasible point for the truncated constraints remains feasible after adding a zero last coordinate.

theorem OlevskiiGram.bpPhi_maximizer_comparison_dropLast {ι : Type u_1} {m : ℕ} (u : ι → Fin (m + 1) → ℝ) (s : ℕ → ℝ) {wCur : Fin (m + 1) → ℝ} {wPrev : Fin m → ℝ} (hmax : ∀ y ∈ constraintPolytope u, weightedSquareSum (bpPhiWeights s m) y ≤ weightedSquareSum (bpPhiWeights s m) wCur) (hPrev : wPrev ∈ constraintPolytope (dropLastConstraints u)) : weightedSquareSum (bpPhiWeights s m) (extendByZero wPrev) ≤ weightedSquareSum (bpPhiWeights s m) wCur

The maximizer comparison used in the Ball--Prodromou induction: a maximizer on C_m dominates the zero-extension of any feasible point from C_{m-1}.

theorem OlevskiiGram.bpPhi_maximizer_comparison_dropLast_sum {ι : Type u_1} {m : ℕ} (u : ι → Fin (m + 1) → ℝ) (s : ℕ → ℝ) {wCur : Fin (m + 1) → ℝ} {wPrev : Fin m → ℝ} (hmax : ∀ y ∈ constraintPolytope u, weightedSquareSum (bpPhiWeights s m) y ≤ weightedSquareSum (bpPhiWeights s m) wCur) (hPrev : wPrev ∈ constraintPolytope (dropLastConstraints u)) : ∑ i : Fin m, (s ↑i - s m) * wPrev i ^ 2 ≤ ∑ i : Fin m, (s ↑i - s m) * wCur i.castSucc ^ 2

The same comparison in explicit coordinate-sum form: ∑_{i<m} (s_i-s_m) wPrev_i^2 ≤ ∑_{i<m} (s_i-s_m) wCur_i^2.

theorem OlevskiiGram.bp_induction_lhs_identity (s y : ℕ → ℝ) (m : ℕ) : ∑ i ∈ Finset.range (m + 1), (s i - s (m + 1)) * y i ^ 2 = ∑ i ∈ Finset.range m, (s i - s m) * y i ^ 2 + (s m - s (m + 1)) * ∑ i ∈ Finset.range (m + 1), y i ^ 2

Algebraic identity behind the Ball--Prodromou induction step, left-hand side. It rewrites the next weighted quadratic sum as the previous weights plus the new spectral gap times the full squared norm.

theorem OlevskiiGram.bp_induction_rhs_identity (s : ℕ → ℝ) (m : ℕ) : ∑ i ∈ Finset.range (m + 1), (s i - s (m + 1)) = ∑ i ∈ Finset.range m, (s i - s m) + (s m - s (m + 1)) * (↑m + 1)

Algebraic identity behind the Ball--Prodromou induction step, right-hand side.

theorem OlevskiiGram.bp_induction_lhs_identity_fin (s : ℕ → ℝ) {m : ℕ} (x : Fin (m + 1) → ℝ) : ∑ i : Fin (m + 1), (s ↑i - s (m + 1)) * x i ^ 2 = ∑ i : Fin m, (s ↑i - s m) * x i.castSucc ^ 2 + (s m - s (m + 1)) * ∑ i : Fin (m + 1), x i ^ 2

Fin-indexed version of the Ball--Prodromou left-hand induction identity.

theorem OlevskiiGram.bp_induction_rhs_identity_fin (s : ℕ → ℝ) (m : ℕ) : ∑ i : Fin (m + 1), (s ↑i - s (m + 1)) = ∑ i : Fin m, (s ↑i - s m) + (s m - s (m + 1)) * (↑m + 1)

Fin-indexed version of the Ball--Prodromou right-hand induction identity.

theorem OlevskiiGram.bp_induction_step (s xPrev xCur : ℕ → ℝ) (m : ℕ) (hmax : ∑ i ∈ Finset.range m, (s i - s m) * xCur i ^ 2 ≥ ∑ i ∈ Finset.range m, (s i - s m) * xPrev i ^ 2) (hprev : ∑ i ∈ Finset.range m, (s i - s m) * xPrev i ^ 2 ≥ ∑ i ∈ Finset.range m, (s i - s m)) (hnorm : ↑m + 1 ≤ ∑ i ∈ Finset.range (m + 1), xCur i ^ 2) (hgap : 0 ≤ s m - s (m + 1)) : ∑ i ∈ Finset.range (m + 1), (s i - s (m + 1)) * xCur i ^ 2 ≥ ∑ i ∈ Finset.range (m + 1), (s i - s (m + 1))

One numerical step in the Ball--Prodromou induction.

The hypotheses correspond exactly to the TeX proof:

• the maximizer comparison for Φ_m;
• the induction hypothesis at level m;
• the norm-lower estimate for the current maximizer;
• nonnegativity of the spectral gap s_m - s_{m+1}.

theorem OlevskiiGram.bp_induction_step_fin (s : ℕ → ℝ) {m : ℕ} (xPrev : Fin m → ℝ) (xCur : Fin (m + 1) → ℝ) (hmax : ∑ i : Fin m, (s ↑i - s m) * xPrev i ^ 2 ≤ ∑ i : Fin m, (s ↑i - s m) * xCur i.castSucc ^ 2) (hprev : ∑ i : Fin m, (s ↑i - s m) ≤ ∑ i : Fin m, (s ↑i - s m) * xPrev i ^ 2) (hnorm : ↑m + 1 ≤ ∑ i : Fin (m + 1), xCur i ^ 2) (hgap : 0 ≤ s m - s (m + 1)) : ∑ i : Fin (m + 1), (s ↑i - s (m + 1)) * xCur i ^ 2 ≥ ∑ i : Fin (m + 1), (s ↑i - s (m + 1))

One numerical Ball--Prodromou induction step in the Fin-indexed form used by the coordinate theorem.

theorem OlevskiiGram.exists_bpInductionWitness {ι : Type u_1} [Fintype ι] (m : ℕ) (u : ι → Fin (m + 1) → ℝ) (hparseval : ∀ (x : Fin (m + 1) → ℝ) (i : Fin (m + 1)), ∑ j : ι, realDot x (u j) * u j i = x i) (s : ℕ → ℝ) (hanti : ∀ {i k : ℕ}, i ≤ k → s k ≤ s i) : ∃ w ∈ constraintPolytope u, ∑ i : Fin (m + 1), (s ↑i - s (m + 1)) ≤ ∑ i : Fin (m + 1), (s ↑i - s (m + 1)) * w i ^ 2

Existential form of the Ball--Prodromou induction in diagonal coordinates.

For a decreasing sequence s, this constructs a feasible point satisfying the induction inequality (2) from the TeX proof.

theorem OlevskiiGram.ballProdromou_diagonal {ι : Type u_1} [Fintype ι] (m : ℕ) (u : ι → Fin (m + 1) → ℝ) (hparseval : ∀ (x : Fin (m + 1) → ℝ) (i : Fin (m + 1)), ∑ j : ι, realDot x (u j) * u j i = x i) (s : ℕ → ℝ) (hanti : ∀ {i k : ℕ}, i ≤ k → s k ≤ s i) (hs_last : s (m + 1) = 0) : ∃ w ∈ constraintPolytope u, ∑ i : Fin (m + 1), s ↑i ≤ ∑ i : Fin (m + 1), s ↑i * w i ^ 2

Diagonal Ball--Prodromou theorem in coordinates.

This is the core of the paper's Ball--Prodromou proof after choosing an orthonormal eigenbasis and setting the next eigenvalue to zero.

def OlevskiiGram.HasBallProdromouDiagonalModel {d : Type u_1} [Fintype d] (A : Matrix d d ℝ) (τ : ℝ) : Prop

The spectral-coordinate data needed to turn the diagonal Ball--Prodromou theorem into the cube quadratic maximum.

In the paper this data comes from the positive spectral subspace of a symmetric matrix A: u j are the coordinates of the projected standard basis vectors, s is the decreasing eigenvalue list with one terminal zero, and τ is the trace of the positive part.

Equations

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

theorem OlevskiiGram.cubeQuadraticMaximum_from_diagonalBP {d : Type u_1} [Fintype d] (A : Matrix d d ℝ) (τ : ℝ) (hmodel : HasBallProdromouDiagonalModel A τ) : ∃ (x : d → ℝ), InRealUnitCube x ∧ τ ≤ realQuadraticForm A x

Ball--Prodromou implies the cube quadratic maximum once the positive spectral subspace has been expressed in diagonal coordinates.

theorem OlevskiiGram.supportInequality_from_diagonalBP {d : Type u_1} [Fintype d] [DecidableEq d] (A Apos : Matrix d d ℝ) (hsupport : HasPositivePartSupportFunction A Apos) (hmodel : HasBallProdromouDiagonalModel A Apos.trace) : ∃ (x : d → ℝ), InRealUnitCube x ∧ ∀ (G : Matrix d d ℝ), RealSymmetric G → RealLoewnerBetweenZeroAndOne G → (A * G).trace ≤ realQuadraticForm A x

For a fixed symmetric test matrix, the positive-part support-function bound and the Ball--Prodromou diagonal model give the support inequality needed for the convex-hull separation argument.

def OlevskiiGram.ambientOfEigenCoordinates {d : Type u_1} {m : ℕ} (v : Fin (m + 1) → d → ℝ) (w : Fin (m + 1) → ℝ) : d → ℝ

Ambient vector represented by coordinates in an orthonormal row system.

Equations

• OlevskiiGram.ambientOfEigenCoordinates v w j = ∑ i : Fin (m + 1), w i * v i j

def OlevskiiGram.coordinateConstraintVectors {d : Type u_1} {m : ℕ} (v : Fin (m + 1) → d → ℝ) : d → Fin (m + 1) → ℝ

Constraint vectors obtained from rows of an ambient orthonormal system.

Equations

• OlevskiiGram.coordinateConstraintVectors v j i = v i j

theorem OlevskiiGram.realDot_euclidean_eq_inner {d : Type u_1} [Fintype d] (x y : EuclideanSpace ℝ d) : (realDot (fun (i : d) => x.ofLp i) fun (i : d) => y.ofLp i) = inner ℝ x y

The project coordinate dot product agrees with the Euclidean inner product.

theorem OlevskiiGram.toEuclideanLin_apply_eq_sum {d : Type u_1} [Fintype d] [DecidableEq d] (A : Matrix d d ℝ) (x : EuclideanSpace ℝ d) (i : d) : ((Matrix.toEuclideanLin A) x).ofLp i = ∑ j : d, A i j * x.ofLp j

Coordinate form of the matrix action A.toEuclideanLin.

theorem OlevskiiGram.realQuadraticForm_euclidean_eq_inner {d : Type u_1} [Fintype d] [DecidableEq d] (A : Matrix d d ℝ) (x : EuclideanSpace ℝ d) : (realQuadraticForm A fun (i : d) => x.ofLp i) = inner ℝ x ((Matrix.toEuclideanLin A) x)

Coordinate quadratic forms are Euclidean inner products against A.toEuclideanLin.

theorem OlevskiiGram.parseval_coordinateConstraintVectors {d : Type u_1} [Fintype d] {m : ℕ} (v : Fin (m + 1) → d → ℝ) (horth : ∀ (i k : Fin (m + 1)), realDot (v i) (v k) = if i = k then 1 else 0) (x : Fin (m + 1) → ℝ) (i : Fin (m + 1)) : ∑ j : d, realDot x (coordinateConstraintVectors v j) * coordinateConstraintVectors v j i = x i

The projected standard-basis vectors form a Parseval family when the coordinate rows are orthonormal.

theorem OlevskiiGram.realQuadraticForm_ambientOfEigenCoordinates {d : Type u_1} [Fintype d] {m : ℕ} (A : Matrix d d ℝ) (v : Fin (m + 1) → d → ℝ) (s : ℕ → ℝ) (horth : ∀ (i k : Fin (m + 1)), realDot (v i) (v k) = if i = k then 1 else 0) (heigen : ∀ (r : Fin (m + 1)) (j : d), ∑ k : d, A j k * v r k = s ↑r * v r j) (w : Fin (m + 1) → ℝ) : realQuadraticForm A (ambientOfEigenCoordinates v w) = ∑ r : Fin (m + 1), s ↑r * w r ^ 2

If the rows are orthonormal eigenvectors of A, then the quadratic form of A is diagonal on their span.

def OlevskiiGram.HasPositiveEigenCoordinateData {d : Type u_1} [Fintype d] (A : Matrix d d ℝ) (τ : ℝ) : Prop

Explicit finite-dimensional spectral-coordinate data sufficient for the Ball--Prodromou diagonal model.

Equations

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

theorem OlevskiiGram.hasPositiveEigenCoordinateData_of_realPSD_fin {m : ℕ} (A : Matrix (Fin (m + 1)) (Fin (m + 1)) ℝ) (hSym : RealSymmetric A) (hPSD : RealPSD A) (hantiEig : Antitone ⋯.eigenvalues) : HasPositiveEigenCoordinateData A A.trace

For a positive semidefinite real symmetric matrix indexed by Fin (m+1), Mathlib's Hermitian spectral theorem supplies the explicit eigen-coordinate data needed by the Ball--Prodromou diagonal model.

theorem OlevskiiGram.symmetricToEuclidean_eigenvalues_antitone_fin {m : ℕ} (A : Matrix (Fin (m + 1)) (Fin (m + 1)) ℝ) (hSym : RealSymmetric A) : Antitone (⋯.eigenvalues ⋯)

The sorted self-adjoint eigenvalues supplied by Mathlib are antitone.

theorem OlevskiiGram.symmetricToEuclidean_apply_eigenvectorBasis_fin {m : ℕ} (A : Matrix (Fin (m + 1)) (Fin (m + 1)) ℝ) (hSym : RealSymmetric A) (i : Fin (m + 1)) : have hT := ⋯; have hn := ⋯; (Matrix.toEuclideanLin A) ((hT.eigenvectorBasis hn) i) = hT.eigenvalues hn i • (hT.eigenvectorBasis hn) i

Mathlib's sorted self-adjoint eigenbasis consists of eigenvectors for A.toEuclideanLin.

theorem OlevskiiGram.symmetricToEuclidean_eigenvectorBasis_realDot {m : ℕ} (A : Matrix (Fin (m + 1)) (Fin (m + 1)) ℝ) (hSym : RealSymmetric A) : have hT := ⋯; have hn := ⋯; ∀ (i k : Fin (m + 1)), (realDot (fun (j : Fin (m + 1)) => ((hT.eigenvectorBasis hn) i).ofLp j) fun (j : Fin (m + 1)) => ((hT.eigenvectorBasis hn) k).ofLp j) = if i = k then 1 else 0

Coordinate orthonormality of Mathlib's sorted Euclidean eigenbasis.

theorem OlevskiiGram.symmetricToEuclidean_eigenvectorBasis_coord {m : ℕ} (A : Matrix (Fin (m + 1)) (Fin (m + 1)) ℝ) (hSym : RealSymmetric A) : have hT := ⋯; have hn := ⋯; ∀ (r j : Fin (m + 1)), ∑ k : Fin (m + 1), A j k * ((hT.eigenvectorBasis hn) r).ofLp k = hT.eigenvalues hn r * ((hT.eigenvectorBasis hn) r).ofLp j

Coordinate form of the sorted Euclidean eigenvector equation.

theorem OlevskiiGram.symmetricToEuclidean_eigenvalues_nonneg_of_realPSD_fin {m : ℕ} (A : Matrix (Fin (m + 1)) (Fin (m + 1)) ℝ) (hSym : RealSymmetric A) (hPSD : RealPSD A) : have hT := ⋯; have hn := ⋯; ∀ (i : Fin (m + 1)), 0 ≤ hT.eigenvalues hn i

Sorted Euclidean eigenvalues are nonnegative under the project PSD predicate.

theorem OlevskiiGram.symmetricToEuclidean_trace_eq_sum_eigenvalues_fin {m : ℕ} (A : Matrix (Fin (m + 1)) (Fin (m + 1)) ℝ) (hSym : RealSymmetric A) : have hT := ⋯; have hn := ⋯; A.trace = ∑ i : Fin (m + 1), hT.eigenvalues hn i

The trace of a real matrix agrees with the sum of Mathlib's sorted eigenvalues.

theorem OlevskiiGram.hasPositiveEigenCoordinateData_of_realPSD_fin_sorted_of_trace {m : ℕ} (A : Matrix (Fin (m + 1)) (Fin (m + 1)) ℝ) (hSym : RealSymmetric A) (hPSD : RealPSD A) (htraceSorted : have hT := ⋯; have hn := ⋯; A.trace = ∑ i : Fin (m + 1), hT.eigenvalues hn i) : HasPositiveEigenCoordinateData A A.trace

Mathlib's sorted Euclidean spectral data gives the project's positive eigen-coordinate data once the trace has been identified with the sorted eigenvalue sum.

theorem OlevskiiGram.hasPositiveEigenCoordinateData_of_realPSD_fin_sorted {m : ℕ} (A : Matrix (Fin (m + 1)) (Fin (m + 1)) ℝ) (hSym : RealSymmetric A) (hPSD : RealPSD A) : HasPositiveEigenCoordinateData A A.trace

Mathlib's sorted Euclidean spectral data gives the positive eigen-coordinate data.

theorem OlevskiiGram.sum_posPart_eq_sum_initialSegment_of_signs {N m : ℕ} (hN : m + 1 ≤ N) (lam : Fin N → ℝ) (hpos : ∀ (r : Fin (m + 1)), 0 ≤ lam (Fin.castLE hN r)) (hnonpos : ∀ (i : Fin N), m + 1 ≤ ↑i → lam i ≤ 0) : ∑ i : Fin N, (lam i)⁺ = ∑ r : Fin (m + 1), lam (Fin.castLE hN r)

For a finite sequence, if an initial block is nonnegative and the remaining tail is nonpositive, then the sum of positive parts is the sum over the initial block.

theorem OlevskiiGram.antitone_fin_nonpos_or_initial_nonneg_segment {N : ℕ} (lam : Fin N → ℝ) (hanti : Antitone lam) : (∀ (i : Fin N), lam i ≤ 0) ∨ ∃ (m : ℕ) (hN : m + 1 ≤ N), (∀ (r : Fin (m + 1)), 0 ≤ lam (Fin.castLE hN r)) ∧ ∀ (i : Fin N), m + 1 ≤ ↑i → lam i ≤ 0

A decreasing finite real sequence is either everywhere nonpositive, or its nonnegative entries form a nonempty initial segment.

theorem OlevskiiGram.hasPositiveEigenCoordinateData_of_sorted_positiveInitialSegment_card {d : Type u_1} [Fintype d] [DecidableEq d] {m : ℕ} (hN : m + 1 ≤ Fintype.card d) (A : Matrix d d ℝ) (hSym : RealSymmetric A) (τ : ℝ) (hpos : have hT := ⋯; have hn := ⋯; ∀ (r : Fin (m + 1)), 0 ≤ hT.eigenvalues hn (Fin.castLE hN r)) (htrace : have hT := ⋯; have hn := ⋯; τ = ∑ r : Fin (m + 1), hT.eigenvalues hn (Fin.castLE hN r)) : HasPositiveEigenCoordinateData A τ

Positive initial segment construction for an arbitrary finite coordinate type, indexed through Mathlib's canonical sorted eigenvalue list.

theorem OlevskiiGram.hasPositiveEigenCoordinateData_of_sorted_positiveInitialSegment {N m : ℕ} (hN : m + 1 ≤ N) (A : Matrix (Fin N) (Fin N) ℝ) (hSym : RealSymmetric A) (τ : ℝ) (hpos : have hT := ⋯; have hn := ⋯; ∀ (r : Fin (m + 1)), 0 ≤ hT.eigenvalues hn (Fin.castLE hN r)) (htrace : have hT := ⋯; have hn := ⋯; τ = ∑ r : Fin (m + 1), hT.eigenvalues hn (Fin.castLE hN r)) : HasPositiveEigenCoordinateData A τ

An initial segment of Mathlib's sorted Euclidean eigenbasis gives the positive eigen-coordinate data consumed by Ball--Prodromou. The hypotheses say that the selected m+1 sorted eigenvalues are nonnegative and have total τ.

theorem OlevskiiGram.hasBallProdromouDiagonalModel_of_eigenCoordinateData {d : Type u_1} [Fintype d] (A : Matrix d d ℝ) (τ : ℝ) (hdata : HasPositiveEigenCoordinateData A τ) : HasBallProdromouDiagonalModel A τ

The explicit eigen-coordinate data obtained from a positive spectral subspace supplies the diagonal model consumed by Ball--Prodromou.

theorem OlevskiiGram.cubeQuadraticMaximum_from_eigenCoordinateData {d : Type u_1} [Fintype d] (A : Matrix d d ℝ) (τ : ℝ) (hdata : HasPositiveEigenCoordinateData A τ) : ∃ (x : d → ℝ), InRealUnitCube x ∧ τ ≤ realQuadraticForm A x

Eigen-coordinate data feeds directly into the BP cube quadratic maximum.

theorem OlevskiiGram.supportInequality_from_upperBound_and_eigenCoordinateData {d : Type u_1} [Fintype d] [DecidableEq d] (A : Matrix d d ℝ) (τ : ℝ) (hupper : ∀ (G : Matrix d d ℝ), RealSymmetric G → RealLoewnerBetweenZeroAndOne G → (A * G).trace ≤ τ) (hdata : HasPositiveEigenCoordinateData A τ) : ∃ (x : d → ℝ), InRealUnitCube x ∧ ∀ (G : Matrix d d ℝ), RealSymmetric G → RealLoewnerBetweenZeroAndOne G → (A * G).trace ≤ realQuadraticForm A x

Any support-function upper bound tr(AG) ≤ τ, together with Ball--Prodromou eigen-coordinate data proving τ ≤ qᵀAq for some cube vector, gives the support inequality needed by the convex-hull argument.

theorem OlevskiiGram.supportInequality_from_eigenCoordinateData {d : Type u_1} [Fintype d] [DecidableEq d] (A Apos : Matrix d d ℝ) (hsupport : HasPositivePartSupportFunction A Apos) (hdata : HasPositiveEigenCoordinateData A Apos.trace) : ∃ (x : d → ℝ), InRealUnitCube x ∧ ∀ (G : Matrix d d ℝ), RealSymmetric G → RealLoewnerBetweenZeroAndOne G → (A * G).trace ≤ realQuadraticForm A x

Positive spectral-coordinate data plus the positive-part support-function property gives the support inequality used in the convex-hull argument.

theorem OlevskiiGram.supportInequality_from_posNegProjection_and_eigenData {d : Type u_1} [Fintype d] [DecidableEq d] (A Apos Aneg Ppos : Matrix d d ℝ) (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) (hdata : HasPositiveEigenCoordinateData A Apos.trace) : ∃ (x : d → ℝ), InRealUnitCube x ∧ ∀ (G : Matrix d d ℝ), RealSymmetric G → RealLoewnerBetweenZeroAndOne G → (A * G).trace ≤ realQuadraticForm A x

The same support inequality, using the abstract positive/negative spectral-part criterion for the support-function property.

theorem OlevskiiGram.supportInequality_from_cfc_posPart_initialSegment {N m : ℕ} (hN : m + 1 ≤ N) (A : Matrix (Fin N) (Fin N) ℝ) (hSym : RealSymmetric A) (hpos : have hT := ⋯; have hn := ⋯; ∀ (r : Fin (m + 1)), 0 ≤ hT.eigenvalues hn (Fin.castLE hN r)) (htrace : have hT := ⋯; have hn := ⋯; A⁺.trace = ∑ r : Fin (m + 1), hT.eigenvalues hn (Fin.castLE hN r)) : ∃ (x : Fin N → ℝ), InRealUnitCube x ∧ ∀ (G : Matrix (Fin N) (Fin N) ℝ), RealSymmetric G → RealLoewnerBetweenZeroAndOne G → (A * G).trace ≤ realQuadraticForm A x

CFC positive part plus a nonnegative sorted initial eigenvalue segment gives the support inequality for the symmetric test matrix A.

theorem OlevskiiGram.trace_posPart_eq_sum_initialSegment_of_sorted_signs {N m : ℕ} (hN : m + 1 ≤ N) (A : Matrix (Fin N) (Fin N) ℝ) (hSym : RealSymmetric A) (htracePosParts : have hT := ⋯; have hn := ⋯; A⁺.trace = ∑ i : Fin N, (hT.eigenvalues hn i)⁺) (hpos : have hT := ⋯; have hn := ⋯; ∀ (r : Fin (m + 1)), 0 ≤ hT.eigenvalues hn (Fin.castLE hN r)) (hnonpos : have hT := ⋯; have hn := ⋯; ∀ (i : Fin N), m + 1 ≤ ↑i → hT.eigenvalues hn i ≤ 0) : have hT := ⋯; have hn := ⋯; A⁺.trace = ∑ r : Fin (m + 1), hT.eigenvalues hn (Fin.castLE hN r)

If the CFC positive-part trace is known to be the sum of positive parts of the sorted eigenvalues, then a sign pattern for an initial segment identifies that trace with the initial segment sum.

theorem OlevskiiGram.supportInequality_from_cfc_posPart_sorted_signs {N m : ℕ} (hN : m + 1 ≤ N) (A : Matrix (Fin N) (Fin N) ℝ) (hSym : RealSymmetric A) (htracePosParts : have hT := ⋯; have hn := ⋯; A⁺.trace = ∑ i : Fin N, (hT.eigenvalues hn i)⁺) (hpos : have hT := ⋯; have hn := ⋯; ∀ (r : Fin (m + 1)), 0 ≤ hT.eigenvalues hn (Fin.castLE hN r)) (hnonpos : have hT := ⋯; have hn := ⋯; ∀ (i : Fin N), m + 1 ≤ ↑i → hT.eigenvalues hn i ≤ 0) : ∃ (x : Fin N → ℝ), InRealUnitCube x ∧ ∀ (G : Matrix (Fin N) (Fin N) ℝ), RealSymmetric G → RealLoewnerBetweenZeroAndOne G → (A * G).trace ≤ realQuadraticForm A x

The support inequality follows from a sorted eigenvalue sign pattern, once the CFC positive-part trace has been identified with the sorted positive-part sum.

theorem OlevskiiGram.trace_posPart_eq_sum_initialSegment_of_sorted_signs_card {d : Type u_1} [Fintype d] [DecidableEq d] {m : ℕ} (hN : m + 1 ≤ Fintype.card d) (A : Matrix d d ℝ) (hSym : RealSymmetric A) (hpos : have hT := ⋯; have hn := ⋯; ∀ (r : Fin (m + 1)), 0 ≤ hT.eigenvalues hn (Fin.castLE hN r)) (hnonpos : have hT := ⋯; have hn := ⋯; ∀ (i : Fin (Fintype.card d)), m + 1 ≤ ↑i → hT.eigenvalues hn i ≤ 0) : have hT := ⋯; have hn := ⋯; A⁺.trace = ∑ r : Fin (m + 1), hT.eigenvalues hn (Fin.castLE hN r)

For an arbitrary finite coordinate type, a sorted eigenvalue sign pattern identifies the CFC positive-part trace with the nonnegative initial segment.

theorem OlevskiiGram.supportInequality_from_cfc_posPart_sorted_signs_card {d : Type u_1} [Fintype d] [DecidableEq d] {m : ℕ} (hN : m + 1 ≤ Fintype.card d) (A : Matrix d d ℝ) (hSym : RealSymmetric A) (hpos : have hT := ⋯; have hn := ⋯; ∀ (r : Fin (m + 1)), 0 ≤ hT.eigenvalues hn (Fin.castLE hN r)) (hnonpos : have hT := ⋯; have hn := ⋯; ∀ (i : Fin (Fintype.card d)), m + 1 ≤ ↑i → hT.eigenvalues hn i ≤ 0) : ∃ (x : d → ℝ), InRealUnitCube x ∧ ∀ (G : Matrix d d ℝ), RealSymmetric G → RealLoewnerBetweenZeroAndOne G → (A * G).trace ≤ realQuadraticForm A x

For an arbitrary finite coordinate type, the CFC positive-part support inequality follows from a sorted eigenvalue sign pattern.

theorem OlevskiiGram.supportInequality_of_cfc_posPart_trace_zero_card {d : Type u_1} [Fintype d] [DecidableEq d] (A : Matrix d d ℝ) (hSym : RealSymmetric A) (htrace0 : A⁺.trace = 0) : ∃ (x : d → ℝ), InRealUnitCube x ∧ ∀ (G : Matrix d d ℝ), RealSymmetric G → RealLoewnerBetweenZeroAndOne G → (A * G).trace ≤ realQuadraticForm A x

If the CFC positive part has zero trace, the support inequality is witnessed by the zero cube vector, for any finite coordinate type.

theorem OlevskiiGram.supportInequality_from_cfc_posPart_card {d : Type u_1} [Fintype d] [DecidableEq d] (A : Matrix d d ℝ) (hSym : RealSymmetric A) : ∃ (x : d → ℝ), InRealUnitCube x ∧ ∀ (G : Matrix d d ℝ), RealSymmetric G → RealLoewnerBetweenZeroAndOne G → (A * G).trace ≤ realQuadraticForm A x

Ball--Prodromou plus the CFC positive part gives the support inequality for every real symmetric test matrix on an arbitrary finite coordinate type.

theorem OlevskiiGram.matrixToEuclidean_mem_closedConvexHull_rankOneCube_of_loewner {d : Type u_1} [Fintype d] [DecidableEq d] (T : Matrix d d ℝ) (hT : RealSymmetric T) (hTbetween : RealLoewnerBetweenZeroAndOne T) : matrixToEuclidean T ∈ (closedConvexHull ℝ) (realRankOneCubeEuclideanSet d)

Ball--Prodromou and separation put every real symmetric 0 ≤ T ≤ I into the closed convex hull of flattened rank-one cube matrices.

The remaining step toward HasRealConvexDecomposition is to replace this closed-hull membership by ordinary convex-hull membership for the compact rank-one cube image.

theorem OlevskiiGram.matrixToEuclidean_mem_convexHull_rankOneCube_of_loewner {d : Type u_1} [Fintype d] [DecidableEq d] (T : Matrix d d ℝ) (hT : RealSymmetric T) (hTbetween : RealLoewnerBetweenZeroAndOne T) : matrixToEuclidean T ∈ (convexHull ℝ) (realRankOneCubeEuclideanSet d)

For the compact rank-one cube image, the closed-convex-hull membership from separation is ordinary convex-hull membership.

theorem OlevskiiGram.hasRealConvexDecomposition (d : Type u_1) [Fintype d] [DecidableEq d] : HasRealConvexDecomposition d

Real convex decomposition of every symmetric matrix satisfying 0 ≤ T ≤ I.

This is the finite-dimensional convex-hull extraction step in the paper: membership of T in the convex hull of the rank-one cube matrices is unpacked into explicit weights and cube vectors.

theorem OlevskiiGram.supportInequality_of_cfc_posPart_trace_zero {N : ℕ} (A : Matrix (Fin N) (Fin N) ℝ) (hSym : RealSymmetric A) (htrace0 : A⁺.trace = 0) : ∃ (x : Fin N → ℝ), InRealUnitCube x ∧ ∀ (G : Matrix (Fin N) (Fin N) ℝ), RealSymmetric G → RealLoewnerBetweenZeroAndOne G → (A * G).trace ≤ realQuadraticForm A x

If the CFC positive part has zero trace, the support inequality is witnessed by the zero cube vector.

theorem OlevskiiGram.cubeQuadraticMaximum_of_realPSD_fin {m : ℕ} (A : Matrix (Fin (m + 1)) (Fin (m + 1)) ℝ) (hSym : RealSymmetric A) (hPSD : RealPSD A) (hantiEig : Antitone ⋯.eigenvalues) : ∃ (x : Fin (m + 1) → ℝ), InRealUnitCube x ∧ A.trace ≤ realQuadraticForm A x

Ball--Prodromou in matrix form for a positive semidefinite real symmetric matrix whose eigenvalues are indexed in decreasing order.

theorem OlevskiiGram.cubeQuadraticMaximum_of_realPSD_fin_sorted_of_trace {m : ℕ} (A : Matrix (Fin (m + 1)) (Fin (m + 1)) ℝ) (hSym : RealSymmetric A) (hPSD : RealPSD A) (htraceSorted : have hT := ⋯; have hn := ⋯; A.trace = ∑ i : Fin (m + 1), hT.eigenvalues hn i) : ∃ (x : Fin (m + 1) → ℝ), InRealUnitCube x ∧ A.trace ≤ realQuadraticForm A x

Ball--Prodromou cube quadratic maximum from Mathlib's sorted Euclidean spectral data, with the remaining trace-identification hypothesis explicit.

theorem OlevskiiGram.cubeQuadraticMaximum_of_realPSD_fin_sorted {m : ℕ} (A : Matrix (Fin (m + 1)) (Fin (m + 1)) ℝ) (hSym : RealSymmetric A) (hPSD : RealPSD A) : ∃ (x : Fin (m + 1) → ℝ), InRealUnitCube x ∧ A.trace ≤ realQuadraticForm A x

Ball--Prodromou in matrix form for a positive semidefinite real symmetric matrix, using Mathlib's sorted Euclidean spectral data directly.

theorem OlevskiiGram.supportInequality_of_realPSD_fin_sorted {m : ℕ} (A : Matrix (Fin (m + 1)) (Fin (m + 1)) ℝ) (hSym : RealSymmetric A) (hPSD : RealPSD A) : ∃ (x : Fin (m + 1) → ℝ), InRealUnitCube x ∧ ∀ (G : Matrix (Fin (m + 1)) (Fin (m + 1)) ℝ), RealSymmetric G → RealLoewnerBetweenZeroAndOne G → (A * G).trace ≤ realQuadraticForm A x

For a positive semidefinite real symmetric test matrix, Ball--Prodromou gives a single cube vector whose quadratic value dominates all trace pairings tr(AG) with 0 ≤ G ≤ I.