OAI/Combinatorics/GotsmanLinial/HilbertSchmidt.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LeanBlast.GotsmanLinial.hsNormSq line 14

    Source documentation

    The Hilbert--Schmidt norm squared for the counting inner product. This explicit entry sum does not use any norm instance on matrices.

    noncomputable def hsNormSq (A : Matrix ι κ ℂ) : ℝ :=
…
  2. theorem OAI.LeanBlast.GotsmanLinial.hsNormSq_nonneg line 17
  3. theorem OAI.LeanBlast.GotsmanLinial.hsNormSq_zero line 20
  4. theorem OAI.LeanBlast.GotsmanLinial.hsNormSq_smul line 23
  5. theorem OAI.LeanBlast.GotsmanLinial.hsNormSq_real_smul line 27
  6. theorem OAI.LeanBlast.GotsmanLinial.hsNormSq_conjTranspose line 32
  7. theorem OAI.LeanBlast.GotsmanLinial.ofReal_sq_norm line 37
  8. theorem OAI.LeanBlast.GotsmanLinial.ofReal_fintype_sum line 40
  9. theorem OAI.LeanBlast.GotsmanLinial.ofReal_sum_sq_norm_column line 45
  10. theorem OAI.LeanBlast.GotsmanLinial.ofReal_hsNormSq line 51
  11. theorem OAI.LeanBlast.GotsmanLinial.hsNormSq_eq_re_trace line 58
  12. theorem OAI.LeanBlast.GotsmanLinial.hsNormSq_eq_sum_columns line 62
  13. theorem OAI.LeanBlast.GotsmanLinial.sum_sq_norm_column_eq_re line 67
  14. theorem OAI.LeanBlast.GotsmanLinial.hsNormSq_mul_left_of_unitary line 71
  15. theorem OAI.LeanBlast.GotsmanLinial.hsNormSq_mul_right_of_unitary line 82
  16. theorem OAI.LeanBlast.GotsmanLinial.hsNormSq_diagonal line 90
  17. theorem OAI.LeanBlast.GotsmanLinial.hsNormSq_one line 94
  18. theorem OAI.LeanBlast.GotsmanLinial.hsNormSq_of_unitary line 99
  19. theorem OAI.LeanBlast.GotsmanLinial.hsNormSq_diagonal_of_norm_one line 104
  20. theorem OAI.LeanBlast.GotsmanLinial.hsNormSq_projection line 109
  21. theorem OAI.LeanBlast.GotsmanLinial.sum_sq_norm_column_of_unitary line 114
  22. theorem OAI.LeanBlast.GotsmanLinial.sq_norm_entry_le_one_of_unitary line 120