OAI/InformationTheory/AmplitudeDamping/ZeroBlockEntropy.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.GAD.trace_re_eq_sum_eigenvalues line 23
  2. theorem OAI.GAD.logDetShift_inv_eq_sum line 28
  3. theorem OAI.GAD.entropy_three_sub_le_deficits line 34
  4. theorem OAI.GAD.deficitLog_inv line 80
  5. theorem OAI.GAD.posSemidef_diag_re line 95
  6. theorem OAI.GAD.gram_diagonal_real line 100
  7. theorem OAI.GAD.zeroBlock_diagonal_log_bound line 108
  8. theorem OAI.GAD.zeroBlock_diagonal_entropy_bound line 147
  9. theorem OAI.GAD.gram_biisometry line 184
  10. theorem OAI.GAD.mass_biisometry line 190
  11. theorem OAI.GAD.entropy_gram_biisometry line 197
  12. theorem OAI.GAD.zeroBlock_bimultiply line 210
  13. theorem OAI.GAD.isometry_fromBlocks line 219
  14. theorem OAI.GAD.coisometry_fromBlocks line 225
  15. theorem OAI.GAD.exists_unitary_singular_decomposition line 238

    Source documentation

    Singular-value decomposition in the same finite coordinate type, including singular matrices. The zero singular directions are completed orthonormally.

    theorem exists_unitary_singular_decomposition (A : Matrix ι ι ℂ) :
    ∃ (U V : Matrix.unitaryGroup ι ℂ) (s : ι → ℝ),
      (∀ i, 0 ≤ s i) ∧ A = (U : Matrix ι ι ℂ) * Matrix.diagonal (fun i ↦ (s i : ℂ)) * star V := by
…
  16. theorem OAI.GAD.zeroBlock_square_entropy_bound line 303
  17. theorem OAI.GAD.zeroBlock_entropy_bound line 339
  18. theorem OAI.GAD.entropy_smul line 365
  19. theorem OAI.GAD.entropy_sqrt_smul line 376
  20. theorem OAI.GAD.mass_sqrt_smul line 384
  21. theorem OAI.GAD.scalarDeficit_normalized line 390
  22. theorem OAI.GAD.zeroBlock_normalized line 402