OAI/Computability/PerfectCompleteness/Foundations/LinearEvaluationLemmas.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniqueGamesTheorem.Gadget.LinearEvaluation.fiberEquivKernel line 26
  2. theorem OAI.UniqueGamesTheorem.Gadget.LinearEvaluation.fiber_card_eq_kernel_of_surjective line 33
  3. theorem OAI.UniqueGamesTheorem.Gadget.LinearEvaluation.fiber_card_mul_pow_of_surjective line 43
  4. theorem OAI.UniqueGamesTheorem.Gadget.LinearEvaluation.fiber_card_mul_card_of_surjective line 52
  5. theorem OAI.UniqueGamesTheorem.Gadget.LinearEvaluation.cancellation_card_mul_pow_of_surjective line 60
  6. theorem OAI.UniqueGamesTheorem.Gadget.LinearEvaluation.cancellation_count_of_surjective_card_le_eight line 68
  7. theorem OAI.UniqueGamesTheorem.Gadget.LinearEvaluation.cancellation_count_at_least_one_eighth_of_surjective line 78
  8. def OAI.UniqueGamesTheorem.Gadget.LinearEvaluation.evaluation line 85
  9. theorem OAI.UniqueGamesTheorem.Gadget.LinearEvaluation.evaluation_apply line 88
  10. theorem OAI.UniqueGamesTheorem.Gadget.LinearEvaluation.evaluation_surjective line 93
  11. theorem OAI.UniqueGamesTheorem.Gadget.LinearEvaluation.evaluation_fiber_card_mul_pow line 101
  12. theorem OAI.UniqueGamesTheorem.Gadget.LinearEvaluation.cancellation_count_at_least_one_eighth line 106
  13. def OAI.UniqueGamesTheorem.Gadget.LinearEvaluation.uniformProbability line 112
  14. theorem OAI.UniqueGamesTheorem.Gadget.LinearEvaluation.cancellation_probability_of_surjective line 117
  15. theorem OAI.UniqueGamesTheorem.Gadget.LinearEvaluation.cancellation_probability_at_least_one_eighth_of_surjective line 131
  16. theorem OAI.UniqueGamesTheorem.Gadget.LinearEvaluation.cancellation_probability_target_dim_zero line 143
  17. theorem OAI.UniqueGamesTheorem.Gadget.LinearEvaluation.evaluation_cancellation_probability line 150
  18. theorem OAI.UniqueGamesTheorem.Gadget.LinearEvaluation.evaluation_cancellation_probability_at_least_one_eighth line 155
  19. theorem OAI.UniqueGamesTheorem.Gadget.LinearEvaluation.cancellation_finset_count_of_surjective line 161
  20. theorem OAI.UniqueGamesTheorem.Gadget.LinearEvaluation.evaluation_cancellation_finset_count line 168
  21. theorem OAI.UniqueGamesTheorem.Gadget.LinearEvaluation.correction_space_card_pos line 175
  22. theorem OAI.UniqueGamesTheorem.Gadget.LinearEvaluation.evaluation_fibers_equal_card line 180
  23. abbrev OAI.PerfectCompleteness.DirectionQuotient.F2 line 194
  24. def OAI.PerfectCompleteness.DirectionQuotient.line line 198
  25. abbrev OAI.PerfectCompleteness.DirectionQuotient.Space line 200
  26. def OAI.PerfectCompleteness.DirectionQuotient.proj line 202
  27. theorem OAI.PerfectCompleteness.DirectionQuotient.proj_surjective line 204
  28. theorem OAI.PerfectCompleteness.DirectionQuotient.mem_line_iff line 207
  29. theorem OAI.PerfectCompleteness.DirectionQuotient.proj_eq_zero_iff line 220
  30. theorem OAI.PerfectCompleteness.DirectionQuotient.proj_eq_iff line 223
  31. theorem OAI.PerfectCompleteness.DirectionQuotient.card_line line 227
  32. theorem OAI.PerfectCompleteness.DirectionQuotient.card_proj_fiber line 233
  33. def OAI.PerfectCompleteness.DirectionQuotient.projectWithSide line 241
  34. theorem OAI.PerfectCompleteness.DirectionQuotient.projectWithSide_surjective line 244
  35. def OAI.PerfectCompleteness.DirectionQuotient.withSideFiberEquiv line 250
  36. theorem OAI.PerfectCompleteness.DirectionQuotient.card_projectWithSide_fiber line 261
  37. theorem OAI.PerfectCompleteness.DirectionQuotient.coarsen_at_most_two line 267
  38. theorem OAI.PerfectCompleteness.DirectionQuotient.coarsenWithSide_at_most_two line 275
  39. abbrev OAI.PerfectCompleteness.BlockQuotient.JointOutput line 296
  40. abbrev OAI.PerfectCompleteness.BlockQuotient.OtherBlocks line 298
  41. def OAI.PerfectCompleteness.BlockQuotient.splitOutput line 300
  42. theorem OAI.PerfectCompleteness.BlockQuotient.splitOutput_selected line 304
  43. theorem OAI.PerfectCompleteness.BlockQuotient.splitOutput_other line 307
  44. theorem OAI.PerfectCompleteness.BlockQuotient.splitOutput_side line 311
  45. def OAI.PerfectCompleteness.BlockQuotient.projectBlock line 316
  46. theorem OAI.PerfectCompleteness.BlockQuotient.projectBlock_selected line 320
  47. theorem OAI.PerfectCompleteness.BlockQuotient.projectBlock_other line 323
  48. theorem OAI.PerfectCompleteness.BlockQuotient.projectBlock_side line 327
  49. theorem OAI.PerfectCompleteness.BlockQuotient.projectBlock_surjective line 330
  50. def OAI.PerfectCompleteness.BlockQuotient.blockFiberEquiv line 334
  51. theorem OAI.PerfectCompleteness.BlockQuotient.card_projectBlock_fiber line 350
  52. theorem OAI.PerfectCompleteness.BlockQuotient.coarsenBlock_at_most_two line 358
  53. def OAI.UniqueGamesTheorem.Integration.CutoffBudget.cutoffSum line 378
  54. theorem OAI.UniqueGamesTheorem.Integration.CutoffBudget.cutoffSum_le line 382
  55. theorem OAI.UniqueGamesTheorem.Integration.CutoffBudget.rho_real_bounds line 406
  56. theorem OAI.UniqueGamesTheorem.Integration.CutoffBudget.cutoffSum_le_budget line 415
  57. theorem OAI.UniqueGamesTheorem.Integration.CutoffBudget.exists_symbol_dimension_cutoff line 423