OAI/Probability/SwitchChain/SliceNormalizedFamily.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem315.SliceNormalized.State line 13
  2. abbrev OAI.Problem315.SliceNormalized.Space line 16
  3. def OAI.Problem315.SliceNormalized.raw line 18
  4. def OAI.Problem315.SliceNormalized.denominator line 22
  5. def OAI.Problem315.SliceNormalized.column line 27
  6. theorem OAI.Problem315.SliceNormalized.raw_diag line 30
  7. theorem OAI.Problem315.SliceNormalized.column_diag line 34
  8. theorem OAI.Problem315.SliceNormalized.raw_symmetric line 37
  9. theorem OAI.Problem315.SliceNormalized.column_symmetric line 41
  10. theorem OAI.Problem315.SliceNormalized.coord_sum line 44
  11. theorem OAI.Problem315.SliceNormalized.centered_eq_binary line 49
  12. theorem OAI.Problem315.SliceNormalized.raw_total line 57
  13. theorem OAI.Problem315.SliceNormalized.column_total line 74
  14. theorem OAI.Problem315.SliceNormalized.raw_inner line 78
  15. theorem OAI.Problem315.SliceNormalized.raw_norm_sq line 98
  16. theorem OAI.Problem315.SliceNormalized.denominator_sq line 109
  17. theorem OAI.Problem315.SliceNormalized.column_inner_unsimplified line 119
  18. theorem OAI.Problem315.SliceNormalized.column_inner line 131
  19. theorem OAI.Problem315.SliceNormalized.column_norm_sq line 149