OAI/Computability/PerfectCompleteness/Foundations/HierarchicalProjectedSliceLemmas.lean

GitHub source file

76 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.HierarchicalProjectedSlice.HiddenTensor line 48
  2. abbrev OAI.PerfectCompleteness.HierarchicalProjectedSlice.visibleMatrix line 50
  3. theorem OAI.PerfectCompleteness.HierarchicalProjectedSlice.visibleMatrix_apply line 53
  4. abbrev OAI.PerfectCompleteness.HierarchicalProjectedSlice.matrix line 61
  5. abbrev OAI.PerfectCompleteness.HierarchicalProjectedSlice.quotientMatrix line 65
  6. abbrev OAI.PerfectCompleteness.HierarchicalProjectedSlice.table line 70
  7. abbrev OAI.PerfectCompleteness.HierarchicalProjectedSlice.VisibleGood line 73
  8. def OAI.PerfectCompleteness.HierarchicalProjectedSlice.witness line 79
  9. def OAI.PerfectCompleteness.HierarchicalProjectedSlice.columnSpace line 86
  10. theorem OAI.PerfectCompleteness.HierarchicalProjectedSlice.columnSpace_eq_pulled line 94
  11. theorem OAI.PerfectCompleteness.HierarchicalProjectedSlice.finrank_columnSpace_le line 105
  12. def OAI.PerfectCompleteness.HierarchicalProjectedSlice.J line 114
  13. def OAI.PerfectCompleteness.HierarchicalProjectedSlice.target line 118
  14. theorem OAI.PerfectCompleteness.HierarchicalProjectedSlice.J_iff_restriction line 128
  15. theorem OAI.PerfectCompleteness.HierarchicalProjectedSlice.J_false_of_not_good line 141
  16. theorem OAI.PerfectCompleteness.HierarchicalProjectedSlice.selectedValue_eq_some line 150
  17. def OAI.PerfectCompleteness.HierarchicalProjectedSlice.correction line 167
  18. def OAI.PerfectCompleteness.HierarchicalProjectedSlice.nativeCorrection line 176
  19. theorem OAI.PerfectCompleteness.HierarchicalProjectedSlice.nativeCorrection_eq_upperTarget line 183
  20. def OAI.PerfectCompleteness.HierarchicalProjectedSlice.visibleOffset line 193
  21. theorem OAI.PerfectCompleteness.HierarchicalProjectedSlice.selectedCorrection_eq_some line 201
  22. theorem OAI.PerfectCompleteness.HierarchicalProjectedSlice.affinePrediction_eq_tensor line 213
  23. def OAI.PerfectCompleteness.HierarchicalProjectedMeeting.useful line 267
  24. def OAI.PerfectCompleteness.HierarchicalProjectedMeeting.leftLaw line 271
  25. theorem OAI.PerfectCompleteness.HierarchicalProjectedMeeting.leftLaw_congr line 278
  26. theorem OAI.PerfectCompleteness.HierarchicalProjectedMeeting.leftLaw_eq_affine line 294
  27. theorem OAI.PerfectCompleteness.HierarchicalProjectedMeeting.columnSpace_eq_nativeQ line 317
  28. theorem OAI.PerfectCompleteness.HierarchicalProjectedMeeting.nativeCorrection_eq_nativeCenter line 326
  29. theorem OAI.PerfectCompleteness.HierarchicalProjectedMeeting.meeting_probability_ge_coset line 337
  30. theorem OAI.PerfectCompleteness.HierarchicalProjectedMeeting.meeting_probability_lower line 366
  31. def OAI.PerfectCompleteness.ProjectedRawAssembly.exteriorBackground line 423
  32. def OAI.PerfectCompleteness.ProjectedRawAssembly.arrays line 432
  33. def OAI.PerfectCompleteness.ProjectedRawAssembly.background line 438
  34. def OAI.PerfectCompleteness.ProjectedRawAssembly.visibleMatrix line 443
  35. theorem OAI.PerfectCompleteness.ProjectedRawAssembly.visibleMatrix_apply line 450
  36. theorem OAI.PerfectCompleteness.ProjectedRawAssembly.arrays_upper line 462
  37. theorem OAI.PerfectCompleteness.ProjectedRawAssembly.background_arrays line 474
  38. theorem OAI.PerfectCompleteness.ProjectedRawAssembly.arrays_eq_matrix_assemble line 485
  39. theorem OAI.PerfectCompleteness.ProjectedRawAssembly.matrix_arrays line 497
  40. abbrev OAI.PerfectCompleteness.SourceProjectedCanonicalQuery.F2 line 543
  41. def OAI.PerfectCompleteness.SourceProjectedCanonicalQuery.query line 550
  42. theorem OAI.PerfectCompleteness.SourceProjectedCanonicalQuery.query_pullback line 554
  43. theorem OAI.PerfectCompleteness.SourceProjectedCanonicalQuery.key_pullback line 565
  44. theorem OAI.PerfectCompleteness.SourceProjectedCanonicalQuery.label_val_pullback line 573
  45. theorem OAI.PerfectCompleteness.SourceProjectedCanonicalQuery.response_pullback line 584
  46. theorem OAI.PerfectCompleteness.SourceProjectedCanonicalQuery.canonicalQuery_pullback line 596
  47. theorem OAI.PerfectCompleteness.SourceProjectedCanonicalQuery.canonical_response_pullback line 604
  48. theorem OAI.PerfectCompleteness.SourceProjectedCanonicalQuery.response_readInput_hidden line 615
  49. theorem OAI.PerfectCompleteness.SourceProjectedCanonicalQuery.response_readInput_hidden_arrays line 638
  50. abbrev OAI.PerfectCompleteness.HierarchicalProjectedRawPrediction.Raw line 693
  51. abbrev OAI.PerfectCompleteness.HierarchicalProjectedRawPrediction.Visible line 694
  52. abbrev OAI.PerfectCompleteness.HierarchicalProjectedRawPrediction.rawArrays line 696
  53. abbrev OAI.PerfectCompleteness.HierarchicalProjectedRawPrediction.rawBackground line 699
  54. abbrev OAI.PerfectCompleteness.HierarchicalProjectedRawPrediction.rawMatrix line 703
  55. abbrev OAI.PerfectCompleteness.HierarchicalProjectedRawPrediction.visibleBackground line 706
  56. abbrev OAI.PerfectCompleteness.HierarchicalProjectedRawPrediction.known line 709
  57. abbrev OAI.PerfectCompleteness.HierarchicalProjectedRawPrediction.hidden line 712
  58. theorem OAI.PerfectCompleteness.HierarchicalProjectedRawPrediction.response_eq_canonical line 715
  59. theorem OAI.PerfectCompleteness.HierarchicalProjectedRawPrediction.response_eq_rightUpper line 734
  60. theorem OAI.PerfectCompleteness.HierarchicalProjectedRawPrediction.response_eq_rightUpper_totalMatrix line 752
  61. def OAI.PerfectCompleteness.HierarchicalProjectedRawPrediction.rawJ line 774
  62. def OAI.PerfectCompleteness.HierarchicalProjectedRawPrediction.rawPrediction line 782
  63. abbrev OAI.PerfectCompleteness.HierarchicalProjectedRawPrediction.VisibleGood line 788
  64. abbrev OAI.PerfectCompleteness.HierarchicalProjectedRawPrediction.tensorJ line 793
  65. abbrev OAI.PerfectCompleteness.HierarchicalProjectedRawPrediction.columnSpace line 799
  66. abbrev OAI.PerfectCompleteness.HierarchicalProjectedRawPrediction.target line 806
  67. abbrev OAI.PerfectCompleteness.HierarchicalProjectedRawPrediction.nativeCorrection line 815
  68. abbrev OAI.PerfectCompleteness.HierarchicalProjectedRawPrediction.visibleOffset line 822
  69. theorem OAI.PerfectCompleteness.HierarchicalProjectedRawPrediction.rawJ_eq_tensorJ line 829
  70. theorem OAI.PerfectCompleteness.HierarchicalProjectedRawPrediction.rawJ_iff_restriction line 842
  71. def OAI.PerfectCompleteness.HierarchicalProjectedRawPrediction.responseMatch line 861
  72. theorem OAI.PerfectCompleteness.HierarchicalProjectedRawPrediction.rawPrediction_eq line 874
  73. def OAI.PerfectCompleteness.HierarchicalProjectedRawPrediction.given line 920
  74. theorem OAI.PerfectCompleteness.HierarchicalProjectedRawPrediction.given_eq_jointEvent line 925
  75. theorem OAI.PerfectCompleteness.HierarchicalProjectedRawPrediction.selection_of_positive line 954
  76. theorem OAI.PerfectCompleteness.HierarchicalProjectedRawPrediction.conditional_prediction_eq line 985