OAI/Computability/PerfectCompleteness/Algebra/TensorRowAdviceLemmas.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.TensorRowAdvice.comp_subtype_eq_zero line 26
  2. theorem OAI.PerfectCompleteness.TensorRowAdvice.rowAdvice_totalMatrix line 32
  3. theorem OAI.PerfectCompleteness.TensorRowAdvice.rowAdvice_projectMatrix line 43
  4. theorem OAI.PerfectCompleteness.TensorRowAdvice.rowAdvice_kernel_totalMatrix line 52
  5. theorem OAI.PerfectCompleteness.TensorRowAdvice.goodRow_iff_of_advice_eq line 66
  6. theorem OAI.PerfectCompleteness.TensorRowAdvice.selectedValue_eq_of_advice_eq line 74
  7. theorem OAI.PerfectCompleteness.TensorRowAdvice.selectWitness_fields_eq_of_advice_eq line 86
  8. theorem OAI.PerfectCompleteness.TensorRowAdvice.goodRow_totalMatrix_iff line 112
  9. theorem OAI.PerfectCompleteness.TensorRowAdvice.selectedValue_totalMatrix_eq line 120
  10. theorem OAI.PerfectCompleteness.TensorRowAdvice.goodRow_projectMatrix_iff line 128
  11. theorem OAI.PerfectCompleteness.TensorRowAdvice.selectedValue_projectMatrix_eq line 138
  12. theorem OAI.PerfectCompleteness.TensorRowAdvice.selectWitness_projectMatrix_fields_eq line 147
  13. abbrev OAI.PerfectCompleteness.TensorSelectedSlice.projectedMatrix line 186
  14. theorem OAI.PerfectCompleteness.TensorSelectedSlice.projectedMatrix_eq_totalMatrix line 190
  15. def OAI.PerfectCompleteness.TensorSelectedSlice.witness line 203
  16. def OAI.PerfectCompleteness.TensorSelectedSlice.columnSpace line 208
  17. theorem OAI.PerfectCompleteness.TensorSelectedSlice.columnSpace_eq_sequential_maps line 215
  18. theorem OAI.PerfectCompleteness.TensorSelectedSlice.finrank_columnSpace_le line 223
  19. theorem OAI.PerfectCompleteness.TensorSelectedSlice.J_eq_decide_columns line 235
  20. theorem OAI.PerfectCompleteness.TensorSelectedSlice.J_false_of_not_good line 254
  21. theorem OAI.PerfectCompleteness.TensorSelectedSlice.J_iff_compatible line 268
  22. theorem OAI.PerfectCompleteness.TensorSelectedSlice.exists_compatible line 291
  23. def OAI.PerfectCompleteness.TensorSelectedSlice.target line 302
  24. theorem OAI.PerfectCompleteness.TensorSelectedSlice.J_iff_restriction line 314
  25. theorem OAI.PerfectCompleteness.TensorSelectedSlice.exists_tensor_slice line 330
  26. abbrev OAI.PerfectCompleteness.HierarchicalTensorSlice.HiddenTensor line 377
  27. abbrev OAI.PerfectCompleteness.HierarchicalTensorSlice.visibleMatrix line 379
  28. abbrev OAI.PerfectCompleteness.HierarchicalTensorSlice.matrix line 381
  29. abbrev OAI.PerfectCompleteness.HierarchicalTensorSlice.quotientMatrix line 385
  30. abbrev OAI.PerfectCompleteness.HierarchicalTensorSlice.table line 390
  31. abbrev OAI.PerfectCompleteness.HierarchicalTensorSlice.VisibleGood line 393
  32. def OAI.PerfectCompleteness.HierarchicalTensorSlice.witness line 399
  33. def OAI.PerfectCompleteness.HierarchicalTensorSlice.columnSpace line 406
  34. theorem OAI.PerfectCompleteness.HierarchicalTensorSlice.columnSpace_eq_pulled line 414
  35. theorem OAI.PerfectCompleteness.HierarchicalTensorSlice.finrank_columnSpace_le line 425
  36. def OAI.PerfectCompleteness.HierarchicalTensorSlice.J line 434
  37. def OAI.PerfectCompleteness.HierarchicalTensorSlice.target line 438
  38. theorem OAI.PerfectCompleteness.HierarchicalTensorSlice.J_iff_restriction line 448
  39. theorem OAI.PerfectCompleteness.HierarchicalTensorSlice.J_false_of_not_good line 461
  40. theorem OAI.PerfectCompleteness.HierarchicalTensorSlice.selectedValue_eq_some line 470
  41. def OAI.PerfectCompleteness.HierarchicalTensorSlice.correction line 487
  42. def OAI.PerfectCompleteness.HierarchicalTensorSlice.nativeCorrection line 496
  43. def OAI.PerfectCompleteness.HierarchicalTensorSlice.visibleOffset line 503
  44. theorem OAI.PerfectCompleteness.HierarchicalTensorSlice.selectedCorrection_eq_some line 511
  45. theorem OAI.PerfectCompleteness.HierarchicalTensorSlice.affinePrediction_eq_tensor line 523