Documentation

LeanPool.ArchonFirstProofResults.FirstProof6.Auxiliary.BarrierPotential

Problem 6: Large epsilon-light vertex subsets -- Barrier Potential #

BSS barrier potential Phi_u(M) = tr((uI - M)^{-1}), trace monotonicity, barrier shift/decrease/gap lemmas, eigenvalue bounds, unitary conjugation, and the Neumann-Loewner trace bound.

Main definitions #

Main theorems #

source
noncomputable def Problem6.barrierPotential {V : Type u_1} [Fintype V] [DecidableEq V] (u : ℝ) (M : Matrix V V ℝ) :
ℝ

The upper barrier potential Φ_u(M) = tr((uI - M)⁻¹), defined for symmetric M with eigenvalues < u.

Equations
Instances For
    source
    theorem Problem6.realSpectralDecomp {V : Type u_1} [Fintype V] [DecidableEq V] {M : Matrix V V ℝ} (hM : M.IsHermitian) :
    M = ↑hM.eigenvectorUnitary * Matrix.diagonal hM.eigenvalues * star ↑hM.eigenvectorUnitary

    Real form of the spectral theorem: a real Hermitian matrix equals U * diagonal eigenvalues * star U for its eigenvector unitary U.

    source
    theorem Problem6.psd_factorization {V : Type u_1} [Fintype V] (P : Matrix V V ℝ) (hP : P.PosSemidef) :
    ∃ (N : Matrix V V ℝ), P = N.conjTranspose * N

    PSD factorization via spectral theorem: P PSD implies P = Nᴴ * N for some N.

    source
    theorem Problem6.posDef_sqrt_exists {V : Type u_1} [Fintype V] [DecidableEq V] (U : Matrix V V ℝ) (hU : U.PosDef) :
    ∃ (R : Matrix V V ℝ), R.IsHermitian ∧ IsUnit R.det ∧ R * R = U

    The Hermitian, invertible square root of a positive definite matrix.

    source
    theorem Problem6.trace_mul_nonneg_of_posSemidef {V : Type u_1} [Fintype V] (P Q : Matrix V V ℝ) (hP : P.PosSemidef) (hQ : Q.PosSemidef) :
    0 ≤ (P * Q).trace

    For PSD matrices P, Q over ℝ, tr(P * Q) ≥ 0. Proof: write P = Nᴴ * N, then tr(PQ) = tr(NQNᴴ) ≥ 0 since NQNᴴ is PSD.

    source
    theorem Problem6.trace_mul_le_of_loewner {V : Type u_1} [Fintype V] (X Y C : Matrix V V ℝ) (hXY : (Y - X).PosSemidef) (hC : C.PosSemidef) :
    (X * C).trace ≤ (Y * C).trace

    Trace monotonicity under Loewner order: if X ≤ Y (Loewner) and C ≥ 0, then tr(X * C) ≤ tr(Y * C). This follows from tr((Y-X)*C) ≥ 0 since Y-X ≥ 0 and C ≥ 0.

    source
    theorem Problem6.barrier_shift_posDef {V : Type u_1} [DecidableEq V] (M : Matrix V V ℝ) (u u' : ℝ) (hu : u < u') (hM : (u • 1 - M).PosDef) :
    (u' • 1 - M).PosDef

    Helper: u'I - M is positive definite when uI - M is positive definite and u' > u.

    source
    theorem Problem6.barrier_potential_decrease {V : Type u_1} [Fintype V] [DecidableEq V] (M : Matrix V V ℝ) (u u' : ℝ) (hu : u < u') (hM : (u • 1 - M).PosDef) :
    barrierPotential u M - barrierPotential u' M ≥ (u' - u) * ((u' • 1 - M)⁻¹ * (u' • 1 - M)⁻¹).trace

    The barrier potential decreases as the barrier level increases: Φ_u(M) - Φ_{u'}(M) ≥ δ · tr(U²) where δ = u' - u and U = (u'I - M)⁻¹.

    source
    theorem Problem6.barrier_gap_pos {V : Type u_1} [Fintype V] [DecidableEq V] [Nonempty V] (M : Matrix V V ℝ) (u u' : ℝ) (hu : u < u') (hM : (u • 1 - M).PosDef) :
    0 < barrierPotential u M - barrierPotential u' M

    Helper: the barrier potential gap is positive when u' > u and M ≺ uI. Requires Nonempty V since trace is 0 on the empty type.

    source
    theorem Problem6.barrier_rearrange {a b c : ℝ} (hc : 0 < c) (_ha_nn : 0 ≤ a) (_hb_nn : 0 ≤ b) (ha_lt : a < 1) (hbarr : a + b / c ≤ 1) :
    b / (1 - a) ≤ c

    Key scalar rearrangement: if a + b/c ≤ 1 with c > 0 and 0 ≤ a < 1, 0 ≤ b, then b/(1-a) ≤ c. This is the algebraic core of the barrier argument.

    source
    theorem Problem6.eigenvalue_le_trace_of_posSemidef {V : Type u_1} [Fintype V] [DecidableEq V] (K : Matrix V V ℝ) (hK : K.PosSemidef) (i : V) :
    ⋯.eigenvalues i ≤ K.trace

    For a PSD matrix, each eigenvalue is at most the trace.

    source
    theorem Problem6.one_sub_posDef_of_trace_lt_one {V : Type u_1} [Fintype V] [DecidableEq V] (K : Matrix V V ℝ) (hK_psd : K.PosSemidef) (htrK_lt : K.trace < 1) :
    (1 - K).PosDef

    If K is PSD with trace < 1, then I - K is positive definite.