OAI/Analysis/MatrixScaling/Continuous.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Kaplansky.continuous_unique_minimizer line 14
2. theorem OAI.Kaplansky.continuous_scalingPotential line 49
3. theorem OAI.Kaplansky.exists_continuous_scaling_minimizer line 61
4. theorem OAI.Kaplansky.gramFactor_inverse_identity line 115
5. theorem OAI.Kaplansky.exists_scaled_tuple line 123
6. theorem OAI.Kaplansky.normalizedTuple_of_minimizer line 172

   Source documentation

   The normalization relations for any invertible Gram factors of a minimizer and its target matrix.

   theorem normalizedTuple_of_minimizer (T : Fin n → Matrix (Fin r) (Fin d) ℂ)
       {P : Matrix (Fin d) (Fin d) ℂ} (hP : P.PosDef)
       (hmin : ∀ R : Matrix (Fin d) (Fin d) ℂ, R.PosDef → scalingPotential T P ≤ scalingPotential T R)
       (A : Matrix (Fin d) (Fin d) ℂ) (hA : IsUnit A) (hAA : A*A.conjTranspose=P)
       (B : Matrix (Fin r) (Fin r) ℂ) (hB : IsUnit B) (hBB : B*B.conjTranspose=1+scalingMap T P) :
       (∑ i, (normalizedTuple T A B⁻¹ i).conjTranspose * normalizedTuple T A B⁻¹ i) = 1 ∧
         ((2/3 : ℂ) • (1 : Matrix (Fin r) (Fin r) ℂ) -
           ∑ i, normalizedTuple T A B⁻¹ i * (normalizedTuple T A B⁻¹ i).conjTranspose).PosSemidef := by
   …

   Mentions: OAI.Kaplansky.scalingPotential, OAI.Kaplansky.scalingMap, OAI.Kaplansky.normalizedTuple

7. theorem OAI.Kaplansky.matrix_sqrt_factor line 207
8. theorem OAI.Kaplansky.continuous_matrix_sqrt line 213
9. theorem OAI.Kaplansky.continuous_matrix_inverse line 218
10. theorem OAI.Kaplansky.exists_continuous_scaled_tuple line 229