InformationTheory

InformationTheory.Shannon.MinkowskiDet

source

Imports 9

Minkowski determinant inequality (Cover-Thomas) #

For positive-definite matrices A, B : Matrix n n ℝ, det(A + B)^(1/n) ≥ det A^(1/n) + det B^(1/n).

Proved by simultaneous diagonalization / congruence reduction. The proof is assembled from the matrix square root (CFC.sqrt), congruence PosDef preservation, the eigenvalue-shift determinant identity det (1 + S) = ∏ (1 + eigenvalues S i) (det_one_add_eq_prod_one_add_eigenvalues), and the scalar geometric-mean superadditivity bound (geom_mean_superadditive).

References #

  • T. M. Cover and J. A. Thomas, Elements of Information Theory (2nd ed.), Wiley, 2006.
theorem

InformationTheory.Shannon.det_rpow_le_arith_mean_eigenvalues

source
{n : Type u_1} [Fintype n] [DecidableEq n] [Nonempty n] {A : Matrix n n ℝ} (hA : A.PosDef) :
A.det ^ (1 / ↑(Fintype.card n)) ≤ 1 / ↑(Fintype.card n) * ∑ i : n, ⋯.eigenvalues i

AM-GM for the determinant of a positive-definite matrix.

For a positive-definite A : Matrix n n ℝ, the n-th root of the determinant is bounded above by the arithmetic mean of its eigenvalues: (det A)^(1/n) ≤ (1/n) ∑ᵢ λᵢ(A).

Building block for the Minkowski determinant inequality (Cover-Thomas): p = 1/n ≤ 1 direction of weighted AM-GM applied to the eigenvalues, using det A = ∏ᵢ λᵢ(A). @audit:ok

Used by
    theorem

    InformationTheory.Shannon.geom_mean_superadditive

    source
    {n : Type u_1} [Fintype n] [Nonempty n] (a b : n → ℝ) (ha : ∀ (i : n), 0 ≤ a i) (hb : ∀ (i : n), 0 ≤ b i) (hab : ∀ (i : n), 0 < a i + b i) :
    (∏ i : n, a i) ^ (1 / ↑(Fintype.card n)) + (∏ i : n, b i) ^ (1 / ↑(Fintype.card n)) ≤ (∏ i : n, (a i + b i)) ^ (1 / ↑(Fintype.card n))

    Scalar Minkowski (superadditivity of the geometric mean).

    For nonnegative reals a i, b i with a i + b i > 0, (∏ a i)^(1/n) + (∏ b i)^(1/n) ≤ (∏ (a i + b i))^(1/n).

    Scalar core of the Minkowski determinant inequality. Follows from weighted AM-GM applied to the normalized weights a i / (a i + b i) and its complement. @audit:ok

    Used by
      theorem

      InformationTheory.Shannon.posDef_cfcSqrt

      source
      {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.PosDef) :
      (CFC.sqrt A).PosDef

      The CFC square root of a positive-definite matrix is positive definite. @audit:ok

      Used by
        theorem

        InformationTheory.Shannon.det_one_add_eq_prod_one_add_eigenvalues

        source
        {n : Type u_1} [Fintype n] [DecidableEq n] {S : Matrix n n ℝ} (hS : S.IsHermitian) :
        (1 + S).det = ∏ i : n, (1 + hS.eigenvalues i)

        det (1 + S) = ∏ (1 + eigenvalues S i) for a Hermitian matrix S.

        Spectral-mapping bridge: S = U diag(λ) Uᴴ gives 1 + S = U diag(1+λ) Uᴴ, hence det (1 + S) = ∏ (1 + λ i). Reusable. @audit:ok

        Used by
          theorem

          InformationTheory.Shannon.minkowskiDeterminantInequality

          source
          {n : Type u_1} [Fintype n] [DecidableEq n] [Nonempty n] {A B : Matrix n n ℝ} (hA : A.PosDef) (hB : B.PosDef) :
          A.det ^ (1 / ↑(Fintype.card n)) + B.det ^ (1 / ↑(Fintype.card n)) ≤ (A + B).det ^ (1 / ↑(Fintype.card n))

          Minkowski determinant inequality.

          For PosDef A B, det(A+B)^(1/n) ≥ det(A)^(1/n) + det(B)^(1/n).

          Genuine proof by simultaneous diagonalization (congruence reduction): let R := CFC.sqrt A (PosDef, posDef_cfcSqrt) and S := R⁻¹ * B * R⁻¹ (PosDef by IsUnit.posDef_star_left_conjugate_iff). Then A + B = R * (1 + S) * R, so det(A+B) = det A · det(1+S). Writing μ i := eigenvalues S i > 0 gives det(1+S) = ∏ (1 + μ i) (det_one_add_eq_prod_one_add_eigenvalues) and ∏ μ i = det S = det B / det A. Apply scalar Minkowski (geom_mean_superadditive with a ≡ 1, b = μ) and multiply through by (det A)^(1/n). @audit:ok

          Used by