AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementJacobianMatrixLogDet

- The literal determinant of the affine identity segment is the product of the affine transforms of the eigenvalues of an SPD matrix. The proof diagonalizes `A` by the canonical unitary eigenbasis, transports the affine combination through the star-algebra automorphism, removes the unitary change of basis at determinant level, and evaluates the diagonal determinant. It therefore does not depend on any equality between ordered eigenvalue functions of `A` and `(1-t) I + t A`.

theorem det_affineIdentityMatrix_eq_prod_eigenvalues
    {ι : Type*} [Fintype ι] [DecidableEq ι]
    (A : Matrix ι ι ℝ) (hA : A.PosDef) (t : ℝ) :
    Matrix.det ((1 - t) • (1 : Matrix ι ι ℝ) + t • A) =
      ∏ i, ((1 - t) + t * hA.isHermitian.eigenvalues i) := by
  let B : Matrix ι ι ℝ := (1 - t) • (1 : Matrix ι ι ℝ) + t • A
  let U : unitary (Matrix ι ι ℝ) := star hA.isHermitian.eigenvectorUnitary
  let φ : Matrix ι ι ℝ ≃⋆ₐ[ℝ] Matrix ι ι ℝ :=
    Unitary.conjStarAlgAut ℝ (Matrix ι ι ℝ) U
  have hmap :
      φ B = (1 - t) • φ (1 : Matrix ι ι ℝ) + t • φ A := by
    calc
      φ B = φ ((1 - t) • (1 : Matrix ι ι ℝ) + t • A) := rfl
      _ = φ ((1 - t) • (1 : Matrix ι ι ℝ)) + φ (t • A) :=
        φ.map_add _ _
      _ = (1 - t) • φ (1 : Matrix ι ι ℝ) + t • φ A := by
        rw [map_smul φ, map_smul φ]
  have hone : φ (1 : Matrix ι ι ℝ) = 1 := φ.map_one
  have hA_diag : φ A = Matrix.diagonal hA.isHermitian.eigenvalues := by
    dsimp [φ, U]
    exact hA.isHermitian.conjStarAlgAut_star_eigenvectorUnitary
  have hdiag :
      φ B = (1 - t) • (1 : Matrix ι ι ℝ) +
        t • Matrix.diagonal hA.isHermitian.eigenvalues := by
    rw [hmap, hone, hA_diag]
  have hdetφ : Matrix.det (φ B) = Matrix.det B := by
    dsimp [φ]
    exact det_conjStarAlgAut_eq U B
  calc
    Matrix.det B = Matrix.det (φ B) := hdetφ.symm
    _ = Matrix.det
        ((1 - t) • (1 : Matrix ι ι ℝ) +
          t • Matrix.diagonal hA.isHermitian.eigenvalues) := by
      rw [hdiag]
    _ = ∏ i, ((1 - t) + t * hA.isHermitian.eigenvalues i) :=
      det_affineIdentity_diagonal hA.isHermitian.eigenvalues t

/-- The finite-spectrum log-det of the affine eigenvalues is exactly the
literal log determinant of the affine matrix. -/

AutoSamplingTheory/TechnicalLemmas/Measure/DisplacementJacobianMatrixLogDet.lean:48published source at 0e31a3cda412

- The finite-spectrum log-det of the affine eigenvalues is exactly the literal log determinant of the affine matrix.

theorem spectrumLogDet_affineIdentity_eigenvalues_eq_log_det
    {ι : Type*} [Fintype ι] [DecidableEq ι]
    (A : Matrix ι ι ℝ) (hA : A.PosDef) (t : ℝ)
    (ht0 : 0 ≤ t) (ht1 : t ≤ 1) :
    spectrumLogDet
        (affineIdentitySpectrum t hA.isHermitian.eigenvalues) =
      Real.log (Matrix.det ((1 - t) • (1 : Matrix ι ι ℝ) + t • A)) := by
  unfold spectrumLogDet affineIdentitySpectrum
  rw [det_affineIdentityMatrix_eq_prod_eigenvalues A hA t]
  exact (Real.log_prod (fun i _ =>
    (affineIdentityEigenvalue_pos (hA.eigenvalues_pos i) ht0 ht1).ne')).symm

/-- Literal SPD matrix form of the `-log det` convexity used in the entropy
half of Chewi Theorem 1.4.5. -/

AutoSamplingTheory/TechnicalLemmas/Measure/DisplacementJacobianMatrixLogDet.lean:87published source at 0e31a3cda412

- Literal SPD matrix form of the `-log det` convexity used in the entropy half of Chewi Theorem 1.4.5.

theorem neg_log_det_affineIdentity_le
    {ι : Type*} [Fintype ι] [DecidableEq ι]
    (A : Matrix ι ι ℝ) (hA : A.PosDef) (t : ℝ)
    (ht0 : 0 ≤ t) (ht1 : t ≤ 1) :
    -Real.log (Matrix.det ((1 - t) • (1 : Matrix ι ι ℝ) + t • A)) ≤
      t * (-Real.log (Matrix.det A)) := by
  have hineq := neg_spectrumLogDet_affineIdentity_le
    hA.isHermitian.eigenvalues t (fun i => hA.eigenvalues_pos i) ht0 ht1
  rw [spectrumLogDet_affineIdentity_eigenvalues_eq_log_det A hA t ht0 ht1,
    spectrumLogDet_eigenvalues_eq_log_det A hA] at hineq
  exact hineq

end

end DisplacementJacobianMatrixLogDet
end Measure
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Measure/DisplacementJacobianMatrixLogDet.lean:101published source at 0e31a3cda412