OAI/Computability/PerfectCompleteness/Algebra/TensorBucketEvaluationLemmas.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.TensorBucketEvaluation.F2 line 17
  2. def OAI.PerfectCompleteness.TensorBucketEvaluation.tensorOutputLinear line 21
  3. def OAI.PerfectCompleteness.TensorBucketEvaluation.tensorOutput line 27
  4. theorem OAI.PerfectCompleteness.TensorBucketEvaluation.tensorOutput_tmul line 31
  5. theorem OAI.PerfectCompleteness.TensorBucketEvaluation.tensorOutput_zero line 36
  6. theorem OAI.PerfectCompleteness.TensorBucketEvaluation.tensorOutput_add line 40
  7. theorem OAI.PerfectCompleteness.TensorBucketEvaluation.tensorOutput_hiddenSum line 45
  8. def OAI.PerfectCompleteness.TensorBucketEvaluation.visibleOutput line 58
  9. theorem OAI.PerfectCompleteness.TensorBucketEvaluation.evaluate_eq_direction_sum line 63
  10. theorem OAI.PerfectCompleteness.TensorBucketEvaluation.evaluate_split line 74
  11. theorem OAI.PerfectCompleteness.TensorBucketEvaluation.evaluate_splitTape line 85
  12. theorem OAI.PerfectCompleteness.TensorBucketEvaluation.evaluate_apply_split line 93
  13. def OAI.PerfectCompleteness.TensorProjectedSlice.totalMatrix line 121
  14. theorem OAI.PerfectCompleteness.TensorProjectedSlice.totalMatrix_apply line 125
  15. def OAI.PerfectCompleteness.TensorProjectedSlice.Compatible line 132
  16. def OAI.PerfectCompleteness.TensorProjectedSlice.targetAt line 136
  17. theorem OAI.PerfectCompleteness.TensorProjectedSlice.compatible_iff_restrictionMap_eq line 140
  18. theorem OAI.PerfectCompleteness.TensorProjectedSlice.targetAt_comp_restrictionZ line 170
  19. theorem OAI.PerfectCompleteness.TensorProjectedSlice.targetAt_independent line 183
  20. def OAI.PerfectCompleteness.TensorProjectedSlice.inducedTarget line 190
  21. theorem OAI.PerfectCompleteness.TensorProjectedSlice.inducedTarget_eq_targetAt line 195
  22. theorem OAI.PerfectCompleteness.TensorProjectedSlice.inducedTarget_comp_restrictionZ line 203
  23. theorem OAI.PerfectCompleteness.TensorProjectedSlice.columnEquations_iff_inducedTarget line 210
  24. def OAI.PerfectCompleteness.TensorProjectedSlice.sliceEquiv line 220
  25. theorem OAI.PerfectCompleteness.TensorProjectedSlice.finrank_projectedColumns_le line 232
  26. theorem OAI.PerfectCompleteness.TensorProjectedSlice.includedEvaluation_eq_tensorOutputLinear line 239
  27. theorem OAI.PerfectCompleteness.TensorProjectedSlice.includedEvaluation_eq_tensorOutput line 250
  28. theorem OAI.PerfectCompleteness.TensorProjectedSlice.prediction_eq_visible_add_tensorOutput line 256
  29. def OAI.PerfectCompleteness.HierarchicalTensorMatrix.visibleMatrix line 280
  30. theorem OAI.PerfectCompleteness.HierarchicalTensorMatrix.visibleMatrix_apply line 287
  31. theorem OAI.PerfectCompleteness.HierarchicalTensorMatrix.matrix_eq_totalMatrix line 299
  32. theorem OAI.PerfectCompleteness.HierarchicalTensorMatrix.prediction_eq_visible_add_tensorOutput line 323
  33. theorem OAI.PerfectCompleteness.TensorTargetCharacter.comp_tensorOutputLinear line 351
  34. theorem OAI.PerfectCompleteness.TensorTargetCharacter.apply_tensorOutput line 364
  35. theorem OAI.PerfectCompleteness.TensorTargetCharacter.character_affine_tensorOutput line 371
  36. theorem OAI.PerfectCompleteness.TensorTargetCharacter.sign_affine_tensorOutput line 378