OAI/Probability/SwitchChain/SliceCoefficientAlgebra.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem315.SliceCoefficients.linearPair line 12
  2. def OAI.Problem315.SliceCoefficients.rowSum line 15
  3. def OAI.Problem315.SliceCoefficients.outside line 17
  4. def OAI.Problem315.SliceCoefficients.meetingSum line 19
  5. def OAI.Problem315.SliceCoefficients.disjointSum line 22
  6. theorem OAI.Problem315.SliceCoefficients.sum_outside line 25
  7. theorem OAI.Problem315.SliceCoefficients.linearPair_rowSum line 33
  8. theorem OAI.Problem315.SliceCoefficients.meetingSum_eq line 43
  9. theorem OAI.Problem315.SliceCoefficients.double_outside_eq line 52
  10. theorem OAI.Problem315.SliceCoefficients.linearPair_symmetric line 76
  11. theorem OAI.Problem315.SliceCoefficients.linearPair_diag line 82
  12. theorem OAI.Problem315.SliceCoefficients.linearPair_total line 86
  13. theorem OAI.Problem315.SliceCoefficients.linearPair_meetingSum line 90
  14. theorem OAI.Problem315.SliceCoefficients.linearPair_disjointSum line 98
  15. theorem OAI.Problem315.SliceCoefficients.rowZero_meetingSum line 108
  16. theorem OAI.Problem315.SliceCoefficients.rowZero_disjointSum line 115
  17. theorem OAI.Problem315.SliceCoefficients.linearPair_injective_of_centered line 123
  18. theorem OAI.Problem315.SliceCoefficients.linearPair_orthogonal_rowZero line 133
  19. theorem OAI.Problem315.SliceCoefficients.linearPair_row_sq line 162
  20. theorem OAI.Problem315.SliceCoefficients.linearPair_norm_sq line 175
  21. def OAI.Problem315.SliceCoefficients.constantPair line 182
  22. theorem OAI.Problem315.SliceCoefficients.constantPair_diag line 185
  23. theorem OAI.Problem315.SliceCoefficients.constantPair_symmetric line 190
  24. theorem OAI.Problem315.SliceCoefficients.constantPair_rowSum line 195
  25. theorem OAI.Problem315.SliceCoefficients.exists_coefficient_decomposition line 203
  26. def OAI.Problem315.SliceCoefficients.intersectionAction line 245
  27. theorem OAI.Problem315.SliceCoefficients.intersectionAction_linearPair line 248
  28. theorem OAI.Problem315.SliceCoefficients.intersectionAction_rowZero line 260