OAI/Computability/PerfectCompleteness/Decoding/LowerCutFiberDisintegrationLemmas.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.LowerCutFiberDisintegration.Scalar line 23
  2. abbrev OAI.PerfectCompleteness.LowerCutFiberDisintegration.Quotient line 24
  3. abbrev OAI.PerfectCompleteness.LowerCutFiberDisintegration.Background line 25
  4. abbrev OAI.PerfectCompleteness.LowerCutFiberDisintegration.Coordinates line 27
  5. def OAI.PerfectCompleteness.LowerCutFiberDisintegration.coordinateEquiv line 30
  6. theorem OAI.PerfectCompleteness.LowerCutFiberDisintegration.coordinateEquiv_apply line 45
  7. def OAI.PerfectCompleteness.LowerCutFiberDisintegration.coordinates line 50
  8. def OAI.PerfectCompleteness.LowerCutFiberDisintegration.law line 55
  9. theorem OAI.PerfectCompleteness.LowerCutFiberDisintegration.coordinates_law line 61
  10. def OAI.PerfectCompleteness.LowerCutFiberDisintegration.arraysAt line 76
  11. theorem OAI.PerfectCompleteness.LowerCutFiberDisintegration.first_eq_arraysAt line 82
  12. theorem OAI.PerfectCompleteness.LowerCutFiberDisintegration.second_eq_arraysAt line 92
  13. def OAI.PerfectCompleteness.LowerCutFiberDisintegration.pair line 104
  14. theorem OAI.PerfectCompleteness.LowerCutFiberDisintegration.pair_coordinates line 109
  15. theorem OAI.PerfectCompleteness.LowerCutFiberDisintegration.arraysPair_law line 116
  16. theorem OAI.PerfectCompleteness.LowerCutFiberDisintegration.probability_pair line 128
  17. theorem OAI.PerfectCompleteness.LowerCutProjection.linearMap_replace line 158
  18. theorem OAI.PerfectCompleteness.LowerCutProjection.original_pullback line 174
  19. theorem OAI.PerfectCompleteness.LowerCutProjection.fresh_pullback line 183
  20. def OAI.PerfectCompleteness.LowerCutProjection.observePullback line 191
  21. theorem OAI.PerfectCompleteness.LowerCutProjection.observe_pullback line 198
  22. theorem OAI.PerfectCompleteness.LowerCutProjection.pushforward_observe line 214
  23. theorem OAI.PerfectCompleteness.LowerCutProjection.uniform_projected_observe line 226
  24. theorem OAI.PerfectCompleteness.LowerCutProjection.HPullback_replace line 235
  25. theorem OAI.PerfectCompleteness.LowerCutProjection.firstRows_pullback line 250
  26. theorem OAI.PerfectCompleteness.LowerCutProjection.selectedPair_pullback line 268
  27. abbrev OAI.PerfectCompleteness.LowerCutSingleFiberDisintegration.Raw line 311
  28. abbrev OAI.PerfectCompleteness.LowerCutSingleFiberDisintegration.Coordinates line 314
  29. def OAI.PerfectCompleteness.LowerCutSingleFiberDisintegration.coordinateEquiv line 317
  30. theorem OAI.PerfectCompleteness.LowerCutSingleFiberDisintegration.coordinateEquiv_apply line 329
  31. def OAI.PerfectCompleteness.LowerCutSingleFiberDisintegration.coordinates line 336
  32. theorem OAI.PerfectCompleteness.LowerCutSingleFiberDisintegration.coordinates_complement line 342
  33. theorem OAI.PerfectCompleteness.LowerCutSingleFiberDisintegration.coordinates_law line 347
  34. theorem OAI.PerfectCompleteness.LowerCutSingleFiberDisintegration.reconstruct_eq_arraysAt line 391
  35. theorem OAI.PerfectCompleteness.LowerCutSingleFiberDisintegration.expectation_fiber line 402
  36. theorem OAI.PerfectCompleteness.LowerCutSingleFiberDisintegration.probability_fiber line 424