OAI/Computability/PerfectCompleteness/Machines/OwnInputAffineSliceLemmas.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.OwnInputAffineSlice.F2 line 17
  2. theorem OAI.PerfectCompleteness.OwnInputAffineSlice.probability_product_and line 23
  3. theorem OAI.PerfectCompleteness.OwnInputAffineSlice.product_slice_positive line 37
  4. theorem OAI.PerfectCompleteness.OwnInputAffineSlice.condition_product_hidden line 50
  5. theorem OAI.PerfectCompleteness.OwnInputAffineSlice.probability_condition_congr line 79
  6. def OAI.PerfectCompleteness.OwnInputAffineSlice.tensorSlice line 99
  7. theorem OAI.PerfectCompleteness.OwnInputAffineSlice.probability_condition_eq_conditionalMatch line 104
  8. abbrev OAI.PerfectCompleteness.OwnInputAffineSlice.VisibleSample line 132
  9. def OAI.PerfectCompleteness.OwnInputAffineSlice.visibleLaw line 136
  10. def OAI.PerfectCompleteness.OwnInputAffineSlice.hiddenOutput line 143
  11. def OAI.PerfectCompleteness.OwnInputAffineSlice.jointEvent line 149
  12. theorem OAI.PerfectCompleteness.OwnInputAffineSlice.joint_probability line 156
  13. theorem OAI.PerfectCompleteness.OwnInputAffineSlice.slice_probability_pos line 173
  14. theorem OAI.PerfectCompleteness.OwnInputAffineSlice.conditional_referenceLaw line 188
  15. theorem OAI.PerfectCompleteness.OwnInputAffineSlice.conditional_observed_response_probability line 208
  16. theorem OAI.PerfectCompleteness.OwnInputAffineSlice.conditional_response_probability line 238
  17. theorem OAI.PerfectCompleteness.OwnInputRawAssembly.backgroundOf_assemble line 292
  18. def OAI.PerfectCompleteness.OwnInputRawAssembly.exteriorBackground line 303
  19. def OAI.PerfectCompleteness.OwnInputRawAssembly.scalarEval line 311
  20. def OAI.PerfectCompleteness.OwnInputRawAssembly.mergedTape line 314
  21. theorem OAI.PerfectCompleteness.OwnInputRawAssembly.split_mergedTape line 319
  22. def OAI.PerfectCompleteness.OwnInputRawAssembly.arrays line 324
  23. def OAI.PerfectCompleteness.OwnInputRawAssembly.background line 329
  24. def OAI.PerfectCompleteness.OwnInputRawAssembly.knownVisible line 333
  25. theorem OAI.PerfectCompleteness.OwnInputRawAssembly.readInput_knownBuckets line 337
  26. theorem OAI.PerfectCompleteness.OwnInputRawAssembly.arrays_upper line 343
  27. theorem OAI.PerfectCompleteness.OwnInputRawAssembly.background_arrays line 349
  28. theorem OAI.PerfectCompleteness.OwnInputRawAssembly.arrays_eq_matrix_assemble line 355
  29. theorem OAI.PerfectCompleteness.OwnInputRawAssembly.matrix_arrays line 365
  30. theorem OAI.PerfectCompleteness.OwnInputRawAssembly.response_eq_canonical line 379
  31. theorem OAI.PerfectCompleteness.OwnInputRawAssembly.response_eq_rightUpper line 396
  32. theorem OAI.PerfectCompleteness.OwnInputRawAssembly.response_eq_rightUpper_totalMatrix line 411