OAI/Computability/PerfectCompleteness/Construction/HiddenBucketBias.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.HiddenBucketBias.F2 line 19
  2. abbrev OAI.PerfectCompleteness.HiddenBucketBias.HiddenDirection line 24
  3. abbrev OAI.PerfectCompleteness.HiddenBucketBias.VisibleDirection line 27
  4. abbrev OAI.PerfectCompleteness.HiddenBucketBias.HiddenTape line 30
  5. abbrev OAI.PerfectCompleteness.HiddenBucketBias.VisibleTape line 31
  6. def OAI.PerfectCompleteness.HiddenBucketBias.hiddenTapeLaw line 33
  7. def OAI.PerfectCompleteness.HiddenBucketBias.visibleTapeLaw line 37
  8. def OAI.PerfectCompleteness.HiddenBucketBias.splitTape line 41
  9. theorem OAI.PerfectCompleteness.HiddenBucketBias.split_tapeLaw line 45
  10. theorem OAI.PerfectCompleteness.HiddenBucketBias.split_tapeLaw_pushforward line 61
  11. theorem OAI.PerfectCompleteness.HiddenBucketBias.product_fst line 68
  12. theorem OAI.PerfectCompleteness.HiddenBucketBias.hidden_marginal line 80
  13. theorem OAI.PerfectCompleteness.HiddenBucketBias.hidden_coordinate_marginal line 88
  14. theorem OAI.PerfectCompleteness.HiddenBucketBias.hidden_coordinates_independent line 93
  15. def OAI.PerfectCompleteness.HiddenBucketBias.directionIn line 100
  16. theorem OAI.PerfectCompleteness.HiddenBucketBias.directionIn_ne_zero line 103
  17. def OAI.PerfectCompleteness.HiddenBucketBias.hiddenSum line 108
  18. def OAI.PerfectCompleteness.HiddenBucketBias.scalarRestriction line 112
  19. theorem OAI.PerfectCompleteness.HiddenBucketBias.scalarRestriction_apply line 116
  20. theorem OAI.PerfectCompleteness.HiddenBucketBias.exists_nonzero_restriction line 120
  21. theorem OAI.PerfectCompleteness.HiddenBucketBias.abs_character line 137
  22. def OAI.PerfectCompleteness.HiddenBucketBias.signCharacter line 143
  23. theorem OAI.PerfectCompleteness.HiddenBucketBias.character_sum line 148
  24. theorem OAI.PerfectCompleteness.HiddenBucketBias.character_hiddenSum line 158
  25. theorem OAI.PerfectCompleteness.HiddenBucketBias.character_expectation_product line 166
  26. theorem OAI.PerfectCompleteness.HiddenBucketBias.abs_expectation_character_le_one line 182
  27. theorem OAI.PerfectCompleteness.HiddenBucketBias.hidden_bias_le line 192
  28. theorem OAI.PerfectCompleteness.HiddenBucketBias.hidden_sign_bias_le line 212
  29. instance OAI.PerfectCompleteness.HiddenBucketBias.tensorFinite line 221
  30. instance OAI.PerfectCompleteness.HiddenBucketBias.tensorFintype line 230
  31. def OAI.PerfectCompleteness.HiddenBucketBias.law line 233
  32. theorem OAI.PerfectCompleteness.HiddenBucketBias.law_from_full_buckets line 237
  33. theorem OAI.PerfectCompleteness.HiddenBucketBias.law_bias_le line 245
  34. theorem OAI.PerfectCompleteness.HiddenBucketBias.law_sign_bias_le line 254
  35. def OAI.PerfectCompleteness.HiddenBucketBias.recursiveLaw line 267
  36. theorem OAI.PerfectCompleteness.HiddenBucketBias.recursive_law_sign_bias_le line 273
  37. def OAI.PerfectCompleteness.HiddenBucketBias.exposedLaw line 293
  38. theorem OAI.PerfectCompleteness.HiddenBucketBias.hidden_condition_exterior line 298
  39. theorem OAI.PerfectCompleteness.HiddenBucketBias.law_condition_exterior line 308