OAI/Computability/PerfectCompleteness/Sampling/BucketUniformLemmas.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.BucketUniform.coordinateDirection line 23
  2. def OAI.PerfectCompleteness.BucketUniform.evaluateLinear line 29
  3. theorem OAI.PerfectCompleteness.BucketUniform.evaluateLinear_apply line 42
  4. theorem OAI.PerfectCompleteness.BucketUniform.evaluate_single line 45
  5. theorem OAI.PerfectCompleteness.BucketUniform.evaluate_coordinate_bucket line 56
  6. def OAI.PerfectCompleteness.BucketUniform.coordinateTape line 65
  7. theorem OAI.PerfectCompleteness.BucketUniform.evaluate_coordinateTape line 68
  8. theorem OAI.PerfectCompleteness.BucketUniform.evaluateLinear_surjective line 74
  9. theorem OAI.PerfectCompleteness.BucketUniform.evaluate_surjective line 78
  10. theorem OAI.PerfectCompleteness.BucketUniform.uniform_evaluate_law line 82
  11. theorem OAI.PerfectCompleteness.BucketUniform.uniform_array_law line 90
  12. def OAI.PerfectCompleteness.BucketUniform.ofRowsLinear line 98
  13. theorem OAI.PerfectCompleteness.BucketUniform.ofRowsLinear_surjective line 112
  14. theorem OAI.PerfectCompleteness.BucketUniform.uniform_matrix_law line 116
  15. def OAI.PerfectCompleteness.RecursiveSamplerBiasAlgebra.squareProduct line 145
  16. theorem OAI.PerfectCompleteness.RecursiveSamplerBiasAlgebra.squareProduct_val line 154
  17. theorem OAI.PerfectCompleteness.RecursiveSamplerBiasAlgebra.square_functional_eq_zero_of_products line 157
  18. def OAI.PerfectCompleteness.RecursiveSamplerBiasAlgebra.childSquareLift line 177
  19. theorem OAI.PerfectCompleteness.RecursiveSamplerBiasAlgebra.childSquareLift_val line 185
  20. def OAI.PerfectCompleteness.RecursiveSamplerBiasAlgebra.childProduct line 189
  21. theorem OAI.PerfectCompleteness.RecursiveSamplerBiasAlgebra.childProduct_val line 195
  22. def OAI.PerfectCompleteness.RecursiveSamplerBiasAlgebra.childBilinear line 200
  23. theorem OAI.PerfectCompleteness.RecursiveSamplerBiasAlgebra.childBilinear_apply line 206
  24. theorem OAI.PerfectCompleteness.RecursiveSamplerBiasAlgebra.eq_zero_of_child_restrictions line 213
  25. theorem OAI.PerfectCompleteness.RecursiveSamplerBiasAlgebra.exists_child_restriction_ne_zero line 232
  26. theorem OAI.PerfectCompleteness.RecursiveSamplerBiasAlgebra.childBilinear_ne_zero line 243
  27. theorem OAI.PerfectCompleteness.RecursiveSamplerBiasAlgebra.ordinary_or_bilinear_ne_zero line 253
  28. theorem OAI.PerfectCompleteness.RecursiveSamplerBiasAlgebra.combine_eq line 266
  29. theorem OAI.PerfectCompleteness.RecursiveSamplerBiasAlgebra.map_combine line 281
  30. abbrev OAI.PerfectCompleteness.RecursiveSampler.CallIndex line 306
  31. abbrev OAI.PerfectCompleteness.RecursiveSampler.OrdinaryTape line 310
  32. abbrev OAI.PerfectCompleteness.RecursiveSampler.CallTapes line 314
  33. def OAI.PerfectCompleteness.RecursiveSampler.splitTapeEquiv line 318
  34. def OAI.PerfectCompleteness.RecursiveSampler.evaluateCalls line 336
  35. def OAI.PerfectCompleteness.RecursiveSampler.splitEvaluatedTape line 342
  36. def OAI.PerfectCompleteness.RecursiveSampler.stepCombine line 350
  37. theorem OAI.PerfectCompleteness.RecursiveSampler.stepCombine_splitEvaluatedTape line 358
  38. instance OAI.PerfectCompleteness.RecursiveSampler.childFamilyFinite line 368
  39. instance OAI.PerfectCompleteness.RecursiveSampler.childSquareFintype line 372
  40. instance OAI.PerfectCompleteness.RecursiveSampler.ordinaryDrawFintype line 378
  41. instance OAI.PerfectCompleteness.RecursiveSampler.ordinaryTapeFintype line 384
  42. instance OAI.PerfectCompleteness.RecursiveSampler.callTapesFintype line 391
  43. def OAI.PerfectCompleteness.RecursiveSampler.ordinaryLaw line 402
  44. def OAI.PerfectCompleteness.RecursiveSampler.callTapeLaw line 413
  45. theorem OAI.PerfectCompleteness.RecursiveSampler.splitTape_law line 421
  46. theorem OAI.PerfectCompleteness.RecursiveSampler.subTape_tuple_law line 443
  47. def OAI.PerfectCompleteness.RecursiveSampler.callScalarLaw line 456
  48. theorem OAI.PerfectCompleteness.RecursiveSampler.evaluateCalls_law line 465
  49. theorem OAI.PerfectCompleteness.RecursiveSampler.splitEvaluatedTape_law line 472
  50. theorem OAI.PerfectCompleteness.RecursiveSampler.law_step line 497