OAI/Analysis/MatrixScaling/Geodesic.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Spectral curves, strict convexity, and geodesic connections.

  1. def OAI.Kaplansky.spectralCurve line 15

    Source documentation

    A positive-definite geodesic in an eigenbasis for its Hermitian direction.

    def spectralCurve (L : Matrix (Fin d) (Fin d) ℂ) (h : Fin d → ℝ) (u : ℝ) :
    Matrix (Fin d) (Fin d) ℂ :=
…
  2. theorem OAI.Kaplansky.spectralCurve_posDef line 19
  3. theorem OAI.Kaplansky.spectralCurve_det line 25
  4. theorem OAI.Kaplansky.spectralCurve_log_det line 39
  5. theorem OAI.Kaplansky.posDef_gram_factor line 58

    Source documentation

    A positive definite matrix has an invertible Gram factor, constructed from its eigenbasis and positive eigenvalues.

    theorem posDef_gram_factor {P : Matrix (Fin d) (Fin d) ℂ} (hP : P.PosDef) :
    ∃ L : Matrix (Fin d) (Fin d) ℂ, IsUnit L ∧ L * L.conjTranspose = P := by
…
  6. theorem OAI.Kaplansky.exists_spectralCurve_between line 85
  7. theorem OAI.Kaplansky.expansion_common_kernel line 143
  8. theorem OAI.Kaplansky.collectiveMatrix_column_nonzero line 164
  9. theorem OAI.Kaplansky.scalingMap_spectralCurve line 183
  10. theorem OAI.Kaplansky.scalingPotential_strictConvex_spectralCurve line 198