OAI/Computability/PerfectCompleteness/Foundations/RecursiveSpaceEquivLemmas.lean

GitHub source file

89 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.RecursiveSpaceEquiv.assignmentEquiv line 26
  2. def OAI.PerfectCompleteness.RecursiveSpaceEquiv.spaceEquiv line 36
  3. theorem OAI.PerfectCompleteness.RecursiveSpaceEquiv.spaceEquiv_apply line 55
  4. def OAI.PerfectCompleteness.RecursiveSpaceEquiv.squarePullback line 59
  5. def OAI.PerfectCompleteness.RecursiveSpaceEquiv.squareEquiv line 66
  6. theorem OAI.PerfectCompleteness.RecursiveSpaceEquiv.squareEquiv_apply line 85
  7. theorem OAI.PerfectCompleteness.RecursiveSpaceEquiv.space_natCard_eq line 89
  8. theorem OAI.PerfectCompleteness.RecursiveSpaceEquiv.square_natCard_eq line 93
  9. theorem OAI.PerfectCompleteness.RecursiveSpaceEquiv.space_card_eq line 98
  10. theorem OAI.PerfectCompleteness.RecursiveSpaceEquiv.square_card_eq line 103
  11. def OAI.PerfectCompleteness.ReducedPartition.ConstantOnFibers line 119
  12. def OAI.PerfectCompleteness.ReducedPartition.fiber line 122
  13. def OAI.PerfectCompleteness.ReducedPartition.parts line 125
  14. theorem OAI.PerfectCompleteness.ReducedPartition.self_mem_fiber line 128
  15. theorem OAI.PerfectCompleteness.ReducedPartition.fiber_nonempty line 132
  16. theorem OAI.PerfectCompleteness.ReducedPartition.fiber_subset_range line 136
  17. theorem OAI.PerfectCompleteness.ReducedPartition.mem_fiber_iff line 141
  18. theorem OAI.PerfectCompleteness.ReducedPartition.fiber_eq_of_output_eq line 150
  19. theorem OAI.PerfectCompleteness.ReducedPartition.fiber_eq_iff line 159
  20. theorem OAI.PerfectCompleteness.ReducedPartition.output_eq_of_common_mem line 169
  21. theorem OAI.PerfectCompleteness.ReducedPartition.fiber_disjoint_of_output_ne line 176
  22. theorem OAI.PerfectCompleteness.ReducedPartition.fiber_eq_or_disjoint line 183
  23. theorem OAI.PerfectCompleteness.ReducedPartition.covered_iff_mem_range line 191
  24. abbrev OAI.PerfectCompleteness.ReducedPartition.Part line 202
  25. def OAI.PerfectCompleteness.ReducedPartition.label line 204
  26. instance OAI.PerfectCompleteness.ReducedPartition.(instance at line 207) line 207
  27. def OAI.PerfectCompleteness.ReducedPartition.representative line 211
  28. theorem OAI.PerfectCompleteness.ReducedPartition.representative_spec line 214
  29. theorem OAI.PerfectCompleteness.ReducedPartition.representative_mem line 218
  30. theorem OAI.PerfectCompleteness.ReducedPartition.part_nonempty line 223
  31. def OAI.PerfectCompleteness.ReducedPartition.output line 227
  32. theorem OAI.PerfectCompleteness.ReducedPartition.output_mem_range line 230
  33. theorem OAI.PerfectCompleteness.ReducedPartition.mem_iff line 234
  34. theorem OAI.PerfectCompleteness.ReducedPartition.output_label line 239
  35. theorem OAI.PerfectCompleteness.ReducedPartition.output_injective line 243
  36. theorem OAI.PerfectCompleteness.ReducedPartition.label_representative line 252
  37. theorem OAI.PerfectCompleteness.ReducedPartition.label_surjective line 257
  38. instance OAI.PerfectCompleteness.ReducedPartition.(instance at line 262) line 262
  39. theorem OAI.PerfectCompleteness.ReducedPartition.card_parts_le line 265
  40. theorem OAI.PerfectCompleteness.ReducedPartition.restoration_bijective line 269
  41. def OAI.PerfectCompleteness.ReducedPartition.rangeMap line 282
  42. def OAI.PerfectCompleteness.ReducedPartition.preimage line 285
  43. theorem OAI.PerfectCompleteness.ReducedPartition.preimage_spec line 288
  44. theorem OAI.PerfectCompleteness.ReducedPartition.rangeMap_preimage line 291
  45. theorem OAI.PerfectCompleteness.ReducedPartition.rangeMap_surjective line 295
  46. def OAI.PerfectCompleteness.ReducedPartition.induced line 299
  47. theorem OAI.PerfectCompleteness.ReducedPartition.induced_rangeMap line 302
  48. theorem OAI.PerfectCompleteness.ReducedPartition.induced_factorization line 306
  49. theorem OAI.PerfectCompleteness.ReducedPartition.induced_unique line 311
  50. theorem OAI.PerfectCompleteness.ReducedPartition.mem_fiber_iff_induced line 319
  51. theorem OAI.PerfectCompleteness.ReducedPartition.fiber_eq_of_pullback line 325
  52. theorem OAI.PerfectCompleteness.ReducedPartition.parts_eq_of_pullback line 339
  53. theorem OAI.PerfectCompleteness.ReducedPartition.output_eq_of_shared_part line 358
  54. def OAI.PerfectCompleteness.RowAdvice.pad line 384
  55. theorem OAI.PerfectCompleteness.RowAdvice.pad_low line 393
  56. theorem OAI.PerfectCompleteness.RowAdvice.pad_high line 397
  57. theorem OAI.PerfectCompleteness.RowAdvice.pad_injective line 401
  58. theorem OAI.PerfectCompleteness.RowAdvice.apply_eq_iff_ker_mkQ_eq line 412
  59. theorem OAI.PerfectCompleteness.RowAdvice.comp_eq_iff_ker_quotient line 420
  60. theorem OAI.PerfectCompleteness.RowAdvice.slice_row_eq line 433
  61. def OAI.PerfectCompleteness.RowAdvice.paddedRowMap line 438
  62. theorem OAI.PerfectCompleteness.RowAdvice.paddedRowMap_apply_eq_iff line 442
  63. theorem OAI.PerfectCompleteness.RowAdvice.ker_paddedRowMap line 455
  64. theorem OAI.PerfectCompleteness.RowAdvice.paddedRowMap_comp_eq_iff line 468
  65. theorem OAI.PerfectCompleteness.RowAdvice.codimension_le_of_order_le line 475
  66. theorem OAI.PerfectCompleteness.RowAdvice.card_rowMaps line 480
  67. theorem OAI.PerfectCompleteness.RowAdvice.card_rowMaps_le line 486
  68. def OAI.PerfectCompleteness.SliceMass.columnEventEquivSlice line 512
  69. theorem OAI.PerfectCompleteness.SliceMass.card_slice line 530
  70. theorem OAI.PerfectCompleteness.SliceMass.card_rowFiber line 540
  71. theorem OAI.PerfectCompleteness.SliceMass.card_rowFiber_eq_card_slice_mul line 548
  72. theorem OAI.PerfectCompleteness.SliceMass.card_ratio line 556
  73. theorem OAI.PerfectCompleteness.SliceMass.probability_columnConstraint line 567
  74. theorem OAI.PerfectCompleteness.SliceMass.probability_columnConstraint_ge line 592
  75. theorem OAI.PerfectCompleteness.SliceMass.probability_columnConstraint_ge_of_finrank_le line 602
  76. theorem OAI.PerfectCompleteness.SmallBias.expectation_mono line 631
  77. theorem OAI.PerfectCompleteness.SmallBias.expectation_const line 637
  78. theorem OAI.PerfectCompleteness.SmallBias.expectation_neg line 641
  79. theorem OAI.PerfectCompleteness.SmallBias.expectation_sum line 645
  80. theorem OAI.PerfectCompleteness.SmallBias.bounded_target_cauchySchwarz line 650
  81. theorem OAI.PerfectCompleteness.SmallBias.gram_energy_bound line 666
  82. theorem OAI.PerfectCompleteness.SmallBias.aligned_heavy_energy line 702
  83. def OAI.PerfectCompleteness.SmallBias.align line 723
  84. theorem OAI.PerfectCompleteness.SmallBias.align_sq line 728
  85. theorem OAI.PerfectCompleteness.SmallBias.align_correlation line 735
  86. theorem OAI.PerfectCompleteness.SmallBias.align_pair_bound line 745
  87. theorem OAI.PerfectCompleteness.SmallBias.heavy_list_card_le line 760
  88. def OAI.PerfectCompleteness.SmallBias.heavySet line 783
  89. theorem OAI.PerfectCompleteness.SmallBias.heavySet_card_le line 787